In Richard Eisenberg's talk on his work with levity polymorphism for dependent Haskell, he clearly shows that this judgement / type is sound:
type Star = (* :: (* :: (* :: *)))
Does this mean that typing judgements themselves have kind *? Or is that more flexible, in that * may have a type of * or the returned... thing from (* :: *) (which I'm not sure of at this moment).
Given this assumption, that (* :: *) :: *, this would also mean that this type would be associative, too:
type Star = (((* :: *) :: *) :: *)
Which I don't think is correct. Could someone please clarify this for me?