Document the synthetic Family args = ? placeholder

New section covering when the placeholder fires (broader than just
"family is external" — anywhere unification fails), the conditional
chain edge to the originating predicate, the per-(family, args)
dedup key, the implementation as a fake FamInstInfo with
_unresolved/unresolved flags, and the matching grey-dashed styling
shared with external family diamonds.

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

diff --git a/docs/INTERNALS.md b/docs/INTERNALS.md
index 573c16d1fb262a7749b526bd7113617b01e9de56..f772fbf431c03304be8297ed5aeb3290915bdde7 100644 (file)
--- a/docs/INTERNALS.md
+++ b/docs/INTERNALS.md
@@ -17,6 +17,7 @@ or an inferred (possibly fragile) reconstruction.
 - [Type-family resolution in the viewer](#type-family-resolution-in-the-viewer)
 - [Are the resolution chains deterministic?](#are-the-resolution-chains-deterministic)
 - [Predicate nodes and how they dedup](#predicate-nodes-and-how-they-dedup)
+- [Synthetic "Family args = ?" placeholders](#synthetic-family-args---placeholders)
 - [What the viewer is *not* doing](#what-the-viewer-is-not-doing)
 
 ## Pipeline at a glance
@@ -409,6 +410,62 @@ A few things to be aware of:
   arg/tyvar context differs). That's fine — predicate nodes are
   scoped to "this view".
 
+## Synthetic "Family args = ?" placeholders
+
+When a context predicate or unmatched superclass mentions a `FamilyApp`
+that *no* fam-instance can be unified with, the viewer synthesises a
+placeholder fam-instance node showing the use-site args and `= ?` for
+the RHS. The chain reads:
+
+```
+SigDSIGN (grey diamond) ──► SigDSIGN Ed448DSIGN = ?  ╶╶►  NoThunks (SigDSIGN Ed448DSIGN)
+```
+
+Where this lives: `addFamilyLinksFromArgs` in `viewer.js`, after the
+real-fam-instance loop. If the loop's `anyRelevant` flag is still
+false at the end, we walk the args again with `collectFamilyAppArgs`
+to find every distinct application of that family and synthesise one
+placeholder per use site.
+
+A few things to know:
+
+- **Trigger is broader than "the family is external".** The
+  placeholder fires whenever no fam-instance unifies with the use site
+  — typically because the family is genuinely external (no equations
+  in our dumps), but also when a local family has equations for `Int`
+  and `Bool` and the constraint mentions `F SomeOtherType`.
+  Structurally honest, just slightly overgenerous in name.
+
+- **Chain edge to the predicate is conditional.** The synthetic
+  placeholder gets a `fam-resolves` chain edge `placeholder →
+  origin-pred-node` *only when* the caller passes an `originPredId`.
+  That's set when the family use was inside a context predicate (we
+  always have a pred-node id) or an unmatched superclass requirement
+  (we just created one). It's `null` for matched superclass calls,
+  where there's no single pred-node target — the placeholder still
+  appears connected to the family, just without the chain leg.
+
+- **Dedup is per (family, use-site args).** If the same `SigDSIGN
+  Ed448DSIGN` shows up in multiple constraints of the focused
+  instance, only one placeholder appears, with multiple incoming
+  chain edges if multiple predicates referred to it. The dedup key
+  is `'unresfaminst:' + qid(family) + ':' + JSON.stringify(args)`.
+
+- **The placeholder pretends to be a fam-instance node.** Internally
+  it's a synthetic `FamInstInfo`-shaped object with `_unresolved:
+  true`, `fiRhs: { tag: 'OtherArg', contents: '?' }`, and the
+  focused-instance's tyvars in `fiTyVars` (so its label renders
+  against the right tyvar context). `ensureFamInstanceNode` mirrors
+  `_unresolved` to a top-level `data.unresolved` so cytoscape
+  selectors can target it for the dashed-grey styling.
+
+- **External families pick up matching styling.** A family node
+  whose `qid` isn't in `pdTypeFamilies` is tagged `external: true`
+  by `ensureFamilyNode`; the cytoscape rule
+  `node[kind = "family"][?external]` paints it grey-dashed. Same
+  visual language as the placeholder, so the chain reads as one
+  continuous "outside this project" thread.
+
 ## What the viewer is *not* doing
 
 A few things we deliberately don't do, in case you wonder: