We should allow partial kind signatures as well as partial type signatures: ```hs type Maybe :: _ -> Type data Maybe a = Nothing | Just a type Proxy :: forall (k :: _). k -> _ data Proxy = MkP ``` Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.