diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-02-08 14:24:11 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-02-08 14:25:47 +0000 |
commit | 6edafe3be0133fe69581fb3851a812c69ab9dbf7 (patch) | |
tree | 00f6f58cb7e5e233199d211b2ed397179b558584 /compiler | |
parent | 059596df51619314a2e240af618fe7f4d2550ff2 (diff) | |
download | haskell-6edafe3be0133fe69581fb3851a812c69ab9dbf7.tar.gz |
Fix isDroppableCt (Trac #14763)
When finishing up an implication constraint, it's a bit tricky to
decide which Derived constraints to retain (for error reporting) and
which to discard. I got this wrong in commit
f20cf982f126aea968ed6a482551550ffb6650cf
(Remove wc_insol from WantedConstraints)
The particular problem in Trac #14763 was that we were reporting as an
error a fundep-generated constraint
(ex ~ T)
where 'ex' is an existentially-bound variable in a pattern match.
But this isn't really an error at all.
This patch fixes the problem. Indeed, since I had to understand
this rather tricky code, I took the opportunity to clean it up
and document better. See
isDroppableCt :: Ct -> Bool
and Note [Dropping derived constraints]
I also removed wl_deriv altogether from the WorkList data type. It
was there in the hope of gaining efficiency by not even processing
lots of derived constraints, but it has turned out that most derived
constraints (notably equalities) must be processed anyway; see
Note [Prioritise equalities] in TcSMonad.
The two are coupled because to decide which constraints to put in
wl_deriv I was using another variant of isDroppableCt. Now it's much
simpler -- and perhaps even more efficient too.
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/typecheck/TcCanonical.hs | 15 | ||||
-rw-r--r-- | compiler/typecheck/TcErrors.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 5 | ||||
-rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 109 | ||||
-rw-r--r-- | compiler/typecheck/TcSMonad.hs | 109 |
5 files changed, 113 insertions, 127 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 868d785b18..5618824ed5 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1700,11 +1700,16 @@ is embarrassing. See #11198 for more tales of destruction. The reason for this odd behavior is much the same as Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the -new `co` is a Wanted. The solution is then not to use `co` to "rewrite" --- that is, cast -- `w`, but instead to keep `w` heterogeneous and irreducible. -Given that we're not using `co`, there is no reason to collect evidence -for it, so `co` is born a Derived. When the Derived is solved (by unification), -the original wanted (`w`) will get kicked out. +new `co` is a Wanted. + + The solution is then not to use `co` to "rewrite" -- that is, cast + -- `w`, but instead to keep `w` heterogeneous and + irreducible. Given that we're not using `co`, there is no reason to + collect evidence for it, so `co` is born a Derived, with a CtOrigin + of KindEqOrigin. + +When the Derived is solved (by unification), the original wanted (`w`) +will get kicked out. Note that, if we had [G] co1 :: k ~ Type available, then none of this code would trigger, because flattening would have rewritten k to Type. That is, diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index fb27b4ed7c..8d2238a985 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -700,7 +700,7 @@ we'll complain about f :: ((Int ~ Bool) => a -> a) -> Int which arguably is OK. It's more debatable for g :: (Int ~ Bool) => Int -> Int -but it's tricky to distinguish these cases to we don't report +but it's tricky to distinguish these cases so we don't report either. The bottom line is this: find_gadt_match looks for an enclosing diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 9a2f64d672..d0bcddf19f 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -686,7 +686,7 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble }) -- which can happen with solveOneFromTheOther, so that -- we get distinct error messages with -fdefer-type-errors -- See Note [Do not add duplicate derived insolubles] - , not (isDroppableDerivedCt workItem) + , not (isDroppableCt workItem) = continueWith workItem | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w @@ -1882,7 +1882,8 @@ improveTopFunEqs ev fam_tc args fsk , ppr eqns ]) ; mapM_ (unifyDerived loc Nominal) eqns } where - loc = ctEvLoc ev + loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2 + -- See Trac #14778 improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 5e52496696..d2c8dd8a43 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -87,7 +87,7 @@ module TcRnTypes( addInsols, insolublesOnly, addSimples, addImplics, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, - isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic, + isDroppableCt, insolubleImplic, arisesFromGivens, Implication(..), newImplication, @@ -1931,13 +1931,10 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples dropDerivedCt :: Ct -> Maybe Ct dropDerivedCt ct = case ctEvFlavour ev of - Given -> Just ct -- Presumably insoluble; keep Wanted WOnly -> Just (ct' { cc_ev = ev_wd }) Wanted _ -> Just ct' - Derived | isDroppableDerivedLoc (ctLoc ct) - -> Nothing - | otherwise - -> Just ct + _ | isDroppableCt ct -> Nothing + | otherwise -> Just ct where ev = ctEvidence ct ev_wd = ev { ctev_nosh = WDeriv } @@ -1953,26 +1950,41 @@ we might miss some fundeps. Trac #13662 showed this up. See Note [The superclass story] in TcCanonical. -} -isDroppableDerivedCt :: Ct -> Bool -isDroppableDerivedCt ct - | isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct) - | otherwise = False - -isDroppableDerivedLoc :: CtLoc -> Bool --- See Note [Dropping derived constraints] -isDroppableDerivedLoc loc - = case ctLocOrigin loc of - HoleOrigin {} -> False - KindEqOrigin {} -> False - GivenOrigin {} -> False - - -- See Note [Dropping derived constraints] - -- For fundeps, drop wanted/wanted interactions - FunDepOrigin2 {} -> False - FunDepOrigin1 _ loc1 _ loc2 - | isGivenLoc loc1 || isGivenLoc loc2 -> False - | otherwise -> True - _ -> True +isDroppableCt :: Ct -> Bool +isDroppableCt ct + = isDerived ev && not keep_deriv + -- Drop only derived constraints, and then only if they + -- obey Note [Dropping derived constraints] + where + ev = ctEvidence ct + loc = ctEvLoc ev + orig = ctLocOrigin loc + + keep_deriv + = case ct of + CHoleCan {} -> True + CIrredCan { cc_insol = insoluble } + -> keep_eq insoluble + _ -> keep_eq False + + keep_eq definitely_insoluble + | isGivenOrigin orig -- Arising only from givens + = definitely_insoluble -- Keep only definitely insoluble + | otherwise + = case orig of + KindEqOrigin {} -> True -- Why? + + -- See Note [Dropping derived constraints] + -- For fundeps, drop wanted/wanted interactions + FunDepOrigin2 {} -> True -- Top-level/Wanted + FunDepOrigin1 _ loc1 _ loc2 + | g1 || g2 -> True -- Given/Wanted errors: keep all + | otherwise -> False -- Wanted/Wanted errors: discard + where + g1 = isGivenLoc loc1 + g2 = isGivenLoc loc2 + + _ -> False arisesFromGivens :: Ct -> Bool arisesFromGivens ct @@ -1995,30 +2007,43 @@ isGivenOrigin _ = False In general we discard derived constraints at the end of constraint solving; see dropDerivedWC. For example - * If we have an unsolved [W] (Ord a), we don't want to complain about - an unsolved [D] (Eq a) as well. + * Superclasses: if we have an unsolved [W] (Ord a), we don't want to + complain about an unsolved [D] (Eq a) as well. * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate - [D] Int ~ Bool, and we don't want to report that because it's incomprehensible. - That is why we don't rewrite wanteds with wanteds! + [D] Int ~ Bool, and we don't want to report that because it's + incomprehensible. That is why we don't rewrite wanteds with wanteds! -But (tiresomely) we do keep *some* Derived insolubles: +But (tiresomely) we do keep *some* Derived constraints: * Type holes are derived constraints, because they have no evidence and we want to keep them, so we get the error report - * Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from - functional dependency interactions: - - Given or Wanted interacting with an instance declaration (FunDepOrigin2) - - Given/Given interactions (FunDepOrigin1); this reflects unreachable code + * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with + KindEqOrigin, may arise from a type equality a ~ Int#, say. See + Note [Equalities with incompatible kinds] in TcCanonical. + + * We keep most derived equalities arising from functional dependencies + - Given/Given interactions (subset of FunDepOrigin1): + The definitely-insoluble ones reflect unreachable code. + + Others not-definitely-insoluble ones like [D] a ~ Int do not + reflect unreachable code; indeed if fundeps generated proofs, it'd + be a useful equality. See Trac #14763. So we discard them. + + - Given/Wanted interacGiven or Wanted interacting with an + instance declaration (FunDepOrigin2) + - Given/Wanted interactions (FunDepOrigin1); see Trac #9612 - But for Wanted/Wanted interactions we do /not/ want to report an - error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with - a fundep on class C. We don't want to report an insoluble Int~Bool; - c.f. "wanteds do not rewrite wanteds". + - But for Wanted/Wanted interactions we do /not/ want to report an + error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with + a fundep on class C. We don't want to report an insoluble Int~Bool; + c.f. "wanteds do not rewrite wanteds". + +To distinguish these cases we use the CtOrigin. -Moreover, we keep *all* derived insolubles under some circumstances: +NB: we keep *all* derived insolubles under some circumstances: * They are looked at by simplifyInfer, to decide whether to generalise. Example: [W] a ~ Int, [W] a ~ Bool @@ -2026,8 +2051,6 @@ Moreover, we keep *all* derived insolubles under some circumstances: and we want simplifyInfer to see that, even though we don't ultimately want to generate an (inexplicable) error message from it -To distinguish these cases we use the CtOrigin. - ************************************************************************ * * @@ -3301,7 +3324,7 @@ data CtOrigin -- visible.) Only used for prioritizing error messages. } - | KindEqOrigin + | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical. TcType (Maybe TcType) -- A kind equality arising from unifying these two types CtOrigin -- originally arising from this (Maybe TypeOrKind) -- the level of the eq this arises from diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 0b1d6e4cbd..0db75095f1 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -5,7 +5,7 @@ module TcSMonad ( -- The work list WorkList(..), isEmptyWorkList, emptyWorkList, - extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, + extendWorkListNonEq, extendWorkListCt, extendWorkListCts, extendWorkListEq, extendWorkListFunEq, appendWorkList, extendWorkListImplic, selectNextWorkItem, @@ -36,7 +36,7 @@ module TcSMonad ( setEvBind, setWantedEq, setEqIfWanted, setWantedEvTerm, setWantedEvBind, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - emitNewDerived, emitNewDeriveds, emitNewDerivedEq, + emitNewDeriveds, emitNewDerivedEq, checkReductionDepth, getInstEnvs, getFamInstEnvs, -- Getting the environments @@ -191,7 +191,8 @@ consider using this depth for prioritization as well in the future. As a simple form of priority queue, our worklist separates out * equalities (wl_eqs); see Note [Prioritise equalities] -* non-equality deriveds (wl_derivs); see Note [Process derived items last] +* type-function equalities (wl_funeqs) +* all the rest (wl_rest) Note [Prioritise equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -202,10 +203,6 @@ It's very important to process equalities /first/: and then kicking it out later. That's extra work compared to just doing the equality first. -* (Derived equalities) Notwithstanding Note [Process derived items - last], we want to process /Derived/ equalities eagerly, for the - (Efficiency) reason above. - * (Avoiding fundep iteration) As Trac #14723 showed, it's possible to get non-termination if we - Emit the Derived fundep equalities for a class constraint, @@ -216,15 +213,21 @@ It's very important to process equalities /first/: equalities in the work-list), but generates yet more fundeps Solution: prioritise derived equalities over class constraints -* (Class equalities) We need to prioritise equalities even if they are - hidden inside a class constraint; see Note [Prioritise class - equalities] +* (Class equalities) We need to prioritise equalities even if they + are hidden inside a class constraint; + see Note [Prioritise class equalities] * (Kick-out) We want to apply this priority scheme to kicked-out constraints too (see the call to extendWorkListCt in kick_out_rewritable E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become homo-kinded when kicked out, and hence we want to priotitise it. +* (Derived equalities) Originally we tried to postpone processing + Derived equalities, in the hope that we might never need to deal + with them at all; but in fact we must process Derived equalities + eagerly, partly for the (Efficiency) reason, and more importantly + for (Avoiding fundep iteration). + Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prioritise equalities in the solver (see selectWorkItem). But class @@ -241,13 +244,6 @@ So we arrange to put these particular class constraints in the wl_eqs. NB: since we do not currently apply the substitution to the inert_solved_dicts, the knot-tying still seems a bit fragile. But this makes it better. - -Note [Process derived items last] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can often solve all goals without processing *any* derived constraints. -The derived constraints are just there to help us if we get stuck. So -we keep them in a separate list. - -} -- See Note [WorkList priorities] @@ -263,29 +259,23 @@ data WorkList , wl_rest :: [Ct] - , wl_deriv :: [CtEvidence] - -- Implicitly non-canonical - -- No equalities in here (they are in wl_eqs) - -- See Note [Process derived items last] - , wl_implics :: Bag Implication -- See Note [Residual implications] } appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1 - , wl_deriv = ders1, wl_implics = implics1 }) + , wl_implics = implics1 }) (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2 - , wl_deriv = ders2, wl_implics = implics2 }) + , wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 , wl_funeqs = funeqs1 ++ funeqs2 , wl_rest = rest1 ++ rest2 - , wl_deriv = ders1 ++ ders2 , wl_implics = implics1 `unionBags` implics2 } workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest }) - = length eqs + length funeqs + length rest + length ders +workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest }) + = length eqs + length funeqs + length rest workListWantedCount :: WorkList -> Int -- Count the things we need to solve @@ -302,9 +292,6 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) extendWorkListEq :: Ct -> WorkList -> WorkList extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } -extendWorkListEqs :: [Ct] -> WorkList -> WorkList -extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl } - extendWorkListFunEq :: Ct -> WorkList -> WorkList extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl } @@ -312,15 +299,9 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList -extendWorkListDerived loc ev wl - | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl } - | otherwise = extendWorkListEq (mkNonCanonical ev) wl - -extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList -extendWorkListDeriveds loc evs wl - | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl } - | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl +extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList +extendWorkListDeriveds evs wl + = extendWorkListCts (map mkNonCanonical evs) wl extendWorkListImplic :: Bag Implication -> WorkList -> WorkList extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl } @@ -350,12 +331,12 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs - , wl_rest = rest, wl_deriv = ders, wl_implics = implics }) - = null eqs && null rest && null funeqs && isEmptyBag implics && null ders + , wl_rest = rest, wl_implics = implics }) + = null eqs && null rest && null funeqs && isEmptyBag implics emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs = [], wl_rest = [] - , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag } + , wl_funeqs = [], wl_implics = emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) -- See Note [Prioritise equalities] @@ -370,39 +351,23 @@ getWorkList :: TcS WorkList getWorkList = do { wl_var <- getTcSWorkListRef ; wrapTcS (TcM.readTcRef wl_var) } -selectDerivedWorkItem :: WorkList -> Maybe (Ct, WorkList) -selectDerivedWorkItem wl@(WL { wl_deriv = ders }) - | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv = evs }) - | otherwise = Nothing - selectNextWorkItem :: TcS (Maybe Ct) -- Pick which work item to do next -- See Note [Prioritise equalities] --- See Note [Process derived items last] selectNextWorkItem = do { wl_var <- getTcSWorkListRef ; wl <- wrapTcS (TcM.readTcRef wl_var) - - ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct) - try mb_work do_this_if_fail - | Just (ct, new_wl) <- mb_work - = do { checkReductionDepth (ctLoc ct) (ctPred ct) - ; wrapTcS (TcM.writeTcRef wl_var new_wl) - ; return (Just ct) } - | otherwise - = do_this_if_fail - - ; try (selectWorkItem wl) $ - - do { ics <- getInertCans - ; if inert_count ics == 0 - then return Nothing - else try (selectDerivedWorkItem wl) (return Nothing) } } + ; case selectWorkItem wl of { + Nothing -> return Nothing ; + Just (ct, new_wl) -> + do { checkReductionDepth (ctLoc ct) (ctPred ct) + ; wrapTcS (TcM.writeTcRef wl_var new_wl) + ; return (Just ct) } } } -- Pretty printing instance Outputable WorkList where ppr (WL { wl_eqs = eqs, wl_funeqs = feqs - , wl_rest = rest, wl_implics = implics, wl_deriv = ders }) + , wl_rest = rest, wl_implics = implics }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ text "Eqs =" <+> vcat (map ppr eqs) @@ -410,8 +375,6 @@ instance Outputable WorkList where text "Funeqs =" <+> vcat (map ppr feqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (null ders) $ - text "Derived =" <+> vcat (map ppr ders) , ppUnless (isEmptyBag implics) $ ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) (text "(Implics omitted)") @@ -2690,7 +2653,7 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside) do { env <- TcM.getLclEnv ; ev_binds_var <- TcM.newTcEvBinds ; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && - null (wl_deriv wl) && null (wl_implics wl), ppr wl ) + null (wl_implics wl), ppr wl ) WC { wc_simple = listToCts eqs , wc_impl = emptyBag } imp = newImplication { ic_tclvl = new_tclvl @@ -3184,12 +3147,6 @@ newWantedNC loc pty | otherwise = newWantedEvVarNC loc pty -emitNewDerived :: CtLoc -> TcPredType -> TcS () -emitNewDerived loc pred - = do { ev <- newDerivedNC loc pred - ; traceTcS "Emitting new derived" (ppr ev) - ; updWorkListTcS (extendWorkListDerived loc ev) } - emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () emitNewDeriveds loc preds | null preds @@ -3197,7 +3154,7 @@ emitNewDeriveds loc preds | otherwise = do { evs <- mapM (newDerivedNC loc) preds ; traceTcS "Emitting new deriveds" (ppr evs) - ; updWorkListTcS (extendWorkListDeriveds loc evs) } + ; updWorkListTcS (extendWorkListDeriveds evs) } emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () -- Create new equality Derived and put it in the work list @@ -3206,7 +3163,7 @@ emitNewDerivedEq loc role ty1 ty2 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } - -- Very important: put in the wl_eqs, /not/ wl_derivs + -- Very important: put in the wl_eqs -- See Note [Prioritise equalities] (Avoiding fundep iteration) newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence |