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