From cfda0421ca2c7c5f762814fd25988cf89871f1d8 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Wed, 1 Oct 2008 09:13:15 +0000 Subject: [PATCH] TcSimplify.reduceImplication: clean up - This cleans up some of the mess in reduceImplication and documents the precondition on the form of wanted equalities properly. - I also made the back off test a bit smarter by allowing to back off in the presence of wanted equalities as long as none of them got solved in the attempt. (That should save generating some superfluous bindings.) MERGE TO 6.10 --- compiler/typecheck/Inst.lhs | 48 +++++-------- compiler/typecheck/TcSimplify.lhs | 133 +++++++++++++++++++++---------------- compiler/typecheck/TcTyFuns.lhs | 4 +- 3 files changed, 93 insertions(+), 92 deletions(-) diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 5ad0bed..47629db 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -40,15 +40,11 @@ module Inst ( InstOrigin(..), InstLoc, pprInstLoc, - mkWantedCo, mkGivenCo, - isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType, - mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo, - mkRightTransEqInstCo, mkAppEqInstCo, - isValidWantedEqInst, - eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, - wantedToLocalEqInst, finalizeEqInst, - eqInstType, updateEqInstCoercion, - eqInstCoercion, eqInstTys + mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo, + mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo, + wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst, + wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion, + eqInstTys ) where #include "HsVersions.h" @@ -121,8 +117,11 @@ instToVar (Dict {tci_name = nm, tci_pred = pred}) instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds}) = mkLocalId nm (mkImplicTy tvs givens wanteds) -instToVar i@(EqInst {}) - = eitherEqInst i id (\(TyVarTy covar) -> covar) +instToVar inst@(EqInst {}) + = eitherEqInst inst id assertCoVar + where + assertCoVar (TyVarTy cotv) = cotv + assertCoVar coty = pprPanic "Inst.instToVar" (ppr coty) instType :: Inst -> Type instType (LitInst {tci_ty = ty}) = ty @@ -970,15 +969,6 @@ isWantedCo :: EqInstCo -> Bool isWantedCo (Left _) = True isWantedCo _ = False -fromGivenCo :: EqInstCo -> Coercion -fromGivenCo (Right co) = co -fromGivenCo _ = panic "fromGivenCo: not a wanted coercion" - -fromWantedCo :: String -> EqInstCo -> TcTyVar -fromWantedCo _ (Left covar) = covar -fromWantedCo msg _ = - panic ("fromWantedCo: not a wanted coercion: " ++ msg) - eqInstCoType :: EqInstCo -> TcType eqInstCoType (Left cotv) = mkTyVarTy cotv eqInstCoType (Right co) = co @@ -1050,12 +1040,12 @@ mkAppEqInstCo (Right co) _ _ Operations on entire EqInst. \begin{code} --- For debugging, make sure the cotv of a wanted is not filled. +-- |A wanted equality is unsolved as long as its cotv is unfilled. -- -isValidWantedEqInst :: Inst -> TcM Bool -isValidWantedEqInst (EqInst {tci_co = Left cotv}) +wantedEqInstIsUnsolved :: Inst -> TcM Bool +wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv}) = liftM not $ isFilledMetaTyVar cotv -isValidWantedEqInst _ = return True +wantedEqInstIsUnsolved _ = return True eitherEqInst :: Inst -- given or wanted EqInst -> (TcTyVar -> a) -- result if wanted @@ -1067,9 +1057,6 @@ eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven Right co -> withGiven co eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i) -mkEqInsts :: [PredType] -> [EqInstCo] -> TcM [Inst] -mkEqInsts preds cos = zipWithM mkEqInst preds cos - mkEqInst :: PredType -> EqInstCo -> TcM Inst mkEqInst (EqPred ty1 ty2) co = do { uniq <- newUnique @@ -1112,11 +1099,11 @@ wantedToLocalEqInst eq = eq -- finalizeEqInst :: Inst -- wanted -> TcM Inst -- given -finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, tci_name = name}) +finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, + tci_name = name, tci_co = Left cotv}) = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2) -- fill the coercion hole - ; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted ; writeMetaTyVar cotv (TyVarTy var) -- set the new coercion @@ -1134,7 +1121,4 @@ eqInstCoercion = tci_co eqInstTys :: Inst -> (TcType, TcType) eqInstTys inst = (tci_left inst, tci_right inst) - -updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst -updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst} \end{code} diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 113de25..9b6fb93 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -971,17 +971,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM ([Inst], TcDictBinds) -- Make a binding that binds 'irreds', by generating an implication --- constraint for them, *and* throwing the constraint into the LIE +-- constraint for them. +-- -- 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 +-- f :: forall qtvs. givens => (ir1, .., irn) +-- qtvs includes coercion variables. -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs - givens -- Guaranteed all Dicts - -- or EqInsts + givens -- Guaranteed all Dicts or EqInsts irreds | null irreds -- If there are no irreds, we are done = return ([], emptyBag) @@ -989,28 +989,38 @@ makeImplicationBind loc all_tvs = do { uniq <- newUnique ; span <- getSrcSpanM ; let (eq_givens, dict_givens) = partition isEqInst givens - eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens) - -- Urgh! See line 2187 or thereabouts. I believe that all these - -- 'givens' must be a simple CoVar. This MUST be cleaned up. - ; let name = mkInternalName uniq (mkVarOcc "ic") span + -- extract equality binders + eq_cotvs = map eqInstType eq_givens + + -- make the implication constraint instance + name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_tyvars = all_tvs, tci_given = (eq_givens ++ dict_givens), - tci_wanted = irreds, tci_loc = loc } - ; let -- only create binder for dict_irreds - (_, dict_irreds) = partition isEqInst irreds + -- same order as binders + tci_wanted = irreds, + tci_loc = loc } + + -- create binders for the irreducible dictionaries + dict_irreds = filter (not . isEqInst) irreds dict_irred_ids = map instToId dict_irreds lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids) - rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) - co = mkWpApps (map instToId dict_givens) - <.> mkWpTyApps eq_tyvar_cos - <.> mkWpTyApps (mkTyVarTys all_tvs) - bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs - | otherwise = PatBind { pat_lhs = lpat, - pat_rhs = unguardedGRHSs rhs, - pat_rhs_ty = hsLPatType lpat, - bind_fvs = placeHolderNames } + + -- create the binding + rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) + co = mkWpApps (map instToId dict_givens) + <.> mkWpTyApps eq_cotvs + <.> mkWpTyApps (mkTyVarTys all_tvs) + bind | [dict_irred_id] <- dict_irred_ids + = VarBind dict_irred_id rhs + | otherwise + = PatBind { pat_lhs = lpat + , pat_rhs = unguardedGRHSs rhs + , pat_rhs_ty = hsLPatType lpat + , bind_fvs = placeHolderNames + } + ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst ; return ([implic_inst], unitBag (L span bind)) } @@ -2200,19 +2210,30 @@ Note that -- -- Note on coercion variables: -- - -- The extra given coercion variables are bound at two different sites: + -- The extra given coercion variables are bound at two different + -- sites: + -- -- -) in the creation context of the implication constraint -- the solved equational constraints use these binders -- -- -) at the solving site of the implication constraint - -- the solved dictionaries use these binders + -- the solved dictionaries use these binders; -- these binders are generated by reduceImplication -- + -- Note [Binders for equalities] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- To reuse the binders of local/given equalities in the binders of + -- implication constraints, it is crucial that these given equalities + -- always have the form + -- cotv :: t1 ~ t2 + -- where cotv is a simple coercion type variable (and not a more + -- complex coercion term). We require that the extra_givens always + -- have this form and exploit the special form when generating binders. reduceImplication env orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc, tci_tyvars = tvs, tci_given = extra_givens, tci_wanted = wanteds - }) + }) = do { -- Solve the sub-problem ; let try_me _ = ReduceMe -- Note [Freeness and implications] env' = env { red_givens = extra_givens ++ red_givens env @@ -2239,15 +2260,17 @@ reduceImplication env -- SLPJ Sept 07: what if improvement happened inside the checkLoop? -- Then we must iterate the outer loop too! + ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds + -- we solve wanted eqs by side effect! + + -- Progress is no longer measered by the number of bindings + -- If there are any irreds, but no bindings and no solved + -- equalities, we back off and do nothing ; let backOff = isEmptyLHsBinds binds && -- no new bindings (not $ null irreds) && -- but still some irreds - all (not . isEqInst) wanteds - -- we may have instantiated a cotv - -- => must make a new implication constraint! + didntSolveWantedEqs -- no instantiated cotv - -- Progress is no longer measered by the number of bindings ; if backOff then -- No progress - -- If there are any irreds, we back off and do nothing return (emptyBag, [orig_implic]) else do { (simpler_implic_insts, bind) @@ -2257,35 +2280,29 @@ reduceImplication env -- case. After all, we only try hard to reduce at top level, or -- when inferring types. - ; let dict_wanteds = filter (not . isEqInst) wanteds - -- TOMDO: given equational constraints bug! - -- we need a different evidence for given - -- equations depending on whether we solve - -- dictionary constraints or equational constraints - - (extra_eq_givens, extra_dict_givens) - = partition isEqInst extra_givens - -- SLPJ Sept 07: I think this is bogus; currently - -- there are no Eqinsts in extra_givens - dict_ids = map instToId extra_dict_givens - - -- Note [Reducing implication constraints] - -- Tom -- update note, put somewhere! - ; let eq_tyvars = varSetElems $ tyVarsOfTypes $ - map eqInstType extra_eq_givens - -- SLPJ Sept07: this looks Utterly Wrong to me, but I think - -- that current extra_givens has no EqInsts, so - -- it makes no difference - co = wrap_inline -- Note [Always inline implication constraints] - <.> mkWpTyLams tvs - <.> mkWpTyLams eq_tyvars - <.> mkWpLams dict_ids - <.> WpLet (binds `unionBags` bind) - wrap_inline | null dict_ids = idHsWrapper - | otherwise = WpInline - rhs = mkLHsWrap co payload - loc = instLocSpan inst_loc - payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds) + ; let -- extract Id binders for dicts and CoTyVar binders for eqs; + -- see Note [Binders for equalities] + (extra_eq_givens, extra_dict_givens) = partition isEqInst + extra_givens + eq_cotvs = map instToVar extra_eq_givens + dict_ids = map instToId extra_dict_givens + + -- Note [Always inline implication constraints] + wrap_inline | null dict_ids = idHsWrapper + | otherwise = WpInline + co = wrap_inline + <.> mkWpTyLams tvs + <.> mkWpTyLams eq_cotvs + <.> mkWpLams dict_ids + <.> WpLet (binds `unionBags` bind) + rhs = mkLHsWrap co payload + loc = instLocSpan inst_loc + -- wanted equalities are solved by updating their + -- cotv; we don't generate bindings for them + dict_bndrs = map (L loc . HsVar . instToId) + . filter (not . isEqInst) + $ wanteds + payload = mkBigLHsTup dict_bndrs ; traceTc (vcat [text "reduceImplication" <+> ppr name, diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 3f3a7c9..77d7205 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -286,7 +286,7 @@ no further propoagation is possible. -- normaliseEqs :: [Inst] -> TcM EqConfig normaliseEqs eqs - = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs ) + = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs ) ; traceTc $ ptext (sLit "Entering normaliseEqs") ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs @@ -352,7 +352,7 @@ finaliseEqsAndDicts (EqConfig { eqs = eqs -- Assert that all cotvs of wanted equalities are still unfilled, and -- zonk all final insts, to make any improvement visible - ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' ) + ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' ) ; zonked_locals <- zonkInsts locals' ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds') ; return (zonked_locals, zonked_wanteds, final_binds, improved) -- 1.7.10.4