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
-------------------------

5 files changed, 67 insertions, 32 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index ef6d4af5ec..22f3c32201 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -122,8 +122,7 @@ module GHC.Core.Coercion (
 
         multToCo,
 
-        hasCoercionHoleTy, hasCoercionHoleCo,
-        HoleSet, coercionHolesOfType, coercionHolesOfCo,
+        hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,
 
         setCoHoleType
        ) where
@@ -156,7 +155,6 @@ import GHC.Builtin.Types.Prim
 import GHC.Data.List.SetOps
 import GHC.Data.Maybe
 import GHC.Types.Unique.FM
-import GHC.Types.Unique.Set
 
 import GHC.Utils.Misc
 import GHC.Utils.Outputable
@@ -2725,16 +2723,13 @@ has_co_hole_co :: Coercion -> Monoid.Any
 (has_co_hole_ty, _, has_co_hole_co, _)
   = foldTyCo folder ()
   where
-    folder = TyCoFolder { tcf_view  = const Nothing
+    folder = TyCoFolder { tcf_view  = noView
                         , tcf_tyvar = const2 (Monoid.Any False)
                         , tcf_covar = const2 (Monoid.Any False)
                         , tcf_hole  = const2 (Monoid.Any True)
                         , tcf_tycobinder = const2
                         }
 
-    const2 :: a -> b -> c -> a
-    const2 x _ _ = x
-
 -- | Is there a coercion hole in this type?
 hasCoercionHoleTy :: Type -> Bool
 hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
@@ -2743,19 +2738,16 @@ hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
 hasCoercionHoleCo :: Coercion -> Bool
 hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
 
--- | A set of 'CoercionHole's
-type HoleSet = UniqSet CoercionHole
-
--- | Extract out all the coercion holes from a given type
-coercionHolesOfType :: Type -> UniqSet CoercionHole
-coercionHolesOfCo   :: Coercion -> UniqSet CoercionHole
-(coercionHolesOfType, _, coercionHolesOfCo, _) = foldTyCo folder ()
+hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
+hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty)
   where
-    folder = TyCoFolder { tcf_view  = const Nothing  -- don't look through synonyms
-                        , tcf_tyvar = \ _ _ -> mempty
-                        , tcf_covar = \ _ _ -> mempty
-                        , tcf_hole  = const unitUniqSet
-                        , tcf_tycobinder = \ _ _ _ -> ()
+    (f, _, _, _) = foldTyCo folder ()
+
+    folder = TyCoFolder { tcf_view  = noView
+                        , tcf_tyvar = const2 (Monoid.Any False)
+                        , tcf_covar = const2 (Monoid.Any False)
+                        , tcf_hole  = \ _ h -> Monoid.Any (getUnique h == getUnique hole)
+                        , tcf_tycobinder = const2
                         }
 
 -- | Set the type of a 'CoercionHole'
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index bf6d10f0f7..3de166364b 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -30,6 +30,7 @@ module GHC.Core.Predicate (
   -- Implicit parameters
   isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
   isCallStackTy, isCallStackPred, isCallStackPredTy,
+  isIPPred_maybe,
 
   -- Evidence variables
   DictId, isEvVar, isDictId
@@ -51,7 +52,9 @@ import GHC.Builtin.Types.Prim ( concretePrimTyCon )
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Utils.Panic
-import GHC.Data.FastString( FastString )
+import GHC.Data.FastString
+
+import Control.Monad ( guard )
 
 
 -- | A predicate in the solver. The solver tries to prove Wanted predicates
@@ -351,6 +354,15 @@ isCallStackTy ty
   = False
 
 
+-- | Decomposes a predicate if it is an implicit parameter. Does not look in
+-- superclasses. See also [Local implicit parameters].
+isIPPred_maybe :: Type -> Maybe (FastString, Type)
+isIPPred_maybe ty =
+  do (tc,[t1,t2]) <- splitTyConApp_maybe ty
+     guard (isIPTyCon tc)
+     x <- isStrLitTy t1
+     return (x,t2)
+
 {- Note [Local implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The function isIPLikePred tells if this predicate, or any of its
@@ -380,7 +392,7 @@ Several wrinkles
   instantiate and check each superclass, one by one, in
   hasIPSuperClasses.
 
-* With -XRecursiveSuperClasses, the superclass hunt can go on forever,
+* With -XUndecidableSuperClasses, the superclass hunt can go on forever,
   so we need a RecTcChecker to cut it off.
 
 * Another apparent additional complexity involves type families. For
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 28929f37f9..e837132fc0 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -265,9 +265,6 @@ runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
 {-# INLINE runTyCoVars #-}
 runTyCoVars f = appEndo f emptyVarSet
 
-noView :: Type -> Maybe Type
-noView _ = Nothing
-
 {- *********************************************************************
 *                                                                      *
           Deep free variables
@@ -382,8 +379,8 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView
 ********************************************************************* -}
 
 
-{- Note [Finding free coercion varibles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Finding free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here we are only interested in the free /coercion/ variables.
 We can achieve this through a slightly different TyCo folder.
 
@@ -392,6 +389,7 @@ Notice that we look deeply, into kinds.
 See #14880.
 -}
 
+-- See Note [Finding free coercion variables]
 coVarsOfType  :: Type       -> CoVarSet
 coVarsOfTypes :: [Type]     -> CoVarSet
 coVarsOfCo    :: Coercion   -> CoVarSet
@@ -432,7 +430,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
                        -- See Note [CoercionHoles and coercion free variables]
                        -- in GHC.Core.TyCo.Rep
 
-
 {- *********************************************************************
 *                                                                      *
           Closing over kinds
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index fae7c7de19..a08da28421 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -65,7 +65,7 @@ module GHC.Core.TyCo.Rep (
         pickLR,
 
         -- ** Analyzing types
-        TyCoFolder(..), foldTyCo,
+        TyCoFolder(..), foldTyCo, noView,
 
         -- * Sizes
         typeSize, coercionSize, provSize,
@@ -150,6 +150,7 @@ data Type
   | ForAllTy
         {-# UNPACK #-} !TyCoVarBinder
         Type            -- ^ A Π type.
+             -- Note [When we quantify over a coercion variable]
              -- INVARIANT: If the binder is a coercion variable, it must
              -- be mentioned in the Type. See
              -- Note [Unused coercion variable in ForAllTy]
@@ -624,6 +625,35 @@ In order to compare FunTys while respecting how they could
 expand into TyConApps, we must check
 the kinds of the arg and the res.
 
+Note [When we quantify over a coercion variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The TyCoVarBinder in a ForAllTy can be (most often) a TyVar or (rarely)
+a CoVar. We support quantifying over a CoVar here in order to support
+a homogeneous (~#) relation (someday -- not yet implemented). Here is
+the example:
+
+  type (:~~:) :: forall k1 k2. k1 -> k2 -> Type
+  data a :~~: b where
+    HRefl :: a :~~: a
+
+Assuming homogeneous equality (that is, with
+  (~#) :: forall k. k -> k -> TYPE (TupleRep '[])
+) after rejigging to make equalities explicit, we get a constructor that
+looks like
+
+  HRefl :: forall k1 k2 (a :: k1) (b :: k2).
+           forall (cv :: k1 ~# k2). (a |> cv) ~# b
+        => (:~~:) k1 k2 a b
+
+Note that we must cast `a` by a cv bound in the same type in order to
+make this work out.
+
+See also https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell/phase2
+which gives a general road map that covers this space.
+
+Having this feature in Core does *not* mean we have it in source Haskell.
+See #15710 about that.
+
 Note [Unused coercion variable in ForAllTy]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -1834,7 +1864,7 @@ We were also worried about
                                      `extendVarSet` tv
 
 Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
-But, amazingly, we get good code here too. GHC is careful not to makr
+But, amazingly, we get good code here too. GHC is careful not to mark
 TyCoFolder data constructor for deep_tcf as a loop breaker, so the
 record selections still cancel.  And eta expansion still happens too.
 -}
@@ -1843,8 +1873,8 @@ data TyCoFolder env a
   = TyCoFolder
       { tcf_view  :: Type -> Maybe Type   -- Optional "view" function
                                           -- E.g. expand synonyms
-      , tcf_tyvar :: env -> TyVar -> a
-      , tcf_covar :: env -> CoVar -> a
+      , tcf_tyvar :: env -> TyVar -> a    -- Does not automatically recur
+      , tcf_covar :: env -> CoVar -> a    -- into kinds of variables
       , tcf_hole  :: env -> CoercionHole -> a
           -- ^ What to do with coercion holes.
           -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep".
@@ -1916,6 +1946,10 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_prov _   (PluginProv _)      = mempty
     go_prov _   (CorePrepProv _)    = mempty
 
+-- | A view function that looks through nothing.
+noView :: Type -> Maybe Type
+noView _ = Nothing
+
 {- *********************************************************************
 *                                                                      *
                    typeSize, coercionSize
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1cacfca468..4fce8c8a09 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -86,7 +86,7 @@ module GHC.Core.Type (
 
         -- ** Analyzing types
         TyCoMapper(..), mapTyCo, mapTyCoX,
-        TyCoFolder(..), foldTyCo,
+        TyCoFolder(..), foldTyCo, noView,
 
         -- (Newtypes)
         newTyConInstRhs,