Fix and simplify DeriveAnyClass's context inference using SubTypePredSpec

As explained in `Note [Gathering and simplifying constraints for DeriveAnyClass]`
in `GHC.Tc.Deriv.Infer`, `DeriveAnyClass` infers instance contexts by emitting
implication constraints. Previously, these implication constraints were
constructed by hand. This is a terribly trick thing to get right, as it
involves a delicate interplay of skolemisation, metavariable instantiation, and
`TcLevel` bumping. Despite much effort, we discovered in #20719 that the
implementation was subtly incorrect, leading to valid programs being rejected.

While we could scrutinize the code that manually constructs implication
constraints and repair it, there is a better, less error-prone way to do
things. After all, the heart of `DeriveAnyClass` is generating code which
fills in each class method with defaults, e.g., `foo = $gdm_foo`. Typechecking
this sort of code is tantamount to calling `tcSubTypeSigma`, as we much ensure
that the type of `$gdm_foo` is a subtype of (i.e., more polymorphic than) the
type of `foo`. As an added bonus, `tcSubTypeSigma` is a battle-tested function
that handles skolemisation, metvariable instantiation, `TcLevel` bumping, and
all other means of tricky bookkeeping correctly.

With this insight, the solution to the problems uncovered in #20719 is simple:
use `tcSubTypeSigma` to check if `$gdm_foo`'s type is a subtype of `foo`'s
type. As a side effect, `tcSubTypeSigma` will emit exactly the implication
constraint that we were attempting to construct by hand previously. Moreover,
it does so correctly, fixing #20719 as a consequence.

This patch implements the solution thusly:

* The `PredSpec` data type (previously named `PredOrigin`) is now split into
  `SimplePredSpec`, which directly stores a `PredType`, and `SubTypePredSpec`,
  which stores the actual and expected types in a subtype check.
  `SubTypePredSpec` is only used for `DeriveAnyClass`; all other deriving
  strategies use `SimplePredSpec`.
* Because `tcSubTypeSigma` manages the finer details of type variable
  instantiation and constraint solving under the hood, there is no longer any
  need to delicately split apart the method type signatures in
  `inferConstraintsAnyclass`. This greatly simplifies the implementation of
  `inferConstraintsAnyclass` and obviates the need to store skolems,
  metavariables, or given constraints in a `ThetaSpec` (previously named
  `ThetaOrigin`). As a bonus, this means that `ThetaSpec` now simply becomes a
  synonym for a list of `PredSpec`s, which is conceptually much simpler than it
  was before.
* In `simplifyDeriv`, each `SubTypePredSpec` results in a call to
  `tcSubTypeSigma`. This is only performed for its side effect of emitting
  an implication constraint, which is fed to the rest of the constraint solving
  machinery in `simplifyDeriv`. I have updated
  `Note [Gathering and simplifying constraints for DeriveAnyClass]` to explain
  this in more detail.

To make the changes in `simplifyDeriv` more manageable, I also performed some
auxiliary refactoring:

* Previously, every iteration of `simplifyDeriv` was skolemising the type
  variables at the start, simplifying, and then performing a reverse
  substitution at the end to un-skolemise the type variables. This is not
  necessary, however, since we can just as well skolemise once at the
  beginning of the `deriving` pipeline and zonk the `TcTyVar`s after
  `simplifyDeriv` is finished. This patch does just that, having been made
  possible by prior work in !7613. I have updated `Note [Overlap and deriving]`
  in `GHC.Tc.Deriv.Infer` to explain this, and I have also left comments on
  the relevant data structures (e.g., `DerivEnv` and `DerivSpec`) to explain
  when things might be `TcTyVar`s or `TyVar`s.
* All of the aforementioned cleanup allowed me to remove an ad hoc
  deriving-related in `checkImplicationInvariants`, as all of the skolems in
  a `tcSubTypeSigma`–produced implication constraint should now be `TcTyVar`
  at the time the implication is created.
* Since `simplifyDeriv` now needs a `SkolemInfo` and `UserTypeCtxt`, I have
  added `ds_skol_info` and `ds_user_ctxt` fields to `DerivSpec` to store these.
  Similarly, I have also added a `denv_skol_info` field to `DerivEnv`, which
  ultimately gets used to initialize the `ds_skol_info` in a `DerivSpec`.

Fixes #20719.

3 files changed, 44 insertions, 15 deletions

diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index 6db596396d..655fb282a7 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -9,18 +9,19 @@ Derived class instances:
     GHC.Base.sconcat ::
       GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes ::
-      forall (b :: *).
-      GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
+      forall (b :: *). GHC.Real.Integral b =>
+                       b -> T14578.Wat f g a -> T14578.Wat f g a
     (GHC.Base.<>)
       = GHC.Prim.coerce
           @(T14578.App (Data.Functor.Compose.Compose f g) a
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
           ((GHC.Base.<>) @(T14578.App (Data.Functor.Compose.Compose f g) a))
     GHC.Base.sconcat
       = GHC.Prim.coerce
-          @(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g) a)
+          @(GHC.Base.NonEmpty
+              (T14578.App (Data.Functor.Compose.Compose f g) a)
             -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
           (GHC.Base.sconcat
@@ -29,7 +30,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(b
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(b -> T14578.Wat f g a -> T14578.Wat f g a)
           (GHC.Base.stimes
              @(T14578.App (Data.Functor.Compose.Compose f g) a))
@@ -37,8 +38,8 @@ Derived class instances:
   instance GHC.Base.Functor f =>
            GHC.Base.Functor (T14578.App f) where
     GHC.Base.fmap ::
-      forall (a :: *) (b :: *).
-      (a -> b) -> T14578.App f a -> T14578.App f b
+      forall (a :: *) (b :: *). (a -> b)
+                                -> T14578.App f a -> T14578.App f b
     (GHC.Base.<$) ::
       forall (a :: *) (b :: *). a -> T14578.App f b -> T14578.App f a
     GHC.Base.fmap
@@ -54,17 +55,17 @@ Derived class instances:
            GHC.Base.Applicative (T14578.App f) where
     GHC.Base.pure :: forall (a :: *). a -> T14578.App f a
     (GHC.Base.<*>) ::
-      forall (a :: *) (b :: *).
-      T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b
+      forall (a :: *) (b :: *). T14578.App f (a -> b)
+                                -> T14578.App f a -> T14578.App f b
     GHC.Base.liftA2 ::
-      forall (a :: *) (b :: *) (c :: *).
-      (a -> b -> c) -> T14578.App f a -> T14578.App f b -> T14578.App f c
+      forall (a :: *) (b :: *) (c :: *). (a -> b -> c)
+                                         -> T14578.App f a -> T14578.App f b -> T14578.App f c
     (GHC.Base.*>) ::
-      forall (a :: *) (b :: *).
-      T14578.App f a -> T14578.App f b -> T14578.App f b
+      forall (a :: *) (b :: *). T14578.App f a
+                                -> T14578.App f b -> T14578.App f b
     (GHC.Base.<*) ::
-      forall (a :: *) (b :: *).
-      T14578.App f a -> T14578.App f b -> T14578.App f a
+      forall (a :: *) (b :: *). T14578.App f a
+                                -> T14578.App f b -> T14578.App f a
     GHC.Base.pure
       = GHC.Prim.coerce
           @(a -> f a) @(a -> T14578.App f a) (GHC.Base.pure @f)
diff --git a/testsuite/tests/deriving/should_compile/T20719.hs b/testsuite/tests/deriving/should_compile/T20719.hs
new file mode 100644
index 0000000000..c2c4a4f282
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T20719.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE DerivingStrategies, DeriveAnyClass, DefaultSignatures #-}
+
+module T20719 where
+
+import Data.Proxy
+
+type Method a = forall b . Eq b => Proxy (a, b)
+
+class Class a where
+  method1         :: Method a
+  default method1 :: Method a
+  method1 = Proxy
+
+  method2         :: Method a
+  default method2 :: forall b . Eq b => Proxy (a, b)
+  method2 = Proxy
+
+  method3         :: forall b . Eq b => Proxy (a, b)
+  default method3 :: Method a
+  method3 = Proxy
+
+  method4         :: forall b . Eq b => Proxy (a, b)
+  default method4 :: forall b . Eq b => Proxy (a, b)
+  method4 = Proxy
+
+data Data
+  deriving anyclass Class
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 05f9e87dcb..c5edb5275f 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -137,4 +137,5 @@ test('T20496', multiline_grep_errmsg(r"rnd\n( .*\n)*"), compile, ['-ddump-tc-tra
 test('T20375', normal, compile, [''])
 test('T20387', normal, compile, [''])
 test('T20501', normal, compile, [''])
+test('T20719', normal, compile, [''])
 test('T20994', normal, compile, [''])