GHC accepts two names for the same kind variable
Consider
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)
data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
GHC rejects this with
Foo.hs:10:9: error:
• Different names for the same type variable: ‘p’ and ‘q’
• In the data declaration for ‘T’
|
10 | data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
| ^^^^^^^^^^^^^^^^^^
If T is a CUSK, it is similarly rejected, abeit with a different message
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)
data T2 (a :: p) (b :: q) = MkT (SameKind a b)
we get
Foo.hs:10:45: error:
• Expected kind ‘p’, but ‘b’ has kind ‘q’
‘q’ is a rigid type variable bound by
the data type declaration for ‘T2’
at Foo.hs:10:10-24
‘p’ is a rigid type variable bound by
the data type declaration for ‘T2’
at Foo.hs:10:10-24
• In the second argument of ‘SameKind’, namely ‘b’
In the type ‘(SameKind a b)’
In the definition of data constructor ‘MkT’
|
10 | data T2 (a :: p) (b :: q) = MkT (SameKind a b)
| ^
because p
and q
are created as distinct skolems.
BUT alas with standalone kind signatures we don't this
{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}
type T3 :: k -> k -> Type
data T3 (a :: p) (b :: q) = MkT
This is accepted by HEAD. That's highly inconsistent. We should reject.