Kill derived constraintswip/derived-refactor

Co-authored by: Sam Derbyshire

Previously, GHC had three flavours of constraint:
Wanted, Given, and Derived. This removes Derived constraints.

Though serving a number of purposes, the most important role
of Derived constraints was to enable better error messages.
This job has been taken over by the new RewriterSets, as explained
in Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint.

Other knock-on effects:
 - Various new Notes as I learned about under-described bits of GHC

 - A reshuffling around the AST for implicit-parameter bindings,
   with better integration with TTG.

 - Various improvements around fundeps. These were caused by the
   fact that, previously, fundep constraints were all Derived,
   and Derived constraints would get dropped. Thus, an unsolved
   Derived didn't stop compilation. Without Derived, this is no
   longer possible, and so we have to be considerably more careful
   around fundeps.

 - A nice little refactoring in GHC.Tc.Errors to center the work
   on a new datatype called ErrorItem. Constraints are converted
   into ErrorItems at the start of processing, and this allows for
   a little preprocessing before the main classification.

 - This commit also cleans up the behavior in generalisation around
   functional dependencies. Now, if a variable is determined by
   functional dependencies, it will not be quantified. This change
   is user facing, but it should trim down GHC's strange behavior
   around fundeps.

 - Previously, reportWanteds did quite a bit of work, even on an empty
   WantedConstraints. This commit adds a fast path.

 - Now, GHC will unconditionally re-simplify constraints during
   quantification. See Note [Unconditionally resimplify constraints when
   quantifying], in GHC.Tc.Solver.

Close #18398.
Close #18406.
Solve the fundep-related non-confluence in #18851.
Close #19131.
Close #19137.
Close #20922.
Close #20668.
Close #19665.

-------------------------
Metric Decrease:
    LargeRecord
    T9872b
    T9872b_defer
    T9872d
    TcPlugin_RewritePerf
-------------------------

1 files changed, 27 insertions, 20 deletions

diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index cfbebcd368..e3baf4c4f9 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -5,7 +5,7 @@
 
 -}
 
-
+{-# LANGUAGE DeriveFunctor #-}
 
 -- | Functional dependencies
 --
@@ -18,6 +18,7 @@ module GHC.Tc.Instance.FunDeps
    , checkInstCoverage
    , checkFunDeps
    , pprFundeps
+   , instFD, closeWrtFunDeps
    )
 where
 
@@ -43,6 +44,7 @@ import GHC.Utils.FV
 import GHC.Utils.Error( Validity'(..), Validity, allValid )
 import GHC.Utils.Misc
 import GHC.Utils.Panic
+import GHC.Utils.Panic.Plain ( assert )
 
 import GHC.Data.Pair             ( Pair(..) )
 import Data.List        ( nubBy )
@@ -118,6 +120,7 @@ data FunDepEqn loc
           , fd_pred1 :: PredType   -- The FunDepEqn arose from
           , fd_pred2 :: PredType   --  combining these two constraints
           , fd_loc   :: loc  }
+    deriving Functor
 
 {-
 Given a bunch of predicates that must hold, such as
@@ -350,7 +353,7 @@ Example
 
 For the coverage condition, we check
    (normal)    fv(t2) `subset` fv(t1)
-   (liberal)   fv(t2) `subset` oclose(fv(t1), theta)
+   (liberal)   fv(t2) `subset` closeWrtFunDeps(fv(t1), theta)
 
 The liberal version  ensures the self-consistency of the instance, but
 it does not guarantee termination. Example:
@@ -363,7 +366,7 @@ it does not guarantee termination. Example:
    instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
 
 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
-But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
+But it is the case that fv([c]) `subset` closeWrtFunDeps( theta, fv(a,[b]) )
 
 But it is a mistake to accept the instance because then this defn:
         f = \ b x y -> if b then x .*. [y] else y
@@ -396,7 +399,7 @@ checkInstCoverage be_liberal clas theta inst_taus
          undetermined_tvs | be_liberal = liberal_undet_tvs
                           | otherwise  = conserv_undet_tvs
 
-         closed_ls_tvs = oclose theta ls_tvs
+         closed_ls_tvs = closeWrtFunDeps theta ls_tvs
          liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
          conserv_undet_tvs = (`minusVarSet` ls_tvs)        <$> rs_tvs
 
@@ -407,7 +410,7 @@ checkInstCoverage be_liberal clas theta inst_taus
                vcat [ -- text "ls_tvs" <+> ppr ls_tvs
                       -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
                       -- , text "theta" <+> ppr theta
-                      -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
+                      -- , text "closeWrtFunDeps" <+> ppr (closeWrtFunDeps theta (closeOverKinds ls_tvs))
                       -- , text "rs_tvs" <+> ppr rs_tvs
                       sep [ text "The"
                             <+> ppWhen be_liberal (text "liberal")
@@ -466,17 +469,17 @@ Is the instance OK? Does {l,r,xs} determine v?  Well:
     we get {l,k,xs} -> b
 
   * Note the 'k'!! We must call closeOverKinds on the seed set
-    ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
+    ls_tvs = {l,r,xs}, BEFORE doing closeWrtFunDeps, else the {l,k,xs}->b
     fundep won't fire.  This was the reason for #10564.
 
-  * So starting from seeds {l,r,xs,k} we do oclose to get
+  * So starting from seeds {l,r,xs,k} we do closeWrtFunDeps to get
     first {l,r,xs,k,b}, via the HMemberM constraint, and then
     {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
 
   * And that fixes v.
 
 However, we must closeOverKinds whenever augmenting the seed set
-in oclose!  Consider #10109:
+in closeWrtFunDeps!  Consider #10109:
 
   data Succ a   -- Succ :: forall k. k -> *
   class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
@@ -492,25 +495,27 @@ the variables free in (Succ {k3} ab).
 Bottom line:
   * closeOverKinds on initial seeds (done automatically
     by tyCoVarsOfTypes in checkInstCoverage)
-  * and closeOverKinds whenever extending those seeds (in oclose)
+  * and closeOverKinds whenever extending those seeds (in closeWrtFunDeps)
 
 Note [The liberal coverage condition]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(oclose preds tvs) closes the set of type variables tvs,
+(closeWrtFunDeps preds tvs) closes the set of type variables tvs,
 wrt functional dependencies in preds.  The result is a superset
 of the argument set.  For example, if we have
         class C a b | a->b where ...
 then
-        oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
+        closeWrtFunDeps [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
 because if we know x and y then that fixes z.
 
 We also use equality predicates in the predicates; if we have an
 assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
 also know `t2` and the other way.
-  eg    oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
+  eg    closeWrtFunDeps [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
 
-oclose is used (only) when checking the coverage condition for
-an instance declaration
+closeWrtFunDeps is used
+ - when checking the coverage condition for an instance declaration
+ - when determining which tyvars are unquantifiable during generalization, in
+   GHC.Tc.Solver.decideMonoTyVars.
 
 Note [Equality superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -521,10 +526,10 @@ Remember from Note [The equality types story] in GHC.Builtin.Types.Prim, that
   * (a ~~ b) is a superclass of (a ~ b)
   * (a ~# b) is a superclass of (a ~~ b)
 
-So when oclose expands superclasses we'll get a (a ~# [b]) superclass.
+So when closeWrtFunDeps expands superclasses we'll get a (a ~# [b]) superclass.
 But that's an EqPred not a ClassPred, and we jolly well do want to
 account for the mutual functional dependencies implied by (t1 ~# t2).
-Hence the EqPred handling in oclose.  See #10778.
+Hence the EqPred handling in closeWrtFunDeps.  See #10778.
 
 Note [Care with type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -534,7 +539,7 @@ Consider (#12803)
   type family G c d = r | r -> d
 
 Now consider
-  oclose (C (F a b) (G c d)) {a,b}
+  closeWrtFunDeps (C (F a b) (G c d)) {a,b}
 
 Knowing {a,b} fixes (F a b) regardless of the injectivity of F.
 But knowing (G c d) fixes only {d}, because G is only injective
@@ -543,12 +548,14 @@ in its second parameter.
 Hence the tyCoVarsOfTypes/injTyVarsOfTypes dance in tv_fds.
 -}
 
-oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
+closeWrtFunDeps :: [PredType] -> TyCoVarSet -> TyCoVarSet
 -- See Note [The liberal coverage condition]
-oclose preds fixed_tvs
+closeWrtFunDeps preds fixed_tvs
   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
-  | otherwise   = fixVarSet extend fixed_tvs
+  | otherwise   = assert (closeOverKinds fixed_tvs == fixed_tvs)
+                $ fixVarSet extend fixed_tvs
   where
+
     extend fixed_tvs = foldl' add fixed_tvs tv_fds
        where
           add fixed_tvs (ls,rs)