Unify unmatched superclass with context predicate node

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) <[email protected]>

diff --git a/data/viewer.html b/data/viewer.html
index ebdbbfb168cd2428f5ce3a620b480a67963f2a98..d1928380af21753452ee1eaa1cfb5c7b1fd793d9 100644 (file)
--- a/data/viewer.html
+++ b/data/viewer.html
@@ -50,8 +50,8 @@
           <h4>Instance-view edges</h4>
           <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge solid green"></span></span><span>Class defines this instance</span></div>
           <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge dotted purple"></span></span><span>Instance context — points at a predicate node</span></div>
-          <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge solid amber"></span></span><span>Instance needs a superclass instance (matched locally)</span></div>
-          <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge dashed gray"></span></span><span>Needs a superclass instance (no local match)</span></div>
+          <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge solid amber"></span></span><span>Superclass constraint, satisfied by an instance in this project</span></div>
+          <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge dashed gray"></span></span><span>Superclass constraint, points at a predicate node (external or context)</span></div>
           <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge solid violet"></span></span><span>Family → one of its type family instances</span></div>
           <div class="legend-row"><span class="swatch swatch-edge-wrap"><span class="swatch-edge dotted teal"></span></span><span>Type family instance resolves to a class instance (chain)</span></div>
 

diff --git a/data/viewer.js b/data/viewer.js
index d0f0822a92cb3bc4ebd8494880292f5ec15c48be..060c73936dfe0480e628472e3f58b280d5641fa2 100644 (file)
--- 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