Guard rewritableTyVarsOfType

We only want to use rewriteableTyVarsOfType on CDictCan,
CFunEqCan (and maybe CIrredCan).  But not CTyEqCan.

But we were -- for insolubles.  So I narrowed the scope of
the insuluble kick-out.

3 files changed, 18 insertions, 14 deletions

diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 7bc955b1c1..1be1724b10 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1495,24 +1495,25 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
            -- See Note [Kicking out CFunEqCan for fundeps]
     (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
-    (insols_out, insols_in) = partitionBag     kick_out_ct insols
-      -- Kick out even insolubles; see Note [Kick out insolubles]
+    (insols_out, insols_in) = partitionBag     kick_out_insol insols
 
     fr_may_rewrite :: CtFlavourRole -> Bool
     fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
         -- Can the new item rewrite the inert item?
 
+    kick_out_insol :: Ct -> Bool
+      -- See Note [Kick out insolubles]
+    kick_out_insol (CTyEqCan { cc_tyvar = tv }) = new_tv == tv
+    kick_out_insol _                            = False
+
     kick_out_ct :: Ct -> Bool
-    -- Kick it out if the new CTyEqCan can rewrite the inert
-    -- one. See Note [kickOutRewritable]
-    -- Or if it has no shadow and the shadow
-    kick_out_ct ct = kick_out_ev (ctEvidence ct)
-
-    kick_out_ev :: CtEvidence -> Bool
-    -- Kick it out if the new CTyEqCan can rewrite the inert
-    -- one. See Note [kickOutRewritable]
-    kick_out_ev ev = fr_may_rewrite (ctEvFlavourRole ev)
-                  && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev)
+    -- Kick it out if the new CTyEqCan can rewrite the inert one
+    -- See Note [kickOutRewritable]
+    -- Used only on CFunEqCan, CDictCan, CIrredCan
+    --   hence no forallls in (ctEvPred ev), hence rewriteableTyVarsOfType ok
+    kick_out_ct ct | let ev = ctEvidence ct
+                   = fr_may_rewrite (ctEvFlavourRole ev)
+                   && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev)
                   -- NB: this includes the fsk of a CFunEqCan.  It can't
                   --     actually be rewritten, but we need to kick it out
                   --     so we get to take advantage of injectivity
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index a2d806359d..2dffed29fd 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -891,6 +891,8 @@ rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys
 
 rewritableTyVarsOfType :: TcType -> TcTyVarSet
 -- Used during kick-out from the inert set
+-- This function is used for the arguments of class and type families,
+--    which should not have any foralls in them
 -- Ignores coercions and casts, because rewriting those does
 -- not help solving, and it's more efficient to ignore them
 rewritableTyVarsOfType ty
diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
index bff6ba544f..2ad8d453e8 100644
--- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -24,7 +24,7 @@ FrozenErrorTests.hs:29:15: error:
       In an equation for ‘test2’: test2 = goo2 (goo1 False undefined)
 
 FrozenErrorTests.hs:30:9: error:
-    • Couldn't match type ‘Int’ with ‘[Int]’
+    • Couldn't match type ‘[Int]’ with ‘[[Int]]’
         arising from a use of ‘goo1’
     • In the expression: goo1 False (goo2 undefined)
       In an equation for ‘test3’: test3 = goo1 False (goo2 undefined)
@@ -39,7 +39,8 @@ FrozenErrorTests.hs:45:15: error:
         test4 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:45:1)
 
 FrozenErrorTests.hs:46:9: error:
-    • Couldn't match type ‘T2 c c’ with ‘M (T2 (T2 c c) c)’
+    • Couldn't match type ‘T2 (T2 c c) c’
+                     with ‘T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)’
         arising from a use of ‘goo3’
     • In the expression: goo3 False (goo4 undefined)
       In an equation for ‘test5’: test5 = goo3 False (goo4 undefined)