Re: [GHC] #10493: Inaccessible code might be accessible with newtypes and Coercible

16 Jun 2015

      #10493: Inaccessible code might be accessible with newtypes and Coercible
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                   Owner:  goldfire
            Type:  bug               |                  Status:  merge
        Priority:  normal            |               Milestone:  7.10.3
       Component:  Compiler          |                 Version:  7.11
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |  typecheck/should_compile/T10493
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => merge
 * testcase:   => typecheck/should_compile/T10493
 * milestone:   => 7.10.3

Old description:
...
If I say
{{{
module A (Age, ageCo) where
import Data.Type.Coercion
newtype Age = MkAge Int
ageCo :: Coercion Age Int
ageCo = Coercion
}}}
{{{
{-# LANGUAGE FlexibleContexts #-}
module B where
import Data.Coerce
import A
foo :: Coercible Age Int => ()
foo = ()
}}}
I get
{{{
B.hs:8:8: error:
    Couldn't match representation of type ‘Age’ with that of ‘Int’
    Inaccessible code in
      the type signature for: foo :: Coercible Age Int => ()
    In the ambiguity check for the type signature for ‘foo’:
      foo :: Coercible Age Int => ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘foo’: foo :: Coercible Age Int => ()
}}}
I agree that module `B` can't directly prove `Coercible Age Int`. But
`ageCo` is in scope which proves exactly this! So it is provable, albeit
directly. GHC should not claim that the code is inaccessible.
Proposed fix: in `canDecomposableTyConApp`, only call `canEqHardFailure`
for a representational equality when both tycons involved say `True` to
`isDistinctTyCon`.
I'm happy to put the fix in, once someone seconds this idea. Getting this
right has proved harder than I thought!
New description:

 If I say

 {{{
 module A (Age, ageCo) where

 import Data.Type.Coercion

 newtype Age = MkAge Int

 ageCo :: Coercion Age Int
 ageCo = Coercion
 }}}

 {{{
 {-# LANGUAGE FlexibleContexts #-}

 module B where

 import Data.Coerce
 import A

 foo :: Coercible Age Int => ()
 foo = ()
 }}}

 I get

 {{{
 B.hs:8:8: error:
     Couldn't match representation of type ‘Age’ with that of ‘Int’
     Inaccessible code in
       the type signature for: foo :: Coercible Age Int => ()
     In the ambiguity check for the type signature for ‘foo’:
       foo :: Coercible Age Int => ()
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘foo’: foo :: Coercible Age Int => ()
 }}}

 I agree that module `B` can't directly prove `Coercible Age Int`. But
 `ageCo` is in scope which proves exactly this! So it is provable, albeit
 indirectly. GHC should not claim that the code is inaccessible.

 Proposed fix: in `canDecomposableTyConApp`, only call `canEqHardFailure`
 for a representational equality when both tycons involved say `True` to
 `isDistinctTyCon`.

 I'm happy to put the fix in, once someone seconds this idea. Getting this
 right has proved harder than I thought!

--

Comment:

 Merge if convenient. This is a real bug, but it's somewhat obscure.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler