Commit 633dd558 authored by dimitris's avatar dimitris

Moved solving of type families to zonkWC and a few simplifications

in TcSimplify. Now unflattening does not happen recursively inside
solveWanteds which should be a good performance win.
parent 7560dd62
......@@ -62,17 +62,22 @@ now?
type ErrEnv = VarEnv [ErrMsg]
reportUnsolved :: Bool -> WantedConstraints -> TcM (Bag EvBind)
-- Important precondition:
-- WantedConstraints are fully zonked and unflattened, that is,
-- zonkWC has already been applied to these constraints.
reportUnsolved runtimeCoercionErrors wanted
| isEmptyWC wanted
= return emptyBag
| otherwise
= do { -- Zonk to un-flatten any flatten-skols
wanted <- zonkWC wanted
= do { traceTc "reportUnsolved (before unflattening)" (ppr wanted)
; env0 <- tcInitTidyEnv
-- If we are deferring we are going to need /all/ evidence around,
-- including the evidence produced by unflattening (zonkWC)
; defer <- if runtimeCoercionErrors
then do { ev <- newTcEvBinds
; return (Just ev) }
then do { ev_binds_var <- newTcEvBinds
; return (Just ev_binds_var) }
else return Nothing
; errs_so_far <- ifErrsM (return True) (return False)
......@@ -87,14 +92,15 @@ reportUnsolved runtimeCoercionErrors wanted
, cec_tidy = tidy_env
, cec_defer = defer }
; traceTc "reportUnsolved:" (vcat [ pprTvBndrs (varSetElems free_tvs)
, ppr wanted ])
; traceTc "reportUnsolved (after unflattening):" $
vcat [ pprTvBndrs (varSetElems free_tvs)
, ppr wanted ]
; reportWanteds err_ctxt wanted
; case defer of
Nothing -> return emptyBag
Just ev -> getTcEvBinds ev }
Nothing -> return emptyBag
Just ev_binds_var -> getTcEvBinds ev_binds_var }
--------------------------------------------
-- Internal functions
......
......@@ -440,8 +440,10 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
| otherwise
= do { tch1 <- isTouchableMetaTyVarTcS tv1
; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" $
ppr workItem
else do { untch <- getUntouchables
; traceTcS "Untouchable LHS, can't spontaneously solve workitem" $
vcat [text "Untouchables =" <+> ppr untch
, text "Workitem =" <+> ppr workItem ]
; return SPCantSolve }
}
......
......@@ -65,8 +65,8 @@ module TcMType (
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar, zonkCt, zonkCts,
zonkImplication, zonkEvVar, zonkWC, zonkId,
zonkTcKind, defaultKindVarToStar,
zonkEvVar, zonkWC, zonkId, zonkCt,
tcGetGlobalTyVars,
) where
......@@ -76,6 +76,7 @@ module TcMType (
-- friends:
import TypeRep
import TcType
import TcEvidence
import Type
import Kind
import Class
......@@ -617,13 +618,15 @@ skolemiseSigTv tv
\begin{code}
zonkImplication :: Implication -> TcM Implication
zonkImplication implic@(Implic { ic_given = given
zonkImplication implic@(Implic { ic_untch = untch
, ic_binds = binds_var
, ic_given = given
, ic_wanted = wanted
, ic_loc = loc })
= do { -- No need to zonk the skolems
; given' <- mapM zonkEvVar given
; loc' <- zonkGivenLoc loc
; wanted' <- zonkWC wanted
; wanted' <- zonkWCRec binds_var untch wanted
; return (implic { ic_given = given'
, ic_fsks = [] -- Zonking removes all FlatSkol tyvars
, ic_wanted = wanted'
......@@ -634,22 +637,97 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
; return (setVarType var ty') }
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
= do { flat' <- mapBagM zonkCt flat
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
-> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
= zonkWCRec binds_var noUntouchables wc
zonkWCRec :: EvBindsVar
-> Untouchables
-> WantedConstraints -> TcM WantedConstraints
zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
= do { flat' <- zonkFlats binds_var untch flat
; implic' <- mapBagM zonkImplication implic
; insol' <- mapBagM zonkCt insol
; insol' <- mapBagM zonkCt insol -- No need to do the more elaborate zonkFlats thing
; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
zonkCt :: Ct -> TcM Ct
-- Zonking a Ct conservatively gives back a CNonCanonical
zonkCt ct
zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
-- This zonks and unflattens a bunch of flat constraints
-- See Note [Unflattening while zonking]
zonkFlats binds_var untch cts =
foldrBagM unflatten_one emptyCts cts >>= mapBagM zonkCt
-- Do the unflattening one-by one and then zonk all the rest in this bag
where
unflatten_one orig_ct cts
= do { zct <- zonkCt orig_ct -- First we need to fully zonk
; mct <- try_zonk_fun_eq zct -- Then try to solve if family equation
; return $ maybe cts (`consBag` cts) mct }
where try_zonk_fun_eq zct
-- Original looks like wanted/derived family equation
| CFunEqCan {} <- orig_ct
, not (isGivenCt orig_ct)
-- New guy still looks like (lhs_ty ~ tv') so check if we can do a unification
, EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
, Just tv' <- getTyVar_maybe ty_rhs
= do { let b1 = isTouchableMetaTyVar untch tv' ||
isFloatedTouchableMetaTyVar untch tv'
b2 = typeKind ty_lhs `tcIsSubKind` tyVarKind tv'
b3 = not (tv' `elemVarSet` tyVarsOfType ty_lhs)
; traceTc "try_zonk_fun_eq" $
vcat [ text "orig_ct =" <+> ppr orig_ct
, text "zct =" <+> ppr zct
, text "current untouchables =" <+> ppr untch
, text "touchable =" <+> ppr b1
, text "kinds compatible=" <+> ppr b2
, text "occurs ok=" <+> ppr b3 ]
; if b1 && b2 && b3 then
do { writeMetaTyVar tv' ty_lhs
; let evterm = EvCoercion (mkTcReflCo ty_lhs)
evvar = ctev_evar (cc_ev zct)
; when (isWantedCt orig_ct) $ addTcEvBind binds_var evvar evterm
; traceTc "zonkFlats/unflattening" $
vcat [ text "zct = " <+> ppr zct,
text "binds_var = " <+> ppr binds_var ]
; return Nothing }
else return (Just zct) }
| otherwise
= return (Just zct)
\end{code}
Note [Unflattening while zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A bunch of wanted constraints could contain wanted equations of the form
(F taus ~ alpha) where alpha is either an ordinary unification variable, or
a flatten unification variable.
These are ordinary wanted constraints and can/should be solved by
ordinary unification alpha := F taus. However the constraint solving
algorithm does not do that, as their 'inert' form is F taus ~ alpha.
We then must have some extra step to 'unflatten' these equations by
performing unification. This unification, if it happens at the end of
constraint solving, cannot produce any more interactions in the
constraint solver so it is safe to do it as the very very last step.
We choose therefore to do it during zonking, in the function
zonkFlats. This is in analgoy to the zonking of given flatten skolems
which are eliminated in favor of the underlying type that they are
equal to.
Note that, because we now have to affect evidence while zonking
(setting some evidence binds to identities), we have to pass to the
zonkWC function an evidence variable to collect all the extra
variables.
\begin{code}
zonkCt :: Ct -> TcM Ct
zonkCt ct
= do { fl' <- zonkCtEvidence (cc_ev ct)
; return $
CNonCanonical { cc_ev = fl'
, cc_depth = cc_depth ct } }
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt
; return (CNonCanonical { cc_ev = fl'
, cc_depth = cc_depth ct }) }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
zonkCtEvidence ctev@(CtGiven { ctev_gloc = loc, ctev_pred = pred })
......
......@@ -23,7 +23,6 @@ import TcType
import TcSMonad
import TcInteract
import Inst
import Unify ( niFixTvSubst, niSubstTvSet )
import Type ( classifyPredType, PredTree(..), getClassPredTys_maybe )
import Class ( Class )
import Var
......@@ -54,31 +53,31 @@ import DynFlags
* *
*********************************************************************************
\begin{code}
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
-- Usually these will be implications,
-- but when there is nothing to quantify we don't wrap
-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
= do { zonked_wanteds <- zonkWC wanteds
; traceTc "simplifyTop {" $ text "zonked_wc =" <+> ppr zonked_wanteds
; (final_wc, binds1) <- runTcS (simpl_top zonked_wanteds)
simplifyTop wanteds
= do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
; ev_binds_var <- newTcEvBinds
; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top
; binds1 <- TcRnMonad.getTcEvBinds ev_binds_var
; traceTc "End simplifyTop }" empty
; traceTc "reportUnsolved {" empty
-- See Note [Deferring coercion errors to runtime]
; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
; binds2 <- reportUnsolved runtimeCoercionErrors final_wc
; binds2 <- reportUnsolved runtimeCoercionErrors zonked_final_wc
; traceTc "reportUnsolved }" empty
; return (binds1 `unionBags` binds2) }
where
-- See Note [Top-level Defaulting Plan]
simpl_top wanteds
= do { wc_first_go <- solveWantedsTcS wanteds
= do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
; applyTyVarDefaulting wc_first_go
; simpl_top_loop wc_first_go }
......@@ -86,7 +85,7 @@ simplifyTop wanteds
| isEmptyWC wc
= return wc
| otherwise
= do { wc_residual <- solveWantedsTcS wc
= do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
; let wc_flat_approximate = approximateWC wc_residual
; something_happened <- applyDefaultingRules wc_flat_approximate
-- See Note [Top-level Defaulting Plan]
......@@ -164,6 +163,9 @@ simplifyDefault theta
; traceTc "reportUnsolved {" empty
-- See Note [Deferring coercion errors to runtime]
; runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
-- Postcondition of solveWantedsTcM is that returned
-- constraints are zonked. So Precondition of reportUnsolved
-- is true.
; _ <- reportUnsolved runtimeCoercionErrors unsolved
; traceTc "reportUnsolved }" empty
......@@ -203,6 +205,7 @@ simplifyDeriv orig pred tvs theta
vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
; (residual_wanted, _ev_binds1)
<- solveWantedsTcM (mkFlatWC wanted)
-- Post: residual_wanted are already zonked
; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
-- See Note [Exotic derived instance contexts]
......@@ -343,8 +346,9 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
= do { runtimeCoercionErrors <- doptM Opt_DeferTypeErrors
; gbl_tvs <- tcGetGlobalTyVars
; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
; zonked_wanteds <- zonkWC wanteds
; ev_binds_var <- newTcEvBinds
; traceTc "simplifyInfer {" $ vcat
[ ptext (sLit "names =") <+> ppr (map fst name_taus)
, ptext (sLit "taus =") <+> ppr (map snd name_taus)
......@@ -352,7 +356,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
, ptext (sLit "closed =") <+> ppr _top_lvl
, ptext (sLit "apply_mr =") <+> ppr apply_mr
, ptext (sLit "wanted =") <+> ppr zonked_wanteds
, ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
]
-- Historical note: Before step 2 we used to have a
......@@ -369,8 +373,9 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- calling solveWanteds will side-effect their evidence
-- bindings, so we can't just revert to the input
-- constraint.
; ev_binds_var <- newTcEvBinds
; wanted_transformed <- solveWantedsWithEvBinds ev_binds_var zonked_wanteds
; wanted_transformed <- solveWantedsTcMWithEvBinds ev_binds_var wanteds $
solve_wanteds_and_drop
-- Post: wanted_transformed are zonked
-- Step 3) Fail fast if there is an insoluble constraint,
-- unless we are deferring errors to runtime
......@@ -385,12 +390,20 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- Step 5) Minimize the quantification candidates
-- Step 6) Final candidates for quantification
-- We discard bindings, insolubles etc, because all we are
-- care aout it
-- care aout it
; (quant_pred_candidates, _extra_binds)
<- runTcS $ do { let quant_candidates = approximateWC wanted_transformed
<- runTcS $ do { let quant_candidates = approximateWC wanted_transformed
; traceTcS "simplifyWithApprox" $
text "quant_candidates = " <+> ppr quant_candidates
; promoteTyVars quant_candidates
; _implics <- solveInteract quant_candidates
; (flats, _insols) <- getInertUnsolved
-- NB: Dimitrios is slightly worried that we will get
-- family equalities (F Int ~ alpha) in the quantification
-- candidates, as we have performed no further unflattening
-- at this point. Nothing bad, but inferred contexts might
-- look complicated.
; return (map ctPred $ filter isWantedCt (bagToList flats)) }
-- NB: quant_pred_candidates is already the fixpoint of any
......@@ -574,8 +587,12 @@ simplifyRule name lhs_wanted rhs_wanted
= do { -- We allow ourselves to unify environment
-- variables: runTcS runs with NoUntouchables
(resid_wanted, _) <- solveWantedsTcM (lhs_wanted `andWC` rhs_wanted)
-- Post: these are zonked and unflattened
; zonked_lhs <- zonkWC lhs_wanted
-- Dimitrios would be happy if we could avoid this zonking here. But
-- I am afraid that if we do not zonk, we will quantify over the wrong things.
; _ev_binds_var <- newTcEvBinds
; zonked_lhs <- zonkWC _ev_binds_var lhs_wanted -- Don't care about binds
; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
quantify_me -- Note [RULE quantification over equalities]
......@@ -645,30 +662,27 @@ compilation. The errors are turned into warnings in `reportUnsolved`.
\begin{code}
solveWantedsTcMWithEvBinds :: EvBindsVar
-> WantedConstraints
-> (WantedConstraints -> TcS WantedConstraints)
-> TcM WantedConstraints
solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action
= do { wc1 <- zonkWC ev_binds_var wc
; traceTc "solveWantedsTcMWithEvBinds" $ text "zonked wanted=" <+> ppr wc1
; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc1)
; zonkWC ev_binds_var wc2 }
solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind)
-- Zonk the input constraints, and simplify them
-- Return the evidence binds in the BagEvBinds result
-- Discards all Derived stuff in result
-- Postcondition: fully zonked and unflattened constraints
solveWantedsTcM wanted
= do { zonked_wanted <- zonkWC wanted
; traceTc "solveWantedsTcM {" (ppr zonked_wanted)
; (wanteds', binds) <- runTcS (solve_wanteds_and_drop zonked_wanted)
; traceTc "solveWantedsTcM end }" (ppr wanteds')
= do { ev_binds_var <- newTcEvBinds
; wanteds' <- solveWantedsTcMWithEvBinds ev_binds_var wanted solve_wanteds_and_drop
; binds <- TcRnMonad.getTcEvBinds ev_binds_var
; return (wanteds', binds) }
solveWantedsWithEvBinds :: EvBindsVar -> WantedConstraints -> TcM WantedConstraints
-- Side-effect the EvBindsVar argument to add new bindings from solving
-- Discards all Derived stuff in result
solveWantedsWithEvBinds ev_binds_var wanted
= runTcSWithEvBinds ev_binds_var (solve_wanteds_and_drop wanted)
solveWantedsTcS :: WantedConstraints -> TcS WantedConstraints
-- Solve, with current untouchables, augmenting the current
-- evidence bindings, ty_binds, and solved caches
-- However, revert the InertCans to the way they were at
-- the beginning (since we are returning the residual)
solveWantedsTcS wanted = nestTcS (solve_wanteds_and_drop wanted)
solve_wanteds_and_drop :: WantedConstraints -> TcS (WantedConstraints)
-- Since solve_wanteds returns the residual WantedConstraints,
-- it should alway be called within a runTcS or something similar,
......@@ -697,10 +711,12 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
; (unsolved_flats, insoluble_flats) <- getInertUnsolved
; wc <- unFlattenWC (WC { wc_flat = unsolved_flats
, wc_impl = unsolved_implics
, wc_insol = insoluble_flats })
-- We used to unflatten here but now we only do it once at top-level
-- during zonking -- see Note [Unflattening while zonking] in TcMType
; let wc = WC { wc_flat = unsolved_flats
, wc_impl = unsolved_implics
, wc_insol = insoluble_flats }
; bb <- getTcEvBindsMap
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
......@@ -876,7 +892,6 @@ approximateWC wc = float_wc emptyVarSet wc
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
\end{code}
\end{code}
Note [Float Equalities out of Implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -995,90 +1010,6 @@ and make them untouchables for the nested implication. In the
example above uf would become untouchable, so beta would be forced
to be unified as beta := uf.
\begin{code}
unFlattenWC :: WantedConstraints -> TcS WantedConstraints
unFlattenWC wc
= do { (subst, remaining_unsolved_flats) <- solveCTyFunEqs (wc_flat wc)
-- See Note [Solving Family Equations]
-- NB: remaining_flats has already had subst applied
; return $
WC { wc_flat = mapBag (substCt subst) remaining_unsolved_flats
, wc_impl = mapBag (substImplication subst) (wc_impl wc)
, wc_insol = mapBag (substCt subst) (wc_insol wc) }
}
where
solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
-- See Note [Solving Family Equations]
-- Returns: a bunch of unsolved constraints from the original Cts and implications
-- where the newly generated equalities (alpha := F xi) have been substituted through.
solveCTyFunEqs cts
= do { untch <- TcSMonad.getUntouchables
; let (unsolved_can_cts, (ni_subst, cv_binds))
= getSolvableCTyFunEqs untch cts
; traceTcS "defaultCTyFunEqs" (vcat [ text "Trying to default family equations:"
, text "untch" <+> ppr untch
, text "subst" <+> ppr ni_subst
, text "binds" <+> ppr cv_binds
, ppr unsolved_can_cts
])
; mapM_ solve_one cv_binds
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
solve_one (CtWanted { ctev_evar = cv }, tv, ty)
= setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
solve_one (CtDerived {}, tv, ty)
= setWantedTyBind tv ty
solve_one arg
= pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
------------
type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
-- The TvSubstEnv is not idempotent, but is loop-free
-- See Note [Non-idempotent substitution] in Unify
emptyFunEqBinds :: FunEqBinds
emptyFunEqBinds = (emptyVarEnv, [])
extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
extendFunEqBinds (tv_subst, cv_binds) fl tv ty
= (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
------------
getSolvableCTyFunEqs :: Untouchables
-> Cts -- Precondition: all Wanteds or Derived!
-> (Cts, FunEqBinds) -- Postcondition: returns the unsolvables
getSolvableCTyFunEqs untch cts
= Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
where
dflt_funeq :: (Cts, FunEqBinds) -> Ct
-> (Cts, FunEqBinds)
dflt_funeq (cts_in, feb@(tv_subst, _))
(CFunEqCan { cc_ev = fl
, cc_fun = tc
, cc_tyargs = xis
, cc_rhs = xi })
| Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
, isTouchableMetaTyVar untch tv
-- And it's a *touchable* unification variable
, typeKind xi `tcIsSubKind` tyVarKind tv
-- Must do a small kind check since TcCanonical invariants
-- on family equations only impose compatibility, not subkinding
, not (tv `elemVarEnv` tv_subst)
-- Check not in extra_binds
-- See Note [Solving Family Equations], Point 1
, not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-- Occurs check: see Note [Solving Family Equations], Point 2
= ASSERT ( not (isGiven fl) )
(cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
dflt_funeq (cts_in, fun_eq_binds) ct
= (cts_in `extendCts` ct, fun_eq_binds)
\end{code}
Note [Solving Family Equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1098,7 +1029,10 @@ When is it ok to do so?
set [beta := F xis] only if beta is not among the free variables of xis.
3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
of type family equations. See Inert Set invariants in TcInteract.
of type family equations. See Inert Set invariants in TcInteract.
This solving is now happening during zonking, see Note [Unflattening during zonking]
in TcMType.
*********************************************************************************
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment