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. SeeNote [tagToEnum#]
in GHC.Tc.Gen.App. -
withDict
is checked in the desugarer; seeNote [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))
wheretagToEnum#
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 whendt
is a typeclass with a single method of typest
, 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:
-
Validate
withDict
in the type checker just liketagToEnum#
. Return a special formXExpr (WithDict ...)
; the desugarer would directly rewrite it to a cast without making any checks. -
Validate
tagToEnum#
in the desugarer. The comment in Note [tagToEnum] in Tc.Gen.App could be then removed. -
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.