From 7baa79a6ad1b1daebc1874562126b37327ec5e0f Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Thu, 7 May 2026 00:33:10 +0200 Subject: [PATCH] Unify unmatched superclass with context predicate node MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit Was: unmatched superclass → class node, edge "needs Foo a b (no local match)". Now: unmatched superclass → predicate node (the same one created from a context constraint when the predicate happens to match, otherwise a fresh role='extern' grey node), edge labelled "superclass constraint". This collapses the case where a constraint appears in *both* the context and as an unmatched superclass — the user sees one node with two edges ("instance context" + "superclass constraint") instead of two disconnected nodes saying the same thing. When the constraint is purely an external superclass, the grey 'extern' predicate node makes "must exist somewhere outside this project" visible at a glance. Co-Authored-By: Claude Opus 4.7 (1M context) --- data/viewer.html | 4 ++-- data/viewer.js | 43 ++++++++++++++++++++++++++++++++++++------- 2 files changed, 38 insertions(+), 9 deletions(-) diff --git a/data/viewer.html b/data/viewer.html index ebdbbfb..d192838 100644 --- a/data/viewer.html +++ b/data/viewer.html @@ -50,8 +50,8 @@

Instance-view edges

Class defines this instance
Instance context — points at a predicate node
-
Instance needs a superclass instance (matched locally)
-
Needs a superclass instance (no local match)
+
Superclass constraint, satisfied by an instance in this project
+
Superclass constraint, points at a predicate node (external or context)
Family → one of its type family instances
Type family instance resolves to a class instance (chain)
diff --git a/data/viewer.js b/data/viewer.js index d0f0822..060c739 100644 --- a/data/viewer.js +++ b/data/viewer.js @@ -814,16 +814,32 @@ const reqLabel = 'superclass constraint'; if (matched.length === 0) { - // No instance found in our data; link to the superclass class - // node (which we have to draw in this branch) and mark it - // external/unresolved. - const scClsId = ensureClassNode(sc.seSuperclass); + // No instance was found in our data — but the original + // module typechecked, so the constraint must be discharged + // somewhere. Two cases: + // + // (a) The same predicate (class + arg shape) is also in + // this instance's context. ensurePredicateNode returns + // the existing id, and the focused instance gains a + // *second* incoming edge ("superclass constraint") + // alongside the "instance context" one already there. + // + // (b) Otherwise this is a constraint defined *outside* the + // project. A fresh predicate node is created with role + // 'extern' (rendered gray), meaning "an instance must + // exist somewhere outside this project". + // + // In both cases the edge label is just "superclass + // constraint"; the predicate node carries class + args. + const pid = ensurePredicateNode( + sc.seSuperclass, reqArgs, 'extern', inst.iiTyVars + ); els.push({ group: 'edges', data: { - id: instId + '#sc#' + si + '#none', + id: instId + '#sc#' + si + '#extern', source: instId, - target: scClsId, + target: pid, kind: 'needs-external', - label: reqLabel + ' (no local match)', + label: reqLabel, }}); } else { // Local match(es) exist. Connect the focused instance directly @@ -1761,6 +1777,19 @@ 'font-family': 'ui-monospace, "SF Mono", Menlo, Consolas, monospace', }, }, + // 'extern' predicate — an unmatched superclass requirement that + // *isn't* in the instance context: an instance must exist, just + // not in this project. Greyed out to read as "external" / + // "unknown" at a glance. + { + selector: 'node[kind = "predicate"][role = "extern"]', + style: { + 'background-color': '#f3f4f6', + color: '#374151', + 'border-color': '#9ca3af', + 'border-style': 'dashed', + }, + }, // Orphan instances get a red dashed border, but only when the // global "Mark orphans" toggle is on. The toggle adds the // `.show-orphan` class to every orphan node in the graph; we only -- 2.54.0