X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=932cb68f425ba706a4114cbd1a1c2e3396a72c60;hp=113de258acc5350653ee6725125ed479935ba40d;hb=e79c9ce01d0ce4412bd4bcd99c8c728a6a2ec569;hpb=1add6282808b5ae98e72ef7034634036c9b91b04 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 113de25..932cb68 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -16,6 +16,8 @@ module TcSimplify ( tcSimplifyDeriv, tcSimplifyDefault, bindInstsOfLocalFuns, + + tcSimplifyStagedExpr, misMatchMsg ) where @@ -58,6 +60,7 @@ import Util import SrcLoc import DynFlags import FastString + import Control.Monad import Data.List \end{code} @@ -861,7 +864,7 @@ Note [NO TYVARS] The excitement comes when simplifying the bindings for h. Initially try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}. -From this we get t1:=:t2, but also various bindings. We can't forget +From this we get t1~t2, but also various bindings. We can't forget the bindings (because of [LOOP]), but in fact t1 is what g is polymorphic in. @@ -971,17 +974,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) +-- 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 +992,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 + tci_given = eq_givens ++ dict_givens, + -- 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)) } @@ -1402,7 +1415,7 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight = do { traceTc (text "tcSimplifyRestricted") - ; wanteds' <- zonkInsts wanteds + ; wanteds_z <- zonkInsts wanteds -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type @@ -1414,7 +1427,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe) - ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1442,6 +1455,13 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds ppr _binds, ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) + -- Zonk wanteds again! The first call to reduceContext may have + -- instantiated some variables. + -- FIXME: If red_improve would work, we could propagate that into + -- the equality solver, too, to prevent instantating any + -- variables. + ; wanteds_zz <- zonkInsts wanteds_z + -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact -- set of type variables to quantify over. @@ -1463,7 +1483,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds (is_nested_group || isDict inst) = Stop | otherwise = ReduceMe env = mkNoImproveRedEnv doc try_me - ; (_imp, binds, irreds) <- reduceContext env wanteds' + ; (_imp, binds, irreds) <- reduceContext env wanteds_zz -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1642,12 +1662,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) @@ -1865,9 +1893,13 @@ reduceContext env wanteds0 } -- Solve the *wanted* *dictionary* constraints (not implications) - -- This may expose some further equational constraints... + -- This may expose some further equational constraints in the course + -- of improvement due to functional dependencies if any of the + -- involved unifications gets deferred. ; 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 @@ -1893,18 +1925,24 @@ reduceContext env wanteds0 -- go round again. We do so in either of two cases: -- (1) If dictionary reduction or equality solving led to -- improvement (i.e., instantiated type variables). - -- (2) If we uncovered extra equalities. We will try to solve them - -- in the next iteration. + -- (2) If we reduced dictionaries (i.e., got dictionary bindings), + -- they may have exposed further opportunities to normalise + -- family applications. See Note [Dictionary Improvement] + -- + -- NB: We do *not* go around for new extra_eqs. Morally, we should, + -- but we can't without risking non-termination (see #2688). By + -- not going around, we miss some legal programs mixing FDs and + -- TFs, but we never claimed to support such programs in the + -- current implementation anyway. ; 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 || reduced_dicts -- improvedHint = (if avails_improved then " [AVAILS]" else "") ++ - (if eq_improved then " [EQ]" else "") ++ - (if extraEqs then " [EXTRA EQS]" else "") + (if eq_improved then " [EQ]" else "") ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", @@ -1982,6 +2020,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,19 +2276,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 +2326,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 +2346,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, @@ -2934,6 +3017,26 @@ tcSimplifyDefault theta = do doc = ptext (sLit "default declaration") \end{code} +@tcSimplifyStagedExpr@ performs a simplification but does so at a new +stage. This is used when typechecking annotations and splices. + +\begin{code} + +tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds) +-- Type check an expression that runs at a top level stage as if +-- it were going to be spliced and then simplify it +tcSimplifyStagedExpr stage tc_action + = setStage stage $ do { + -- Typecheck the expression + (thing', lie) <- getLIE tc_action + + -- Solve the constraints + ; const_binds <- tcSimplifyTop lie + + ; return (thing', const_binds) } + +\end{code} + %************************************************************************ %* *