GitLab

(This about Core for now, but writing a GHC proposal to bring simple inference of levity-polymorphism into the surface language is on my long-term TODO/wish list. I think #15532 is more relevant to the surface language.)

Today, UnliftedType (= TYPE (BoxedRep Unlifted)) is effectively a sub-kind of Type (= TYPE (BoxedRep Lifted)). But

1. It's currently impossible to re-use functions expecting Type with values of kind UnliftedType. It's always safe to coerce a value of UnliftedType into a Type and it should be pretty simple to do so! (But Coercible's coercions today are symmetric. The sub-kinding relation is not.)
2. Not every UnliftedType has a Type twin. I don't see why! Until recently, data types have been exclusively of lifted kind. UnliftedDatatypes changed that, now we can even have levity polymorhpic datatypes. By contrast, Array# etc. could all reasonably have lifted counterparts at which point we can make their type constructors levity-polymorphic, too.

If we can fix (2), we'll have an easy time at fixing (1): I propose that binders in Core that have kind Type to be reducible to the form (forall l. TYPE (BoxedRep l)) Lifted at all times, so that it's easy to switch the Lifted to Unlifted when needed. I imagine a simple transformation that does levity generalisation that would probably be quite simple. Then we can make case binders have UnliftedType and get the goodness of tag inference (#16970 (closed)) right in the kind system, for free!

Worker/wrapper can exploit strictness on boxed types that it has no unboxed equivalent for by making the binders of the worker have UnliftedType. Example from the UnliftedDatatypes proposal:

data IntSet
  = Branch !IntSet !Int !IntSet
  | Leaf

member :: Int -> IntSet -> Bool
member !k Leaf = False
member k (Branch l k' r)
  | k == k'   = True
  | k <  k'   = member k l
  | otherwise = member k r

turns into

type IntSet :: forall l. TYPE (BoxedRep l) -- automatically generalised in Core
Branch :: forall l. IntSet @Unlifted -> Int# -> IntSet @Unlifted -> IntSet @l
Leaf :: forall l. Proxy# () -> IntSet @l -- quick fix for #19487

member :: forall l1 l2. Int @l1 -> IntSet @l2 -> Bool @Lifted
member k s = case k of (k' :: Int @Unlifted) { I# k'' ->
  case s of (s' :: IntSet @Unlifted) { __DEFAULT ->
  $wmember k'' s'
  }
  }

$wmember :: Int# -> IntSet @Unlifted -> Bool @Lifted
$wmember k s = case s of 
  Leaf -> False
  Branch l k' r -> case k ==# k' of
    1# -> True
    0# -> case k <# k' of
      1# -> $wmember k l
      0# -> $wmember k r

Whether or not the user declared IntSet to be levity-polymorphic, it is automatically lowered as levity-polymorphic, because of (1). Note the lowered field types of Branch: Strict fields are lowered as fields of the UnliftedType twin. No need for dataConRepStrictness anymore, it's all in the kind!

And it pays off, too: The wrapper member does the seq to maintain the invariant that the binder s has UnliftedType and thus is always tagged. Nice! No tag checks, the same generated code as if the user had declared IntSet to be an UnliftedType in the first place.

In the long run, I hope that we can lift part of the levity generalisation transformation into the type inference engine, so that it will infer a levity-polymorphic kind for a let-binding if that's possible. But that's pretty far in the future at the moment...