Relax Note [Phantom type variables in kinds] to allow for phantom levity vars
While implementing the unlifted datatypes proposal (!2218 (closed)), I realised that an edge case violates the kinding rules (Note [Phantom type variables in kinds]
, in particular). Specifically
type T :: forall (l :: Levity). TYPE (BoxedRep l)
data T = MkT
Note that

T
has a nullary data conMkT

T
is levitypolymorphic
That means the type of MkT
, forall {l::Levity}. T @l
, is illkinded! We have T @l :: TYPE (BoxedRep l)
and the forall
is supposed to bind the l
. But the kind rule for forall a. TYPE rep
demands that a
is not free in rep
:
ty : TYPE rep
`a` is not free in rep
(FORALL1) 
forall a. ty : TYPE rep
I argue that there is no harm in allowing TYPE (BoxedRep l)
here, because l
does not affect the representation of T
. I'm unaware of any other implications this might have.
We have to be a bit careful with evaluation semantics, but we have better means (#15532 (comment 239845), #17521) to decide whether levity polymorphism is OK at the term level. In any instance, MkT
is a data constructor and thus is a value under both callbyneed and callbyvalue semantics. I'm reasonably positive that allowing MkT
to be wellkinded is OK. You can't do anything with it at the term level unless you apply it to a Levity
anyway.