Improve partial signatures

As #20921 showed, with partial signatures, it is helpful to use the
same algorithm (namely findInferredDiff) for
* picking the constraints to retain for the /group/
  in Solver.decideQuantification
* picking the contraints to retain for the /individual function/
  in Bind.chooseInferredQuantifiers

This is still regrettably declicate, but it's a step forward.

4 files changed, 75 insertions, 1 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
index 286ca25671..4d3a668241 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
@@ -3,7 +3,7 @@ T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found extra-constraints wildcard standing for ‘Reduce z zq’
       Where: ‘z’, ‘zq’ are rigid type variables bound by
                the inferred type of
-                 bench_mulPublic :: (LiftOf zq ~ z, Reduce z zq) =>
+                 bench_mulPublic :: (z ~ LiftOf zq, Reduce z zq) =>
                                     Cyc zp -> Cyc z -> IO (zp, zq)
                at T14715.hs:13:27-33
     • In the type signature:
diff --git a/testsuite/tests/partial-sigs/should_compile/T20921.hs b/testsuite/tests/partial-sigs/should_compile/T20921.hs
new file mode 100644
index 0000000000..e6f9fb6df1
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T20921.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module PsigBug where
+
+import Data.Kind
+  ( Constraint )
+import GHC.TypeLits
+  ( ErrorMessage(..), TypeError )
+import GHC.TypeNats ( Nat )
+
+type family OK (i :: Nat) :: Constraint where
+  OK 1 = ()
+  OK 2 = ()
+  OK n = TypeError (ShowType n :<>: Text "is not OK")
+
+class C (i :: Nat) where
+  foo :: Int
+
+instance C 1 where
+  foo = 1
+instance C 2 where
+  foo = 2
+
+type family Boo (i :: Nat) :: Nat where
+  Boo i = i
+
+bar :: Int
+bar =
+  let
+    quux :: forall (i :: Nat). ( OK (Boo i), _ ) => Int
+    quux = foo @(Boo i)
+  in quux @1 + quux @2
+
+{-
+From RHS of quux
+  [W] C (Boo i)
+  [W] OK (Boo i)  -- Note [Add signature contexts as wanteds]
+
+Simplifies to
+  [W] C i, OK i
+
+Add back in OK (Boo i) (in decideQuantification),
+and mkMinimalBySCs (which does not eliminate (OK i)
+  (OK (Boo i), OK i, C i)
+
+-}
diff --git a/testsuite/tests/partial-sigs/should_compile/T20921.stderr b/testsuite/tests/partial-sigs/should_compile/T20921.stderr
new file mode 100644
index 0000000000..6c2156cc9f
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T20921.stderr
@@ -0,0 +1,20 @@
+
+T20921.hs:37:46: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found extra-constraints wildcard standing for ‘C i’
+      Where: ‘i’ is a rigid type variable bound by
+               the inferred type of quux :: (OK (Boo i), C i) => Int
+               at T20921.hs:37:21
+    • In the type signature:
+        quux :: forall (i :: Nat). (OK (Boo i), _) => Int
+      In the expression:
+        let
+          quux :: forall (i :: Nat). (OK (Boo i), _) => Int
+          quux = foo @(Boo i)
+        in quux @1 + quux @2
+      In an equation for ‘bar’:
+          bar
+            = let
+                quux :: forall (i :: Nat). (OK (Boo i), _) => Int
+                quux = foo @(Boo i)
+              in quux @1 + quux @2
+    • Relevant bindings include bar :: Int (bound at T20921.hs:35:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 6367aa16f5..e38358f88a 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -101,3 +101,4 @@ test('T18008', normal, compile, [''])
 test('T16762d', normal, compile, [''])
 test('T14658', normal, compile, [''])
 test('T18646', normal, compile, [''])
+test('T20921', normal, compile, [''])