Commit de01427e authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Minor refactor around quantified constraints

This patch clarifies a dark corner of quantified
constraints.

* See Note [Yukky eq_sel for a HoleDest] in TcSMonad

* Minor refactor, breaking out new function
     TcInteract.doTopReactEqPred
parent 1fd766ca
......@@ -1833,28 +1833,36 @@ doTopReactOther work_item
= continueWith work_item
| EqPred eq_rel t1 t2 <- classifyPredType pred
= -- See Note [Looking up primitive equalities in quantified constraints]
case boxEqPred eq_rel t1 t2 of
Nothing -> continueWith work_item
Just (cls, tys)
-> do { res <- matchLocalInst (mkClassPred cls tys) loc
; case res of
OneInst { cir_mk_ev = mk_ev }
-> chooseInstance work_item
(res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
where
_ -> continueWith work_item }
= doTopReactEqPred work_item eq_rel t1 t2
| otherwise
= do { res <- matchLocalInst pred loc
; case res of
OneInst {} -> chooseInstance work_item res
_ -> continueWith work_item }
where
ev = ctEvidence work_item
ev = ctEvidence work_item
loc = ctEvLoc ev
pred = ctEvPred ev
doTopReactEqPred :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
doTopReactEqPred work_item eq_rel t1 t2
-- See Note [Looking up primitive equalities in quantified constraints]
| Just (cls, tys) <- boxEqPred eq_rel t1 t2
= do { res <- matchLocalInst (mkClassPred cls tys) loc
; case res of
OneInst { cir_mk_ev = mk_ev }
-> chooseInstance work_item
(res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
_ -> continueWith work_item }
| otherwise
= continueWith work_item
where
ev = ctEvidence work_item
loc = ctEvLoc ev
mk_eq_ev cls tys mk_ev evs
= case (mk_ev evs) of
EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
......
......@@ -3402,13 +3402,33 @@ setWantedEvTerm (HoleDest hole) tm
= do { useVars (coVarsOfCo co)
; wrapTcS $ TcM.fillCoercionHole hole co }
| otherwise
= do { let co_var = coHoleCoVar hole
= -- See Note [Yukky eq_sel for a HoleDest]
do { let co_var = coHoleCoVar hole
; setEvBind (mkWantedEvBind co_var tm)
; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) }
setWantedEvTerm (EvVarDest ev_id) tm
= setEvBind (mkWantedEvBind ev_id tm)
{- Note [Yukky eq_sel for a HoleDest]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
How can it be that a Wanted with HoleDest gets evidence that isn't
just a coercion? i.e. evTermCoercion_maybe returns Nothing.
Consider [G] forall a. blah => a ~ T
[W] S ~# T
Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~
T) in the quantified constraints, and wraps the (boxed) evidence it
gets back in an eq_sel to extract the unboxed (S ~# T). We can't put
that term into a coercion, so we add a value binding
h = eq_sel (...)
and the coercion variable h to fill the coercion hole.
We even re-use the CoHole's Id for this binding!
Yuk!
-}
setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted ev tm
= case ev of
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment