design-md-consolidation audit-tidy: close 3 architect drift items (Def kinds class/instance + Type::Forall constraints + letrec correction)

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`.