feat: recursive data types as iso-recursive mu, with fold and unfold (E9, D7)

TEST-NEEDS.adoc

@@ -21,9 +21,9 @@ compliance, 16 tests)
 performance, correctness, 13 tests)
 * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`,
 `+src/ephapax-vram-cache/benches/cache_bench.rs+`
-* Total: *625 tests* (`+cargo test --workspace --all-targets+`);
+* Total: *633 tests* (`+cargo test --workspace --all-targets+`);
 pass/fail enforced by `+rust-ci.yml+`
-* Documented all-target tests: 625
+* Documented all-target tests: 633
 
 === CRG Testing Taxonomy — Status
 
@@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4)
 ==== Build & Execution
 
 * [x] cargo build — compiles
-* [x] cargo test –workspace –all-targets — 625 pass, 0 fail
+* [x] cargo test –workspace –all-targets — 633 pass, 0 fail
 * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green
 (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated
 compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays

docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc

@@ -1395,6 +1395,8 @@ Ephapax's soundness statements are *theory* under PROOF-POLICY §1: the typing j
 
 === D7 — Recursive types
 
+*Ratified 2026-11-10 (owner):* the recommended option, iso-recursive `TMu` with fold/unfold inserted by desugar. Its first use is rung E9 in the Rust implementation (gate `src/ephapax-cli/tests/recursive_types.rs`), behind `--unstable-core`. In that step a `data` type can refer only to itself: a cycle through another `data` type, and a reference with other type arguments, are named errors.
+
 [cols="3,1,1,4",options="header"]
 |===
 |Option |(a) |(b) |Comment

ephapax-linear/src/affine.rs

@@ -179,7 +179,10 @@ impl AffineChecker {
                 self.walk_expr(inner);
             }
 
-            ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => {
+            ExprKind::Inl { value, .. }
+            | ExprKind::Inr { value, .. }
+            | ExprKind::Fold { value, .. }
+            | ExprKind::Unfold(value) => {
                 self.walk_expr(value);
             }
 

ephapax-linear/src/linear.rs

@@ -210,7 +210,10 @@ impl LinearChecker {
             }
 
             // --- Sum injections ---
-            ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => {
+            ExprKind::Inl { value, .. }
+            | ExprKind::Inr { value, .. }
+            | ExprKind::Fold { value, .. }
+            | ExprKind::Unfold(value) => {
                 self.walk_expr(value);
             }
 

scripts/probe-battery.sh

@@ -34,7 +34,9 @@
 # Verdicts: ok | ok:<value> | error:<Kind> | crash:<exit>[-stack-overflow]
 #   | timeout | no-module | unavailable:no-wasmtime
 # Kinds: InvalidWasm AnnotationNotEnforced CodegenError DesugarError
-#   TypeError ParseError RuntimeError Other, and Trap:<message> (wasm-run)
+#   TypeError ParseError RuntimeError UnstableCore Other, and
+#   Trap:<message> (wasm-run). UnstableCore: a form that is behind the
+#   flag `--unstable-core` (v2 plan rung E9), which the battery does not give.
 #
 # Output: a TSV on stdout (or --out FILE), one line per row:
 #   file  command  exit  verdict  status  baseline  target  diagnostic
@@ -74,7 +76,7 @@ while [ $# -gt 0 ]; do
     --bin) bin="$2"; shift 2 ;;
     --out) out="$2"; shift 2 ;;
     --update) update=1; shift ;;
-    -h|--help) sed -n '2,59p' "$0"; exit 0 ;;
+    -h|--help) sed -n '2,62p' "$0"; exit 0 ;;
     *) echo "probe-battery: unknown argument $1" >&2; exit 3 ;;
   esac
 done
@@ -154,6 +156,7 @@ classify() {
   elif grep -q 'Type error' <<<"$text"; then kind=TypeError
   elif grep -qi 'parse error' <<<"$text"; then kind=ParseError
   elif grep -q 'Runtime error' <<<"$text"; then kind=RuntimeError
+  elif grep -q 'behind the flag `--unstable-core`' <<<"$text"; then kind=UnstableCore
   fi
   echo "error:$kind"
 }

src/ephapax-analysis/src/escape.rs

@@ -134,7 +134,10 @@ impl EscapeAnalysis {
                 Self::analyze_expr(inner, escaping, in_escaping_context);
             }
 
-            ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => {
+            ExprKind::Inl { value, .. }
+            | ExprKind::Inr { value, .. }
+            | ExprKind::Fold { value, .. }
+            | ExprKind::Unfold(value) => {
                 Self::analyze_expr(value, escaping, in_escaping_context);
             }
 

src/ephapax-analysis/src/free_vars.rs

@@ -139,7 +139,10 @@ impl FreeVarAnalysis {
                 Self::collect(right, free, bound);
             }
 
-            ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => {
+            ExprKind::Inl { value, .. }
+            | ExprKind::Inr { value, .. }
+            | ExprKind::Fold { value, .. }
+            | ExprKind::Unfold(value) => {
                 Self::collect(value, free, bound);
             }
 

src/ephapax-analysis/src/liveness.rs

@@ -144,7 +144,10 @@ impl LivenessAnalysis {
                 Self::compute(right, live);
             }
 
-            ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => {
+            ExprKind::Inl { value, .. }
+            | ExprKind::Inr { value, .. }
+            | ExprKind::Fold { value, .. }
+            | ExprKind::Unfold(value) => {
                 Self::compute(value, live);
             }
 

src/ephapax-cli/src/main.rs

@@ -42,8 +42,9 @@ struct Cli {
     verbose: bool,
 
     /// Accept the forms of the core language that the proofs do not cover
-    /// yet (v2 plan rung E9): a lambda with an I64, F32 or F64 parameter
-    /// or result. Applies to `run`, `check` and `compile`.
+    /// yet (v2 plan rung E9): a recursive `data` type, and a lambda with
+    /// an I64, F32 or F64 parameter or result. Applies to `run`, `check`
+    /// and `compile`.
     #[arg(long, global = true)]
     unstable_core: bool,
 }

src/ephapax-cli/tests/linearity_holes.rs

@@ -419,21 +419,63 @@ fn list_index_from_linear_list_rejected() {
     assert_cli_rejects("listidx", LISTIDX);
 }
 
+/// `rec1` has a `data` type that refers to itself. It aborted the compiler
+/// with a stack overflow, and then it was a named desugar error. Since
+/// rung E9 the core has recursive types: the probe desugars and checks,
+/// and the command line refuses it by name without `--unstable-core`.
 #[test]
-fn rec1_is_a_named_desugar_error_not_a_crash() {
-    match pipeline(REC1) {
-        Err(PipelineError::Desugar(DesugarError::RecursiveType { name, .. })) => {
-            assert_eq!(name, "L");
-        }
-        other => panic!("expected DesugarError::RecursiveType, got {other:?}"),
-    }
+fn rec1_is_behind_the_flag_not_a_crash() {
+    assert!(pipeline(REC1).is_ok(), "{:?}", pipeline(REC1));
     let stderr = assert_cli_rejects("rec1", REC1);
     assert!(
-        stderr.contains("recursive type `L`"),
-        "stderr should name the recursive type:\n{stderr}"
+        stderr.contains("behind the flag `--unstable-core`: the recursive type `L`"),
+        "stderr should name the flag and the recursive type:\n{stderr}"
+    );
+
+    let dir = tempfile::tempdir().expect("tempdir");
+    let path = write_probe(dir.path(), "rec1", REC1);
+    let out = Command::new(ephapax_bin())
+        .args(["check", "--unstable-core"])
+        .arg(&path)
+        .output()
+        .expect("run ephapax check");
+    assert!(
+        out.status.success(),
+        "with the flag:\n{}",
+        String::from_utf8_lossy(&out.stderr)
     );
 }
 
+/// Each recursive form that has no lowering is a named desugar error.
+#[test]
+fn a_recursive_form_with_no_lowering_is_a_named_desugar_error() {
+    let refused = |src: &str| match pipeline(src) {
+        Err(PipelineError::Desugar(error)) => error,
+        other => panic!("expected a desugar error, got {other:?}"),
+    };
+    // 2 `data` types that refer to each other.
+    assert!(matches!(
+        refused(
+            "data Tree = Leaf | Node(Forest)\ndata Forest = FNil | FCons(Tree, Forest)\n\
+             fn f(t: Tree): I32 = 0\nfn main(): I32 = 0\n"
+        ),
+        DesugarError::MutualRecursion { cycle } if cycle == "Tree -> Forest -> Tree"
+    ));
+    // A `data` type that refers to itself with other type arguments.
+    assert!(matches!(
+        refused(
+            "data Grow(a) = Stop | More(Grow((a, a)))\nfn f(t: Grow(I32)): I32 = 0\n\
+             fn main(): I32 = 0\n"
+        ),
+        DesugarError::NonRegularRecursion { name, .. } if name == "Grow"
+    ));
+    // A `type` alias that refers to itself with no `data` type between.
+    assert!(matches!(
+        refused("type A = (I32, B)\ntype B = (I32, A)\nfn f(t: A): I32 = 0\nfn main(): I32 = 0\n"),
+        DesugarError::RecursiveAlias { .. }
+    ));
+}
+
 #[test]
 fn nested_data_application_is_not_mistaken_for_recursion() {
     let src = "\