Fix TcLevel manipulation in TcDerivInfer.simplifyDeriv

The level numbers we were getting simply didn't obey the
invariant (ImplicInv) in TcType
   Note [TcLevel and untouchable type variables]

That leads to chaos. Easy to fix.  I improved the documentation.

I also added an assertion in TcSimplify that checks that
level numbers go up by 1 as we dive inside implications, so
that we catch the problem at source rather than than through
its obscure consequences.

That in turn showed up that TcRules was also generating
constraints that didn't obey (ImplicInv), so I fixed that too.
I have no idea what consequences were lurking behing that
bug, but anyway now it's fixed.  Hooray.

3 files changed, 101 insertions, 64 deletions

diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index 4489d4547b..3f4192fb42 100644
--- a/compiler/typecheck/TcDerivInfer.hs
+++ b/compiler/typecheck/TcDerivInfer.hs
@@ -679,26 +679,34 @@ simplifyDeriv pred tvs thetas
                     ; pure wanteds }
 
        -- See [STEP DAC BUILD]
-       -- Generate the implication constraints constraints to solve with the
-       -- skolemized variables
-       ; wanteds <- mapM mk_wanteds thetas
+       -- Generate the implication constraints, one for each method, to solve
+       -- with the skolemized variables.  Start "one level down" because
+       -- we are going to wrap the result in an implication with tvs_skols,
+       -- in step [DAC RESIDUAL]
+       ; (wanteds, tc_lvl) <- pushTcLevelM $
+                              mapM mk_wanteds thetas
 
        ; traceTc "simplifyDeriv inputs" $
          vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
 
        -- See [STEP DAC SOLVE]
-       -- Simplify the constraints
-       ; solved_implics <- runTcSDeriveds $ solveWantedsAndDrop
-                                          $ unionsWC wanteds
+       -- Simplify the constraints, starting at the same level at which
+       -- they are generated (c.f. the call to runTcSWithEvBinds in
+       -- simplifyInfer)
+       ; solved_wanteds <- setTcLevel tc_lvl   $
+                           runTcSDeriveds      $
+                           solveWantedsAndDrop $
+                           unionsWC wanteds
+
        -- It's not yet zonked!  Obviously zonk it before peering at it
-       ; solved_implics <- zonkWC solved_implics
+       ; solved_wanteds <- zonkWC solved_wanteds
 
        -- See [STEP DAC HOIST]
        -- Split the resulting constraints into bad and good constraints,
        -- building an @unsolved :: WantedConstraints@ representing all
        -- the constraints we can't just shunt to the predicates.
        -- See Note [Exotic derived instance contexts]
-       ; let residual_simple = approximateWC True solved_implics
+       ; let residual_simple = approximateWC True solved_wanteds
              (bad, good) = partitionBagWith get_good residual_simple
 
              get_good :: Ct -> Either Ct PredType
@@ -730,10 +738,9 @@ simplifyDeriv pred tvs thetas
 
        -- See [STEP DAC RESIDUAL]
        ; min_theta_vars <- mapM newEvVar min_theta
-       ; tc_lvl <- getTcLevel
        ; (leftover_implic, _)
-           <- buildImplicationFor (pushTcLevel tc_lvl) skol_info tvs_skols
-                                  min_theta_vars solved_implics
+           <- buildImplicationFor tc_lvl skol_info tvs_skols
+                                  min_theta_vars solved_wanteds
        -- This call to simplifyTop is purely for error reporting
        -- See Note [Error reporting for deriving clauses]
        -- See also Note [Exotic derived instance contexts], which are caught
@@ -815,24 +822,28 @@ it would
 [STEP DAC BUILD]
 So that's what we do.  We build the constraint (call it C1)
 
-   forall b. Ix b => (Show (Maybe s), Ix cc,
-                      Maybe s -> b -> String
-                          ~ Maybe s -> cc -> String)
+   forall[2] b. Ix b => (Show (Maybe s), Ix cc,
+                        Maybe s -> b -> String
+                            ~ Maybe s -> cc -> String)
+
+Here:
+* The level of this forall constraint is forall[2], because we are later
+  going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
 
-Here, the 'b' comes from the quantified type variable in the expected type
-of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
-variable that comes from instantiating the quantified type variable 'c' in
-$gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
+* The 'b' comes from the quantified type variable in the expected type
+  of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
+  variable that comes from instantiating the quantified type variable 'c' in
+  $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
 
-The (Ix b) constraint comes from the context of bar's type
-(i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
-constraints come from the context of $gdm_bar's type
-(i.e., 'to_anyclass_givens' in 'ThetaOrigin').
+* The (Ix b) constraint comes from the context of bar's type
+  (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
+  constraints come from the context of $gdm_bar's type
+  (i.e., 'to_anyclass_givens' in 'ThetaOrigin').
 
-The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
-comes from marrying up the instantiated type of $gdm_bar with the specified
-type of bar. Notice that the type variables from the instance, 's' in this
-case, are global to this constraint.
+* The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
+  comes from marrying up the instantiated type of $gdm_bar with the specified
+  type of bar. Notice that the type variables from the instance, 's' in this
+  case, are global to this constraint.
 
 Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
 unification variable for each iteration of simplifyDeriv. If we re-use the same
@@ -841,8 +852,8 @@ such as Trac #14933.
 
 Similarly for 'baz', givng the constraint C2
 
-   forall. Eq (Maybe s) => (Ord a, Show a,
-                            Maybe s -> Maybe s -> Bool
+   forall[2]. Eq (Maybe s) => (Ord a, Show a,
+                              Maybe s -> Maybe s -> Bool
                                 ~ Maybe s -> Maybe s -> Bool)
 
 In this case baz has no local quantification, so the implication
@@ -853,9 +864,9 @@ variables.
 We can combine these two implication constraints into a single
 constraint (C1, C2), and simplify, unifying cc:=b, to get:
 
-   forall b. Ix b => Show a
+   forall[2] b. Ix b => Show a
    /\
-   forall. Eq (Maybe s) => (Ord a, Show a)
+   forall[2]. Eq (Maybe s) => (Ord a, Show a)
 
 [STEP DAC HOIST]
 Let's call that (C1', C2').  Now we need to hoist the unsolved
@@ -874,7 +885,7 @@ And that's what GHC uses for CX.
 In this case we have solved all the leftover constraints, but what if
 we don't?  Simple!  We just form the final residual constraint
 
-   forall s. CX => (C1',C2')
+   forall[1] s. CX => (C1',C2')
 
 and simplify that. In simple cases it'll succeed easily, because CX
 literally contains the constraints in C1', C2', but if there is anything
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 421cdd69f9..552aa38296 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -64,35 +64,23 @@ tcRuleDecls (HsRules _ src decls)
 tcRuleDecls (XRuleDecls _) = panic "tcRuleDecls"
 
 tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
-tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
-  = addErrCtxt (ruleCtxt $ snd $ unLoc name)  $
-    do { traceTc "---- Rule ------" (pprFullRuleName name)
+tcRule (HsRule fvs rname@(L _ (_,name))
+               act hs_bndrs lhs rhs)
+  = addErrCtxt (ruleCtxt name)  $
+    do { traceTc "---- Rule ------" (pprFullRuleName rname)
 
         -- Note [Typechecking rules]
-       ; (vars, bndr_wanted) <- captureConstraints $
-                                tcRuleBndrs hs_bndrs
-              -- bndr_wanted constraints can include wildcard hole
-              -- constraints, which we should not forget about.
-              -- It may mention the skolem type variables bound by
-              -- the RULE.  c.f. Trac #10072
+       ; (stuff, tc_lvl) <- pushTcLevelM $
+                            generateRuleConstraints hs_bndrs lhs rhs
 
-       ; let (id_bndrs, tv_bndrs) = partition isId vars
-       ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
-            <- tcExtendTyVarEnv tv_bndrs $
-               tcExtendIdEnv    id_bndrs $
-               do { -- See Note [Solve order for RULES]
-                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
-                  ; (rhs', rhs_wanted) <- captureConstraints $
-                                          tcMonoExpr rhs (mkCheckExpType rule_ty)
-                  ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
+       ; let ( id_bndrs, lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) = stuff
 
-       ; traceTc "tcRule 1" (vcat [ pprFullRuleName name
+       ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname
                                   , ppr lhs_wanted
                                   , ppr rhs_wanted ])
-       ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
-       ; (lhs_evs, residual_lhs_wanted) <- simplifyRule (snd $ unLoc name)
-                                              all_lhs_wanted
-                                              rhs_wanted
+
+       ; (lhs_evs, residual_lhs_wanted)
+            <- simplifyRule name tc_lvl lhs_wanted rhs_wanted
 
        -- SimplfyRule Plan, step 4
        -- Now figure out what to quantify over
@@ -113,7 +101,7 @@ tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
        ; gbls  <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
                                       -- monomorphic bindings from the MR; test tc111
        ; qtkvs <- quantifyTyVars gbls forall_tkvs
-       ; traceTc "tcRule" (vcat [ pprFullRuleName name
+       ; traceTc "tcRule" (vcat [ pprFullRuleName rname
                                 , ppr forall_tkvs
                                 , ppr qtkvs
                                 , ppr rule_ty
@@ -125,19 +113,44 @@ tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
        -- For the LHS constraints we must solve the remaining constraints
        -- (a) so that we report insoluble ones
        -- (b) so that we bind any soluble ones
-       ; let skol_info = RuleSkol (snd (unLoc name))
-       ; (lhs_implic, lhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
+       ; let skol_info = RuleSkol name
+       ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
                                          lhs_evs residual_lhs_wanted
-       ; (rhs_implic, rhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
+       ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
                                          lhs_evs rhs_wanted
 
        ; emitImplications (lhs_implic `unionBags` rhs_implic)
-       ; return (HsRule (HsRuleRn fv_lhs fv_rhs)name act
+       ; return (HsRule fvs rname act
                     (map (noLoc . RuleBndr noExt . noLoc) (qtkvs ++ tpl_ids))
                     (mkHsDictLet lhs_binds lhs')
                     (mkHsDictLet rhs_binds rhs')) }
 tcRule (XRuleDecl _) = panic "tcRule"
 
+generateRuleConstraints :: [LRuleBndr GhcRn] -> LHsExpr GhcRn -> LHsExpr GhcRn
+                        -> TcM ( [TcId]
+                               , LHsExpr GhcTc, WantedConstraints
+                               , LHsExpr GhcTc, WantedConstraints
+                               , TcType )
+generateRuleConstraints hs_bndrs lhs rhs
+  = do { (vars, bndr_wanted) <- captureConstraints $
+                                tcRuleBndrs hs_bndrs
+              -- bndr_wanted constraints can include wildcard hole
+              -- constraints, which we should not forget about.
+              -- It may mention the skolem type variables bound by
+              -- the RULE.  c.f. Trac #10072
+
+       ; let (id_bndrs, tv_bndrs) = partition isId vars
+       ; tcExtendTyVarEnv tv_bndrs $
+         tcExtendIdEnv    id_bndrs $
+    do { -- See Note [Solve order for RULES]
+         ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
+       ; (rhs',            rhs_wanted) <- captureConstraints $
+                                          tcMonoExpr rhs (mkCheckExpType rule_ty)
+       ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
+       ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
+                -- Slightly curious that tv_bndrs is not returned
+
+
 tcRuleBndrs :: [LRuleBndr GhcRn] -> TcM [Var]
 tcRuleBndrs []
   = return []
@@ -307,6 +320,7 @@ terrible, so we avoid the problem by cloning the constraints.
 -}
 
 simplifyRule :: RuleName
+             -> TcLevel                 -- Level at which to solve the constraints
              -> WantedConstraints       -- Constraints from LHS
              -> WantedConstraints       -- Constraints from RHS
              -> TcM ( [EvVar]               -- Quantify over these LHS vars
@@ -314,7 +328,7 @@ simplifyRule :: RuleName
 -- See Note [The SimplifyRule Plan]
 -- NB: This consumes all simple constraints on the LHS, but not
 -- any LHS implication constraints.
-simplifyRule name lhs_wanted rhs_wanted
+simplifyRule name tc_lvl lhs_wanted rhs_wanted
   = do {
        -- Note [The SimplifyRule Plan] step 1
        -- First solve the LHS and *then* solve the RHS
@@ -322,12 +336,13 @@ simplifyRule name lhs_wanted rhs_wanted
        -- Why clone?  See Note [Simplify cloned constraints]
        ; lhs_clone <- cloneWC lhs_wanted
        ; rhs_clone <- cloneWC rhs_wanted
-       ; runTcSDeriveds $
-             do { _ <- solveWanteds lhs_clone
-                ; _ <- solveWanteds rhs_clone
+       ; setTcLevel tc_lvl $
+         runTcSDeriveds    $
+         do { _ <- solveWanteds lhs_clone
+            ; _ <- solveWanteds rhs_clone
                   -- Why do them separately?
                   -- See Note [Solve order for RULES]
-                ; return () }
+            ; return () }
 
        -- Note [The SimplifyRule Plan] step 2
        ; lhs_wanted <- zonkWC lhs_wanted
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index da7807558f..c504ad9bdb 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1495,6 +1495,8 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
   = do { inerts <- getTcSInerts
        ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
 
+       ; when debugIsOn check_tc_level
+
          -- Solve the nested constraints
        ; (no_given_eqs, given_insols, residual_wanted)
             <- nestImplicTcS ev_binds_var tclvl $
@@ -1538,6 +1540,15 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
 
        ; return (floated_eqs, res_implic) }
 
+  where
+    -- TcLevels must be strictly increasing (see (ImplicInv) in
+    -- Note [TcLevel and untouchable type variables] in TcType),
+    -- and in fact I thinkthey should always increase one level at a time.
+    check_tc_level = do { cur_lvl <- TcS.getTcLevel
+                        ; MASSERT2( tclvl == pushTcLevel cur_lvl
+                                  , text "Cur lvl =" <+> ppr cur_lvl $$
+                                    text "Imp lvl =" <+> ppr tclvl ) }
+
 ----------------------
 setImplicationStatus :: Implication -> TcS (Maybe Implication)
 -- Finalise the implication returned from solveImplication: