From: Javier Sagredo Date: Thu, 7 May 2026 01:08:27 +0000 (+0200) Subject: Revert per-pivot reduction in replaceFamilyApp X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=5306040244edaad2d04675fb498b91e462e82680;p=classgraph.git 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) --- diff --git a/data/viewer.js b/data/viewer.js index 90719e0..8355b8a 100644 --- 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 f73bdcb..df2ebf0 100644 --- 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).