X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=f87b04426e86dd2e439590a2dd01fae155123a17;hb=b99310f05faee2abec850da4349fcd5c0498f7ca;hp=db1201131b761bf022568cf5dd32446e4fa83b58;hpb=0f5731ee92009fe43e9cc0bd276b4562e0c37089;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index db12011..f87b044 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -47,6 +47,7 @@ import VarEnv import FiniteMap import Bag import Outputable +import Maybes import ListSetOps import Util import SrcLoc @@ -637,47 +638,68 @@ tcSimplifyInfer \begin{code} tcSimplifyInfer doc tau_tvs wanted - = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) - ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars + = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars ; gbl_tvs <- tcGetGlobalTyVars - ; let preds = fdPredsOfInsts wanted' - qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs + ; let preds1 = fdPredsOfInsts wanted' + gbl_tvs1 = oclose preds1 gbl_tvs + qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1 -- See Note [Choosing which variables to quantify] -- To maximise sharing, remove from consideration any -- constraints that don't mention qtvs at all - ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted' - ; extendLIEs free1 + ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted' + ; extendLIEs free -- To make types simple, reduce as much as possible - ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ - ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound)) + ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ + ppr gbl_tvs1 $$ ppr free $$ ppr bound)) ; (irreds1, binds1) <- tryHardCheckLoop doc bound -- Note [Inference and implication constraints] ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1 - -- By now improvment may have taken place, and we must *not* - -- quantify over any variable free in the environment - -- tc137 (function h inside g) is an example - ; gbl_tvs <- tcGetGlobalTyVars - ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs) - ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs)) - - -- Do not quantify over constraints that *now* do not - -- mention quantified type variables, because they are - -- simply ambiguous (or might be bound further out). Example: - -- f :: Eq b => a -> (a, b) - -- g x = fst (f x) - -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta) - -- We decide to quantify over 'alpha' alone, but free1 does not include f77 - -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous) - -- constraint (Eq beta), which we dump back into the free set - -- See test tcfail181 - ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2 - ; extendLIEs free3 - + -- Now work out all over again which type variables to quantify, + -- exactly in the same way as before, but starting from irreds2. Why? + -- a) By now improvment may have taken place, and we must *not* + -- quantify over any variable free in the environment + -- tc137 (function h inside g) is an example + -- + -- b) Do not quantify over constraints that *now* do not + -- mention quantified type variables, because they are + -- simply ambiguous (or might be bound further out). Example: + -- f :: Eq b => a -> (a, b) + -- g x = fst (f x) + -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta) + -- We decide to quantify over 'alpha' alone, but free1 does not include f77 + -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous) + -- constraint (Eq beta), which we dump back into the free set + -- See test tcfail181 + -- + -- c) irreds may contain type variables not previously mentioned, + -- e.g. instance D a x => Foo [a] + -- wanteds = Foo [a] + -- Then after simplifying we'll get (D a x), and x is fresh + -- We must quantify over x else it'll be totally unbound + ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1) + ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1) + -- Note that we start from gbl_tvs1 + -- We use tcGetGlobalTyVars, then oclose wrt preds2, because + -- we've already put some of the original preds1 into frees + -- E.g. wanteds = C a b (where a->b) + -- gbl_tvs = {a} + -- tau_tvs = {b} + -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and + -- irreds2 will be empty. But we don't want to generalise over b! + ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked + qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2 + ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2 + ; extendLIEs free + + -- Turn the quantified meta-type variables into real type variables + ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs) + -- We can't abstract over any remaining unsolved -- implications so instead just float them outwards. Ugh. ; let (q_dicts, implics) = partition isDict irreds3 @@ -735,7 +757,7 @@ with 'given' implications. So our best approximation is to make (D [a]) part of the inferred context, so we can use that to discharge the implication. Hence -the strange function getImplicWanteds. +the strange function get_dictsin approximateImplications. The common cases are more clear-cut, when we have things like forall a. C a => C b @@ -1902,20 +1924,22 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc ppr reft, ppr wanteds, ppr avails ]) ; avails <- reduceList env' wanteds avails - -- Extract the binding + -- Extract the results + -- Note [Reducing implication constraints] ; (binds, irreds) <- extractResults avails wanteds - + ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds + ; traceTc (text "reduceImplication result" <+> vcat - [ ppr irreds, ppr binds]) + [ ppr outer, ppr inner, ppr binds]) -- We always discard the extra avails we've generated; -- but we remember if we have done any (global) improvement ; let ret_avails = updateImprovement orig_avails avails - ; if isEmptyLHsBinds binds then -- No progress + ; if isEmptyLHsBinds binds && null outer then -- No progress return (ret_avails, NoInstance) else do - { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds + { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner ; let dict_ids = map instToId extra_givens co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) @@ -1924,11 +1948,36 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc payload | [wanted] <- wanteds = HsVar (instToId wanted) | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed - -- If there are any irreds, we back off and return NoInstance - ; return (ret_avails, GenInst implic_insts (L loc rhs)) + ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs)) } } \end{code} +Note [Reducing implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are trying to simplify + (Ord a, forall b. C a b => (W [a] b, D c b)) +where + instance (C a b, Ord a) => W [a] b +When solving the implication constraint, we'll start with + Ord a -> Irred +in the Avails. Then we add (C a b -> Given) and solve. Extracting +the results gives us a binding for the (W [a] b), with an Irred of +(Ord a, D c b). Now, the (Ord a) comes from "outside" the implication, +but the (D d b) is from "inside". So we want to generate a Rhs binding +like this + + ic = /\b \dc:C a b). (df a b dc do, ic' b dc) + depending on + do :: Ord a + ic' :: forall b. C a b => D c b + +The 'depending on' part of the Rhs is important, because it drives +the extractResults code. + +The "inside" and "outside" distinction is what's going on with 'inner' and +'outer' in reduceImplication + + Note [Freeness and implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's hard to say when an implication constraint can be floated out. Consider @@ -1984,7 +2033,7 @@ type ImprovementDone = Bool -- True <=> some unification has happened type AvailEnv = FiniteMap Inst AvailHow data AvailHow - = IsIrred TcId -- Used for irreducible dictionaries, + = IsIrred -- Used for irreducible dictionaries, -- which are going to be lambda bound | Given TcId -- Used for dictionaries for which we have a binding @@ -2007,9 +2056,9 @@ instance Outputable AvailHow where ------------------------- pprAvail :: AvailHow -> SDoc -pprAvail (IsIrred x) = text "Irred" <+> ppr x +pprAvail IsIrred = text "Irred" pprAvail (Given x) = text "Given" <+> ppr x -pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs) +pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)] ------------------------- extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv @@ -2067,8 +2116,8 @@ extractResults (Avails _ avails) wanteds go avails binds irreds (w:ws) = case findAvailEnv avails w of - Nothing -> pprTrace "Urk: extractResults" (ppr w) $ - go avails binds irreds ws + Nothing -> pprTrace "Urk: extractResults" (ppr w) $ + go avails binds irreds ws Just (Given id) | id == w_id -> go avails binds irreds ws @@ -2076,9 +2125,7 @@ extractResults (Avails _ avails) wanteds -- The sought Id can be one of the givens, via a superclass chain -- and then we definitely don't want to generate an x=x binding! - Just (IsIrred id) - | id == w_id -> go (add_given avails w) binds (w:irreds) ws - | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws + Just IsIrred -> go (add_given avails w) binds (w:irreds) ws -- The add_given handles the case where we want (Ord a, Eq a), and we -- don't want to emit *two* Irreds for Ord a, one via the superclass chain -- This showed up in a dupliated Ord constraint in the error message for @@ -2165,7 +2212,7 @@ than with the Avails handling stuff in TcSimplify \begin{code} addIrred :: WantSCs -> Avails -> Inst -> TcM Avails addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails ) - addAvailAndSCs want_scs avails irred (IsIrred (instToId irred)) + addAvailAndSCs want_scs avails irred IsIrred addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails addAvailAndSCs want_scs avails inst avail @@ -2330,14 +2377,14 @@ disambiguate doc interactive dflags insts = return (insts, emptyBag) | null defaultable_groups - = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups]) + = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups]) ; return (insts, emptyBag) } | otherwise = do { -- Figure out what default types to use default_tys <- getDefaultTys extended_defaulting ovl_strings - ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups]) + ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups]) ; mapM_ (disambigGroup default_tys) defaultable_groups -- disambigGroup does unification, hence try again @@ -2701,7 +2748,7 @@ report_no_instances tidy_env mb_what insts parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+> quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"), - ptext SLIT("when compiling the other instances")])] + ptext SLIT("when compiling the other instance declarations")])] where ispecs = [ispec | (ispec, _) <- matches]