This ticket concerns two closely related items regarding levity polymorphism. 1. Consider ``` f1 :: forall (p :: RuntimeRep -> Type) (r :: RuntimeRep). p r -> p r f1 x = x -- Inferred type g1 :: forall (p :: RuntimeRep -> Type). p 'LiftedRep -> p 'LiftedRep g1 = f1 f2 :: (p :: Bool -> Type) (r :: Bool). p r -> p r f2 x = x -- Inferred type g2 :: forall (p :: Bool -> Type) (r :: Bool). p r -> p r g2 = f2 f3 :: forall k (p :: k -> Type) (r :: k). p r -> p r f3 x = x -- Inferred type g3 :: forall k (p :: k -> Type) (r :: k). p r -> p r g3 = f3 type family R type instance R = RuntimeRep f4 :: (p :: R-> Type) (r :: R). p r -> p r f2 x = x -- Inferred type g4 :: forall (p :: R -> Type) (r :: R). p r -> p r g4 = f4 ``` As you can see `g1` gets a less general type than `g2`, but the only difference is `RuntimeRep` vs `Bool`. And `g3` also gets a more general type, even though `k` could be instantiated to `RuntimeRep` in a call. And `g4` disguises `RuntimeRep` behind a type family, and so becomes polymorphic. This inconsistency is all pretty disgusting. Proposed alternative: * When we typecheck a binder, we unify the kind of its type with `TYPE q`, and emit a new constraint `StaticRuntimeRep q`. Similarly for other places where levity polymorphsm * Never generalise over `StaticRuntimeRep` constraints. * Default any unsolved `StaticRuntimeRep` constraints at the end. That could even be connected the defaulting mechanism, so that you could say `default (UnliftedRep)` in a module, or `default (One)` for multiplicity polymorphism in linear types. Richard says that a lot of machinery for `TypeLike` (#15979) will overlap with this ticket. 2. Consider ``` f x = x g = f 0# ``` Currently, when `f` is typechecked, it's argument is inferred to be lifted, and typechecking of `g` fails. An alternative strategy is to mimic monomorphism restriction. Rather than *defaulting* RuntimeRep varaibles in `TcMType.defaultTyVar`, simply *refrain from quantifying over it*. The type of `f` would be `forall (a :: TYPE q). a -> a`, where `q` is a free unification variable.