Are there some theoretical reasons for that (like that the type checking or type inference would become undecidable), or practical reasons (too difficult to implement properly)?
Currently, we can wrap things into newtype like
newtype Pair a = Pair (a, a)
and then have Pair :: * -> *
but we cannot do something like λ(a:*). (a,a).
(There are some languages that have them, for example, Scala does.)
2
Type inference with type level lambdas would require higher order unification which is undecidable. This is the motivation for disallowing them. But as has happened with other undecidable features (like type inference for GADTs), it might be possible to require type signatures and allow it. I’m not sure if that’s been investigated by anyone.