Kill derived constraints

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

2 files changed, 74 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_compile/LopezJuan.hs b/testsuite/tests/dependent/should_compile/LopezJuan.hs
new file mode 100644
index 0000000000..bc7cc89201
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/LopezJuan.hs
@@ -0,0 +1,73 @@
+{-
+
+This test is inspired by
+  Practical dependent type checking using twin types
+  Victor López Juan and Nils Anders Danielsson
+  TyDe '20
+  https://dl.acm.org/doi/10.1145/3406089.3409030
+
+The challenge is whether we can unify two types where the only
+way to know that the kinds are equal is to unify the types. This
+would fail in an algorithm that required kind unification before
+type unification.
+-}
+
+{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
+             StandaloneKindSignatures, PolyKinds, GADTs,
+             TypeFamilies, NamedWildCards, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module LopezJuan where
+
+import Data.Type.Equality ( (:~~:)(..) )
+import Data.Kind ( Type )
+import Data.Proxy ( Proxy )
+
+-- amazingly, this worked without modification
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+data BoolOp where
+  None :: Bool -> BoolOp
+  Some :: Bool -> BoolOp
+
+type F :: Bool -> Type
+type family F b
+
+get :: BoolOp -> Bool
+get (None _) = True
+get (Some x) = x
+
+type Get :: BoolOp -> Bool
+type family Get x where
+  Get (None _) = True
+  Get (Some x) = x
+
+type TyFun :: Type -> Type -> Type
+data TyFun arg res
+
+type (~>) :: Type -> Type -> Type
+type arg ~> res = TyFun arg res -> Type
+infixr 0 ~>
+
+data Const :: a -> (b ~> a)
+
+f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
+                       @(F True ~> BoolOp)
+                       (Const (None x))
+                       (Const (_alpha x))
+f _ = HRefl
+
+-- and something simpler:
+
+type family Idish guard a where
+  Idish True a = a
+  Idish False a = Int
+
+g :: (:~~:) @(Idish _alpha Type)
+            @Type
+            (Proxy _alpha)
+            (Proxy True)
+g = HRefl
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5f947f5e37..93d9164768 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -72,3 +72,4 @@ test('T16344b', normal, compile, [''])
 test('T16347', normal, compile, [''])
 test('T18660', normal, compile, [''])
 test('T12174', normal, compile, [''])
+test('LopezJuan', normal, compile, [''])