Kill floatEqualities completelywip/T17656

This patch delivers on #17656, by entirel killing off the complex
floatEqualities mechanism.  Previously, floatEqualities would float an
equality out of an implication, so that it could be solved at an outer
level. But now we simply do unification in-place, without floating the
constraint, relying on level numbers to determine untouchability.

There are a number of important new Notes:

* GHC.Tc.Utils.Unify Note [Unification preconditions]
  describes the preconditions for unification, including both
  skolem-escape and touchability.

* GHC.Tc.Solver.Interact Note [Solve by unification]
  describes what we do when we do unify

* GHC.Tc.Solver.Monad Note [The Unification Level Flag]
  describes how we control solver iteration under this new scheme

* GHC.Tc.Solver.Monad Note [Tracking Given equalities]
  describes how we track when we have Given equalities

* GHC.Tc.Types.Constraint Note [HasGivenEqs]
  is a new explanation of the ic_given_eqs field of an implication

A big raft of subtle Notes in Solver, concerning floatEqualities,
disappears.

Main code changes:

* GHC.Tc.Solver.floatEqualities disappears entirely

* GHC.Tc.Solver.Monad: new fields in InertCans, inert_given_eq_lvl
  and inert_given_eq, updated by updateGivenEqs
  See Note [Tracking Given equalities].

* In exchange for updateGivenEqa, GHC.Tc.Solver.Monad.getHasGivenEqs
  is much simpler and more efficient

* I found I could kill of metaTyVarUpdateOK entirely

One test case T14683 showed a 5.1% decrease in compile-time
allocation; and T5631 was down 2.2%. Other changes were small.

Metric Decrease:
    T14683
    T5631

1 files changed, 87 insertions, 41 deletions

diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index dc20b90260..e8ab8ad82a 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, MultiWayIf #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
@@ -14,7 +14,6 @@ import GHC.Prelude
 import GHC.Types.Basic ( SwapFlag(..),
                          infinity, IntWithInf, intGtLimit )
 import GHC.Tc.Solver.Canonical
-import GHC.Tc.Utils.Unify( canSolveByUnification )
 import GHC.Types.Var.Set
 import GHC.Core.Type as Type
 import GHC.Core.InstEnv         ( DFunInstType )
@@ -39,6 +38,7 @@ import GHC.Tc.Types
 import GHC.Tc.Types.Constraint
 import GHC.Core.Predicate
 import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo )
 import GHC.Tc.Solver.Monad
 import GHC.Data.Bag
 import GHC.Utils.Monad ( concatMapM, foldlM )
@@ -106,8 +106,6 @@ solveSimpleGivens givens
                      go new_givens }
 
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
--- NB: 'simples' may contain /derived/ equalities, floated
---     out from a nested implication. So don't discard deriveds!
 -- The result is not necessarily zonked
 solveSimpleWanteds simples
   = do { traceTcS "solveSimpleWanteds {" (ppr simples)
@@ -430,12 +428,11 @@ interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
 
 interactWithInertsStage wi
   = do { inerts <- getTcSInerts
-       ; lvl  <- getTcLevel
        ; let ics = inert_cans inerts
        ; case wi of
-             CEqCan    {} -> interactEq lvl  ics wi
-             CIrredCan {} -> interactIrred   ics wi
-             CDictCan  {} -> interactDict    ics wi
+             CEqCan    {} -> interactEq    ics wi
+             CIrredCan {} -> interactIrred ics wi
+             CDictCan  {} -> interactDict  ics wi
              _ -> pprPanic "interactWithInerts" (ppr wi) }
                 -- CNonCanonical have been canonicalised
 
@@ -734,25 +731,26 @@ Example of (b): assume a top-level class and instance declaration:
 
 Assume we have started with an implication:
 
-  forall c. Eq c => { wc_simple = D [c] c [W] }
+  forall c. Eq c => { wc_simple = [W] D [c] c }
 
-which we have simplified to:
+which we have simplified to, with a Derived constraing coming from
+D's functional dependency:
 
-  forall c. Eq c => { wc_simple = D [c] c [W]
-                                  (c ~ [c]) [D] }
+  forall c. Eq c => { wc_simple = [W] D [c] c [W]
+                                  [D] (c ~ [c]) }
 
-For some reason, e.g. because we floated an equality somewhere else,
-we might try to re-solve this implication. If we do not do a
-dropDerivedWC, then we will end up trying to solve the following
-constraints the second time:
+When iterating the solver, we might try to re-solve this
+implication. If we do not do a dropDerivedWC, then we will end up
+trying to solve the following constraints the second time:
 
-  (D [c] c) [W]
-  (c ~ [c]) [D]
+  [W] (D [c] c)
+  [D] (c ~ [c])
 
 which will result in two Deriveds to end up in the insoluble set:
 
-  wc_simple   = D [c] c [W]
-               (c ~ [c]) [D], (c ~ [c]) [D]
+  wc_simple = [W] D [c] c
+              [D] (c ~ [c])
+              [D] (c ~ [c])
 -}
 
 {-
@@ -1439,8 +1437,8 @@ inertsCanDischarge inerts lhs rhs fr
       | otherwise
       = False  -- Work item is fully discharged
 
-interactEq :: TcLevel -> InertCans -> Ct -> TcS (StopOrContinue Ct)
-interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs
+interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
+interactEq inerts workItem@(CEqCan { cc_lhs = lhs
                                          , cc_rhs = rhs
                                          , cc_ev = ev
                                          , cc_eq_rel = eq_rel })
@@ -1465,24 +1463,43 @@ interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs
   = do { traceTcS "Not unifying representational equality" (ppr workItem)
        ; continueWith workItem }
 
-    -- try improvement, if possible
-  | TyFamLHS fam_tc fam_args <- lhs
-  , isImprovable ev
-  = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs
-       ; continueWith workItem }
-
-  | TyVarLHS tv <- lhs
-  , canSolveByUnification tclvl tv rhs
-  = do { solveByUnification ev tv rhs
-       ; n_kicked <- kickOutAfterUnification tv
-       ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
-
   | otherwise
-  = continueWith workItem
-
-interactEq _ _ wi = pprPanic "interactEq" (ppr wi)
-
-solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
+  = case lhs of
+       TyVarLHS tv -> tryToSolveByUnification workItem ev tv rhs
+
+       TyFamLHS tc args -> do { when (isImprovable ev) $
+                                 -- Try improvement, if possible
+                                improveLocalFunEqs ev inerts tc args rhs
+                              ; continueWith workItem }
+
+interactEq _ wi = pprPanic "interactEq" (ppr wi)
+
+----------------------
+-- We have a meta-tyvar on the left, and metaTyVarUpateOK has said "yes"
+-- So try to solve by unifying.
+-- Three reasons why not:
+--    Skolem escape
+--    Given equalities (GADTs)
+--    Unifying a TyVarTv with a non-tyvar type
+tryToSolveByUnification :: Ct -> CtEvidence
+                        -> TcTyVar   -- LHS tyvar
+                        -> TcType    -- RHS
+                        -> TcS (StopOrContinue Ct)
+tryToSolveByUnification work_item ev tv rhs
+  = do { can_unify <- unifyTest ev tv rhs
+       ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs
+                                                  , ppr can_unify ])
+
+       ; case can_unify of
+           NoUnify -> continueWith work_item
+           -- For the latter two cases see Note [Solve by unification]
+           UnifySameLevel -> solveByUnification ev tv rhs
+           UnifyOuterLevel free_metas tv_lvl
+             -> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas
+                   ; setUnificationFlag tv_lvl
+                   ; solveByUnification ev tv rhs } }
+
+solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct)
 -- Solve with the identity coercion
 -- Precondition: kind(xi) equals kind(tv)
 -- Precondition: CtEvidence is Wanted or Derived
@@ -1504,9 +1521,10 @@ solveByUnification wd tv xi
                              text "Coercion:" <+> pprEq tv_ty xi,
                              text "Left Kind is:" <+> ppr (tcTypeKind tv_ty),
                              text "Right Kind is:" <+> ppr (tcTypeKind xi) ]
-
        ; unifyTyVar tv xi
-       ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
+       ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi))
+       ; n_kicked <- kickOutAfterUnification tv
+       ; return (Stop wd (text "Solved by unification" <+> pprKicked n_kicked)) }
 
 {- Note [Avoid double unifications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1542,6 +1560,34 @@ and we want to get alpha := N b.
 See also #15144, which was caused by unifying a representational
 equality.
 
+Note [Solve by unification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we solve
+   alpha[n] ~ ty
+by unification, there are two cases to consider
+
+* UnifySameLevel: if the ambient level is 'n', then
+  we can simply update alpha := ty, and do nothing else
+
+* UnifyOuterLevel free_metas n: if the ambient level is greater than
+  'n' (the level of alpha), in addition to setting alpha := ty we must
+  do two other things:
+
+  1. Promote all the free meta-vars of 'ty' to level n.  After all,
+     alpha[n] is at level n, and so if we set, say,
+          alpha[n] := Maybe beta[m],
+     we must ensure that when unifying beta we do skolem-escape checks
+     etc relevent to level n.  Simple way to do that: promote beta to
+     level n.
+
+  2. Set the Unification Level Flag to record that a level-n unification has
+     taken place. See Note [The Unification Level Flag] in GHC.Tc.Solver.Monad
+
+NB: UnifySameLevel is just an optimisation for UnifyOuterLevel. Promotion
+would be a no-op, and setting the unification flag unnecessarily would just
+make the solver iterate more often.  (We don't need to iterate when unifying
+at the ambient level becuase of the kick-out mechanism.)
+
 
 ************************************************************************
 *                                                                      *