decideMonoTyVars: account for CoVars in candidates

The "candidates" passed to decideMonoTyVars can contain coercion holes.
This is because we might well decide to quantify over some unsolved
equality constraints, as long as they are not definitely insoluble.

In that situation, decideMonoTyVars was passing a set of type variables
that was not closed over kinds to closeWrtFunDeps, which was tripping
up an assertion failure.

Fixes #21404

4 files changed, 34 insertions, 3 deletions

diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index e3baf4c4f9..5b215490af 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -44,7 +44,6 @@ 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 )
@@ -552,7 +551,10 @@ closeWrtFunDeps :: [PredType] -> TyCoVarSet -> TyCoVarSet
 -- See Note [The liberal coverage condition]
 closeWrtFunDeps preds fixed_tvs
   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
-  | otherwise   = assert (closeOverKinds fixed_tvs == fixed_tvs)
+  | otherwise   = assertPpr (closeOverKinds fixed_tvs == fixed_tvs)
+                    (vcat [ text "closeWrtFunDeps: fixed_tvs is not closed over kinds"
+                          , text "fixed_tvs:" <+> ppr fixed_tvs
+                          , text "closure:" <+> ppr (closeOverKinds fixed_tvs) ])
                 $ fixVarSet extend fixed_tvs
   where
 
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 1ea5ba7de1..31e2f7ed93 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1672,7 +1672,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; tc_lvl <- TcM.getTcLevel
        ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
 
-             co_vars = coVarsOfTypes (psig_tys ++ taus)
+             co_vars = coVarsOfTypes (psig_tys ++ taus ++ candidates)
              co_var_tvs = closeOverKinds co_vars
                -- The co_var_tvs are tvs mentioned in the types of covars or
                -- coercion holes. We can't quantify over these covars, so we
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index 2cc457e635..408708a564 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,4 +1,27 @@
 
+T14584.hs:57:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce (SingI a) arising from a use of ‘sing’
+      from the context: (Action act, Monoid a, Good m1)
+        bound by the instance declaration at T14584.hs:55:10-89
+    • In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+
+T14584.hs:57:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Cannot use equality for substitution: a0 ~ a
+      Doing so would be ill-kinded.
+    • In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:57:3)
+
 T14584.hs:57:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Could not deduce (m1 ~ *)
       from the context: (Action act, Monoid a, Good m1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
index febc57797d..a7706d723e 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
@@ -1,4 +1,10 @@
 
+T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+      Probable cause: ‘id’ is applied to too few arguments
+    • In the expression: id @m :: _
+      In an equation for ‘f’: f = id @m :: _
+
 T14584a.hs:12:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expected a type, but ‘m’ has kind ‘k’
       ‘k’ is a rigid type variable bound by