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

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