Commit 3acd6164 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Improve kick-out in the constraint solver

This patch was provoked by Trac #14363.  Turned out that we were
kicking out too many constraints in TcSMonad.kickOutRewritable, and
that mean that the work-list never became empty: infinite loop!

That in turn made me look harder at the Main Theorem in
Note [Extending the inert equalities].

Main changes

* Replace TcType.isTyVarExposed by TcType.isTyVarHead.  The
  over-agressive isTyVarExposed is what caused Trac #14363.
  See Note [K3: completeness of solving] in TcSMonad.

* TcType.Make anyRewriteableTyVar role-aware.  In particular,
      a ~R ty
  cannot rewrite
      b ~R f a
  See Note [anyRewriteableTyVar must be role-aware].  That means
  it has to be given a role argument, which forces a little
  refactoring.

  I think this change is fixing a bug that hasn't yet been reported.
  The actual reported bug is handled by the previous bullet.  But
  this change is definitely the Right Thing

The main changes are in TcSMonad.kick_out_rewritable, and in TcType
(isTyVarExposed ---> isTyVarHead).

I did a little unforced refactoring:

 * Use the cc_eq_rel field of a CTyEqCan when it is available, rather
   than recomputing it.

 * Define eqCanRewrite :: EqRel -> EqRel -> EqRel, and use it, instead
   of duplicating its logic
parent c1efc6e6
...@@ -1397,12 +1397,13 @@ flatten_tyvar2 tv fr@(_, eq_rel) ...@@ -1397,12 +1397,13 @@ flatten_tyvar2 tv fr@(_, eq_rel)
; case lookupDVarEnv ieqs tv of ; case lookupDVarEnv ieqs tv of
Just (ct:_) -- If the first doesn't work, Just (ct:_) -- If the first doesn't work,
-- the subsequent ones won't either -- the subsequent ones won't either
| CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct | CTyEqCan { cc_ev = ctev, cc_tyvar = tv
, let ct_fr = ctEvFlavourRole ctev , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
, let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
, ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
-> do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) -> do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
; let rewrite_co1 = mkSymCo (ctEvCoercion ctev) ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
rewrite_co = case (ctEvEqRel ctev, eq_rel) of rewrite_co = case (ct_eq_rel, eq_rel) of
(ReprEq, _rel) -> ASSERT( _rel == ReprEq ) (ReprEq, _rel) -> ASSERT( _rel == ReprEq )
-- if this ASSERT fails, then -- if this ASSERT fails, then
-- eqCanRewriteFR answered incorrectly -- eqCanRewriteFR answered incorrectly
......
...@@ -1490,24 +1490,26 @@ test when solving pairwise CFunEqCan. ...@@ -1490,24 +1490,26 @@ test when solving pairwise CFunEqCan.
********************************************************************** **********************************************************************
-} -}
inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtEvidence inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtFlavourRole
-> Maybe ( CtEvidence -- The evidence for the inert -> Maybe ( CtEvidence -- The evidence for the inert
, SwapFlag -- Whether we need mkSymCo , SwapFlag -- Whether we need mkSymCo
, Bool) -- True <=> keep a [D] version , Bool) -- True <=> keep a [D] version
-- of the [WD] constraint -- of the [WD] constraint
inertsCanDischarge inerts tv rhs ev inertsCanDischarge inerts tv rhs fr
| (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
, cc_eq_rel = eq_rel }
<- findTyEqs inerts tv <- findTyEqs inerts tv
, ev_i `eqCanDischarge` ev , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
, rhs_i `tcEqType` rhs ] , rhs_i `tcEqType` rhs ]
= -- Inert: a ~ ty = -- Inert: a ~ ty
-- Work item: a ~ ty -- Work item: a ~ ty
Just (ev_i, NotSwapped, keep_deriv ev_i) Just (ev_i, NotSwapped, keep_deriv ev_i)
| Just tv_rhs <- getTyVar_maybe rhs | Just tv_rhs <- getTyVar_maybe rhs
, (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
, cc_eq_rel = eq_rel }
<- findTyEqs inerts tv_rhs <- findTyEqs inerts tv_rhs
, ev_i `eqCanDischarge` ev , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
, rhs_i `tcEqType` mkTyVarTy tv ] , rhs_i `tcEqType` mkTyVarTy tv ]
= -- Inert: a ~ b = -- Inert: a ~ b
-- Work item: b ~ a -- Work item: b ~ a
...@@ -1519,7 +1521,7 @@ inertsCanDischarge inerts tv rhs ev ...@@ -1519,7 +1521,7 @@ inertsCanDischarge inerts tv rhs ev
where where
keep_deriv ev_i keep_deriv ev_i
| Wanted WOnly <- ctEvFlavour ev_i -- inert is [W] | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
, Wanted WDeriv <- ctEvFlavour ev -- work item is [WD] , (Wanted WDeriv, _) <- fr -- work item is [WD]
= True -- Keep a derived verison of the work item = True -- Keep a derived verison of the work item
| otherwise | otherwise
= False -- Work item is fully discharged = False -- Work item is fully discharged
...@@ -1531,7 +1533,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv ...@@ -1531,7 +1533,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
, cc_ev = ev , cc_ev = ev
, cc_eq_rel = eq_rel }) , cc_eq_rel = eq_rel })
| Just (ev_i, swapped, keep_deriv) | Just (ev_i, swapped, keep_deriv)
<- inertsCanDischarge inerts tv rhs ev <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
= do { setEvBindIfWanted ev $ = do { setEvBindIfWanted ev $
EvCoercion (maybeSym swapped $ EvCoercion (maybeSym swapped $
tcDowngradeRole (eqRelRole eq_rel) tcDowngradeRole (eqRelRole eq_rel)
......
...@@ -121,8 +121,8 @@ module TcRnTypes( ...@@ -121,8 +121,8 @@ module TcRnTypes(
CtFlavour(..), ShadowInfo(..), ctEvFlavour, CtFlavour(..), ShadowInfo(..), ctEvFlavour,
CtFlavourRole, ctEvFlavourRole, ctFlavourRole, CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
eqCanRewriteFR, eqMayRewriteFR, eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
eqCanDischarge, eqCanDischargeFR,
funEqCanDischarge, funEqCanDischargeF, funEqCanDischarge, funEqCanDischargeF,
-- Pretty printing -- Pretty printing
...@@ -2768,9 +2768,19 @@ type CtFlavourRole = (CtFlavour, EqRel) ...@@ -2768,9 +2768,19 @@ type CtFlavourRole = (CtFlavour, EqRel)
ctEvFlavourRole :: CtEvidence -> CtFlavourRole ctEvFlavourRole :: CtEvidence -> CtFlavourRole
ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev) ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
-- | Extract the flavour, role, and boxity from a 'Ct' -- | Extract the flavour and role from a 'Ct'
ctFlavourRole :: Ct -> CtFlavourRole ctFlavourRole :: Ct -> CtFlavourRole
ctFlavourRole = ctEvFlavourRole . cc_ev -- Uses short-cuts to role for special cases
ctFlavourRole (CDictCan { cc_ev = ev })
= (ctEvFlavour ev, NomEq)
ctFlavourRole (CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel })
= (ctEvFlavour ev, eq_rel)
ctFlavourRole (CFunEqCan { cc_ev = ev })
= (ctEvFlavour ev, NomEq)
ctFlavourRole (CHoleCan { cc_ev = ev })
= (ctEvFlavour ev, NomEq)
ctFlavourRole ct
= ctEvFlavourRole (cc_ev ct)
{- Note [eqCanRewrite] {- Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~
...@@ -2817,14 +2827,18 @@ ReprEq we could conceivably get a Derived NomEq improvement (by decomposing ...@@ -2817,14 +2827,18 @@ ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
a type constructor with Nomninal role), and hence unify. a type constructor with Nomninal role), and hence unify.
-} -}
eqCanRewrite :: EqRel -> EqRel -> Bool
eqCanRewrite NomEq _ = True
eqCanRewrite ReprEq ReprEq = True
eqCanRewrite ReprEq NomEq = False
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-- Can fr1 actually rewrite fr2? -- Can fr1 actually rewrite fr2?
-- Very important function! -- Very important function!
-- See Note [eqCanRewrite] -- See Note [eqCanRewrite]
-- See Note [Wanteds do not rewrite Wanteds] -- See Note [Wanteds do not rewrite Wanteds]
-- See Note [Deriveds do rewrite Deriveds] -- See Note [Deriveds do rewrite Deriveds]
eqCanRewriteFR (Given, NomEq) (_, _) = True eqCanRewriteFR (Given, r1) (_, r2) = eqCanRewrite r1 r2
eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True
eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
eqCanRewriteFR _ _ = False eqCanRewriteFR _ _ = False
...@@ -2894,14 +2908,10 @@ We /do/ say that a [W] can discharge a [WD]. In evidence terms it ...@@ -2894,14 +2908,10 @@ We /do/ say that a [W] can discharge a [WD]. In evidence terms it
certainly can, and the /caller/ arranges that the otherwise-lost [D] certainly can, and the /caller/ arranges that the otherwise-lost [D]
is spat out as a new Derived. -} is spat out as a new Derived. -}
eqCanDischarge :: CtEvidence -> CtEvidence -> Bool
-- See Note [eqCanDischarge]
eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1)
(ctEvFlavourRole ev2)
eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanDischargeFR (_, ReprEq) (_, NomEq) = False -- See Note [eqCanDischarge]
eqCanDischargeFR (f1,_) (f2, _) = eqCanDischargeF f1 f2 eqCanDischargeFR (f1,r1) (f2, r2) = eqCanRewrite r1 r2
&& eqCanDischargeF f1 f2
eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
eqCanDischargeF Given _ = True eqCanDischargeF Given _ = True
......
...@@ -783,36 +783,38 @@ guarantee that this recursive use will terminate. ...@@ -783,36 +783,38 @@ guarantee that this recursive use will terminate.
Note [Extending the inert equalities] Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Theorem [Stability under extension] Main Theorem [Stability under extension]
This is the main theorem!
Suppose we have a "work item" Suppose we have a "work item"
a -fw-> t a -fw-> t
and an inert generalised substitution S, and an inert generalised substitution S,
such that ThEN the extended substitution T = S+(a -fw-> t)
is an inert generalised substitution
PROVIDED
(T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_) (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_)
(T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
(T3) a not in t -- No occurs check in the work item (T3) a not in t -- No occurs check in the work item
(K1) for every (a -fs-> s) in S, then not (fw >= fs) AND, for every (b -fs-> s) in S:
Reason: the work item is fully rewritten by S, hence not (fs >= fw) (K0) not (fw >= fs)
but if (fw >= fs) then the work item could rewrite Reason: suppose we kick out (a -fs-> s),
the inert item and add (a -fw-> t) to the inert set.
The latter can't rewrite the former,
so the kick-out achieved nothing
(K2) for every (b -fs-> s) in S, where b /= a, then OR { (K1) not (a = b)
(K2a) not (fs >= fs) Reason: if fw >= fs, WF1 says we can't have both
or (K2b) fs >= fw a -fw-> t and a -fs-> s
or (K2c) not (fw >= fs)
or (K2d) a not in s
(K3) See Note [K3: completeness of solving] AND (K2): guarantees inertness of the new substitution
If (b -fs-> s) is in S with (fw >= fs), then { (K2a) not (fs >= fs)
(K3a) If the role of fs is nominal: s /= a OR (K2b) fs >= fw
(K3b) If the role of fs is representational: EITHER OR (K2d) a not in s }
a not in s, OR
the path from the top of s to a includes at least one non-newtype AND (K3) See Note [K3: completeness of solving]
{ (K3a) If the role of fs is nominal: s /= a
(K3b) If the role of fs is representational:
s is not of form (a t1 .. tn) } }
then the extended substitution T = S+(a -fw-> t)
is an inert generalised substitution.
Conditions (T1-T3) are established by the canonicaliser Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewritable Conditions (K1-K3) are established by TcSMonad.kickOutRewritable
...@@ -840,11 +842,12 @@ The idea is that ...@@ -840,11 +842,12 @@ The idea is that
us to kick out an inert wanted that mentions a, because of (K2a). This us to kick out an inert wanted that mentions a, because of (K2a). This
is a common case, hence good not to kick out. is a common case, hence good not to kick out.
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold. * Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
Proof: using Definition [Can-rewrite relation], fw can't rewrite anything Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
and so K1-K3 hold. Intuitively, since fw can't rewrite anything, and so K0 holds. Intuitively, since fw can't rewrite anything,
adding it cannot cause any loops adding it cannot cause any loops
This is a common case, because Wanteds cannot rewrite Wanteds. This is a common case, because Wanteds cannot rewrite Wanteds.
It's used to avoid even looking for constraint to kick out.
* Lemma (L1): The conditions of the Main Theorem imply that there is no * Lemma (L1): The conditions of the Main Theorem imply that there is no
(a -fs-> t) in S, s.t. (fs >= fw). (a -fs-> t) in S, s.t. (fs >= fw).
...@@ -921,26 +924,35 @@ is somewhat accidental. ...@@ -921,26 +924,35 @@ is somewhat accidental.
When considering roles, we also need the second clause (K3b). Consider When considering roles, we also need the second clause (K3b). Consider
inert-item a -W/R-> b c
work-item c -G/N-> a work-item c -G/N-> a
inert-item a -W/R-> b c
The work-item doesn't get rewritten by the inert, because (>=) doesn't hold. The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were But we don't kick out the inert item because not (W/R >= W/R). So we just
condition (K3a), then we would keep the inert around and add the work item. add the work item. But then, consider if we hit the following:
But then, consider if we hit the following:
work-item2 b -G/N-> Id
work-item b -G/N-> Id
inert-items a -W/R-> b c
c -G/N-> a
where where
newtype Id x = Id x newtype Id x = Id x
For similar reasons, if we only had (K3a), we wouldn't kick the For similar reasons, if we only had (K3a), we wouldn't kick the
representational inert out. And then, we'd miss solving the inert, which representational inert out. And then, we'd miss solving the inert, which
now reduced to reflexivity. The solution here is to kick out representational now reduced to reflexivity.
inerts whenever the tyvar of a work item is "exposed", where exposed means
not under some proper data-type constructor, like [] or Maybe. See The solution here is to kick out representational inerts whenever the
isTyVarExposed in TcType. This is encoded in (K3b). tyvar of a work item is "exposed", where exposed means being at the
head of the top-level application chain (a t1 .. tn). See
TcType.isTyVarHead. This is encoded in (K3b).
Beware: if we make this test succeed too often, we kick out too much,
and the solver might loop. Consider (Trac #14363)
work item: [G] a ~R f b
inert item: [G] b ~R f a
In GHC 8.2 the completeness tests more aggressive, and kicked out
the inert item; but no rewriting happened and there was an infinite
loop. All we need is to have the tyvar at the head.
Note [Flavours with roles] Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -1272,11 +1284,13 @@ shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys }) ...@@ -1272,11 +1284,13 @@ shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys })
-- NB True: ignore coercions -- NB True: ignore coercions
-- See Note [Splitting WD constraints] -- See Note [Splitting WD constraints]
shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty }) shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty
, cc_eq_rel = eq_rel })
= tv `elemDVarEnv` inert_eqs = tv `elemDVarEnv` inert_eqs
|| anyRewritableTyVar False (`elemDVarEnv` inert_eqs) ty || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
-- NB False: do not ignore casts and coercions -- NB False: do not ignore casts and coercions
-- See Note [Splitting WD constraints] -- See Note [Splitting WD constraints]
where
shouldSplitWD _ _ = False -- No point in splitting otherwise shouldSplitWD _ _ = False -- No point in splitting otherwise
...@@ -1284,10 +1298,18 @@ should_split_match_args :: InertEqs -> [TcType] -> Bool ...@@ -1284,10 +1298,18 @@ should_split_match_args :: InertEqs -> [TcType] -> Bool
-- True if the inert_eqs can rewrite anything in the argument -- True if the inert_eqs can rewrite anything in the argument
-- types, ignoring casts and coercions -- types, ignoring casts and coercions
should_split_match_args inert_eqs tys should_split_match_args inert_eqs tys
= any (anyRewritableTyVar True (`elemDVarEnv` inert_eqs)) tys = any (anyRewritableTyVar True NomEq (canRewriteTv inert_eqs)) tys
-- NB True: ignore casts coercions -- NB True: ignore casts coercions
-- See Note [Splitting WD constraints] -- See Note [Splitting WD constraints]
canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
canRewriteTv inert_eqs eq_rel tv
| Just (ct : _) <- lookupDVarEnv inert_eqs tv
, CTyEqCan { cc_eq_rel = eq_rel1 } <- ct
= eq_rel1 `eqCanRewrite` eq_rel
| otherwise
= False
isImprovable :: CtEvidence -> Bool isImprovable :: CtEvidence -> Bool
-- See Note [Do not do improvement for WOnly] -- See Note [Do not do improvement for WOnly]
isImprovable (CtWanted { ctev_nosh = WOnly }) = False isImprovable (CtWanted { ctev_nosh = WOnly }) = False
...@@ -1398,9 +1420,10 @@ addInertEq ct ...@@ -1398,9 +1420,10 @@ addInertEq ct
; ics <- getInertCans ; ics <- getInertCans
; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel })
<- maybeEmitShadow ics ct
; (_, ics1) <- kickOutRewritable (ctEvFlavourRole ev) tv ics ; (_, ics1) <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct ; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct
, inert_count = bumpUnsolvedCount ev (inert_count ics1) } , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
...@@ -1510,6 +1533,15 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs ...@@ -1510,6 +1533,15 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
-- Of course we must kick out irreducibles like (c a), in case -- Of course we must kick out irreducibles like (c a), in case
-- we can rewrite 'c' to something more useful -- we can rewrite 'c' to something more useful
(_, new_role) = new_fr
fr_can_rewrite_ty :: EqRel -> Type -> Bool
fr_can_rewrite_ty role ty = anyRewritableTyVar False role
fr_can_rewrite_tv ty
fr_can_rewrite_tv :: EqRel -> TyVar -> Bool
fr_can_rewrite_tv role tv = new_role `eqCanRewrite` role
&& tv == new_tv
fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
-- Can the new item rewrite the inert item? -- Can the new item rewrite the inert item?
...@@ -1517,9 +1549,9 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs ...@@ -1517,9 +1549,9 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
kick_out_ct :: Ct -> Bool kick_out_ct :: Ct -> Bool
-- Kick it out if the new CTyEqCan can rewrite the inert one -- Kick it out if the new CTyEqCan can rewrite the inert one
-- See Note [kickOutRewritable] -- See Note [kickOutRewritable]
kick_out_ct ct | let ev = ctEvidence ct kick_out_ct ct | let fs@(_,role) = ctFlavourRole ct
= fr_may_rewrite (ctEvFlavourRole ev) = fr_may_rewrite fs
&& anyRewritableTyVar False (== new_tv) (ctEvPred ev) && fr_can_rewrite_ty role (ctPred ct)
-- False: ignore casts and coercions -- False: ignore casts and coercions
-- NB: this includes the fsk of a CFunEqCan. It can't -- NB: this includes the fsk of a CFunEqCan. It can't
-- actually be rewritten, but we need to kick it out -- actually be rewritten, but we need to kick it out
...@@ -1533,33 +1565,34 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs ...@@ -1533,33 +1565,34 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
[] -> acc_in [] -> acc_in
(eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in) (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
where where
(eqs_in, eqs_out) = partition keep_eq eqs (eqs_out, eqs_in) = partition kick_out_eq eqs
-- Implements criteria K1-K3 in Note [Extending the inert equalities] -- Implements criteria K1-K3 in Note [Extending the inert equalities]
keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty
, cc_eq_rel = eq_rel }) , cc_ev = ev, cc_eq_rel = eq_rel })
| tv == new_tv | not (fr_may_rewrite fs)
= not (fr_may_rewrite fs) -- (K1) = False -- Keep it in the inert set if the new thing can't rewrite it
-- Below here (fr_may_rewrite fs) is True
| tv == new_tv = True -- (K1)
| kick_out_for_inertness = True
| kick_out_for_completeness = True
| otherwise = False
| otherwise
= check_k2 && check_k3
where where
fs = ctEvFlavourRole ev fs = (ctEvFlavour ev, eq_rel)
check_k2 = not (fs `eqMayRewriteFR` fs) -- (K2a) kick_out_for_inertness
|| (fs `eqMayRewriteFR` new_fr) -- (K2b) = (fs `eqMayRewriteFR` fs) -- (K2a)
|| not (fr_may_rewrite fs) -- (K2c) && not (fs `eqMayRewriteFR` new_fr) -- (K2b)
|| not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d) && fr_can_rewrite_ty eq_rel rhs_ty -- (K2d)
-- (K2c) is guaranteed by the first guard of keep_eq
check_k3
| fr_may_rewrite fs kick_out_for_completeness
= case eq_rel of = case eq_rel of
NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) NomEq -> rhs_ty `eqType` mkTyVarTy new_tv
ReprEq -> not (isTyVarExposed new_tv rhs_ty) ReprEq -> isTyVarHead new_tv rhs_ty
| otherwise
= True
keep_eq ct = pprPanic "keep_eq" (ppr ct) kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
kickOutAfterUnification :: TcTyVar -> TcS Int kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification new_tv kickOutAfterUnification new_tv
......
...@@ -79,7 +79,7 @@ module TcType ( ...@@ -79,7 +79,7 @@ module TcType (
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck, isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead, checkValidClsArgs, hasTyVarHead,
isRigidTy, isRigidTy,
...@@ -909,39 +909,60 @@ exactTyCoVarsOfType ty ...@@ -909,39 +909,60 @@ exactTyCoVarsOfType ty
exactTyCoVarsOfTypes :: [Type] -> TyVarSet exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
anyRewritableTyVar :: Bool -> (TcTyVar -> Bool) anyRewritableTyVar :: Bool -- Ignore casts and coercions
-> EqRel -- Ambient role
-> (EqRel -> TcTyVar -> Bool)
-> TcType -> Bool -> TcType -> Bool
-- (anyRewritableTyVar ignore_cos pred ty) returns True -- (anyRewritableTyVar ignore_cos pred ty) returns True
-- if the 'pred' returns True of free TyVar in 'ty' -- if the 'pred' returns True of any free TyVar in 'ty'
-- Do not look inside casts and coercions if 'ignore_cos' is True -- Do not look inside casts and coercions if 'ignore_cos' is True
-- See Note [anyRewritableTyVar] -- See Note [anyRewritableTyVar must be role-aware]
anyRewritableTyVar ignore_cos pred ty anyRewritableTyVar ignore_cos role pred ty
= go emptyVarSet ty = go role emptyVarSet ty
where where
go_tv bound tv | tv `elemVarSet` bound = False go_tv rl bvs tv | tv `elemVarSet` bvs = False
| otherwise = pred tv | otherwise = pred rl tv
go bound (TyVarTy tv) = go_tv bound tv go rl bvs (TyVarTy tv) = go_tv rl bvs tv
go _ (LitTy {}) = False go _ _ (LitTy {}) = False
go bound (TyConApp _ tys) = any (go bound) tys go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys
go bound (AppTy fun arg) = go bound fun || go bound arg go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg
go bound (FunTy arg res) = go bound arg || go bound res go rl bvs (FunTy arg res) = go rl bvs arg || go rl bvs res
go bound (ForAllTy tv ty) = go (bound `extendVarSet` binderVar tv) ty go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
go bound (CastTy ty co) = go bound ty || go_co bound co go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co
go bound (CoercionTy co) = go_co bound co go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check
go_co bound co go_tc NomEq bvs _ tys = any (go NomEq bvs) tys
go_tc ReprEq bvs tc tys = foldr ((&&) . go_arg bvs) False $
(tyConRolesRepresentational tc `zip` tys)
go_arg _ (Phantom, _) = False -- ToDo: check
go_arg bvs (Nominal, ty) = go NomEq bvs ty
go_arg bvs (Representational, ty) = go ReprEq bvs ty
go_co rl bvs co
| ignore_cos = False | ignore_cos = False
| otherwise = anyVarSet (go_tv bound) (tyCoVarsOfCo co) | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co)
-- We don't have an equivalent of anyRewritableTyVar for coercions -- We don't have an equivalent of anyRewritableTyVar for coercions
-- (at least not yet) so take the free vars and test them -- (at least not yet) so take the free vars and test them
{- Note [anyRewritableTyVar] {- Note [anyRewritableTyVar must be role-aware]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
anyRewritableTyVar is used during kick-out from the inert set, anyRewritableTyVar is used during kick-out from the inert set,
to decide if, given a new equality (a ~ ty), we should kick out 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' 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. is among them, we instead pass in a predicate; this is just efficiency.