Levity polymorphism and defaulting
This ticket concerns two closely related items regarding levity polymorphism.
f :: forall p (r :: RuntimeRep). p r -> p r f x = x g = f
g is inferred to be
p 'LiftedRep -> p 'LiftedRep. However, there is no good reason to restrict
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
g becomes polymorphic in
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.
f x = x g = f 0#
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.