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

[GHC]

#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