Change rewritableTyVarsOfType to anyRewritableTyVar

This fixes the regression in FrozenErrorTests, eliminates the
awkward "crash on forall" in rewritableTyVars, and makes it more
efficient too.

compiler/typecheck/TcSMonad.hs

@@ -1077,9 +1077,10 @@ work?
 * CDictCan (C tys) or CFunEqCan (F tys ~ fsk):
   Yes if the inert set could rewrite tys to make the class constraint,
   or type family, fire.  That is, yes if the inert_eqs intersects
-  with the free vars of tys.  For this test we use rewritableTyVars
-  which ignores casts and coercions in tys, because rewriting the
-  casts or coercions won't make the thing fire more often.
+  with the free vars of tys.  For this test we use
+  (anyRewritableTyVar True) which ignores casts and coercions in tys,
+  because rewriting the casts or coercions won't make the thing fire
+  more often.
 
 * CTyEqCan (a ~ ty): Yes if the inert set could rewrite 'a' or 'ty'.
   We need to check both 'a' and 'ty' against the inert set:
@@ -1093,12 +1094,9 @@ work?
       canonicalise another [D] constraint mentioning 'a', we'd
       get an infinite loop
 
-  Moreover we must use the full-blown (tyVarsOfType ty) for the
-  RHS, for two reasons:
-     1. even tyvars in the casts and coercions could give
-        an infinite loop
-     2. rewritableTyVarsOfType doesn't handle foralls (just
-        because it doesn't need to)
+  Moreover we must use (anyRewritableTyVar False) for the RHS,
+  because even tyvars in the casts and coercions could give
+  an infinite loop if we don't expose it
 
 * Others: nothing is gained by splitting.
 
@@ -1248,30 +1246,31 @@ shouldSplitWD :: InertEqs -> Ct -> Bool
 -- True <=> we should split ct ito [W] and [D] because
 --          the inert_eqs can make progress on the [D]
 -- See Note [Splitting WD constraints]
+
 shouldSplitWD inert_eqs (CFunEqCan { cc_tyargs = tys })
-  = inert_eqs `intersects_with` rewritableTyVarsOfTypes tys
+  = should_split_match_args inert_eqs tys
     -- We don't need to split if the tv is the RHS fsk
 
 shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys })
-  = inert_eqs `intersects_with` rewritableTyVarsOfTypes tys
+  = should_split_match_args inert_eqs tys
+    -- NB True: ignore coercions
+    -- See Note [Splitting WD constraints]
 
 shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
   =  tv `elemDVarEnv` inert_eqs
-  || inert_eqs `intersects_with` tyCoVarsOfType ty
+  || anyRewritableTyVar False (`elemDVarEnv` inert_eqs) ty
+  -- NB False: do not ignore casts and coercions
   -- See Note [Splitting WD constraints]
 
 shouldSplitWD _ _ = False   -- No point in splitting otherwise
 
-intersects_with :: InertEqs -> TcTyVarSet -> Bool
-intersects_with inert_eqs free_vars
-  = not (disjointUdfmUfm inert_eqs free_vars)
-      -- Test whether the inert equalities could rewrite
-      -- a derived version of this constraint
-      -- The low-level use of disjointUFM might seem surprising.
-      -- InertEqs = TyVarEnv EqualCtList, and we want to see if its domain
-      -- is disjoint from that of a TcTyCoVarSet.  So we drop down
-      -- to the underlying UniqFM.  A bit yukky, but efficient.
-
+should_split_match_args :: InertEqs -> [TcType] -> Bool
+-- True if the inert_eqs can rewrite anything in the argument
+-- types, ignoring casts and coercions
+should_split_match_args inert_eqs tys
+  = any (anyRewritableTyVar True (`elemDVarEnv` inert_eqs)) tys
+    -- NB True: ignore casts coercions
+    -- See Note [Splitting WD constraints]
 
 isImprovable :: CtEvidence -> Bool
 -- See Note [Do not do improvement for WOnly]
@@ -1495,25 +1494,20 @@ 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_insol insols
+    (insols_out, insols_in) = partitionBag     kick_out_ct insols
+      -- Kick out even insolubles: See Note [Kick out insolubles]
 
     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]
-    -- Used only on CFunEqCan, CDictCan, CIrredCan
-    --   hence no foralls in (ctEvPred ev), hence rewritableTyVarsOfType ok
     kick_out_ct ct | let ev = ctEvidence ct
                    = fr_may_rewrite (ctEvFlavourRole ev)
-                   && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev)
+                   && anyRewritableTyVar False (== new_tv) (ctEvPred ev)
+                  -- False: ignore casts and coercions
                   -- 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

compiler/typecheck/TcType.hs

@@ -103,7 +103,7 @@ module TcType (
   -- * Finding "exact" (non-dead) type variables
   exactTyCoVarsOfType, exactTyCoVarsOfTypes,
   splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
-  rewritableTyVarsOfTypes, rewritableTyVarsOfType,
+  anyRewritableTyVar,
 
   -- * Extracting bound variables
   allBoundVariables, allBoundVariabless,
@@ -886,27 +886,40 @@ exactTyCoVarsOfType ty
 exactTyCoVarsOfTypes :: [Type] -> TyVarSet
 exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
 
-rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet
-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
-  = go ty
+anyRewritableTyVar :: Bool -> (TcTyVar -> Bool)
+                   -> TcType -> Bool
+-- (anyRewritableTyVar ignore_cos pred ty) returns True
+--    if the 'pred' returns True of free TyVar in 'ty'
+-- Do not look inside casts and coercions if 'ignore_cos' is True
+-- See Note [anyRewritableTyVar]
+anyRewritableTyVar ignore_cos pred ty
+  = go emptyVarSet ty
   where
-    go (TyVarTy tv)     = unitVarSet tv
-    go (LitTy {})       = emptyVarSet
-    go (TyConApp _ tys) = rewritableTyVarsOfTypes tys
-    go (AppTy fun arg)  = go fun `unionVarSet` go arg
-    go (FunTy arg res)  = go arg `unionVarSet` go res
-    go ty@(ForAllTy {}) = pprPanic "rewritableTyVarOfType" (ppr ty)
-    go (CastTy ty _co)  = go ty
-    go (CoercionTy _co) = emptyVarSet
-
+    go_tv bound tv | tv `elemVarSet` bound = False
+                   | otherwise             = pred tv
+
+    go bound (TyVarTy tv)     = go_tv bound tv
+    go _     (LitTy {})       = False
+    go bound (TyConApp _ tys) = any (go bound) tys
+    go bound (AppTy fun arg)  = go bound fun || go bound arg
+    go bound (FunTy arg res)  = go bound arg || go bound res
+    go bound (ForAllTy tv ty) = go (bound `extendVarSet` binderVar tv) ty
+    go bound (CastTy ty co)   = go bound ty || go_co bound co
+    go bound (CoercionTy co)  = go_co bound co
+
+    go_co bound co
+      | ignore_cos = False
+      | otherwise  = varSetAny (go_tv bound) (tyCoVarsOfCo co)
+      -- We don't have an equivalent of anyRewritableTyVar for coercions
+      -- (at least not yet) so take the free vars and test them
+
+{- Note [anyRewritableTyVar]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+anyRewritableTyVar is used during kick-out from the inert set,
+to decide if, given a new equality (a ~ ty), we should kick out
+a constraint C.  Rather than gather free variables and see if 'a'
+is among them, we instead pass in a predicate; this is just efficiency.
+-}
 
 {- *********************************************************************
 *                                                                      *

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,8 +39,7 @@ 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 (T2 c c) c’
-                     with ‘T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)’
+    • Couldn't match type ‘T2 c c’ with ‘M (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)