Wildcards in standalone kind signatures
We should allow partial kind signatures as well as partial type signatures:
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information