Guard rewritableTyVarsOfType
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 9 Feb 2017 12:12:21 +0000 (12:12 +0000)
committerBen Gamari <ben@smart-cactus.org>
Thu, 9 Feb 2017 21:34:01 +0000 (16:34 -0500)
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.

compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcType.hs
testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr

index 7bc955b..1be1724 100644 (file)
@@ -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
index a2d8063..2dffed2 100644 (file)
@@ -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
index bff6ba5..2ad8d45 100644 (file)
@@ -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)