X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=d481146811530df1a152b780afc84cd045705517;hb=ead3abe7fbf33f019549a05ad9dd3cd22ef3adab;hp=cbcabe91b1fb3ba2d4116404c71d7f24fa423d4c;hpb=ea2d0a53ff4ca7e6331d09225ad84ec9c9efe6d8;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index cbcabe9..d481146 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -15,7 +15,7 @@ module TcSimplify ( tcSimplifyBracket, tcSimplifyCheckPat, tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns + bindInstsOfLocalFuns, bindIrreds, ) where #include "HsVersions.h" @@ -28,11 +28,10 @@ import Inst import TcEnv import InstEnv import TcGadt -import TcMType import TcType +import TcMType import TcIface import Var -import TyCon import Name import NameSet import Class @@ -48,6 +47,7 @@ import VarEnv import FiniteMap import Bag import Outputable +import Maybes import ListSetOps import Util import SrcLoc @@ -133,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 @@ -163,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! @@ -181,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) - - ------------------------------------------ - -Choosing Q -~~~~~~~~~~ -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 ) @@ -246,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 @@ -657,40 +629,162 @@ tcSimplifyInfer :: SDoc -> TcTyVarSet -- fv(T); type vars -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) - TcDictBinds, -- Bindings - [TcId]) -- Dict Ids that must be bound here (zonked) + -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified) + [Inst], -- Dict Ids that must be bound here (zonked) + TcDictBinds) -- Bindings -- Any free (escaping) Insts are tossed into the environment \end{code} \begin{code} -tcSimplifyInfer doc tau_tvs wanted_lie - = do { let try_me inst | isDict inst = Stop -- Dicts - | otherwise = ReduceMe NoSCs -- Lits, Methods, - -- and impliciation constraints - -- In an effort to make the inferred types simple, we try - -- to squeeze out implication constraints if we can. - -- See Note [Squashing methods] - - ; (binds1, irreds) <- checkLoop (mkRedEnv doc try_me []) wanted_lie - - ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) +tcSimplifyInfer doc tau_tvs wanted + = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars ; gbl_tvs <- tcGetGlobalTyVars - ; let preds = fdPredsOfInsts irreds + ; let preds = fdPredsOfInsts wanted' qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs - (free, bound) = partition (isFreeWhenInferring qtvs) irreds + -- 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 + + -- 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)) + ; (irreds1, binds1) <- tryHardCheckLoop doc bound - -- Remove redundant superclasses from 'bound' - -- The 'Stop' try_me result does not do so, - -- see Note [No superclasses for Stop] - ; let try_me inst = ReduceMe AddSCs - ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) 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 + + -- We can't abstract over any remaining unsolved + -- implications so instead just float them outwards. Ugh. + ; let (q_dicts, implics) = partition isDict irreds3 + ; loc <- getInstLoc (ImplicOrigin doc) + ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics - ; extendLIEs free - ; return (varSetElems qtvs, binds1 `unionBags` binds2, map instToId irreds) } + ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) } -- NB: when we are done, we might have some bindings, but -- the final qtvs might be empty. See Note [NO TYVARS] below. + +approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds) +-- Note [Inference and implication constraints] +-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by +-- - fetching any dicts inside them that are free +-- - using those dicts as cruder constraints, to solve the implications +-- - returning the extra ones too + +approximateImplications doc want_dict irreds + | null extra_dicts + = return (irreds, emptyBag) + | otherwise + = do { extra_dicts' <- mapM cloneDict extra_dicts + ; tryHardCheckLoop doc (extra_dicts' ++ irreds) } + -- By adding extra_dicts', we make them + -- available to solve the implication constraints + where + extra_dicts = get_dicts (filter isImplicInst irreds) + + get_dicts :: [Inst] -> [Inst] -- Returns only Dicts + -- Find the wanted constraints in implication constraints that satisfy + -- want_dict, and are not bound by forall's in the constraint itself + get_dicts ds = concatMap get_dict ds + + get_dict d@(Dict {}) | want_dict d = [d] + | otherwise = [] + get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds}) + = [ d | let tv_set = mkVarSet tvs + , d <- get_dicts wanteds + , not (tyVarsOfInst d `intersectsVarSet` tv_set)] + get_dict other = pprPanic "approximateImplications" (ppr other) +\end{code} + +Note [Inference and implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have a wanted implication constraint (perhaps arising from +a nested pattern match) like + C a => D [a] +and we are now trying to quantify over 'a' when inferring the type for +a function. In principle it's possible that there might be an instance + instance (C a, E a) => D [a] +so the context (E a) would suffice. The Right Thing is to abstract over +the implication constraint, but we don't do that (a) because it'll be +surprising to programmers and (b) because we don't have the machinery to deal +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 get_dictsin approximateImplications. + +The common cases are more clear-cut, when we have things like + forall a. C a => C b +Here, abstracting over (C b) is not an approximation at all -- but see +Note [Freeness and implications]. + +See Trac #1430 and test tc228. + + +\begin{code} +----------------------------------------------------------- +-- tcSimplifyInferCheck is used when we know the constraints we are to simplify +-- against, but we don't know the type variables over which we are going to quantify. +-- This happens when we have a type signature for a mutually recursive group +tcSimplifyInferCheck + :: InstLoc + -> TcTyVarSet -- fv(T) + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM ([TyVar], -- Fully zonked, and quantified + TcDictBinds) -- Bindings + +tcSimplifyInferCheck loc tau_tvs givens wanteds + = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + + -- Figure out which type variables to quantify over + -- You might think it should just be the signature tyvars, + -- but in bizarre cases you can get extra ones + -- f :: forall a. Num a => a -> a + -- f x = fst (g (x, head [])) + 1 + -- g a b = (b,a) + -- Here we infer g :: forall a b. a -> b -> (b,a) + -- We don't want g to be monomorphic in b just because + -- f isn't quantified over b. + ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) + ; all_tvs <- zonkTcTyVarsAndFV all_tvs + ; gbl_tvs <- tcGetGlobalTyVars + ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) + -- We could close gbl_tvs, but its not necessary for + -- soundness, and it'll only affect which tyvars, not which + -- dictionaries, we quantify over + + ; qtvs' <- zonkQuantifiedTyVars qtvs + + -- Now we are back to normal (c.f. tcSimplCheck) + ; implic_bind <- bindIrreds loc qtvs' givens irreds + + ; return (qtvs', binds `unionBags` implic_bind) } \end{code} Note [Squashing methods] @@ -771,10 +865,9 @@ tcSimplifyCheck :: InstLoc -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheck loc qtvs givens wanteds - = ASSERT( all isSkolemTyVar qtvs ) - do { (binds, irreds) <- innerCheckLoop loc givens wanteds - ; implic_bind <- bindIrreds loc [] emptyRefinement - qtvs givens irreds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + ; implic_bind <- bindIrreds loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- @@ -786,26 +879,37 @@ tcSimplifyCheckPat :: InstLoc -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds - = ASSERT( all isSkolemTyVar qtvs ) - do { (binds, irreds) <- innerCheckLoop loc givens wanteds - ; implic_bind <- bindIrreds loc co_vars reft - qtvs givens irreds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + ; implic_bind <- bindIrredsR loc qtvs co_vars reft + givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- -bindIrreds :: InstLoc -> [CoVar] -> Refinement - -> [TcTyVar] -> [Inst] -> [Inst] - -> TcM TcDictBinds +bindIrreds :: InstLoc -> [TcTyVar] + -> [Inst] -> [Inst] + -> TcM TcDictBinds +bindIrreds loc qtvs givens irreds + = bindIrredsR loc qtvs [] emptyRefinement givens irreds + +bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] + -> Refinement -> [Inst] -> [Inst] + -> TcM TcDictBinds -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE -bindIrreds loc co_vars reft qtvs givens irreds +bindIrredsR loc qtvs co_vars reft givens irreds + | null irreds + = return emptyBag + | otherwise = do { let givens' = filter isDict givens -- The givens can include methods + -- See Note [Pruning the givens in an implication constraint] - -- If there are no 'givens', then it's safe to + -- If there are no 'givens' *and* the refinement is empty + -- (the refinement is like more givens), then it's safe to -- partition the 'wanteds' by their qtvs, thereby trimming irreds -- See Note [Freeness and implications] - ; irreds' <- if null givens' + ; irreds' <- if null givens' && isEmptyRefinement reft then do { let qtv_set = mkVarSet qtvs (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds @@ -815,7 +919,8 @@ bindIrreds loc co_vars reft qtvs givens irreds ; let all_tvs = qtvs ++ co_vars -- Abstract over all these ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds' - -- This call does the real work + -- This call does the real work + -- If irreds' is empty, it does something sensible ; extendLIEs implics ; return bind } @@ -828,6 +933,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- The binding looks like -- (ir1, .., irn) = f qtvs givens -- where f is (evidence for) the new implication constraint +-- f :: forall qtvs. {reft} givens => (ir1, .., irn) +-- qtvs includes coercion variables -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs reft @@ -838,7 +945,7 @@ makeImplicationBind loc all_tvs reft | otherwise -- Otherwise we must generate a binding = do { uniq <- newUnique ; span <- getSrcSpanM - ; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span) + ; let name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs, tci_given = givens, @@ -859,24 +966,23 @@ makeImplicationBind loc all_tvs reft return ([implic_inst], unitBag (L span bind)) } ----------------------------------------------------------- -topCheckLoop :: SDoc +tryHardCheckLoop :: SDoc -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) -topCheckLoop doc wanteds +tryHardCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds where try_me inst = ReduceMe AddSCs + -- Here's the try-hard bit ----------------------------------------------------------- -innerCheckLoop :: InstLoc +gentleCheckLoop :: InstLoc -> [Inst] -- Given -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) -innerCheckLoop inst_loc givens wanteds +gentleCheckLoop inst_loc givens wanteds = checkLoop env wanteds where env = mkRedEnv (pprInstLoc inst_loc) try_me givens @@ -902,23 +1008,22 @@ Inside the pattern match, which binds (a:*, x:a), we know that Hence we have a dictionary for Show [a] available; and indeed we need it. We are going to build an implication contraint forall a. (b~[a]) => Show [a] -Later, we will solve this constraint using the knowledge (Show b) +Later, we will solve this constraint using the knowledg e(Show b) But we MUST NOT reduce (Show [a]) to (Show a), else the whole thing becomes insoluble. So we simplify gently (get rid of literals and methods only, plus common up equal things), deferring the real work until top level, when we solve the implication constraint -with topCheckLooop. +with tryHardCheckLooop. \begin{code} ----------------------------------------------------------- checkLoop :: RedEnv -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible --- Precondition: the try_me never returns Free --- givens are completely rigid + -> TcM ([Inst], TcDictBinds) +-- Precondition: givens are completely rigid +-- Postcondition: returned Insts are zonked checkLoop env wanteds = do { -- Givens are skolems, so no need to zonk them @@ -927,7 +1032,7 @@ checkLoop env wanteds ; (improved, binds, irreds) <- reduceContext env wanteds' ; if not improved then - return (binds, irreds) + return (irreds, binds) else do -- If improvement did some unification, we go round again. @@ -935,8 +1040,8 @@ checkLoop env wanteds -- Using an instance decl might have introduced a fresh type variable -- which might have been unified, so we'd get an infinite loop -- if we started again with wanteds! See Note [LOOP] - { (binds1, irreds1) <- checkLoop env irreds - ; return (binds `unionBags` binds1, irreds1) } } + { (irreds1, binds1) <- checkLoop env irreds + ; return (irreds1, binds `unionBags` binds1) } } \end{code} Note [LOOP] @@ -957,45 +1062,6 @@ on both the Lte and If constraints. What we *can't* do is start again with (Max Z (S x) y)! -\begin{code} ------------------------------------------------------------ --- tcSimplifyInferCheck is used when we know the constraints we are to simplify --- against, but we don't know the type variables over which we are going to quantify. --- This happens when we have a type signature for a mutually recursive group -tcSimplifyInferCheck - :: InstLoc - -> TcTyVarSet -- fv(T) - -> [Inst] -- Given - -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Variables over which to quantify - TcDictBinds) -- Bindings - -tcSimplifyInferCheck loc tau_tvs givens wanteds - = do { (binds, irreds) <- innerCheckLoop loc givens wanteds - - -- Figure out which type variables to quantify over - -- You might think it should just be the signature tyvars, - -- but in bizarre cases you can get extra ones - -- f :: forall a. Num a => a -> a - -- f x = fst (g (x, head [])) + 1 - -- g a b = (b,a) - -- Here we infer g :: forall a b. a -> b -> (b,a) - -- We don't want g to be monomorphic in b just because - -- f isn't quantified over b. - ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) - ; all_tvs <- zonkTcTyVarsAndFV all_tvs - ; gbl_tvs <- tcGetGlobalTyVars - ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) - -- We could close gbl_tvs, but its not necessary for - -- soundness, and it'll only affect which tyvars, not which - -- dictionaries, we quantify over - - -- Now we are back to normal (c.f. tcSimplCheck) - ; implic_bind <- bindIrreds loc [] emptyRefinement - qtvs givens irreds - ; return (qtvs, binds `unionBags` implic_bind) } -\end{code} - %************************************************************************ %* * @@ -1048,14 +1114,14 @@ tcSimplifySuperClasses -> [Inst] -- Wanted -> TcM TcDictBinds tcSimplifySuperClasses loc givens sc_wanteds - = do { (binds1, irreds) <- checkLoop env sc_wanteds + = do { (irreds, binds1) <- checkLoop env sc_wanteds ; let (tidy_env, tidy_irreds) = tidyInsts irreds ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds ; return binds1 } where env = mkRedEnv (pprInstLoc loc) try_me givens try_me inst = ReduceMe NoSCs - -- Like topCheckLoop, but with NoSCs + -- Like tryHardCheckLoop, but with NoSCs \end{code} @@ -1167,7 +1233,7 @@ tcSimplifyRestricted -- Used for restricted binding groups -> [Name] -- Things bound in this group -> TcTyVarSet -- Free in the type of the RHSs -> [Inst] -- Free in the RHSs - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) + -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified) TcDictBinds) -- Bindings -- tcSimpifyRestricted returns no constraints to -- quantify over; by definition there are none. @@ -1175,7 +1241,7 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight - = mappM zonkInst wanteds `thenM` \ wanteds' -> + = do { wanteds' <- mappM zonkInst wanteds -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type @@ -1186,23 +1252,34 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- BUT do no improvement! See Plan D above -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint - let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) - in - reduceContext env wanteds' `thenM` \ (_imp, _binds, constrained_dicts) -> + ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over - zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' -> - tcGetGlobalTyVars `thenM` \ gbl_tvs' -> - mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' -> - let - constrained_tvs' = tyVarsOfInsts constrained_dicts' - qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs') - `minusVarSet` constrained_tvs' - in - traceTc (text "tcSimplifyRestricted" <+> vcat [ + ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; gbl_tvs' <- tcGetGlobalTyVars + ; constrained_dicts' <- mappM zonkInst constrained_dicts + + ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs' + -- As in tcSimplifyInfer + + -- Do not quantify over constrained type variables: + -- this is the monomorphism restriction + constrained_tvs' = tyVarsOfInsts constrained_dicts' + qtvs = qtvs1 `minusVarSet` constrained_tvs' + pp_bndrs = pprWithCommas (quotes . ppr) bndrs + + -- Warn in the mono + ; warn_mono <- doptM Opt_WarnMonomorphism + ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1)) + (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding") + <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs, + ptext SLIT("Consider giving a type signature for") <+> pp_bndrs]) + + ; traceTc (text "tcSimplifyRestricted" <+> vcat [ pprInsts wanteds, pprInsts constrained_dicts', ppr _binds, - ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) `thenM_` + ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact @@ -1220,27 +1297,23 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- -- At top level, we *do* squash methods becuase we want to -- expose implicit parameters to the test that follows - let - is_nested_group = isNotTopLevel top_lvl - try_me inst | isFreeWrtTyVars qtvs inst, - (is_nested_group || isDict inst) = Stop - | otherwise = ReduceMe AddSCs - env = mkNoImproveRedEnv doc try_me - in - reduceContext env wanteds' `thenM` \ (_imp, binds, irreds) -> - ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured + ; let is_nested_group = isNotTopLevel top_lvl + try_me inst | isFreeWrtTyVars qtvs inst, + (is_nested_group || isDict inst) = Stop + | otherwise = ReduceMe AddSCs + env = mkNoImproveRedEnv doc try_me + ; (_imp, binds, irreds) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" - if is_nested_group then - extendLIEs irreds `thenM_` - returnM (varSetElems qtvs, binds) - else - let - (bad_ips, non_ips) = partition isIPDict irreds - in - addTopIPErrs bndrs bad_ips `thenM_` - extendLIEs non_ips `thenM_` - returnM (varSetElems qtvs, binds) + ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured + if is_nested_group then + extendLIEs irreds + else do { let (bad_ips, non_ips) = partition isIPDict irreds + ; addTopIPErrs bndrs bad_ips + ; extendLIEs non_ips } + + ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) + ; return (qtvs', binds) } \end{code} @@ -1319,7 +1392,7 @@ tcSimplifyRuleLhs wanteds -- to fromInteger; this looks fragile to me ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws) + GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws) NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) } \end{code} @@ -1334,7 +1407,7 @@ this bracket again at its usage site. \begin{code} tcSimplifyBracket :: [Inst] -> TcM () tcSimplifyBracket wanteds - = do { topCheckLoop doc wanteds + = do { tryHardCheckLoop doc wanteds ; return () } where doc = text "tcSimplifyBracket" @@ -1437,7 +1510,7 @@ bindInstsOfLocalFuns wanteds local_ids returnM emptyLHsBinds | otherwise - = do { (binds, irreds) <- checkLoop env for_me + = do { (irreds, binds) <- checkLoop env for_me ; extendLIEs not_for_me ; extendLIEs irreds ; return binds } @@ -1547,7 +1620,11 @@ reduceContext env wanteds ; init_state <- foldlM addGiven emptyAvails (red_givens env) -- Do the real work - ; avails <- reduceList env wanteds init_state + -- Process non-implication constraints first, so that they are + -- available to help solving the implication constraints + -- ToDo: seems a bit inefficient and ad-hoc + ; let (implics, rest) = partition isImplicInst wanteds + ; avails <- reduceList env (rest ++ implics) init_state ; let improved = availsImproved avails ; (binds, irreds) <- extractResults avails wanteds @@ -1560,6 +1637,7 @@ reduceContext env wanteds text "----", text "avails" <+> pprAvails avails, text "improved =" <+> ppr improved, + text "irreds = " <+> ppr irreds, text "----------------------" ])) @@ -1820,37 +1898,65 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc , red_try_me = try_me } ; traceTc (text "reduceImplication" <+> vcat - [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ]) + [ ppr orig_avails, + ppr (red_givens env), ppr extra_givens, + ppr reft, ppr wanteds, ppr avails ]) ; avails <- reduceList env' wanteds avails - -- Extract the binding (no frees, because try_me never says Free) + -- 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 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 - -- This binding is useless if the recursive simplification - -- made no progress; but currently we don't try to optimise that - -- case. After all, we only try hard to reduce at top level, or - -- when inferring types. + { (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) rhs = mkHsWrap co payload loc = instLocSpan inst_loc - payload | isSingleton wanteds = HsVar (instToId (head wanteds)) + 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 @@ -1876,6 +1982,20 @@ We can satisfy the (C Int) from the superclass of D, so we don't want to float the (C Int) out, even though it mentions no type variable in the constraints! +Note [Pruning the givens in an implication constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to form the implication constraint + forall tvs. Eq a => Ord b +The (Eq a) cannot contribute to the (Ord b), because it has no access to +the type variable 'b'. So we could filter out the (Eq a) from the givens. + +Doing so would be a bit tidier, but all the implication constraints get +simplified away by the optimiser, so it's no great win. So I don't take +advantage of that at the moment. + +If you do, BE CAREFUL of wobbly type variables. + + %************************************************************************ %* * Avails and AvailHow: the pool of evidence @@ -1892,7 +2012,7 @@ type ImprovementDone = Bool -- True <=> some unification has happened type AvailEnv = FiniteMap Inst AvailHow data AvailHow - = IsIrred -- Used for irreducible dictionaries, + = IsIrred TcId -- Used for irreducible dictionaries, -- which are going to be lambda bound | Given TcId -- Used for dictionaries for which we have a binding @@ -1915,9 +2035,9 @@ instance Outputable AvailHow where ------------------------- pprAvail :: AvailHow -> SDoc -pprAvail IsIrred = text "Irred" +pprAvail (IsIrred x) = text "Irred" <+> ppr x 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 @@ -1975,28 +2095,32 @@ 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 - - Just IsIrred -> go (add_given avails w) binds (w:irreds) ws + Nothing -> pprTrace "Urk: extractResults" (ppr w) $ + go avails binds irreds ws Just (Given id) - | id == instToId w - -> go avails binds irreds ws + | id == w_id -> go avails binds irreds ws + | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws -- 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! - | otherwise - -> go avails (addBind binds w (nlHsVar id)) irreds ws + Just (IsIrred _) -> go (add_given avails w) binds (w:irreds) ws + -- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) 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 + -- test tcfail043 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws) - where - new_binds = addBind binds w rhs + where + new_binds = addBind binds w_id rhs + where + w_id = instToId w add_given avails w = extendAvailEnv avails w (Given (instToId w)) + -- Don't add the same binding twice -addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst) - (VarBind (instToId inst) rhs)) +addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs)) \end{code} @@ -2029,7 +2153,9 @@ addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails addRefinedGiven reft (refined_givens, avails) given | isDict given -- We sometimes have 'given' methods, but they -- are always optional, so we can drop them - , Just (co, pred) <- refinePred reft (dictPred given) + , let pred = dictPred given + , isRefineablePred pred -- See Note [ImplicInst rigidity] + , Just (co, pred) <- refinePred reft pred = do { new_given <- newDictBndr (instLoc given) pred ; let rhs = L (instSpan given) $ HsWrap (WpCo co) (HsVar (instToId given)) @@ -2040,10 +2166,33 @@ addRefinedGiven reft (refined_givens, avails) given -- and hopefully the optimiser will spot the duplicated work | otherwise = return (refined_givens, avails) +\end{code} + +Note [ImplicInst rigidity] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + C :: forall ab. (Eq a, Ord b) => b -> T a + + ...(case x of C v ->
)... + +From the case (where x::T ty) we'll get an implication constraint + forall b. (Eq ty, Ord b) =>