summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2020-01-08 16:29:38 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-01-12 21:32:45 -0500
commitde01427e6b1d45122c84eaf03122fda26c4dc688 (patch)
tree2556221369f06d8cff5e4662867a6df6263c0e3e
parent1fd766ca7ac1feea1e9c752f8ce438fab8e01d35 (diff)
downloadhaskell-de01427e6b1d45122c84eaf03122fda26c4dc688.tar.gz
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
-rw-r--r--compiler/typecheck/TcInteract.hs32
-rw-r--r--compiler/typecheck/TcSMonad.hs22
2 files changed, 41 insertions, 13 deletions
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 2383f22480..e594b10895 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -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)
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 411a1c7e6e..01df5df46e 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -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