diff options
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 155 |
1 files changed, 94 insertions, 61 deletions
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 6c02ade8d2..d4dae8e31e 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1142,7 +1142,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds = do { -- When quantifying, we want to preserve any order of variables as they -- appear in partial signatures. cf. decideQuantifiedTyVars let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs - , (_,Bndr tv _) <- sig_inst_skols sig ] + , (_,Bndr tv _) <- sig_inst_skols sig ] psig_theta = [ pred | sig <- partial_sigs , pred <- sig_inst_theta sig ] @@ -1535,8 +1535,7 @@ decideQuantification decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates = do { -- Step 1: find the mono_tvs ; (candidates, co_vars, mono_tvs0) - <- decidePromotedTyVars infer_mode - name_taus psigs candidates + <- decidePromotedTyVars infer_mode name_taus psigs candidates -- Step 2: default any non-mono tyvars, and re-simplify -- This step may do some unification, but result candidates is zonked @@ -1736,7 +1735,7 @@ decidePromotedTyVars infer_mode name_taus psigs candidates -- by some variable that is free in the env't mono_tvs = (mono_tvs2 `unionVarSet` constrained_tvs) - `delVarSetList` psig_qtvs + `delVarSetList` psig_qtvs -- (`delVarSetList` psig_qtvs): if the user has explicitly -- asked for quantification, then that request "wins" -- over the MR. @@ -1755,6 +1754,8 @@ decidePromotedTyVars infer_mode name_taus psigs candidates ; traceTc "decidePromotedTyVars" $ vcat [ text "infer_mode =" <+> ppr infer_mode + , text "psigs =" <+> ppr psigs + , text "psig_qtvs =" <+> ppr psig_qtvs , text "mono_tvs0 =" <+> ppr mono_tvs0 , text "no_quant =" <+> ppr no_quant , text "maybe_quant =" <+> ppr maybe_quant @@ -1876,7 +1877,8 @@ decideQuantifiedTyVars skol_info name_taus psigs candidates -- See Note [pickQuantifiablePreds] pickQuantifiablePreds :: TyVarSet -- Quantifying over these - -> TcTyVarSet -- These ones are free in the enviroment + -> TcTyVarSet -- mono_tvs0: variables mentioned a candidate + -- constraint that come from some outer level -> TcThetaType -- Proposed constraints to quantify -> TcM TcThetaType -- A subset that we can actually quantify -- This function decides whether a particular constraint should be @@ -1888,9 +1890,9 @@ pickQuantifiablePreds qtvs mono_tvs0 theta mapMaybe (pick_me is_nested) theta) } where pick_me is_nested pred - | let pred_tvs = tyCoVarsOfType pred + = let pred_tvs = tyCoVarsOfType pred mentions_qtvs = pred_tvs `intersectsVarSet` qtvs - = case classifyPredType pred of + in case classifyPredType pred of ClassPred cls tys | Just {} <- isCallStackPred cls tys @@ -2141,15 +2143,16 @@ Definitely not. Since we're not quantifying over beta, it has been promoted; and then will be zapped to Any in the final zonk. So we end up with a (perhaps exported) type involving forall a. Zork a (Z [Char]) Any => blah -No no no. We never want to show the programmer a type with `Any` in it. +No no no: + + Key principle: we never want to show the programmer + a type with `Any` in it. What we really want (to catch the Zork example) is this: -Hence, for a top-level binding, we eliminate the candidate from the -pool, by asking - Do not quantify over the constraint if it mentions a variable that is - (a) not quantified (i.e. is determined by the type environment), but - (b) do not appear literally in the environment (mono_tvs0)? + Quantify over the constraint only if all its free variables are + (a) quantified, or + (b) appears in the type of something in the environment (mono_tvs0). To understand (b) consider @@ -2163,14 +2166,24 @@ In `f1` should we quantify over that `(C b alpha)`? Answer: since `alpha` is free in the type envt, yes we should. After all, if we'd typechecked `intify` first, we'd have set `alpha := Int`, and /then/ we'd certainly quantify. The delicate Zork situation applies when beta is completely -unconstrained -- except by the fudep. - -However this subtle reasoning is needed only for /top-level/ declarations. -For /nested/ decls we can see all the calls, so we'll instantiate that -quantifed `Zork a (Z [Char]) beta` constraint at call sites, and either solve -it or not (probably not). We won't be left with a still-callable function -with Any in its type. So for nested definitions we don't make this tricky -test. +unconstrained (not free in the environment) -- except by the fundep. + +Another way to put it: let's say `alpha` is in `mono_tvs0`. It must be that +some variable `x` has `alpha` free in its type. If we are at top-level (and we +are, because nested decls don't go through this path all), then `x` must also +be at top-level. And, by induction, `x` will not have Any in its type when all +is said and done. The induction is well-founded because, if `x` is mutually +recursive with the definition at hand, then their constraints get processed +together (or `x` has a type signature, in which case the type doesn't have +`Any`). So the key thing is that we must not introduce a new top-level +unconstrained variable here. + +However this regrettably-subtle reasoning is needed only for /top-level/ +declarations. For /nested/ decls we can see all the calls, so we'll +instantiate that quantifed `Zork a (Z [Char]) beta` constraint at call sites, +and either solve it or not (probably not). We won't be left with a +still-callable function with Any in its type. So for nested definitions we +don't make this tricky test. Historical note: we had a different, and more complicated test before, but it was utterly wrong: #23199. @@ -3187,32 +3200,41 @@ defaultTyVarTcS the_tv | otherwise = return False -- the common case -approximateWC :: Bool -> WantedConstraints -> Cts +approximateWC :: Bool -- See Wrinkle (W3) in Note [ApproximateWC] + -> WantedConstraints + -> Cts -- Second return value is the depleted wc --- Third return value is YesFDsCombined <=> multiple constraints for the same fundep floated -- Postcondition: Wanted Cts -- See Note [ApproximateWC] -- See Note [floatKindEqualities vs approximateWC] approximateWC float_past_equalities wc - = float_wc emptyVarSet wc + = float_wc False emptyVarSet wc where - float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts - float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) - = filterBag (is_floatable trapping_tvs) simples `unionBags` - concatMapBag (float_implic trapping_tvs) implics - float_implic :: TcTyCoVarSet -> Implication -> Cts - float_implic trapping_tvs imp - | float_past_equalities || ic_given_eqs imp /= MaybeGivenEqs - = float_wc new_trapping_tvs (ic_wanted imp) - | otherwise -- Take care with equalities - = emptyCts -- See (1) under Note [ApproximateWC] + float_wc :: Bool -- True <=> there are enclosing equalities + -> TcTyCoVarSet -- Enclosing skolem binders + -> WantedConstraints -> Cts + float_wc encl_eqs trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) + = filterBag (is_floatable encl_eqs trapping_tvs) simples `unionBags` + concatMapBag (float_implic encl_eqs trapping_tvs) implics + + float_implic :: Bool -> TcTyCoVarSet -> Implication -> Cts + float_implic encl_eqs trapping_tvs imp + = float_wc new_encl_eqs new_trapping_tvs (ic_wanted imp) where new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp - - is_floatable skol_tvs ct - | isGivenCt ct = False - | insolubleEqCt ct = False - | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs + new_encl_eqs = encl_eqs || ic_given_eqs imp == MaybeGivenEqs + + is_floatable encl_eqs skol_tvs ct + | isGivenCt ct = False + | insolubleEqCt ct = False + | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = False + | otherwise + = case classifyPredType (ctPred ct) of + EqPred {} -> float_past_equalities || not encl_eqs + -- See Wrinkle (W1) + ClassPred {} -> True -- See Wrinkle (W2) + IrredPred {} -> True -- ..both in Note [ApproximateWC] + ForAllPred {} -> False {- Note [ApproximateWC] ~~~~~~~~~~~~~~~~~~~~~~~ @@ -3225,28 +3247,39 @@ out from inside, if they are not captured by skolems. The same function is used when doing type-class defaulting (see the call to applyDefaultingRules) to extract constraints that might be defaulted. -There is one caveat: - -1. When inferring most-general types (in simplifyInfer), we do *not* - float anything out if the implication binds equality constraints, - because that defeats the OutsideIn story. Consider - data T a where - TInt :: T Int - MkT :: T a - - f TInt = 3::Int - - We get the implication (a ~ Int => res ~ Int), where so far we've decided - f :: T a -> res - We don't want to float (res~Int) out because then we'll infer - f :: T a -> Int - which is only on of the possible types. (GHC 7.6 accidentally *did* - float out of such implications, which meant it would happily infer - non-principal types.) - - HOWEVER (#12797) in findDefaultableGroups we are not worried about - the most-general type; and we /do/ want to float out of equalities. - Hence the boolean flag to approximateWC. +Wrinkle (W1) + When inferring most-general types (in simplifyInfer), we + do *not* float an equality constraint if the implication binds + equality constraints, because that defeats the OutsideIn story. + Consider data T a where TInt :: T Int MkT :: T a + + f TInt = 3::Int + + We get the implication (a ~ Int => res ~ Int), where so far we've decided + f :: T a -> res + We don't want to float (res~Int) out because then we'll infer + f :: T a -> Int + which is only on of the possible types. (GHC 7.6 accidentally *did* + float out of such implications, which meant it would happily infer + non-principal types.) + +Wrinkle (W2) + We do allow /class/ constraints to float, even if + the implication binds equalities. This is a subtle point: see #23224. + In principle, a class constraint might ultimately be satisfiable from + a constraint bound by an implication (see #19106 for an example of this + kind), but it's extremely obscure and I was unable to construct a + concrete example. In any case, in super-subtle cases where this might + make a difference, you would be much better advised to simply write a + type signature. + + I included IrredPred here too, for good measure. In general, + abstracting over more constraints does no harm. + +Wrinkle (W3) + In findDefaultableGroups we are not worried about the + most-general type; and we /do/ want to float out of equalities + (#12797). Hence the boolean flag to approximateWC. ------ Historical note ----------- There used to be a second caveat, driven by #8155 |