From b459422c5227b98bdb35a317ed256b2bc5fd7e44 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Thu, 7 May 2026 03:03:58 +0200 Subject: [PATCH] Reduce pivot's sub-args before unifying in replaceFamilyApp MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit 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) --- data/viewer.js | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/data/viewer.js b/data/viewer.js index 8355b8a..90719e0 100644 --- 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 -- 2.54.0