[Haskell-cafe] Actual levity polymorphism

[Tom Ellis]

I'm investigating unboxed types in GHC 9.2.  Levity polymorphism seems
to be severely limited in a way that makes it hard to envisage a
Haskell ecosystem which comfortably combines lifted and unlifted
types.  Am I missing something?

Understandably, the following attempt at defining a
RuntimeRep-polymorphic identity does not work:

    myId1 :: forall (r :: RuntimeRep) (t :: TYPE r). t -> t
    myId1 x = x

The GHC Users Guide explains why[1].  It's impossible to generate code
for myId1 because there is no way of determining the machine
representation of the argument x.

But worse, it's not even possible to define a *Levity*-polymorphic
identity:

    myId2 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)). t -> t
    myId2 x = x

In this case the argument can only have kind TYPE LiftedRep or TYPE
UnliftedRep.  The machine representation is the same in each case.
The problem this time is that the code generator doesn't know whether
it should emit code to evaluate the argument (UnliftedRep case) or not
(LiftedRep case). But this seems like a solvable problem.  Surely a
KnownLevity type class (possibly magical) could solve the problem.
This seems like it should work

    myId3 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)).
             KnownLevity lev =>
	     t -> t
    myId3 x = x

and in fact I wouldn't be surprised if this could be made to work:

    myId4 :: forall (r :: RuntimeRep) (t :: TYPE r).
             KnownRuntimeRep r =>
	     t -> t
    myId4 x = x

So what is the situation here?

1. myId3 already works (then where is KnownLevity made available and
   why isn't it mentioned in the Users Guide?)

2. myId3 can never work (then why not?)

3. myId3 might be able to work but it's an open research problem (then
   who is working on it, if anyone?)

4. myId3 would work and it would be useful but no one's proposed or
   implemented it (then who would be the best person to collaborate
   with on that?)

5. myId3 would work but it would not actually be useful (then what
   have I misunderstood?)

I suspect the answer is 1 (or maybe 4) based on the following passage
in the Levity Polymorphism[2] paper by RE & SPJ[2]:

> users can use a runtime type check (though GHC’s Typeable feature)
> to determine the memory representation of an as-yet- unbound
> argument to a function

(and the same questions for myId4).

Thanks,

Tom

[1] https://downloads.haskell.org/~ghc/9.4.4/docs/users_guide/exts/representation_polymorphism.html#no-representation-polymorphic-variables-or-arguments

[2] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/levity-pldi17.pdf