[GHC] #10493: Inaccessible code might be accessible with newtypes and Coercible
GHC
ghc-devs at haskell.org
Fri Jun 5 20:13:14 UTC 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
More information about the ghc-tickets
mailing list