[commit: ghc] wip/impredicativity: Apply instantiation also when checking type classes from the inert set (3a4762f)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/impredicativity
Link       : http://ghc.haskell.org/trac/ghc/changeset/3a4762f44df65c886a4c0bfe8a2ab2af181097fb/ghc

>---------------------------------------------------------------

commit 3a4762f44df65c886a4c0bfe8a2ab2af181097fb
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Wed Jul 15 14:22:56 2015 +0200

    Apply instantiation also when checking type classes from the inert set


>---------------------------------------------------------------

3a4762f44df65c886a4c0bfe8a2ab2af181097fb
 compiler/typecheck/TcInteract.hs | 44 ++++++++++++++++++++++++++++++++--------
 1 file changed, 35 insertions(+), 9 deletions(-)

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 706bc09..2df6354 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -673,7 +673,12 @@ interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 -}
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
+interactDict inerts workItem
+  = do { lazyEqs <- inerts_to_lazy_eqs (inert_irreds inerts)
+       ; interactDict' inerts lazyEqs workItem }
+
+interactDict' :: InertCans -> LazyEqs [TcPredType] -> Ct -> TcS (StopOrContinue Ct)
+interactDict' inerts lazyEqs workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
   -- don't ever try to solve CallStack IPs directly from other dicts,
   -- we always build new dicts instead.
   -- See Note [Overview of implicit CallStacks]
@@ -693,8 +698,12 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
        setWantedEvBind (ctEvId ev_w) ev_tm
        stopWith ev_w "Wanted CallStack IP"
 
-  | Just ctev_i <- lookupInertDict inerts cls tys
-  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
+  | Just (ctev_i, qs) <- over_lazy_eqs (lookupInertDict inerts cls) lazyEqs tys
+  = do { -- Apply obtained lazy equation
+         qs_evs <- mapM (newWantedEvVarNC (ctev_loc ev_w)) (extract_lazy_eqs qs)
+       ; emitWorkNC qs_evs
+         -- Perform interaction
+       ; (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
        ; case inert_effect of
            IRKeep    -> return ()
            IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
@@ -712,7 +721,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
   = do { addFunDepWork inerts ev_w cls
        ; continueWith workItem  }
 
-interactDict _ wi = pprPanic "interactDict" (ppr wi)
+interactDict' _ _ wi = pprPanic "interactDict" (ppr wi)
 
 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
 -- Add derived constraints from type-class functional dependencies.
@@ -1187,13 +1196,13 @@ doTopReact work_item
 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
 -- Try to use type-class instance declarations to simplify the constraint
 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
-                                          , cc_tyargs = xis })
+                                           , cc_tyargs = xis })
   | isGiven fl   -- Never use instances for Given constraints
   = do { try_fundep_improvement
        ; continueWith work_item }
 
   | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
-  = do { setEvBindIfWanted fl (ctEvTerm ev);
+  = do { setEvBindIfWanted fl (ctEvTerm ev)
        ; stopWith fl "Dict/Top (cached)" }
 
   | isDerived fl  -- Use type-class instances for Deriveds, in the hope
@@ -1695,10 +1704,9 @@ matchClassInst _ _ clas [k,t] _
   | className clas == typeableClassName
   = matchTypeableClass clas k t
 
-matchClassInst dflags _ clas tys loc
+matchClassInst dflags inerts clas tys loc
    = do { instEnvs <- getInstEnvs
-        ; inertCans <- getInertCans
-        ; lazyEqs <- inerts_to_lazy_eqs (inert_irreds inertCans)
+        ; lazyEqs <- inerts_to_lazy_eqs (inert_irreds (inert_cans inerts))
         ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
                                            , text "lazy_eqs =" <+> ppr lazyEqs ]
         ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
@@ -1760,6 +1768,24 @@ inerts_to_lazy_eqs = flatMapBagM $ \ct ->
 extract_lazy_eqs :: LazyEqs [TcPredType] -> [TcPredType]
 extract_lazy_eqs leqs = concatMap (\(_,_,qs) -> qs) (bagToList leqs)
 
+over_lazy_eqs :: ([Type] -> Maybe a) -> LazyEqs l -> [Type] -> Maybe (a, LazyEqs l)
+over_lazy_eqs f leqs tys
+  = go (subsets (bagToList leqs))
+  where
+    subsets :: [(Type, Type, l)] -> [(TvSubst, LazyEqs l)]
+    subsets [] = [(emptyTvSubst, emptyBag)]
+    subsets (elt@(ty1,ty2,_):xs)
+      | Just v <- getTyVar_maybe ty1
+      = let sxs = subsets xs
+        in sxs ++ flip map sxs (\(s, b) -> ( extendTvSubst s v ty2
+                                           , consBag elt b ))
+      | otherwise = pprPanic "Lazy eqs without var in the LHS" (ppr ty1)
+
+    go [] = Nothing
+    go ((subst, l):rest) = case f (substTys subst tys) of
+                             Just x  -> Just (x, l)
+                             Nothing -> go rest
+
 
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~