[commit: ghc] wip/impredicativity: Instantiation in approximation is now deep (3d5a3f2)

[git at git.haskell.org]

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

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

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

commit 3d5a3f20e1c849992783c794e30cfc2e2fd57ae2
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Wed Jul 29 08:00:39 2015 +0200

    Instantiation in approximation is now deep
    
    If we have a left-over constraint
      `forall a. Q => (forall b. Q' => t) <~ v`
    previously it would be approximated to
      `v ~ [a -> alpha](forall b. Q' => t)  /\  [a -> alpha]Q`
    whereas now it is approximated to
      `v ~ [a -> alpha, b -> beta]t  /\  [a -> alpha]Q
           /\  [a -> alpha, b -> beta]Q'`
    
    This fixes several problems compiling the base Data.Category module.


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

3d5a3f20e1c849992783c794e30cfc2e2fd57ae2
 compiler/typecheck/TcRules.hs    | 26 ++++++++++++++++++++------
 compiler/typecheck/TcSMonad.hs   | 23 +++++++++++++++++------
 compiler/typecheck/TcSimplify.hs |  2 +-
 3 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 7a12cfa..4803aa7 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -317,10 +317,10 @@ simplifyRule name lhs_wanted rhs_wanted
        ; let lhs_wanted_simple = wc_simple lhs_wanted
        ; (lhs_wanted_inst, _) <- runTcS $
            fmap andManyCts $ mapM instantiateWC (bagToList lhs_wanted_simple)
-       ; let same_type x y = ctPred x == ctPred y
-             none_with_same_type x = not (anyBag (same_type x) lhs_wanted_simple)
-             lhs_wanted_inst' = filterBag none_with_same_type lhs_wanted_inst
-
+       ; let lhs_wanted_inst' = remove_duplicates lhs_wanted_simple lhs_wanted_inst
+                 -- Build new WantedConstraints by adding the new instantiated
+                 -- We need to be careful not to duplicate constraints,
+                 -- because it would lead to too many forall's
        ; let new_lhs_wanted_simple = wc_simple lhs_wanted `unionBags` lhs_wanted_inst'
              new_lhs_wanted = lhs_wanted { wc_simple = new_lhs_wanted_simple }
 
@@ -331,8 +331,15 @@ simplifyRule name lhs_wanted rhs_wanted
                 ; rhs_resid <- solveWanteds rhs_wanted
                 ; return (insolubleWC tc_lvl lhs_resid || insolubleWC tc_lvl rhs_resid) }
 
-       ; zonked_lhs_simples <- zonkSimples new_lhs_wanted_simple
-       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_simples
+       ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
+       ; zonked_lhs_inst    <- zonkSimples lhs_wanted_inst'
+                  -- We need to remove duplicates once again,
+                  -- because we might get new duplicated constraints
+                  -- from unification of variables
+       ; let zonked_lhs = zonked_lhs_simples `unionBags`
+                            remove_duplicates zonked_lhs_simples zonked_lhs_inst
+
+       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs
              quantify_me  -- Note [RULE quantification over equalities]
                | insoluble = quantify_insol
                | otherwise = quantify_normal
@@ -358,3 +365,10 @@ simplifyRule name lhs_wanted rhs_wanted
 
        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
                 , lhs_wanted { wc_simple = non_q_cts }) }
+
+remove_duplicates :: Cts -> Cts -> Cts
+remove_duplicates main new
+  = filterBag none_with_same_type new
+  where
+    same_type x y = ctPred x == ctPred y
+    none_with_same_type x = not (anyBag (same_type x) main)
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index cf391ce..a0c36d4 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -15,8 +15,8 @@ module TcSMonad (
     TcS, runTcS, runTcSWithEvBinds,
     failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
 
-    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq, splitInst,
-    deferTcSForAllInstanceOf,
+    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
+    splitInst, deeplySplitInst, deferTcSForAllInstanceOf,
 
     -- Tracing etc
     panicTcS, traceTcS,
@@ -2930,7 +2930,18 @@ splitInst :: Type -> TcS ([TyVar], ThetaType, Type)
 splitInst sigma
   = do { let (qvars, q, ty) = tcSplitSigmaTy sigma
          -- instantiate variables for q and ty
-         ; (subst, inst_vars) <- wrapTcS $ TcM.tcInstTyVars qvars
-         ; let q_subst  = map (Type.substTy subst) q
-               ty_subst = Type.substTy subst ty
-         ; return (inst_vars, q_subst, ty_subst) }
+       ; (subst, inst_vars) <- wrapTcS $ TcM.tcInstTyVars qvars
+       ; let q_subst  = map (Type.substTy subst) q
+             ty_subst = Type.substTy subst ty
+       ; return (inst_vars, q_subst, ty_subst) }
+
+-- Split a sigma type and instantiate its variables, deeply
+deeplySplitInst :: Type -> TcS ([TyVar], ThetaType, Type)
+deeplySplitInst sigma
+  = do { (qvars, q, ty) <- splitInst sigma
+       ; case (qvars, q) of
+           ([], [])
+             -> return (qvars, q, ty)
+           (_, _)
+             -> do { (qvars', q', ty') <- deeplySplitInst ty
+                   ; return ( qvars ++ qvars', q ++ q', ty') } }
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index e37df77..f080c09 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1366,7 +1366,7 @@ instantiateWC :: Ct -> TcS Cts
 instantiateWC ct
   | isWantedCt ct, InstanceOfPred lhs rhs <- classifyPredType (ctPred ct)
   = do { let loc = ctLoc ct
-       ; (_qvars, q, ty) <- splitInst lhs
+       ; (_qvars, q, ty) <- deeplySplitInst lhs
        ; new_ev_qs <- mapM (newWantedEvVarNC loc) q
        ; let eq = mkTcEqPred ty rhs
        ; new_ev_ty <- newWantedEvVarNC loc eq