Comments only

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

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