Inaccessible code might be accessible with newtypes and Coercible
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!