Skip to content

Confusing GADTSyntax newtype error with invisible kinds

Consider the following:

type N :: TYPE r -> Type
newtype N a where
  MkN :: (a -> N a) -> N a

This seems fine, right? Except that the user didn't write a forall in the type of MkN, so the kind of a is defaulted. Making the kinds explicit, it's as if we wrote:

type N :: forall (r :: RuntimeRep). TYPE r -> Type
newtype N @r a where
  MkN :: (a -> N a) -> N @LiftedRep a

and this isn't allowed: we can't have a newtype which is a genuine GADT, where the type variables in the return kind don't match those in the head of the declaration.

However, the error message is quite confusing:

    * A newtype constructor must have a return type of form T a1 ... an
      MkN :: forall a. (a -> N a) -> N a
    * In the definition of data constructor `MkN'
      In the newtype declaration for `N'
   |
10 |   MkN :: (a -> N a) -> N a
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information