Provide a mechanism for backtracking in the constraint solver
Consider the following code in GHC.Tc.Solver.disambGroup
:
disambigGroup :: [Type] -> (TcTyVar, [Ct]) -> TcS Bool
disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= do { fake_ev_binds_var <- TcS.newTcEvBinds
; tclvl <- TcS.getTcLevel
; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
; if success then
do { unifyTyVar the_tv default_ty; ... }
else ...
}
where
try_group
| Just subst <- mb_subst
= do { ..
; wanted_evs <- sequence [ newWantedNC loc rewriters pred'
| wanted <- wanteds
, CtWanted { ctev_pred = pred
, ctev_rewriters = rewriters }
<- return (ctEvidence wanted)
, let pred' = substTy subst pred ]
; fmap isEmptyWC $
solveSimpleWanteds $ listToBag $
map mkNonCanonical wanted_evs }
| otherwise
= return False
the_ty = mkTyVarTy the_tv
mb_subst = tcMatchTyKi the_ty default_ty
The way this works is that we have a set of Wanted constraints wanteds
and a defaulting proposal the_tv ~> default_ty
. We want to check whether substituting the_tv ~> default_ty
allows us to solve all of the Wanted constraints. To do that, we apply the susbstitution and create new Wanteds, and call solveSimpleWanteds
on these. Only when we get an empty set of residual constraints do we then decide that the defaulting assignment was valid, and thus only then do we perform the unification the_tv := default_ty
(the call to unifyTyVar
).
However, there is nothing that stops the solver from performing its own unifications. For example, after substituting, we could plausibly solve a class constraint using an instance whose superclass contains an equality. This equality could then cause unifications to happen, before we have decided we want to accept the defaulting proposal!
The problem is that we want to try a certain defaulting proposal, test it out with a run of the constraint solver, and backtrack if it turns out to not be fruitful. To achieve this, we could instead call the solver on a completely separate collection of type variables and constraints, so that any unifications that take place are isolated from the original type variables and constraints. Another option would be to have a way to "roll back" any unifications that took place.
Another application of this "roll-back" functionality is the if-instance
typechecker plugin. The way it works is that, to solve a constraint disjunction ct1 || ct2
, it first tries to solve ct1
(using solveSimpleWanteds
); and if that fails it tries to solve ct2
. The problem is that attempting to solve ct1
might have caused unifications to take place, which we don't want. So again we should isolate the solver run to avoid it committing to certain undesirable unifications.