Coercion application broken by newtype constructor
Summary
In core-spec there's an inference rule for applying a coercion to an argument (Co_AppCo) that amounts to the following haskell type:
coAppCo :: Coercion f g -> x :~: y -> Coercion (f x) (g y)
and indeed the type-checker is able to use this rule since the following implementation type-checks:
coAppCo Coercion Refl = Coercion
However, if we specialize the type signature by substituting f
and g
with uses of a newtype type constructor whose data constructor is not in scope, the implementation fails.
import Control.Monad.ST (ST)
coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion
<interactive>:12:26: error: [GHC-18872]
• Couldn't match representation of type: ST s x
with that of: ST s' x
arising from a use of ‘Coercion’
The data constructor ‘GHC.ST.ST’ of newtype ‘ST’ is not in scope
• In the expression: Coercion
In an equation for ‘coAppCo'’: coAppCo' Coercion Refl = Coercion
• Relevant bindings include
coAppCo' :: Coercion (ST s) (ST s')
-> (x :~: y) -> Coercion (ST s x) (ST s' y)
(bound at <interactive>:12:1)
Note that an implementation that simply delegates to the more general version (coAppCo' = coAppCo
) type-checks just fine. Likewise if instead of ST
I use something that is not a newtype, it also type-checks just fine.
Steps to reproduce
import Control.Monad.ST (ST)
import Data.Type.Coercion
import Data.Type.Equality
coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion
Expected behavior
coAppCo'
should type-check
Environment
- GHC version used: 9.6.2