X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=534c5d0601c8e74bd841b1c86da8a845f78ba43d;hp=a274cab231fbd37bdca7518012b46a15a7238fe0;hb=ebec49fed627b7dd17e297ddc79a9c677a2ce538;hpb=5045af3106f3d1e3cb223c254af2de6a8a265797 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index a274cab..534c5d0 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)) } @@ -1642,12 +1652,20 @@ tcSimplifyIPs given_ips wanteds ; let env = mkRedEnv doc try_me given_ips' ; (improved, binds, irreds) <- reduceContext env wanteds' - ; if not improved then + ; if null irreds || not improved then ASSERT( all is_free irreds ) do { extendLIEs irreds ; return binds } - else - tcSimplifyIPs given_ips wanteds } + else do + -- If improvement did some unification, we go round again. + -- We start again with irreds, not 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 <- tcSimplifyIPs given_ips' irreds + ; return $ binds `unionBags` binds1 + } } where doc = text "tcSimplifyIPs" <+> ppr given_ips ip_set = mkNameSet (ipNamesOfInsts given_ips) @@ -1868,6 +1886,8 @@ reduceContext env wanteds0 -- This may expose some further equational constraints... ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds' ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state) + -- The getLIE is reqd because reduceList does improvement + -- (via extendAvails) which may in turn do unification ; (dict_binds, bound_dicts, dict_irreds) <- extractResults avails wanted_dicts @@ -1895,12 +1915,16 @@ reduceContext env wanteds0 -- improvement (i.e., instantiated type variables). -- (2) If we uncovered extra equalities. We will try to solve them -- in the next iteration. + -- (3) If we reduced dictionaries (i.e., got dictionary bindings), + -- they may have exposed further opportunities to normalise + -- family applications. See Note [Dictionary Improvement] ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs avails_improved = availsImproved avails improvedFlexible = avails_improved || eq_improved extraEqs = (not . null) extra_eqs - improved = improvedFlexible || extraEqs + reduced_dicts = not (isEmptyBag dict_binds) + improved = improvedFlexible || extraEqs || reduced_dicts -- improvedHint = (if avails_improved then " [AVAILS]" else "") ++ (if eq_improved then " [EQ]" else "") ++ @@ -1982,6 +2006,44 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env ; return (tidy_env, msg) } \end{code} +Note [Dictionary Improvement] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In reduceContext, we first reduce equalities and then class constraints. +However, the letter may expose further opportunities for the former. Hence, +we need to go around again if dictionary reduction produced any dictionary +bindings. The following example demonstrated the point: + + data EX _x _y (p :: * -> *) + data ANY + + class Base p + + class Base (Def p) => Prop p where + type Def p + + instance Base () + instance Prop () where + type Def () = () + + instance (Base (Def (p ANY))) => Base (EX _x _y p) + instance (Prop (p ANY)) => Prop (EX _x _y p) where + type Def (EX _x _y p) = EX _x _y p + + data FOO x + instance Prop (FOO x) where + type Def (FOO x) = () + + data BAR + instance Prop BAR where + type Def BAR = EX () () FOO + +During checking the last instance declaration, we need to check the superclass +cosntraint Base (Def BAR), which family normalisation reduced to +Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us +Base (Def (FOO ANY)), which again requires family normalisation of Def to +Base () before we can finish. + + The main context-reduction function is @reduce@. Here's its game plan. \begin{code} @@ -2200,18 +2262,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 }) + 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 @@ -2225,13 +2299,6 @@ reduceImplication env [ ppr (red_givens env), ppr extra_givens, ppr wanteds]) ; (irreds, binds) <- checkLoop env' wanteds - ; let (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! ; traceTc (text "reduceImplication result" <+> vcat [ppr irreds, ppr binds]) @@ -2245,17 +2312,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! - - ; traceTc $ text "reduceImplication condition" <+> ppr backOff + 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) @@ -2265,26 +2332,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 - - 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 - <.> mkWpLams 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,