kind: 'fam-instance',
familyId: qid(fi.fiFamily),
famInstance: fi,
+ // Mirror the synthetic-placeholder flag at the top level so
+ // cytoscape selectors can pick these out for distinct styling.
+ unresolved: !!fi._unresolved,
}});
return id;
}
// the matched class-instance node. This makes the chain
// focused-instance → family → concrete fam-instance → Eq instance
// visible as one path instead of two unrelated arrows.
- function addFamilyLinksFromArgs(args, originId, edgeTag, predClassQn) {
+ function addFamilyLinksFromArgs(args, originId, edgeTag, predClassQn,
+ boundTvs, originPredId) {
// The "via Bar" arrow that used to connect @originId@ → family
// was removed (its meaning wasn't obvious). The function's
// remaining job is to surface fam-instance nodes plus the
// resolution chain that ends at a matching class instance.
+ //
+ // @boundTvs@ is the tyvar context (typically the focused
+ // instance's iiTyVars) used to render the synthetic fam-instance
+ // placeholder labels when no relevant fam-instance is found.
+ // @originPredId@ is the predicate node id this family use was
+ // observed inside (when called from a context predicate); the
+ // synthetic placeholder gets a fam-resolves chain edge to it so
+ // the user can see "this fam application is what the predicate
+ // needed".
const fams = collectFamilyRefs(args);
for (const fa of fams) {
const famNodeId = ensureFamilyNode(fa);
+ let anyRelevant = false;
// Surface only the type family instances whose LHS *can* describe
// the focused instance's family-app — anything else is unrelated
// noise. Run the relevance check *before* creating the
resolvedArgs = args.map(a => replaceFamilyApp(a, fa, fi));
if (resolvedArgs.some(a => a === null)) continue;
}
+ anyRelevant = true;
const fiNodeId = ensureFamInstanceNode(fi);
const fdId = famNodeId + '=>' + fiNodeId;
}
}
}
+
+ // No fam-instance was relevant — typically because the family is
+ // defined outside this project and we don't have its equations.
+ // Synthesize a placeholder fam-instance node "Family args = ?"
+ // for each distinct use site so the chain has somewhere to
+ // land. Connect family → placeholder (fam-defines) and, when
+ // we know the originating predicate node, placeholder →
+ // predicate (fam-resolves) so the user reads:
+ // SigDSIGN ──► SigDSIGN Ed448DSIGN = ? ╶╶► NoThunks (SigDSIGN Ed448DSIGN)
+ if (!anyRelevant) {
+ const useSites = collectFamilyAppArgs(args, fa);
+ for (const ua of useSites) {
+ const synFi = {
+ fiFamily: fa,
+ fiArgs: ua,
+ fiRhs: { tag: 'OtherArg', contents: '?' },
+ fiTyVars: boundTvs || [],
+ fiSrc: null,
+ fiDoc: null,
+ fiIsData: false,
+ fiDefinedIn: null,
+ _unresolved: true,
+ };
+ const synHint = 'unresfaminst:' + qid(fa) + ':' + JSON.stringify(ua);
+ const synId = ensureFamInstanceNode(synFi, synHint);
+ const fdId = famNodeId + '=>' + synId;
+ if (!seenNodes.has(fdId)) {
+ seenNodes.add(fdId);
+ els.push({ group: 'edges', data: {
+ id: fdId,
+ source: famNodeId,
+ target: synId,
+ kind: 'fam-defines',
+ }});
+ }
+ if (originPredId) {
+ const resId = synId + '=>resolves=>' + originPredId;
+ if (!seenNodes.has(resId)) {
+ seenNodes.add(resId);
+ els.push({ group: 'edges', data: {
+ id: resId,
+ source: synId,
+ target: originPredId,
+ kind: 'fam-resolves',
+ }});
+ }
+ }
+ }
+ }
}
}
// is a type family that must be defined for that era). For each
// fam-instance we surface, we also try to resolve `pred.piClass`
// for the fam-instance's RHS and chain to the matching instance.
- addFamilyLinksFromArgs(pred.piArgs, instId, 'ctx-fam', pred.piClass);
+ addFamilyLinksFromArgs(pred.piArgs, instId, 'ctx-fam',
+ pred.piClass, inst.iiTyVars, pid);
});
// Associated type families: when the focused class declares assoc
// already been replaced by some fam-instance's RHS and the chain
// never gets a chance to enumerate alternative fam-instances.
const subbedArgs = sc.seArgs.map(a => substTypeArgRaw(a, inst.iiArgs));
- addFamilyLinksFromArgs(subbedArgs, instId, 'sc-fam-' + si, sc.seSuperclass);
// Direct-match path uses the reduced args as before.
const reqArgs = subbedArgs.map(reduceTypeArg);
const matched = findMatchingInstances(sc.seSuperclass, reqArgs);
// edge would just duplicate it.
const reqLabel = 'superclass constraint';
+ // chainTarget gets passed to addFamilyLinksFromArgs further
+ // down: when we land in the unmatched branch and create a
+ // predicate node, the synthetic "Family args = ?" placeholders
+ // will chain to it. For the matched branch there's no single
+ // chain endpoint (matched instances are heterogeneous), so we
+ // leave it null.
+ let chainTarget = null;
+
if (matched.length === 0) {
// No instance was found in our data — but the original
// module typechecked, so the constraint must be discharged
kind: 'needs-external',
label: reqLabel,
}});
+ chainTarget = pid;
} else {
// Local match(es) exist. Connect the focused instance directly
// to each matched instance — we deliberately *don't* also pull
}});
}
}
+
+ // Family-chain work runs *after* the predicate-node decision so
+ // we can hand the synthetic "Family args = ?" placeholders the
+ // pred-node id to chain into.
+ addFamilyLinksFromArgs(subbedArgs, instId, 'sc-fam-' + si,
+ sc.seSuperclass, inst.iiTyVars, chainTarget);
});
});
return [...seen.values()];
}
+ // For a given family @qn@, return every distinct argument list it's
+ // applied to inside @args@. Used to surface "use sites" of an
+ // unresolvable family — e.g. a constraint `NoThunks (SigDSIGN
+ // Ed448DSIGN)` mentions `SigDSIGN [Ed448DSIGN]` once, so we want
+ // exactly one synthetic placeholder for that use.
+ //
+ // Dedup is structural (JSON.stringify of the inner args).
+ function collectFamilyAppArgs(args, qn) {
+ const targetQid = qid(qn);
+ const out = [];
+ const seenStr = new Set();
+ function go(t) {
+ if (!t || !t.tag) return;
+ if (t.tag === 'FamilyApp') {
+ const [q, inner] = t.contents;
+ if (qid(q) === targetQid) {
+ const key = JSON.stringify(inner || []);
+ if (!seenStr.has(key)) {
+ seenStr.add(key);
+ out.push(inner || []);
+ }
+ }
+ for (const x of (inner || [])) go(x);
+ } else if (t.tag === 'TyConApp') {
+ const [, inner] = t.contents;
+ for (const x of (inner || [])) go(x);
+ }
+ }
+ for (const a of (args || [])) go(a);
+ return out;
+ }
+
// Returns the infix operator string for a TyCon name that should render
// infix (currently the various equality and coercion-evidence forms).
// Detect whether a TypeFamilyInfo (from familyById) describes a data
function renderFamInstPanel(fi) {
const head = escape(fi.fiFamily.qnName) + ' ' +
escape(renderArgsCompact(fi.fiArgs, fi.fiTyVars));
+ if (fi._unresolved) {
+ return `
+ <h2>${head}</h2>
+ <p class="pkgmod">${escape(fi.fiFamily.qnPackage)} · ${escape(fi.fiFamily.qnModule)}</p>
+ <dl>
+ <dt>Status</dt><dd><em>Use site of an external type family — the equation isn't in this project's dumps, so the right-hand side can't be resolved here.</em></dd>
+ </dl>`;
+ }
const rhs = escape(renderArg(fi.fiRhs, fi.fiTyVars));
const tvs = fi.fiTyVars.length === 0 ? '<dd><em>none</em></dd>' :
`<dd><ul>${fi.fiTyVars.map(v =>
'border-style': 'dashed',
},
},
+ // External type family — we know the family is referenced but
+ // it isn't defined in this project (no entry in pdTypeFamilies).
+ // Render the diamond grey to signal "defined elsewhere".
+ {
+ selector: 'node[kind = "family"][?external]',
+ style: {
+ 'background-color': '#e5e7eb',
+ 'border-color': '#9ca3af',
+ color: '#374151',
+ 'border-style': 'dashed',
+ },
+ },
// Ghost class node (one-hop neighbour in a focus-filtered classes view)
{
selector: 'node[kind = "class"][?ghost]',
'font-size': 11,
},
},
+ // Unresolved fam-instance placeholder — `Family args = ?`. We
+ // don't have the equation, just the use site. Greyed out to
+ // signal "fam-instance must exist somewhere outside this
+ // project", with a dashed border to echo the external-family
+ // grey-diamond styling.
+ {
+ selector: 'node[kind = "fam-instance"][?unresolved]',
+ style: {
+ 'background-color': '#f3f4f6',
+ color: '#374151',
+ 'border-color': '#9ca3af',
+ 'border-style': 'dashed',
+ },
+ },
// Edges
{
selector: 'edge',