[commit: ghc] wip/impredicativity: Fix incorrect instantiation of quantifiers in RULES (c54e4d6)

[git at git.haskell.org]

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

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

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

commit c54e4d67729fdcdae595378a8cc06207c1d0c007
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Mon Jun 29 12:26:37 2015 +0200

    Fix incorrect instantiation of quantifiers in RULES


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

c54e4d67729fdcdae595378a8cc06207c1d0c007
 compiler/typecheck/TcExpr.hs  |  4 ++--
 compiler/typecheck/TcHsSyn.hs | 12 +++++++-----
 compiler/typecheck/TcRules.hs | 18 +++++++++---------
 3 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index ea84eec..860d301 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -1050,7 +1050,7 @@ tc_app fun args fun_ty res_ty special
         -- > f x = S (error x)
         -- Without it, the `a` coming from `f` cannot be unified with
         -- the second type variable of `error`
-        ; case getTyVar_maybe res_ty of
+        ; case getTyVar_maybe actual_res_ty of
           { Nothing
               -> do { ev_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $
                         emitWanted AppOrigin (mkInstanceOfPred actual_res_ty res_ty)
@@ -1065,7 +1065,7 @@ tc_app fun args fun_ty res_ty special
                     ; return $ NormalTcAppResult
                        (mkLHsWrapCo co_fun fun1)  -- Instantiated function
                        args1                      -- Arguments
-                       (mkHsWrapCo co_res) } } } -- Coercion to expected result type
+                       (mkHsWrapCo co_res) } } }  -- Coercion to expected result type
 
 mk_app_msg :: LHsExpr Name -> SDoc
 mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index f9eacf6..8853607 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1322,7 +1322,8 @@ zonkEvBind env (EvBind { eb_lhs = var, eb_rhs = term, eb_is_given = is_given })
          -- This has a very big effect on some programs (eg Trac #5030)
        ; term' <- case getEqPredTys_maybe (idType var') of
            Just (r, ty1, ty2) | ty1 `eqType` ty2
-                  -> return (EvCoercion (mkTcReflCo r ty1))
+                  -> do { ty1' <- zonkTcTypeToType env ty1
+                        ; return (EvCoercion (mkTcReflCo r ty1')) }
            _other -> zonkEvTerm env term
 
       ; return (EvBind { eb_lhs = var', eb_rhs = term', eb_is_given = is_given }) }
@@ -1339,10 +1340,11 @@ zonkEvInstanceOf env (EvInstanceOfInst tys co q)
        ; q' <- mapM (zonkEvTerm env) q
        ; return (EvInstanceOfInst tys' co' q') }
 zonkEvInstanceOf env (EvInstanceOfLet tys qvars bnds i)
-  = do { let qvars' = map (zonkIdOcc env) qvars
-       ; (env', bnds') <- zonkTcEvBinds env bnds
-       ; let i' = zonkIdOcc env' i
-       ; return (EvInstanceOfLet tys qvars' bnds' i') }
+  = do { (env', tys') <- zonkTyBndrsX env tys
+       ; let qvars' = map (zonkIdOcc env') qvars
+       ; (env'', bnds') <- zonkTcEvBinds env' bnds
+       ; let i' = zonkIdOcc env'' i
+       ; return (EvInstanceOfLet tys' qvars' bnds' i') }
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 9972af0..4335717 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -299,20 +299,19 @@ simplifyRule :: RuleName
 simplifyRule name lhs_wanted rhs_wanted
   = do {         -- We allow ourselves to unify environment
                  -- variables: runTcS runs with topTcLevel
-         (insoluble, _) <- runTcS $
+         ((insoluble, lhs_extra), _) <- runTcS $
              do { -- First solve the LHS and *then* solve the RHS
                   -- See Note [Solve order for RULES]
                   lhs_resid <- solveWanteds lhs_wanted
+                ; let lhs_resid_simple = wc_simple lhs_resid
                 ; lhs_inst <- fmap andManyCts $
-                    mapM instantiateWC (bagToList (wc_simple lhs_resid))
+                    mapM instantiateWC (bagToList lhs_resid_simple)
                 ; lhs_inst_resid <- solveWanteds lhs_resid { wc_simple = lhs_inst }
                 ; rhs_resid <- solveWanteds rhs_wanted
-                ; return (insolubleWC lhs_inst_resid || insolubleWC rhs_resid) }
+                ; return (insolubleWC lhs_inst_resid || insolubleWC rhs_resid, lhs_inst) }
 
-       ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
-       ; (zonked_lhs_inst, _) <- runTcS $ fmap andManyCts $
-           mapM instantiateWC (bagToList zonked_lhs_simples)
-       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_inst
+       ; zonked_lhs <- zonkSimples (wc_simple lhs_wanted `unionBags` lhs_extra)
+       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs
              quantify_me  -- Note [RULE quantification over equalities]
                | insoluble = quantify_insol
                | otherwise = quantify_normal
@@ -322,6 +321,8 @@ simplifyRule name lhs_wanted rhs_wanted
              quantify_normal ct
                | EqPred NomEq t1 t2 <- classifyPredType (ctPred ct)
                = not (t1 `tcEqType` t2)
+               | InstanceOfPred _ _ <- classifyPredType (ctPred ct)
+               = False
                | otherwise
                = True
 
@@ -329,8 +330,7 @@ simplifyRule name lhs_wanted rhs_wanted
          vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
               , text "lhs_wantd" <+> ppr lhs_wanted
               , text "rhs_wantd" <+> ppr rhs_wanted
-              , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
-              , text "zonked_lhs_inst" <+> ppr zonked_lhs_inst
+              , text "zonked_lhs" <+> ppr zonked_lhs
               , text "q_cts"      <+> ppr q_cts
               , text "non_q_cts"  <+> ppr non_q_cts ]