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
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^