Skip to content

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.

Edited by Richard Eisenberg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information