GitLab

With -XPolyKinds, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling.

{-# LANGUAGE PolyKinds, GADTs #-}

import GHC.TypeLits

data Foo
  (x :: k)
  a
  where
    C1 :: (KnownNat x) => a -> Foo x a
    C2 :: a -> Foo Int a

error:
  • Expected kind ‘k’, but ‘x1’ has kind ‘Nat’
  • In the first argument of ‘Foo’, namely ‘x’
    In the type ‘Foo x a’
    In the definition of data constructor ‘C1’

From this error, I would never expect that putting a kind signature on a would help here. But a signature shouldn't be required at all: it's clear from the GADT constructors that a :: *.