Improve kick-out in the constraint solver
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 20 Oct 2017 11:08:04 +0000 (12:08 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 20 Oct 2017 11:08:55 +0000 (12:08 +0100)
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

compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcType.hs
testsuite/tests/typecheck/should_compile/T14363.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T14363a.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 4d23b55..3c44cde 100644 (file)
@@ -1397,12 +1397,13 @@ flatten_tyvar2 tv fr@(_, eq_rel)
        ; case lookupDVarEnv ieqs tv of
            Just (ct:_)   -- If the first doesn't work,
                          -- the subsequent ones won't either
-             | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
-             , let ct_fr = ctEvFlavourRole ctev
+             | CTyEqCan { cc_ev = ctev, cc_tyvar = tv
+                        , 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
              ->  do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr 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 )
                                     -- if this ASSERT fails, then
                                     -- eqCanRewriteFR answered incorrectly
index 04ff0f8..0413626 100644 (file)
@@ -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
                             , SwapFlag    -- Whether we need mkSymCo
                             , Bool)       -- True <=> keep a [D] version
                                           --          of the [WD] constraint
-inertsCanDischarge inerts tv rhs ev
-  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
+inertsCanDischarge inerts tv rhs fr
+  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
+                                    , cc_eq_rel = eq_rel }
                              <- findTyEqs inerts tv
-                         , ev_i `eqCanDischarge` ev
+                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
                          , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ ty
      -- Work item: a ~ ty
     Just (ev_i, NotSwapped, keep_deriv ev_i)
 
   | 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
-                         , ev_i `eqCanDischarge` ev
+                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
@@ -1519,7 +1521,7 @@ inertsCanDischarge inerts tv rhs ev
   where
     keep_deriv ev_i
       | 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
       | otherwise
       = False  -- Work item is fully discharged
@@ -1531,7 +1533,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                           , cc_ev = ev
                                           , cc_eq_rel = eq_rel })
   | Just (ev_i, swapped, keep_deriv)
-       <- inertsCanDischarge inerts tv rhs ev
+       <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
   = do { setEvBindIfWanted ev $
          EvCoercion (maybeSym swapped $
                      tcDowngradeRole (eqRelRole eq_rel)
index a109764..e73fdd6 100644 (file)
@@ -121,8 +121,8 @@ module TcRnTypes(
 
         CtFlavour(..), ShadowInfo(..), ctEvFlavour,
         CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
-        eqCanRewriteFR, eqMayRewriteFR,
-        eqCanDischarge,
+        eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
+        eqCanDischargeFR,
         funEqCanDischarge, funEqCanDischargeF,
 
         -- Pretty printing
@@ -2768,9 +2768,19 @@ type CtFlavourRole = (CtFlavour, EqRel)
 ctEvFlavourRole :: CtEvidence -> CtFlavourRole
 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 = 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]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -2817,14 +2827,18 @@ ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
 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
 -- Can fr1 actually rewrite fr2?
 -- Very important function!
 -- See Note [eqCanRewrite]
 -- See Note [Wanteds do not rewrite Wanteds]
 -- See Note [Deriveds do rewrite Deriveds]
-eqCanRewriteFR (Given, NomEq)         (_, _)           = True
-eqCanRewriteFR (Given, ReprEq)        (_, ReprEq)      = True
+eqCanRewriteFR (Given,         r1)    (_,       r2)    = eqCanRewrite r1 r2
 eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True
 eqCanRewriteFR (Derived,       NomEq) (Derived, NomEq) = True
 eqCanRewriteFR _                      _                = False
@@ -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]
 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 (_, ReprEq) (_, NomEq) = False
-eqCanDischargeFR (f1,_)      (f2, _)    = eqCanDischargeF f1 f2
+-- See Note [eqCanDischarge]
+eqCanDischargeFR (f1,r1) (f2, r2) =  eqCanRewrite r1 r2
+                                  && eqCanDischargeF f1 f2
 
 eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
 eqCanDischargeF Given   _                  = True
index 3038def..c5c1102 100644 (file)
@@ -783,36 +783,38 @@ guarantee that this recursive use will terminate.
 
 Note [Extending the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Theorem [Stability under extension]
-   This is the main theorem!
+Main Theorem [Stability under extension]
    Suppose we have a "work item"
        a -fw-> t
    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,_)
       (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
 
-      (K1) for every (a -fs-> s) in S, then not (fw >= fs)
-           Reason: the work item is fully rewritten by S, hence not (fs >= fw)
-                   but if (fw >= fs) then the work item could rewrite
-                   the inert item
+      AND, for every (b -fs-> s) in S:
+           (K0) not (fw >= fs)
+                Reason: suppose we kick out (a -fs-> s),
+                        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
-              (K2a) not (fs >= fs)
-           or (K2b) fs >= fw
-           or (K2c) not (fw >= fs)
-           or (K2d) a not in s
+           OR { (K1) not (a = b)
+                     Reason: if fw >= fs, WF1 says we can't have both
+                             a -fw-> t  and  a -fs-> s
 
-      (K3) See Note [K3: completeness of solving]
-           If (b -fs-> s) is in S with (fw >= fs), then
-        (K3a) If the role of fs is nominal: s /= a
-        (K3b) If the role of fs is representational: EITHER
-                a not in s, OR
-                the path from the top of s to a includes at least one non-newtype
+                AND (K2): guarantees inertness of the new substitution
+                    {  (K2a) not (fs >= fs)
+                    OR (K2b) fs >= fw
+                    OR (K2d) a not in s }
+
+                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 (K1-K3) are established by TcSMonad.kickOutRewritable
@@ -840,11 +842,12 @@ The idea is that
   us to kick out an inert wanted that mentions a, because of (K2a).  This
   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
-         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
   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
               (a -fs-> t) in S, s.t.  (fs >= fw).
@@ -921,26 +924,35 @@ is somewhat accidental.
 
 When considering roles, we also need the second clause (K3b). Consider
 
-  inert-item   a -W/R-> b c
   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.
-We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were
-condition (K3a), then we would keep the inert around and add the work item.
-But then, consider if we hit the following:
-
-  work-item2   b -G/N-> Id
+But we don't kick out the inert item because not (W/R >= W/R).  So we just
+add the work item. But then, consider if we hit the following:
 
+  work-item    b -G/N-> Id
+  inert-items  a -W/R-> b c
+               c -G/N-> a
 where
-
   newtype Id x = Id x
 
 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
-now reduced to reflexivity. The solution here is to kick out representational
-inerts whenever the tyvar of a work item is "exposed", where exposed means
-not under some proper data-type constructor, like [] or Maybe. See
-isTyVarExposed in TcType. This is encoded in (K3b).
+now reduced to reflexivity.
+
+The solution here is to kick out representational inerts whenever the
+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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1272,11 +1284,13 @@ shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys })
     -- NB True: ignore coercions
     -- 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
-  || anyRewritableTyVar False (`elemDVarEnv` inert_eqs) ty
+  || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
   -- NB False: do not ignore casts and coercions
   -- See Note [Splitting WD constraints]
+  where
 
 shouldSplitWD _ _ = False   -- No point in splitting otherwise
 
@@ -1284,10 +1298,18 @@ 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
+  = any (anyRewritableTyVar True NomEq (canRewriteTv inert_eqs)) tys
     -- NB True: ignore casts coercions
     -- 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
 -- See Note [Do not do improvement for WOnly]
 isImprovable (CtWanted { ctev_nosh = WOnly }) = False
@@ -1398,9 +1420,10 @@ addInertEq ct
 
        ; 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
                          , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
@@ -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
       -- 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 fs = new_fr `eqMayRewriteFR` fs
         -- 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
     kick_out_ct :: Ct -> Bool
     -- Kick it out if the new CTyEqCan can rewrite the inert one
     -- See Note [kickOutRewritable]
-    kick_out_ct ct | let ev = ctEvidence ct
-                   = fr_may_rewrite (ctEvFlavourRole ev)
-                   && anyRewritableTyVar False (== new_tv) (ctEvPred ev)
+    kick_out_ct ct | let fs@(_,role) = ctFlavourRole ct
+                   = fr_may_rewrite fs
+                   && fr_can_rewrite_ty role (ctPred ct)
                   -- 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
@@ -1533,33 +1565,34 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                                []      -> acc_in
                                (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
       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]
-    keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
-                      , cc_eq_rel = eq_rel })
-      | tv == new_tv
-      = not (fr_may_rewrite fs)  -- (K1)
+    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty
+                          , cc_ev = ev, cc_eq_rel = eq_rel })
+      | not (fr_may_rewrite fs)
+      = 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
-        fs = ctEvFlavourRole ev
-        check_k2 = not (fs  `eqMayRewriteFR` fs)                   -- (K2a)
-                ||     (fs  `eqMayRewriteFR` new_fr)               -- (K2b)
-                || not (fr_may_rewrite  fs)                        -- (K2c)
-                || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d)
-
-        check_k3
-          | fr_may_rewrite fs
+        fs = (ctEvFlavour ev, eq_rel)
+        kick_out_for_inertness
+          =        (fs `eqMayRewriteFR` fs)       -- (K2a)
+            && not (fs `eqMayRewriteFR` new_fr)   -- (K2b)
+            && fr_can_rewrite_ty eq_rel rhs_ty    -- (K2d)
+            -- (K2c) is guaranteed by the first guard of keep_eq
+
+        kick_out_for_completeness
           = case eq_rel of
-              NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
-              ReprEq -> not (isTyVarExposed new_tv rhs_ty)
-
-          | otherwise
-          = True
+              NomEq  -> rhs_ty `eqType` mkTyVarTy new_tv
+              ReprEq -> isTyVarHead new_tv rhs_ty
 
-    keep_eq ct = pprPanic "keep_eq" (ppr ct)
+    kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
 
 kickOutAfterUnification :: TcTyVar -> TcS Int
 kickOutAfterUnification new_tv
index 4d65fcd..7b27ce1 100644 (file)
@@ -79,7 +79,7 @@ module TcType (
   isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
   hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
-  isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck,
+  isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
   checkValidClsArgs, hasTyVarHead,
   isRigidTy,
 
@@ -909,39 +909,60 @@ exactTyCoVarsOfType ty
 exactTyCoVarsOfTypes :: [Type] -> TyVarSet
 exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
 
-anyRewritableTyVar :: Bool -> (TcTyVar -> Bool)
+anyRewritableTyVar :: Bool    -- Ignore casts and coercions
+                   -> EqRel   -- Ambient role
+                   -> (EqRel -> TcTyVar -> Bool)
                    -> TcType -> Bool
 -- (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
--- See Note [anyRewritableTyVar]
-anyRewritableTyVar ignore_cos pred ty
-  = go emptyVarSet ty
+-- See Note [anyRewritableTyVar must be role-aware]
+anyRewritableTyVar ignore_cos role pred ty
+  = go role emptyVarSet ty
   where
-    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
+    go_tv rl bvs tv | tv `elemVarSet` bvs = False
+                    | otherwise           = pred rl tv
+
+    go rl bvs (TyVarTy tv)      = go_tv rl bvs tv
+    go _ _     (LitTy {})       = False
+    go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys
+    go rl bvs (AppTy fun arg)   = go rl bvs fun || go NomEq bvs arg
+    go rl bvs (FunTy arg res)   = go rl bvs arg || go rl bvs res
+    go rl bvs (ForAllTy tv ty)  = go rl (bvs `extendVarSet` binderVar tv) ty
+    go rl bvs (CastTy ty co)    = go rl bvs ty || go_co rl bvs co
+    go rl bvs (CoercionTy co)   = go_co rl bvs co  -- ToDo: check
+
+    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
-      | 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
       -- (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,
 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.
+
+Moreover, consider
+  work item:   [G] a ~R f b
+  inert item:  [G] b ~R f a
+We use anyRewritableTyVar to decide whether to kick out the inert item,
+on the grounds that the work item might rewrite it. Well, 'a' is certainly
+free in [G] b ~R f a.  But becuase the role of a type variable ('f' in
+this case) is nominal, the work item can't actually rewrite the inert item.
+Moreover, if we were to kick out the inert item the exact same situation
+would re-occur and we end up with an infninite loop in which each kicks
+out the other (Trac #14363).
 -}
 
 {- *********************************************************************
@@ -2147,22 +2168,17 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
                         Just (tc, _) -> uniq == getUnique tc
                         Nothing      -> False
 
--- | Does the given tyvar appear in the given type outside of any
--- non-newtypes? Assume we're looking for @a@. Says "yes" for
--- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for
--- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype.
-isTyVarExposed :: TcTyVar -> TcType -> Bool
-isTyVarExposed tv (TyVarTy tv')   = tv == tv'
-isTyVarExposed tv (TyConApp tc tys)
-  | isNewTyCon tc                 = any (isTyVarExposed tv) tys
-  | otherwise                     = False
-isTyVarExposed _  (LitTy {})      = False
-isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
-                                 || isTyVarExposed tv arg
-isTyVarExposed _  (ForAllTy {})   = False
-isTyVarExposed _  (FunTy {})      = False
-isTyVarExposed tv (CastTy ty _)   = isTyVarExposed tv ty
-isTyVarExposed _  (CoercionTy {}) = False
+-- | Does the given tyvar appear at the head of a chain of applications
+--     (a t1 ... tn)
+isTyVarHead :: TcTyVar -> TcType -> Bool
+isTyVarHead tv (TyVarTy tv')   = tv == tv'
+isTyVarHead tv (AppTy fun _)   = isTyVarHead tv fun
+isTyVarHead tv (CastTy ty _)   = isTyVarHead tv ty
+isTyVarHead _ (TyConApp {})    = False
+isTyVarHead _  (LitTy {})      = False
+isTyVarHead _  (ForAllTy {})   = False
+isTyVarHead _  (FunTy {})      = False
+isTyVarHead _  (CoercionTy {}) = False
 
 -- | Is the equality
 --        a ~r ...a....
diff --git a/testsuite/tests/typecheck/should_compile/T14363.hs b/testsuite/tests/typecheck/should_compile/T14363.hs
new file mode 100644 (file)
index 0000000..fe8966e
--- /dev/null
@@ -0,0 +1,11 @@
+module T14363 where
+
+import Data.Coerce
+
+foo x = [fmap, coerce]
+-- Should work
+-- foo :: forall b (f :: * -> *) a p.
+--        (Functor f, Coercible a (f a), Coercible b (f b)) =>
+--        p -> [(a -> b) -> f a -> f b]
+--
+-- Failed in 8.2
diff --git a/testsuite/tests/typecheck/should_compile/T14363a.hs b/testsuite/tests/typecheck/should_compile/T14363a.hs
new file mode 100644 (file)
index 0000000..4a38ab5
--- /dev/null
@@ -0,0 +1,8 @@
+module T14363a where
+
+import Data.Coerce
+
+contra :: (a -> b) -> (f b -> f a)
+contra = undefined
+
+foo x = [coerce, contra]
index ac18cce..a83e41a 100644 (file)
@@ -578,3 +578,5 @@ test('T14154', normal, compile, [''])
 test('T14158', normal, compile, [''])
 test('T13943', normal, compile, ['-fsolve-constant-dicts'])
 test('T14333', normal, compile, [''])
+test('T14363', normal, compile, [''])
+test('T14363a', normal, compile, [''])