From 63df0c085c0c36c7290a1b24309ce053f42513a5 Mon Sep 17 00:00:00 2001
From: Brummel <mould@mycelium.de>
Date: Sun, 10 May 2026 13:20:40 +0200
Subject: [PATCH] design-md-consolidation audit-tidy: close 3 architect drift
 items (Def kinds class/instance + Type::Forall constraints + letrec
 correction)

---
 docs/DESIGN.md | 47 +++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 41 insertions(+), 6 deletions(-)

diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 663b742..a594723 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1732,7 +1732,8 @@ contract is what makes growing the schema cheap.
 
 ### Def
 
-`kind ∈ { "fn", "const", "type" }`. All three are real surface forms.
+`kind ∈ { "fn", "const", "type", "class", "instance" }`. All five
+are real surface forms.
 
 ```jsonc
 // fn (the unit that gets a content hash)
@@ -1764,6 +1765,32 @@ contract is what makes growing the schema cheap.
   "doc": "<optional string>",
   "drop-iterative": true   // opt-in; omitted when false (hash-stable when omitted)
 }
+
+// class (typeclass declaration; see Decision 11)
+{ "kind": "class",
+  "name": "<id>",          // class name (e.g. "Show")
+  "param": "<id>",          // single class parameter, kind *
+  "superclass": null,       // or { "class": "<id>", "type": "<param>" }
+  "methods": [
+    { "name": "<id>",
+      "type": Type,         // FnSig over the class param
+      "default": Term       // optional fallback body; null = abstract-required
+    }
+    ...
+  ],
+  "doc": "<optional string>"
+}
+
+// instance (typeclass instance; see Decision 11)
+{ "kind": "instance",
+  "class": "<id>",          // class being instantiated
+  "type": Type,             // concrete type expression (never the class param)
+  "methods": [
+    { "name": "<id>", "body": Term }
+    ...
+  ],
+  "doc": "<optional string>"
+}
 ```
 
 **`Suppress`** (entry in `FnDef.suppress`):
@@ -1872,8 +1899,12 @@ Patterns are linear: each pattern variable may appear at most once.
 
 { "k": "var", "name": "<id>" }
 
-// Top-level polymorphism only.
-{ "k": "forall", "vars": ["<id>"...], "body": Type }
+// Top-level polymorphism only. `constraints` carries class
+// constraints (Decision 11); omitted when empty (hash-stable when omitted).
+{ "k": "forall",
+  "vars": ["<id>"...],
+  "constraints": [{ "class": "<id>", "type": "<id>" }, ...],
+  "body": Type }
 ```
 
 **`ParamMode`** (Decision 10):
@@ -1987,9 +2018,13 @@ as iterations land; the JOURNAL records when.
   instantiation, deferred.
 - No higher-rank polymorphism. Passing a polymorphic fn to another
   polymorphic fn (`apply(id, 42)`) is not supported.
-- No local recursive `let`. `let f = ... in ...` only sees `f`'s
-  binding inside the body, not inside its own RHS — recursion needs
-  a top-level def.
+- No recursive `let` for non-fn values. Plain `let x = … in …` only
+  sees `x` inside the body, not inside its own RHS — recursive value
+  bindings would break Decision 10's acyclicity invariant. Recursive
+  *fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
+  ... }`); the desugar pass lifts most occurrences to a synthetic
+  top-level fn, with `lift_letrecs` finishing the residue after
+  typecheck.
 - No visibility rules in imports. Every top-level def of an imported module
   is reachable; there is no `pub` / `priv`.