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.

1 files changed, 42 insertions, 31 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