diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-02-13 13:53:14 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-02-20 08:52:32 +0000 |
commit | f3e5c3049197e8f9e03375749ce0b024e2d1a1aa (patch) | |
tree | ff58f14fad3ff111bbe30df1bc788bb5006e3e5d | |
parent | 9c78d09e344e97d2d5c37b9bb46e311a3cf031e2 (diff) | |
download | haskell-f3e5c3049197e8f9e03375749ce0b024e2d1a1aa.tar.gz |
Comments only
-rw-r--r-- | compiler/typecheck/TcFlatten.hs | 34 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 57 |
2 files changed, 57 insertions, 34 deletions
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 9554bb05b5..ba25b8bb95 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -124,38 +124,8 @@ Note [The flattening story] This just unites the two fsks into one. Always solve given from wanted if poss. -* [Firing rule: wanteds] - (work item) [W] x : F tys ~ fmv - instantiate axiom: ax_co : F tys ~ rhs - - Dischard fmv: - fmv := alpha - x := ax_co ; sym x2 - [W] x2 : alpha ~ rhs (Non-canonical) - discharging the work item. This is the way that fmv's get - unified; even though they are "untouchable". - - NB: this deals with the case where fmv appears in xi, which can - happen; it just happens through the non-canonical stuff - - Possible short cut (shortCutReduction) if rhs = G rhs_tys, - where G is a type function. Then - - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis) - - Add G rhs_xis ~ fmv to flat cache - - New wanted [W] x2 : G rhs_xis ~ fmv - - Discharge x := co ; G cos ; x2 - -* [Firing rule: givens] - (work item) [G] g : F tys ~ fsk - instantiate axiom: co : F tys ~ rhs - - Now add non-canonical (since rhs is not flat) - [G] (sym g ; co) : fsk ~ rhs - - Short cut (shortCutReduction) for when rhs = G rhs_tys and G is a type function - [G] (co ; g) : G tys ~ fsk - But need to flatten tys: flat_cos : tys ~ flat_tys - [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk +* For top-level reductions, see Note [Top-level reductions for type functions] + in TcInteract Why given-fsks, alone, doesn't work diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index ee4ac6ad8c..5ebeb270b1 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1327,6 +1327,7 @@ doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) -------------------- doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct) +-- Note [Short cut for top-level reaction] doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc , cc_tyargs = args , cc_fsk = fsk }) = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families @@ -1394,6 +1395,7 @@ doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w) shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) +-- See Note [Top-level reductions for type functions] shortCutReduction old_ev fsk ax_co fam_tc tc_args | isGiven old_ev = ASSERT( ctEvEqRel old_ev == NomEq ) @@ -1424,7 +1426,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args -- new_ev :: G xis ~ fsk -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev - ; new_ev <- newWantedEvVarNC deeper_loc + ; new_ev <- newWantedEvVarNC deeper_loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)) ; setWantedEvBind (ctEvId old_ev) (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos) @@ -1453,7 +1455,58 @@ dischargeFmv evar fmv co xi ; n_kicked <- kickOutRewritable Given NomEq fmv ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } -{- +{- Note [Top-level reductions for type functions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +c.f. Note [The flattening story] in TcFlatten + +Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom. +Here is what we do, in four cases: + +* Wanteds: general firing rule + (work item) [W] x : F tys ~ fmv + instantiate axiom: ax_co : F tys ~ rhs + + Then: + Discharge fmv := alpha + Discharge x := ax_co ; sym x2 + New wanted [W] x2 : alpha ~ rhs (Non-canonical) + This is *the* way that fmv's get unified; even though they are + "untouchable". + + NB: it can be the case that fmv appears in the (instantiated) rhs. + In that case the new Non-canonical wanted will be loopy, but that's + ok. But it's good reason NOT to claim that it is canonical! + +* Wanteds: short cut firing rule + Applies when the RHS of the axiom is another type-function application + (work item) [W] x : F tys ~ fmv + instantiate axiom: ax_co : F tys ~ G rhs_tys + + It would be a waste to create yet another fmv for (G rhs_tys). + Instead (shortCutReduction): + - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis) + - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv) + - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan) + - Discharge x := ax_co ; G cos ; x2 + +* Givens: general firing rule + (work item) [G] g : F tys ~ fsk + instantiate axiom: ax_co : F tys ~ rhs + + Now add non-canonical given (since rhs is not flat) + [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical) + +* Givens: short cut firing rule + Applies when the RHS of the axiom is another type-function application + (work item) [G] g : F tys ~ fsk + instantiate axiom: ax_co : F tys ~ G rhs_tys + + It would be a waste to create yet another fsk for (G rhs_tys). + Instead (shortCutReduction): + - Flatten rhs_tys: flat_cos : tys ~ flat_tys + - Add new Canonical given + [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan) + Note [Cached solved FunEqs] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ When trying to solve, say (FunExpensive big-type ~ ty), it's important |