Note [mkRuntimeRepCo]
Given
class C a where { op :: Maybe a }
we will get an axiom
axC a :: (C a :: CONSTRAINT r1) ~ (Maybe a :: TYPE r2)
(See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.)
Then we may call mkRuntimeRepCo on (axC ty), and that will return
mkSelCo (SelTyCon 0 Nominal) (Kind (axC ty)) :: r1 ~ r2
So mkSelCo needs to be happy with decomposing a coercion of kind
CONSTRAINT r1 ~ TYPE r2
Hence the use of `tyConIsTYPEorCONSTRAINT` in the assertion `good_call`
in `mkSelCo`. See #23018 for a concrete example. (In this context it's
important that TYPE and CONSTRAINT have the same arity and kind, not
merely that they are not-apart; otherwise SelCo would not make sense.) References 1
- Type and Constraint are not apart GHC.Builtin.Types.Prim
Referenced by 2
- GHC.Core.Coercion call site ×2