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 onemethod 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 builtin 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 ondemand (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 uservisible effects.