X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=c22973316496787112e30ad3f4abaf4a69b96823;hb=b47302cbee70802076638ee58fe1c00853eae10a;hp=773b312cc428ec5ecd557e46850669c0d073d753;hpb=884b0a57dde7b1d9556a4c47f6a14a11d39c3c64;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 773b312..c229733 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 @@ -132,14 +133,9 @@ from. The Right Thing is to improve whenever the constraint set changes at all. Not hard in principle, but it'll take a bit of fiddling to do. - - - -------------------------------------- - Notes on quantification - -------------------------------------- - -Suppose we are about to do a generalisation step. -We have in our hand +Note [Choosing which variables to quantify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to do a generalisation step. We have in our hand G the environment T the type of the RHS @@ -162,11 +158,12 @@ Here are the things that *must* be true: (A) Q intersect fv(G) = EMPTY limits how big Q can be (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be -(A) says we can't quantify over a variable that's free in the -environment. (B) says we must quantify over all the truly free -variables in T, else we won't get a sufficiently general type. We do -not *need* to quantify over any variable that is fixed by the free -vars of the environment G. + (A) says we can't quantify over a variable that's free in the environment. + (B) says we must quantify over all the truly free variables in T, else + we won't get a sufficiently general type. + +We do not *need* to quantify over any variable that is fixed by the +free vars of the environment G. BETWEEN THESE TWO BOUNDS, ANY Q WILL DO! @@ -180,38 +177,15 @@ Example: class H x y | x->y where ... So Q can be {c,d}, {b,c,d} +In particular, it's perfectly OK to quantify over more type variables +than strictly necessary; there is no need to quantify over 'b', since +it is determined by 'a' which is free in the envt, but it's perfectly +OK to do so. However we must not quantify over 'a' itself. + Other things being equal, however, we'd like to quantify over as few variables as possible: smaller types, fewer type applications, more -constraints can get into Ct instead of Cq. - - ------------------------------------------ -We will make use of - - fv(T) the free type vars of T - - oclose(vs,C) The result of extending the set of tyvars vs - using the functional dependencies from C - - grow(vs,C) The result of extend the set of tyvars vs - using all conceivable links from C. - - E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e} - Then grow(vs,C) = {a,b,c} - - Note that grow(vs,C) `superset` grow(vs,simplify(C)) - That is, simplfication can only shrink the result of grow. - -Notice that - oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs - grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C) - - ------------------------------------------ - -Note [Choosing which variables to quantify] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Here's a good way to choose Q: +constraints can get into Ct instead of Cq. Here's a good way to +choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) @@ -245,9 +219,8 @@ all the functional dependencies yet: T = c->c C = (Eq (T c d)) - Now oclose(fv(T),C) = {c}, because the functional dependency isn't - apparent yet, and that's wrong. We must really quantify over d too. - +Now oclose(fv(T),C) = {c}, because the functional dependency isn't +apparent yet, and that's wrong. We must really quantify over d too. There really isn't any point in quantifying over any more than grow( fv(T), C ), because the call sites can't possibly influence @@ -763,7 +736,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 @@ -1930,20 +1903,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) @@ -1952,11 +1927,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 @@ -2012,7 +2012,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 @@ -2035,9 +2035,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 @@ -2095,8 +2095,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 @@ -2104,9 +2104,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 @@ -2193,7 +2191,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 @@ -2358,14 +2356,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