# Levity polymorphism and defaulting

This ticket concerns two closely related items regarding levity polymorphism.

- 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.

- 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.