Skip to content

GitLab

Closed
Created by Richard Eisenberg@raeDeveloper

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.