Typechecking of withDict and tagToEnum#

Problem

The functions

tagToEnum# :: Int -> a
withDict :: st -> (dt => r) -> r

have a common property: they are not fully polymorphic and have to be instantiated at specific types. (tagToEnum# works only with enumerations, withDict with one-method dictionaries.)

• The condition for tagToEnum# is checked in the typechecker. See Note [tagToEnum#] in GHC.Tc.Gen.App.
• withDict is checked in the desugarer; see Note [withDict] in GHC.HsToCore.Expr.

This is all bad:

• Both are gross hacks.
• They are implemented totally differently.
• The tagToEnum# one is vulnerable to the order of constraint solving.
• The withDict one led to #21328 (closed)
• Neither supports abstraction -- you can only use these things monomorphically.

Solution

Introduce a special class:

class TagToEnum a where
  tagToEnum :: Int -> a

Plus, make the constraint solver have a built-in solving mechansim, just as it does for (say) Typeable. The rule is this: to solve (TagToEnum (T ty1 ... tyn)),

• Check whether T is an enumeration type
• If so, the evidence is MkTagToEnum (tagToEnum# @(T ty1 .. tyn)) where tagToEnum# is the primop (which is magically polymorophic over all enumeration types).
• Users are not allowed to write instances for TagToEnum.

Now we can write functions we can't write at all today

f :: TagToEnum a => a -> Int
f x = tagToEnum x + 1

Similarly for withDict:

type WithDict :: Type -> Constraint -> Constraint
class WithDict st dt | dt -> st where
  withDict :: forall (r :: RuntimeRep) (a :: TYPE r). st -> (dt => a) -> a

Again the constraint solver has a special way to solve WithDict st dt.

• The constraint solver solves for WithDict st dt precisely when dt is a typeclass with a single method of type st, e.g. WithDict (TypeRep a) (Typeable a).
• Users cannot define their own instances.
• This approach can readily be adapted if classes become datatypes rather than newtypes.
• Just like with Typeable, instances could be generated on-demand (as, effectively, happens now), rather than

There could be a functional dependency dt -> st, or st could be a type family Evidence (dt :: Constraint) :: Type instead of a parameter. I'm not sure which.

See also

See also #21575

Old notes

Just here for historical interest, and to give context for early comments.*

I see three options:

1. Validate withDict in the type checker just like tagToEnum#. Return a special form XExpr (WithDict ...); the desugarer would directly rewrite it to a cast without making any checks.

2. Validate tagToEnum# in the desugarer. The comment in Note [tagToEnum] in Tc.Gen.App could be then removed.

3. According to Note [tagToEnum], the "correct" solution is to add a class, but it's too heavyweight. Maybe this would become manageable when we have predicates in the constraint solver.

This ticket is a pure refactoring - no user-visible effects.