Revert per-pivot reduction in replaceFamilyApp

The previous change ('Reduce pivot's sub-args before unifying in
replaceFamilyApp') traded "F (G a) won't resolve" for "every
concrete fam-instance of F now matches once G a unwraps to a
TyVarRef". That blew up real cases — a ChainDepState use site
intended for Praos / TPraos started matching the BFT and PBFT
data instances too, because biUnify wildcards both sides on
TyVarRef.

Roll back to the conservative behaviour: don't pre-reduce the
pivot's sub-args. Use sites with nested families that we can't
unify directly take the placeholder path. INTERNALS.md updated
to describe the trade-off as a deliberate non-feature.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

diff --git a/data/viewer.js b/data/viewer.js
index 90719e08b544fce66ceae27c1b5bcc42900e0bcf..8355b8ac281dcdea9fb25082f429dc93560ad119 100644 (file)
--- a/data/viewer.js
+++ b/data/viewer.js
@@ -1297,15 +1297,7 @@
     }
     find(t);
     if (!pivot) return t;
-    // Reduce the pivot's sub-args before unifying. This unwraps nested
-    // type-family applications — e.g. for a use site
-    //   F (G a)            (where G has a `type instance G _ = something` rule)
-    // the pivot is `FamilyApp F [FamilyApp G [a]]`; reducing the sub-args
-    // turns that into `FamilyApp F [something]`, which then has a real
-    // shot at unifying with concrete fi.fiArgs like `[TyConApp Bar [...]]`.
-    // Without this step the outer family looks unresolvable even when
-    // the equations to make it resolvable are in the dumps.
-    const pivotArgs = pivot.contents[1].map(reduceTypeArg);
+    const pivotArgs = pivot.contents[1];
     if (!fi.fiArgs || fi.fiArgs.length !== pivotArgs.length) return null;
     const substFi   = {};   // fi-side tyvars → pred-side values
     const substPred = {};   // pred-side tyvars → fi-side values

diff --git a/docs/INTERNALS.md b/docs/INTERNALS.md
index f73bdcb5fc4b558543e6a098d0788d99df30b203..df2ebf0f14b1ca8fdf9a4d3144b0067419d0c423 100644 (file)
--- a/docs/INTERNALS.md
+++ b/docs/INTERNALS.md
@@ -277,36 +277,30 @@ The algorithm:
 
 2. **For each fam-instance `fi` of that family:**
 
-   1. **Reduce the pivot's sub-args first.** Before unifying we run
-      `reduceTypeArg` over the *FamilyApp pivot's sub-args*, so a
-      nested family application gets unwrapped where possible. For
-      a use site `F (G a)` with `type instance G _ = something`,
-      the pivot's args go from `[FamilyApp G [a]]` to
-      `[something]` — which is what gives `biUnify` a chance to
-      match `F`'s fam-instances. Without this step nested-family
-      use sites looked unresolvable even when the equations to make
-      them resolvable were right there.
-
-   2. **Bidirectional unification** between `fi.fiArgs` and the
-      (reduced) `FamilyApp`'s args. `biUnify` allows TyVarRefs on
-      either side to bind to anything on the other side. *If
-      unification fails, this `fi` is irrelevant — skip it
-      entirely.* (This is what stops e.g. a `Foo Int`-shaped
-      predicate from being matched against a `type instance F Bool
-      = …` equation.) The wildcard rule is intentionally
-      permissive — when the inner reduction unwraps to a `TyVarRef`
-      (an abstract tyvar in the use site), every concrete
-      data-instance of the outer family ends up matching it. The
-      user sees a chain edge per match; we deliberately don't try
-      to disambiguate further.
-
-   3. **Substitute `fi.fiRhs` into the predicate.** The bidirectional
+   1. **Bidirectional unification** between `fi.fiArgs` and the
+      `FamilyApp`'s args. `biUnify` allows TyVarRefs on either side
+      to bind to anything on the other side. *If unification fails,
+      this `fi` is irrelevant — skip it entirely.* (This is what
+      stops e.g. a `Foo Int`-shaped predicate from being matched
+      against a `type instance F Bool = …` equation.) Note that
+      `biUnify` operates on the args *as written*: we deliberately
+      do **not** pre-reduce nested type-family applications inside
+      the pivot's args before unifying. Doing so would let the
+      outer family match every concrete fam-instance once the
+      inner reduction collapsed to a tyvar, which produces an
+      explosion of spurious chain edges (every concrete data
+      instance "matches" an abstract `F a`). The trade-off: we
+      miss legitimate chains through nested families like `F (G
+      a)` where `G a` would reduce to a useful shape — those will
+      take the placeholder path in the next section.
+
+   2. **Substitute `fi.fiRhs` into the predicate.** The bidirectional
       unification gave us substitutions for both fi's tyvars (used to
       rewrite fi's RHS) and the predicate's tyvars (used to specialise
       the rest of the predicate). The result is a fully-substituted
       predicate with no occurrence of the originating family.
 
-   4. **Reduce the result.** `reduceTypeArg` walks the resulting
+   3. **Reduce the result.** `reduceTypeArg` walks the resulting
       `TypeArg` and tries to apply *any* available fam-instance
       (using one-sided unification — predicate vars stay free) to
       collapse remaining family applications. This handles chained
@@ -315,13 +309,13 @@ The algorithm:
       structurally equal to the LHS post-rewrite, so naïve
       recursion looped forever).
 
-   5. **Find a matching class instance.** `findMatchingInstances`
+   4. **Find a matching class instance.** `findMatchingInstances`
       scans `pdInstances` for an instance of the predicate's class
       whose `iiArgs` shape-match the reduced args (TyVarRefs on
       either side acting as wildcards). If one or more are found,
       draw a `fam-resolves` edge from the `fi` node to each.
 
-   6. **Fall back to the predicate node.** If no class instance
+   5. **Fall back to the predicate node.** If no class instance
       matched (typically because the class's defining package
       isn't in the dumps), draw a `fam-resolves` edge from the
       `fi` node to the originating *predicate node* (the one
@@ -330,7 +324,7 @@ The algorithm:
       orphaned even though we knew exactly which constraint it was
       discharging.
 
-   7. **Draw the chain.** Net result: focused instance → predicate
+   6. **Draw the chain.** Net result: focused instance → predicate
       node → fam-instance(s) → class instance(s) (or back to the
       predicate node if no class instance was found).