Reduce pivot's sub-args before unifying in replaceFamilyApp

When a constraint nests type families — `F (G a)` where `G` has a
known type-instance equation — the outer family's pivot search
finds `FamilyApp F [FamilyApp G [...]]`, but biUnify against
`fi.fiArgs = [TyConApp Bar [...]]` fails because tags differ. The
fam-instance is rejected and a placeholder fires, even though the
inner reduction would produce a unifiable shape.

Reduce the pivot's sub-args via reduceTypeArg before biUnify.
For the user's case `ChainDepState (BlockProtocol (ShelleyBlock proto era))`:
* Without this fix: pivot args = `[FamilyApp BlockProtocol [...]]`,
  biUnify against `TyConApp Praos [TyVarRef 0]` fails.
* With this fix: reduced pivot args = `[TyVarRef proto]`, biUnify
  succeeds (TyVarRef wildcards both sides per biUnify semantics),
  and the chain edges from the data fam-instances `ChainDepState
  (Praos c)` / `ChainDepState (TPraos c)` to the predicate node
  finally surface.

Trade-off: when the inner reduction unwraps a family to a TyVarRef
(as above), every concrete data-instance of the outer family now
matches via biUnify's wildcard rule. So instead of a single chain
the user sees one per concrete instance — Praos AND TPraos in this
example. That's consistent with the existing "Are the resolution
chains deterministic?" caveat in INTERNALS.md: ambiguous matches
surface as multiple chain edges and let the reader pick.

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

diff --git a/data/viewer.js b/data/viewer.js
index 8355b8ac281dcdea9fb25082f429dc93560ad119..90719e08b544fce66ceae27c1b5bcc42900e0bcf 100644 (file)
--- a/data/viewer.js
+++ b/data/viewer.js
@@ -1297,7 +1297,15 @@
     }
     find(t);
     if (!pivot) return t;
-    const pivotArgs = pivot.contents[1];
+    // 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);
     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