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

5 Jun 2015

      #10493: Inaccessible code might be accessible with newtypes and Coercible
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.11
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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!

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