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?
No. I think you've misinterpreted what is going on. :: at the type level is like :: at the value level. Consider:
three :: Int
three = 3 :: (Int :: *)
This is just 3 :: Int which is just 3. Already in Haskell + kind signatures you've been able to write: (((Int :: *) :: *) :: *) which is just the same as Int. Or in plain Haskell 2010, (((3 :: Int) :: Int) :: Int). Before, you were limited to how far you could go in the "right associated" way because kinds didn't themselves have kinds. The axiom * :: * changes that.
:: means what it always meant. I wouldn't view :: as an operator that "returns" something. It's just a piece of syntax that allows providing information to the type checker, but is otherwise irrelevant. If you really, really want to view it as some kind of operator, it would behave like const albeit it would be difficult to write down what its "type" would be.