Levity polymorphism and defaulting
This ticket concerns two closely related items regarding levity polymorphism.
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
g3 also gets a more general type, even though
k could be instantiated to
RuntimeRep in a call.
RuntimeRep behind a type family, and so becomes polymorphic.
This inconsistency is all pretty disgusting.
- 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
- Default any unsolved
StaticRuntimeRepconstraints 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.
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. 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.