Iter 6: deps hardening, multi-diagnose, DESIGN audit

- ail deps now filters builtins, fn params, and let/match-pattern
  bindings. New value_names() in ailang-check::builtins is the single
  source of truth shared with the typechecker install path. walk_term
  threads a scope set; qualified `prefix.def` refs pass through.
- check_in_workspace returns Vec<CheckError>; check_workspace
  accumulates body diagnostics across defs and modules. Pass-1
  (top-level symbol table) and per-module type-def setup stay
  fail-fast — corrupt env would taint later diagnostics.
- DESIGN.md "What the MVP is NOT" was lying (ADTs, strings landed
  in Iter 2/3). Renamed to "What is not (yet) supported" and split
  into "not yet" + supported/smoke-tested. JOURNAL Iter 6 entry
  records the architecture self-check.

Tests: 47 green (was 44). +2 deps filter tests in e2e,
+1 multi-diagnose test in ailang-check workspace integration.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

crates/ail/src/main.rs

@@ -735,11 +735,32 @@ fn workspace_error_to_diagnostic(
     }
 }
 
+/// Collects the *external* references of a definition: everything its body
+/// depends on that lives outside the def itself. Filtered out:
+///
+/// - **Built-ins** (`+`, `-`, `==`, `not`, …): operators provided by the
+///   runtime, not the user. The list is owned by `ailang_check::builtins`.
+/// - **Parameters** of the surrounding `fn`.
+/// - **Local bindings** introduced by `let` and by pattern variables in
+///   `match` arms.
+///
+/// Cross-module references (`<prefix>.<def>`) are always kept — a local
+/// binding can never shadow a dotted name (the typechecker rejects defs
+/// with a dot, see DESIGN.md "qualified cross-module references").
 fn collect_refs(def: &ailang_core::Def) -> std::collections::BTreeSet<String> {
     let mut out = std::collections::BTreeSet::new();
+    let builtins: std::collections::HashSet<&'static str> =
+        ailang_check::builtins::value_names().into_iter().collect();
     match def {
-        ailang_core::Def::Fn(f) => walk_term(&f.body, &mut out),
-        ailang_core::Def::Const(c) => walk_term(&c.value, &mut out),
+        ailang_core::Def::Fn(f) => {
+            let mut scope: std::collections::HashSet<String> =
+                f.params.iter().cloned().collect();
+            walk_term(&f.body, &mut out, &builtins, &mut scope);
+        }
+        ailang_core::Def::Const(c) => {
+            let mut scope = std::collections::HashSet::new();
+            walk_term(&c.value, &mut out, &builtins, &mut scope);
+        }
         ailang_core::Def::Type(td) => {
             // A type def references the types of its fields.
             for c in &td.ctors {
@@ -754,54 +775,103 @@ fn collect_refs(def: &ailang_core::Def) -> std::collections::BTreeSet<String> {
     out
 }
 
-fn walk_term(t: &ailang_core::Term, out: &mut std::collections::BTreeSet<String>) {
+fn walk_term(
+    t: &ailang_core::Term,
+    out: &mut std::collections::BTreeSet<String>,
+    builtins: &std::collections::HashSet<&'static str>,
+    scope: &mut std::collections::HashSet<String>,
+) {
     use ailang_core::Term;
     match t {
         Term::Lit { .. } => {}
         Term::Var { name } => {
+            // Qualified (`prefix.def`) — always external; the typechecker
+            // forbids dots in def names, so no shadowing risk.
+            if name.contains('.') {
+                out.insert(name.clone());
+                return;
+            }
+            if scope.contains(name) || builtins.contains(name.as_str()) {
+                return;
+            }
             out.insert(name.clone());
         }
         Term::App { callee, args } => {
-            walk_term(callee, out);
+            walk_term(callee, out, builtins, scope);
             for a in args {
-                walk_term(a, out);
+                walk_term(a, out, builtins, scope);
             }
         }
-        Term::Let { value, body, .. } => {
-            walk_term(value, out);
-            walk_term(body, out);
+        Term::Let { name, value, body } => {
+            // `value` is in the outer scope; only `body` sees the binding.
+            walk_term(value, out, builtins, scope);
+            let inserted = scope.insert(name.clone());
+            walk_term(body, out, builtins, scope);
+            if inserted {
+                scope.remove(name);
+            }
         }
         Term::If { cond, then, else_ } => {
-            walk_term(cond, out);
-            walk_term(then, out);
-            walk_term(else_, out);
+            walk_term(cond, out, builtins, scope);
+            walk_term(then, out, builtins, scope);
+            walk_term(else_, out, builtins, scope);
         }
         Term::Do { op, args } => {
             // Mark effect ops as `effect:io/print_int` so they can be
             // separated from normal function calls.
             out.insert(format!("effect:{op}"));
             for a in args {
-                walk_term(a, out);
+                walk_term(a, out, builtins, scope);
             }
         }
         Term::Ctor { type_name, ctor, args } => {
             out.insert(format!("ctor:{type_name}/{ctor}"));
             for a in args {
-                walk_term(a, out);
+                walk_term(a, out, builtins, scope);
             }
         }
         Term::Match { scrutinee, arms } => {
-            walk_term(scrutinee, out);
+            walk_term(scrutinee, out, builtins, scope);
             for arm in arms {
                 if let ailang_core::ast::Pattern::Ctor { ctor, .. } = &arm.pat {
                     out.insert(format!("ctor:{ctor}"));
                 }
-                walk_term(&arm.body, out);
+                let bound = bind_pattern(&arm.pat, scope);
+                walk_term(&arm.body, out, builtins, scope);
+                for n in bound {
+                    scope.remove(&n);
+                }
             }
         }
     }
 }
 
+/// Adds the variable bindings introduced by a pattern to `scope` and
+/// returns the names that were freshly inserted (so the caller can roll
+/// them back). MVP-restricted: nested ctor patterns only contain
+/// `Var`/`Wild` — see DESIGN.md.
+fn bind_pattern(
+    p: &ailang_core::ast::Pattern,
+    scope: &mut std::collections::HashSet<String>,
+) -> Vec<String> {
+    use ailang_core::ast::Pattern;
+    let mut added = Vec::new();
+    match p {
+        Pattern::Wild | Pattern::Lit { .. } => {}
+        Pattern::Var { name } => {
+            if scope.insert(name.clone()) {
+                added.push(name.clone());
+            }
+        }
+        Pattern::Ctor { fields, .. } => {
+            for sub in fields {
+                added.extend(bind_pattern(sub, scope));
+            }
+        }
+    }
+    added
+}
+
 // --- ail diff -------------------------------------------------------------
 
 /// Purely structural module diff. Top-level defs are identified by

crates/ail/tests/e2e.rs

@@ -349,6 +349,73 @@ fn describe_workspace_resolves_qualified_name() {
     );
 }
 
+/// Guards Iter 6: `ail deps` no longer surfaces built-ins, params, or
+/// let-bindings as edges. The single-module `sum` def in `sum.ail.json`
+/// uses `+`, `-`, `==`, the param `n`, and the recursive call `sum`.
+/// Only the recursive call must remain.
+#[test]
+fn deps_filters_builtins_params_locals() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
+    let src = workspace.join("examples").join("sum.ail.json");
+
+    let output = Command::new(ail_bin())
+        .args(["deps", src.to_str().unwrap(), "--of", "sum", "--json"])
+        .output()
+        .expect("ail deps failed to run");
+    assert!(
+        output.status.success(),
+        "ail deps exited non-zero; stderr: {}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+
+    let stdout = String::from_utf8(output.stdout).expect("stdout utf8");
+    let v: serde_json::Value = serde_json::from_str(stdout.trim()).expect("valid JSON");
+    let arr = v.as_array().expect("array of {name, refs}");
+    let entry = arr
+        .iter()
+        .find(|e| e["name"].as_str() == Some("sum"))
+        .expect("sum entry present");
+    let refs: Vec<&str> = entry["refs"]
+        .as_array()
+        .expect("refs array")
+        .iter()
+        .filter_map(|x| x.as_str())
+        .collect();
+    assert_eq!(
+        refs,
+        vec!["sum"],
+        "expected only the recursive call `sum`; got {refs:?}"
+    );
+}
+
+/// Guards Iter 6 in workspace mode: edges into built-ins (`ws_lib.+`)
+/// and into the params (`ws_lib.a`, `ws_lib.b`) of `ws_lib.add` must be
+/// gone after the deps refactor.
+#[test]
+fn deps_workspace_filters_builtins_and_params() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
+    let entry = workspace.join("examples").join("ws_main.ail.json");
+
+    let output = Command::new(ail_bin())
+        .args(["deps", entry.to_str().unwrap(), "--workspace", "--json"])
+        .output()
+        .expect("ail deps --workspace failed to run");
+    assert!(output.status.success());
+
+    let stdout = String::from_utf8(output.stdout).expect("stdout utf8");
+    let v: serde_json::Value = serde_json::from_str(stdout.trim()).expect("valid JSON");
+    let edges = v["edges"].as_array().expect("edges array");
+
+    for e in edges {
+        let to_def = e.get("to_def").and_then(|x| x.as_str()).unwrap_or("");
+        assert_ne!(to_def, "+", "built-in `+` must not appear: {e}");
+        assert_ne!(to_def, "a", "param `a` must not appear: {e}");
+        assert_ne!(to_def, "b", "param `b` must not appear: {e}");
+    }
+}
+
 /// Guards Iter 5d: `ail deps --workspace` contains a cross-module edge
 /// `ws_main.main -> ws_lib.add`, because `ws_main` calls `ws_lib.add(2,3)`.
 #[test]

crates/ailang-check/src/builtins.rs

@@ -61,6 +61,21 @@ pub fn install(env: &mut crate::Env) {
     );
 }
 
+/// Names of value-level built-ins (operators, `not`) — the ones that
+/// show up as `Term::Var { name }` references in user code. Effect ops
+/// are excluded because they reach codegen via `Term::Do`, not `Var`.
+///
+/// Single source of truth: derived from `list()` by filtering out the
+/// effect-op rows. Kept as a function (not a `const`) because `list()`
+/// already allocates; this is only consulted by tooling (`ail deps`).
+pub fn value_names() -> Vec<&'static str> {
+    list()
+        .into_iter()
+        .filter(|(_, sig)| !sig.contains("[effect op]"))
+        .map(|(n, _)| n)
+        .collect()
+}
+
 /// Returns the list of all registered built-ins. Useful for the CLI subcommand
 /// `ail builtins`, when the LLM wants to check expected signatures.
 pub fn list() -> Vec<(&'static str, &'static str)> {

crates/ailang-check/src/lib.rs

@@ -211,9 +211,16 @@ impl CheckError {
 
 /// Top-level API for structured diagnostics.
 ///
-/// Empty Vec = green. In the current state, processing aborts on the first
-/// error, so the Vec contains either 0 or 1 element. Multiple diagnostics
-/// per run are a future feature; the format already allows them.
+/// Empty Vec = green. From Iter 6 onwards the body-check phase is
+/// multi-diagnose: each def in each module is checked independently and
+/// failures accumulate, so a single `ail check` run reports every
+/// independent body error in the workspace.
+///
+/// Pass-1 errors (top-level symbol-table construction:
+/// `invalid-def-name`, `duplicate-def`) are still fail-fast — those
+/// errors corrupt the symbol table, and any further diagnostic would be
+/// unreliable. Likewise, the type-def installation is fail-fast within
+/// a single module, but other modules continue being checked.
 ///
 /// Backwards compatibility: a bare `&Module` is internally lifted into a
 /// trivial workspace (`modules = {m.name: m}`, `entry = m.name`) so that
@@ -241,8 +248,10 @@ pub fn check_module(m: &Module) -> Vec<Diagnostic> {
 /// as `<prefix>.<def>`; `<prefix>` is an import alias (or the module name,
 /// if imported without an alias).
 ///
-/// As with `check_module`: at most **one** diagnostic per run
-/// (single-shot). Multi-diagnostic is a future feature.
+/// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
+/// Pass-1 (symbol table) stays fail-fast — see `check_module`.
+/// Module iteration order is deterministic: entry first, then the rest in
+/// BTreeMap order, so output ordering is stable.
 pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
     // Pass 1: build per-module top-level symbol table — without checking
     // bodies. This lets module A access defs from module B even when B
@@ -255,10 +264,8 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
     };
 
     // Pass 2: body-check per module. `check_in_workspace` builds the env
-    // with additional cross-module globals and an import map.
-    // Iteration order: entry module first, then the rest in
-    // BTreeMap order. This makes the first reported diagnostic for
-    // workspaces deterministic and close to the entry.
+    // with additional cross-module globals and an import map. Errors
+    // accumulate across modules.
     let mut order: Vec<&String> = Vec::new();
     if ws.modules.contains_key(&ws.entry) {
         order.push(&ws.entry);
@@ -268,13 +275,14 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
             order.push(name);
         }
     }
+    let mut diagnostics: Vec<Diagnostic> = Vec::new();
     for name in order {
         let m = &ws.modules[name];
-        if let Err(e) = check_in_workspace(m, ws, &module_globals) {
-            return vec![e.to_diagnostic()];
+        for e in check_in_workspace(m, ws, &module_globals) {
+            diagnostics.push(e.to_diagnostic());
         }
     }
-    Vec::new()
+    diagnostics
 }
 
 /// Result of typechecking a module: mapping from symbol name to
@@ -294,7 +302,12 @@ pub fn check(m: &Module) -> Result<CheckedModule> {
         root_dir: std::path::PathBuf::from("."),
     };
     let module_globals = build_module_globals(&ws)?;
-    check_in_workspace(m, &ws, &module_globals)?;
+    // `check` keeps single-error semantics for callers (snapshot tests,
+    // legacy code). Multi-diagnose is exposed via `check_module` /
+    // `check_workspace`.
+    if let Some(first) = check_in_workspace(m, &ws, &module_globals).into_iter().next() {
+        return Err(first);
+    }
     // Collect symbols for the return value (existing semantics).
     let mut symbols = IndexMap::new();
     for def in &m.defs {
@@ -354,27 +367,38 @@ fn build_module_globals(
 /// Assumption: `module_globals` already contains the top-level symbol
 /// tables for **all** modules of the workspace (including `m`) — built
 /// by `build_module_globals`.
+///
+/// Returns **all** errors found in this module, in def declaration order:
+///
+/// - The type-def setup phase is fail-fast within the module (duplicate
+///   type or ctor names corrupt the env, so we abort *this* module after
+///   the first such error and let the outer loop continue with others).
+/// - The body-check phase is multi-diagnose: each def is checked
+///   independently against the assembled env; a failure is recorded and
+///   the next def is attempted.
 fn check_in_workspace(
     m: &Module,
     ws: &Workspace,
     module_globals: &BTreeMap<String, IndexMap<String, Type>>,
-) -> Result<()> {
+) -> Vec<CheckError> {
     let mut env = Env::new();
     builtins::install(&mut env);
+    let mut errors: Vec<CheckError> = Vec::new();
 
     // Register type defs (local per module; cross-module ADT sharing is
     // explicitly not part of 5b).
     for def in &m.defs {
         if let Def::Type(td) = def {
             if env.types.contains_key(&td.name) {
-                return Err(CheckError::Def(
+                errors.push(CheckError::Def(
                     td.name.clone(),
                     Box::new(CheckError::DuplicateType(td.name.clone())),
                 ));
+                return errors;
             }
             for c in &td.ctors {
                 if let Some(prev) = env.ctor_index.get(&c.name) {
-                    return Err(CheckError::Def(
+                    errors.push(CheckError::Def(
                         td.name.clone(),
                         Box::new(CheckError::DuplicateCtor {
                             ctor: c.name.clone(),
@@ -382,6 +406,7 @@ fn check_in_workspace(
                             b: td.name.clone(),
                         }),
                     ));
+                    return errors;
                 }
                 env.ctor_index.insert(
                     c.name.clone(),
@@ -421,9 +446,11 @@ fn check_in_workspace(
     let _ = ws;
 
     for def in &m.defs {
-        check_def(def, &env).map_err(|e| CheckError::Def(def.name().to_string(), Box::new(e)))?;
+        if let Err(e) = check_def(def, &env) {
+            errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
+        }
     }
-    Ok(())
+    errors
 }
 
 fn check_def(def: &Def, env: &Env) -> Result<()> {

crates/ailang-check/tests/workspace.rs

@@ -99,3 +99,72 @@ fn invalid_def_name_with_dot_is_reported() {
         Some("contains-dot")
     );
 }
+
+/// Iter 6: body-check is multi-diagnose. A module with two independent
+/// errors in different defs must produce two diagnostics — the first
+/// error must not short-circuit the second.
+#[test]
+fn body_errors_accumulate_across_defs() {
+    use ailang_core::ast::*;
+    use std::collections::BTreeMap;
+
+    // Two fns, each with a different body error:
+    //   bad_a: arity mismatch — calls `+` with three arguments.
+    //   bad_b: references a name that does not exist anywhere.
+    let bad_a = Def::Fn(FnDef {
+        name: "bad_a".into(),
+        ty: Type::Fn {
+            params: vec![],
+            ret: Box::new(Type::int()),
+            effects: vec![],
+        },
+        params: vec![],
+        body: Term::App {
+            callee: Box::new(Term::Var { name: "+".into() }),
+            args: vec![
+                Term::Lit { lit: Literal::Int { value: 1 } },
+                Term::Lit { lit: Literal::Int { value: 2 } },
+                Term::Lit { lit: Literal::Int { value: 3 } },
+            ],
+        },
+        doc: None,
+    });
+    let bad_b = Def::Fn(FnDef {
+        name: "bad_b".into(),
+        ty: Type::Fn {
+            params: vec![],
+            ret: Box::new(Type::int()),
+            effects: vec![],
+        },
+        params: vec![],
+        body: Term::Var {
+            name: "this_does_not_exist".into(),
+        },
+        doc: None,
+    });
+
+    let m = Module {
+        schema: ailang_core::SCHEMA.into(),
+        name: "two_errors".into(),
+        imports: vec![],
+        defs: vec![bad_a, bad_b],
+    };
+    let mut modules = BTreeMap::new();
+    modules.insert(m.name.clone(), m.clone());
+    let ws = ailang_core::Workspace {
+        entry: m.name.clone(),
+        modules,
+        root_dir: std::path::PathBuf::from("."),
+    };
+    let diags = check_workspace(&ws);
+
+    assert_eq!(diags.len(), 2, "want both errors, got: {:#?}", diags);
+
+    // Each diagnostic carries the offending def name as `def`.
+    let defs: Vec<&str> = diags
+        .iter()
+        .filter_map(|d| d.def.as_deref())
+        .collect();
+    assert!(defs.contains(&"bad_a"), "missing bad_a; got {defs:?}");
+    assert!(defs.contains(&"bad_b"), "missing bad_b; got {defs:?}");
+}