<div dir="ltr"><div>I have a bad feeling this would complicate the parser and pretty printer a lot, and thus isn't feasible, but what about allowing wildcards in kind signatures?</div><div><br></div><div>I mean, in</div><div><br></div><div>forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b</div><div><br></div><div>the `w` variable seems superfluous, as it's only there to give it a kind signature. I think there's enough information in `TYPE w` to infer the kind (`TYPE` can only be parametrized with `Levity`?) so maybe something like this would work:</div><div><br></div><div>forall a (b :: TYPE _). (a -> b) -> a -> b</div><div><br></div><div>This could be "some" compromise between "lying" about the type and being scary to beginners, as at the very least all the type variables introduced are actually used in the type signature.</div><div><br></div><div>Best regards,</div><div>Marcin Mrotek</div><div><br></div></div>