X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=adf0f780884c72a9c64caa1240ea2ed136ef7871;hb=ab241c5d6187a93acffc609bdbffdae30ff9b284;hp=2347d3785436c7b53a84dd4ed8fccc5851d598f1;hpb=2e9952b703341351298739b5d4f869fbdfc8490e;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 2347d37..adf0f78 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 @@ -210,8 +209,8 @@ Notice that ----------------------------------------- -Choosing Q -~~~~~~~~~~ +Note [Choosing which variables to quantify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Here's a good way to choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) @@ -657,40 +656,141 @@ 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 - -- Remove redundant superclasses from 'bound' - -- The 'Stop' try_me result does not do so, - -- see Note [No superclasses for Stop] + -- 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)) ; let try_me inst = ReduceMe AddSCs - ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound + red_env = mkRedEnv doc try_me [] + ; (irreds1, binds1) <- checkLoop red_env bound + + -- Note [Inference and implication constraints] + -- By putting extra_dicts first, we make them available + -- to solve the implication constraints + ; let extra_dicts = getImplicWanteds qtvs irreds1 + ; (irreds2, binds2) <- if null extra_dicts + then return (irreds1, emptyBag) + else do { extra_dicts' <- mapM cloneDict extra_dicts + ; checkLoop red_env (extra_dicts' ++ 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. + +getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst] +-- See Note [Inference and implication constraints] +-- Find the wanted constraints in implication constraints that mention the +-- quantified type variables, and are not bound by forall's in the constraint itself +-- Returns only Dicts +getImplicWanteds qtvs implics + = concatMap get implics + where + get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d] + | otherwise = [] + get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds}) + = [ d | let tv_set = mkVarSet tvs + , d <- getImplicWanteds qtvs wanteds + , not (tyVarsOfInst d `intersectsVarSet` tv_set)] +\end{code} + +Note [Inference and implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can't (or at least don't) abstract over implications. But we might +have an implication constraint (perhaps arising from a nested pattern +match) like + C a => D a +when we are now trying to quantify over 'a'. Our best approximation +is to make (D a) part of the inferred context, so we can use that to +discharge the implication. Hence getImplicWanteds. + +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) <- 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 + + ; 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 +871,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) <- innerCheckLoop loc givens wanteds + ; implic_bind <- bindIrreds loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- @@ -786,26 +885,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) <- innerCheckLoop 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 +925,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 +939,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 +951,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, @@ -861,8 +974,7 @@ makeImplicationBind loc all_tvs reft ----------------------------------------------------------- topCheckLoop :: SDoc -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) topCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds @@ -873,8 +985,7 @@ topCheckLoop doc wanteds innerCheckLoop :: InstLoc -> [Inst] -- Given -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) innerCheckLoop inst_loc givens wanteds = checkLoop env wanteds @@ -902,7 +1013,7 @@ 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 @@ -915,10 +1026,8 @@ with topCheckLooop. ----------------------------------------------------------- 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 checkLoop env wanteds = do { -- Givens are skolems, so no need to zonk them @@ -927,7 +1036,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 +1044,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 +1066,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,7 +1118,7 @@ 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 } @@ -1167,7 +1237,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 +1245,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 +1256,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 +1301,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 - (non_ips, bad_ips) = partition isClassDict 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 +1396,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} @@ -1437,7 +1514,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 } @@ -1560,6 +1637,7 @@ reduceContext env wanteds text "----", text "avails" <+> pprAvails avails, text "improved =" <+> ppr improved, + text "irreds = " <+> ppr irreds, text "----------------------" ])) @@ -1820,12 +1898,17 @@ 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 binding ; (binds, irreds) <- extractResults avails wanteds + ; traceTc (text "reduceImplication result" <+> vcat + [ ppr irreds, 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 @@ -1834,16 +1917,12 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc 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. ; 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 @@ -1876,6 +1955,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 +1985,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,7 +2008,7 @@ 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) @@ -1978,28 +2071,30 @@ extractResults (Avails _ avails) wanteds Nothing -> pprTrace "Urk: extractResults" (ppr w) $ go avails binds irreds ws - Just IsIrred -> go (add_given avails w) binds (w: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 id) + | id == w_id -> 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 - w_span = instSpan w - w_id = instToId w + 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} @@ -2032,7 +2127,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)) @@ -2043,10 +2140,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) =>