## Levity polymorphism and defaulting

This ticket concerns two closely related items regarding levity polymorphism.

- Consider

```
f :: forall p (r :: RuntimeRep). p r -> p r
f x = x
g = f
```

Currently, `g`

is inferred to be `p 'LiftedRep -> p 'LiftedRep`

. However, there is no good reason to restrict `r`

to `LiftedRep`

.

The current strategy is to default all variables of kind `RuntimeRep`

. If I define a type family `T`

such that `type instance T = RuntimeRep`

and change `f`

to use `T`

instead of `RuntimeRep`

, then `g`

becomes polymorphic in `r`

.

Proposed alternative: when we typecheck a binder, we unify the kind of its type with `TYPE q`

. Mark all such variables `q`

, and only such variables, for defaulting.

- 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. The type of `f`

would be `forall (a :: TYPE q). a -> a`

, where `q`

is a weakly polymorphic variable, that must be instantiated.

This could be implemented with a special constraint, say `KnownRuntimeRep`

that would have to be instantiated (could not be quantified over). That would make the levity restriction in line with the French approach of generating and solving constraints, rather than being an ad hoc defaulting step.

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.