Skip data fam-instances in reduceTypeArg to avoid infinite recursion

The data-family R: rewrite makes a data fam-instance's fiRhs
structurally equal to its FamilyApp LHS (e.g. for `data instance
Crate Int`, fiRhs is `FamilyApp Crate [Int]`). reduceTypeArg used
to unify the use site against fiArgs and recurse on
applySubst(fiRhs, subst) — which produced the same FamilyApp shape
again and looped forever for any constraint mentioning a data
fam-instance.

Skip data fam-instances in reduceTypeArg entirely. Their RHS is
opaque (the synthetic R: TyCon pre-rewrite, the circular FamilyApp
post-rewrite); reducing through them never makes progress, only
ever loops. The use-site FamilyApp falls through unchanged, which
addFamilyLinksFromArgs / the predicate-node + chain machinery then
handle as the data-family use site they actually are.

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

diff --git a/data/viewer.js b/data/viewer.js
index cb84f9fdf67606b21224955b64261500721f7d2a..f56ff8a1df3350001508733e7bda832f3eed52f6 100644 (file)
--- a/data/viewer.js
+++ b/data/viewer.js
@@ -1117,6 +1117,13 @@
       const reducedArgs = args.map(reduceTypeArg);
       for (const fi of graph.meta.pdFamInstances) {
         if (qid(fi.fiFamily) !== qid(q)) continue;
+        // Skip data fam-instances: their fiRhs is opaque (the
+        // synthetic R: TyCon, or after the data-family rewrite the
+        // *abstract* FamilyApp form that's structurally equal to the
+        // LHS). Recursing on either form either loops forever or
+        // produces no progress, so leave the FamilyApp untouched and
+        // let the outer flow handle it as a use site.
+        if (fi.fiIsData) continue;
         if (fi.fiArgs.length !== reducedArgs.length) continue;
         const subst = {};
         let ok = true;