Kind inference for newtypes in GADT syntax is deeply broken
Here are some tales of destruction, all with -XUnliftedNewtypes
and -XNoCUSKs
:
newtype N :: forall k. TYPE k where
MkN :: N -> N
gives
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N -> N
gives
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N -> N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
gives
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the res_kind
passed to kcConArgTys
has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.