GitLab

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.