diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 58 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 102 |
2 files changed, 98 insertions, 62 deletions
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 0474f747e2..7d7f265b78 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1793,11 +1793,10 @@ superClassesMightHelp :: Ct -> Bool -- expose more equalities or functional dependencies) might help to -- solve this constraint. See Note [When superclases help] superClassesMightHelp ct - | CDictCan { cc_class = cls } <- ct - , cls `hasKey` ipClassKey - = False - | otherwise - = True + = isWantedCt ct && not (is_ip ct) + where + is_ip (CDictCan { cc_class = cls }) = isIPClass cls + is_ip _ = False {- Note [When superclasses help] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1805,26 +1804,35 @@ First read Note [The superclass story] in TcCanonical. We expand superclasses and iterate only if there is at unsolved wanted for which expansion of superclasses (e.g. from given constraints) -might actually help. Usually the answer is "yes" but for implicit -paramters it is "no". If we have [W] ?x::ty, expanding superclasses -won't help: - - Superclasses can't be implicit parameters - - If we have a [G] ?x:ty2, then we'll have another unsolved - [D] ty ~ ty2 (from the functional dependency) - which will trigger superclass expansion. - -It's a bit of a special case, but it's easy to do. The runtime cost -is low because the unsolved set is usually empty anyway (errors -aside), and the first non-imlicit-parameter will terminate the search. - -The special case is worth it (Trac #11480, comment:2) because it -applies to CallStack constraints, which aren't type errors. If we have - f :: (C a) => blah - f x = ...undefined... -we'll get a CallStack constraint. If that's the only unsolved constraint -it'll eventually be solved by defaulting. So we don't want to emit warnings -about hitting the simplifier's iteration limit. A CallStack constraint -really isn't an unsolved constraint; it can always be solved by defaulting. +might actually help. The function superClassesMightHelp tells if +doing this superclass expansion might help solve this constraint. +Note that + + * Superclasses help only for Wanted constraints. Derived constraints + are not really "unsolved" and we certainly don't want them to + trigger superclass expansion. This was a good part of the loop + in Trac #11523 + + * Even for Wanted constraints, we say "no" for implicit paramters. + we have [W] ?x::ty, expanding superclasses won't help: + - Superclasses can't be implicit parameters + - If we have a [G] ?x:ty2, then we'll have another unsolved + [D] ty ~ ty2 (from the functional dependency) + which will trigger superclass expansion. + + It's a bit of a special case, but it's easy to do. The runtime cost + is low because the unsolved set is usually empty anyway (errors + aside), and the first non-imlicit-parameter will terminate the search. + + The special case is worth it (Trac #11480, comment:2) because it + applies to CallStack constraints, which aren't type errors. If we have + f :: (C a) => blah + f x = ...undefined... + we'll get a CallStack constraint. If that's the only unsolved + constraint it'll eventually be solved by defaulting. So we don't + want to emit warnings about hitting the simplifier's iteration + limit. A CallStack constraint really isn't an unsolved + constraint; it can always be solved by defaulting. -} singleCt :: Ct -> Cts diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index edcedf7701..9cb2b9b955 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -554,8 +554,10 @@ Result data InertCans -- See Note [Detailed InertCans Invariants] for more = IC { inert_model :: InertModel + -- See Note [inert_model: the inert model] , inert_eqs :: TyVarEnv EqualCtList + -- See Note [inert_eqs: the inert equalities] -- All Given/Wanted CTyEqCans; index is the LHS tyvar , inert_funeqs :: FunEqMap Ct @@ -664,6 +666,10 @@ Note [inert_model: the inert model] - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in inert_eqs. + * The model is not subject to "kicking-out". Reason: we make a Derived + shadow copy of any Given/Wanted (a ~ ty), and that Derived copy will + be fully rewritten by the model before it is added + * The principal reason for maintaining the model is to generate equalities that tell us how to unify a variable: that is, what Mark Jones calls "improvement". The same idea is sometimes also @@ -1101,33 +1107,39 @@ Note [Adding an inert canonical constraint the InertCans] * Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq). - * Always (G/W/D) kick out constraints that can be rewritten - (respecting flavours) by the new constraint. This is done - by kickOutRewritable. + (A) Always (G/W/D) kick out constraints that can be rewritten + (respecting flavours) by the new constraint. This is done + by kickOutRewritable. + + (B) Applies only to nominal equalities: a ~ ty. Four cases: - Then, when adding: + [Representational] [G/W/D] a ~R ty: + Just add it to inert_eqs - * [Derived] a ~N ty - 1. Add (a~ty) to the model - NB: 'a' cannot be in fv(ty), because the constraint is canonical. + [Derived Nominal] [D] a ~N ty: + 1. Add (a~ty) to the model + NB: 'a' cannot be in fv(ty), because the constraint is canonical. - 2. (DShadow) Do emitDerivedShadows - For every inert G/W constraint c, st - (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]), - and - (b) the model cannot rewrite c - kick out a Derived *copy*, leaving the original unchanged. - Reason for (b) if the model can rewrite c, then we have already - generated a shadow copy + 2. (DShadow) Do emitDerivedShadows + For every inert G/W constraint c, st + (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]), + and + (b) the model cannot rewrite c + kick out a Derived *copy*, leaving the original unchanged. + Reason for (b) if the model can rewrite c, then we have already + generated a shadow copy - * [Given/Wanted] a ~N ty + [Given/Wanted Nominal] [G/W] a ~N ty: 1. Add it to inert_eqs 2. Emit [D] a~ty - As a result of (2), the current model will rewrite the new [D] a~ty - during canonicalisation, and then it'll be added to the model using - the steps of [Derived] above. + Step (2) is needed to allow the current model to fully + rewrite [D] a~ty before adding it using the [Derived Nominal] + steps above. - * [Representational equalities] a ~R ty: just add it to inert_eqs + We must do this even for Givens, because + work-item [G] a ~ [b], model has [D] b ~ a. + We need a shadow [D] a ~ [b] in the work-list + When we process it, we'll rewrite to a ~ [a] and get an occurs check * Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D] @@ -1207,21 +1219,11 @@ add_inert_eq ics@(IC { inert_count = n | ReprEq <- eq_rel = return new_ics --- | isGiven ev --- = return (new_ics { inert_model = extendVarEnv old_model tv ct }) } --- No no! E.g. --- work-item [G] a ~ [b], model has [D] b ~ a. --- We must not add the given to the model as-is. Instead, --- we put a shadow [D] a ~ [b] in the work-list --- When we process it, we'll rewrite to a ~ [a] and get an occurs check - | isDerived ev = do { emitDerivedShadows ics tv ; return (ics { inert_model = extendVarEnv old_model tv ct }) } - -- Nominal equality (tv ~N ty), Given/Wanted - -- See Note [Emitting shadow constraints] - | otherwise -- modelCanRewrite old_model rw_tvs -- Shadow of new ct isn't inert; emit it + | otherwise -- Given/Wanted Nominal equality [W] tv ~N ty = do { emitNewDerived loc pred ; return new_ics } where @@ -1722,8 +1724,10 @@ getUnsolvedInerts , inert_dicts = idicts , inert_insols = insols , inert_model = model } <- getInertCans + ; keep_derived <- keepSolvingDeriveds - ; let der_tv_eqs = foldVarEnv (add_der tv_eqs) emptyCts model -- Want to float these + ; let der_tv_eqs = foldVarEnv (add_der_eq keep_derived tv_eqs) + emptyCts model unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts unsolved_irreds = Bag.filterBag is_unsolved irreds @@ -1743,8 +1747,10 @@ getUnsolvedInerts -- Keep even the given insolubles -- so that we can report dead GADT pattern match branches where - add_der tv_eqs ct cts + add_der_eq keep_derived tv_eqs ct cts + -- See Note [Unsolved Derived equalities] | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct + , isMetaTyVar tv || keep_derived , not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts | otherwise = cts add_if_unsolved :: Ct -> Cts -> Cts @@ -1856,7 +1862,20 @@ prohibitedSuperClassSolve from_loc solve_loc | otherwise = False -{- +{- Note [Unsolved Derived equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In getUnsolvedInerts, we return a derived equality from the model +for two possible reasons: + + * Because it is a candidate for floating out of this implication. + We only float equalities with a meta-tyvar on the left, so we only + pull those out here. + + * If we are only solving derived constraints (i.e. tcs_need_derived + is true; see Note [Solving for Derived constraints]), then we + those Derived constraints are effectively unsolved, and we need + them! + Note [When does an implication have given equalities?] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider an implication @@ -2252,6 +2271,16 @@ All you can do is Filling in a dictionary evidence variable means to create a binding for it, so TcS carries a mutable location where the binding can be added. This is initialised from the innermost implication constraint. + +Note [Solving for Derived constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Sometimes we invoke the solver on a bunch of Derived constraints, not to +generate any evidence, but just to cause unification side effects or to +produce a simpler set of constraints. If that is what we are doing, we +should do two things differently: + a) Don't stop when you've solved all the Wanteds; instead keep going + if there are any Deriveds in the work queue. + b) In getInertUnsolved, include Derived ones -} data TcSEnv @@ -2277,9 +2306,8 @@ data TcSEnv -- See also Note [Tracking redundant constraints] in TcSimplify tcs_need_deriveds :: Bool - -- should we keep trying to solve even if all the unsolved - -- constraints are Derived? Usually False, but used whenever - -- toDerivedWC is used. + -- Keep solving, even if all the unsolved constraints are Derived + -- See Note [Solving for Derived constraints] } --------------- |