Unlifted types in constraints and unlifted constraints

Motivation

We should probably break Constraint up into type Constraint = CONSTRAINT 'LiftedRep like we did Type. Constraint is a synonym for Type. Let's look at some of the things this allows.

At first blush this seems unusable, as after all, what can construct something unlifted at the top level where instances live?

Unlifted Implicit Parameters

The first usecase that comes to mind is unlifted implicit parameters

(?foo :: Int#) => ...

now implicit parameters can be introduced and used without incurring the overhead of a mandatory boxing/unboxing. Since they are on the left of the =>, worker-wrapper transformations is currently basically unable to do nothing to optimize implicit parameters down to unboxed form, but they are becoming an effective way to implement effect systems.

User-visible unlifted (~)

Right now the (~) a user can talk about is a full Constraint, but a primitive (~#) :: forall i. i -> i -> Constraint ('TupleRep '[]) could then be exposed to users without the box in the way.

Dictionaries as unlifted tuples

This opens the open of having dictionaries themselves where the record is an unlifted tuple. There is a bit of a subtlety here.

Given something like

class Bounded (a :: TYPE 'IntRep) where
  minBound, maxBound :: a

You can't instantiate it.

But minBound :: Bounded a => a lives in Type, so it really should be able to return an a of any TYPE r it wants.

Currently ghc says no to this code because a is unlifted, and I suppose, it expects to be able to pull the argument out of the dictionary its building and sit it at the top level.

To work around this right now, I have to use something like

class Bounded (a :: TYPE 'IntRep) where
  minBound, maxBound :: ()~() => a

But this exposes the ()~() to the user. In theory we could flip things around and say the dictionary is constructed by some procedure that takes a 0-width object and gives back the result, allowing us to construct unboxed dictionaries in any representation we want, which should be able to hold such unlifted values just fine.

As Haskell evolves to become better at being good at both strict and non-strict computation things becomes more and more valuable.

Reflection/magicDict like tricks can also be used to manufacture such instances even if we disallow the user from instantiating them directly. Right now I can't write them down at all.

Proposal

My proposal is to generalize Constraint to match the generalizations we're doing to Type, and chase through the compiler the ensuing issues. Each of these could offer pretty nice performance wins/opportunities for different types of code.