fix(hy-check): reject untyped nil local declarations (var x = nil / x := nil / let x = nil) with HYB-E4003, the N1 untyped leg (fixes #672)

compiler/crates/hy-check/src/closures.rs

@@ -487,6 +487,18 @@ fn check_stmt_boundaries<'a>(ck: &mut Checker<'_>, st: &mut FnState, stmt: &'a S
                         );
                     }
                 }
+            } else if l.kind != LocalKind::Const {
+                // N1, untyped leg (HYB-E4003): a closure-body `var x = nil` /
+                // `x := nil` / `let x = nil` — same gap as the flat walk's
+                // process_local (no ascription → Unknown shape → the emitter
+                // emits `var x = nil`, which Go rejects). Local
+                // `const c = nil` is the E6003 constant-expression guard
+                // (issue #640) — different locus, do not double-fire.
+                for (name, value) in l.names.iter().zip(l.values.iter()) {
+                    if Checker::is_nil_literal(value) {
+                        ck.emit_untyped_nil_decl_error(name, value.span());
+                    }
+                }
             }
             for v in &l.values {
                 ck.check_composite_nils(st, v);

compiler/crates/hy-check/src/loans.rs

@@ -1567,6 +1567,17 @@ impl<'a> Checker<'a> {
                             );
                         }
                     }
+                } else if l.kind != LocalKind::Const
+                    && Checker::is_nil_literal(value)
+                {
+                    // N1, untyped leg (HYB-E4003): `var x = nil` / `x := nil`
+                    // / `let x = nil` — no ascription means nothing proves a
+                    // nil home, `shape_of_expr(nil)` is Unknown, and the
+                    // emitter emits `var x = nil`, which Go rejects outright
+                    // (`use of untyped nil in variable declaration`). Local
+                    // `const c = nil` is the E6003 constant-expression guard
+                    // (issue #640) — different locus, do not double-fire.
+                    self.emit_untyped_nil_decl_error(name, value.span());
                 }
                 // N1 for composite literals: `job{m: nil}` carries its own
                 // type context (the struct def / map value / slice elem) —

compiler/crates/hy-check/src/sendability.rs

@@ -907,6 +907,29 @@ impl<'a> Checker<'a> {
             .push(Diagnostic::error("HYB-E4001", self.path.clone(), span, msg).with_notes(notes));
     }
 
+    /// Emit HYB-E4003: an UNTYPED nil declaration — `var x = nil` / `x := nil`
+    /// / `let x = nil` (no ascription). The E4001 sites all require a declared
+    /// type to prove the nil against; with no ascription there is no type at
+    /// all, `shape_of_expr(nil)` is Unknown, and the checker used to accept the
+    /// declaration — then the emitter emitted `var x = nil`, which Go rejects
+    /// outright (`use of untyped nil in variable declaration`). nil has exactly
+    /// two homes (N1): `error` and the foreign-Go perimeter, and both must be
+    /// visible in a DECLARED type — an untyped nil can never name either.
+    pub(crate) fn emit_untyped_nil_decl_error(&mut self, name: &str, span: Span) {
+        let msg = format!(
+            "`{}` is declared from an untyped `nil`: Go rejects the emitted declaration (`use of untyped nil in variable declaration`)",
+            name
+        );
+        let notes = vec![
+            "why: nil has exactly two homes (N1) — `error` and the foreign-Go perimeter (N2) — and both must be visible in a DECLARED type; an untyped nil can never name either, so the emitted `var x = nil` fails `go build`".to_string(),
+            "fix: declare the nil home explicitly — `var e error = nil` (error's zero value) or `var h Foreign.handle = nil` at the foreign perimeter (N1/N2)".to_string(),
+            "fix: declare the binding without an initializer — the zero value of the intended type IS the value (N3): `var ch chan int` (zero channel), `var s []int` (zero slice), `var m map[string]int` (zero map)".to_string(),
+            "fix: if absence is the meaning, use `option[T]` — its zero value is `none` (N3)".to_string(),
+        ];
+        self.diags
+            .push(Diagnostic::error("HYB-E4003", self.path.clone(), span, msg).with_notes(notes));
+    }
+
     /// N1 for composite literals: `job{m: nil}` with a map-typed field used
     /// to pass the checker — classify_composite has no per-field type
     /// context, so the bare-nil check at the five direct-flow sites never

compiler/crates/hy-check/tests/untyped_nil_decl.rs

@@ -0,0 +1,204 @@
+//! untyped_nil_decl.rs — N1's untyped leg (HYB-E4003): `var x = nil`,
+//! `x := nil`, `let x = nil` — a declaration with NO ascription. The E4001
+//! sites all require a declared type to prove the nil against; with no
+//! ascription `shape_of_expr(nil)` is Unknown, the checker used to accept
+//! the declaration, and the emitter emitted `var x = nil` — which Go
+//! rejects outright (`use of untyped nil in variable declaration`).
+//! Accepted-but-unbuildable (BUILDABLE rule). Local `const c = nil` is
+//! the E6003 constant-expression guard (issue #640) — different locus.
+
+use hy_check::{check_file, Verdict};
+use hy_diag::Severity;
+use hy_syntax::parse_file;
+
+fn check(src: &str) -> hy_check::CheckResult {
+    let path = "inline.hy";
+    let ast = parse_file(path, src)
+        .unwrap_or_else(|diags| panic!("must parse (parser contract): {:?}", diags));
+    check_file(&ast)
+}
+
+fn codes(r: &hy_check::CheckResult) -> Vec<String> {
+    r.diagnostics
+        .iter()
+        .filter(|d| d.severity == Severity::Error)
+        .map(|d| d.code.clone())
+        .collect()
+}
+
+// ---------------------------------------------------------------------------
+// The four spellings that Go rejects: var x = nil / x := nil / let x = nil /
+// parallel untyped nil in a multi-value define.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn var_untyped_nil_is_e4003() {
+    let r = check("fn main() {\n    var ch = nil\n    _ = ch\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for `var ch = nil`, got {:?}",
+        cs
+    );
+    assert_eq!(r.verdict, Verdict::Reject);
+}
+
+#[test]
+fn short_define_untyped_nil_is_e4003() {
+    let r = check("fn main() {\n    ch := nil\n    _ = ch\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for `ch := nil`, got {:?}",
+        cs
+    );
+    assert_eq!(r.verdict, Verdict::Reject);
+}
+
+#[test]
+fn let_untyped_nil_is_e4003() {
+    let r = check("fn main() {\n    let x = nil\n    _ = x\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for `let x = nil`, got {:?}",
+        cs
+    );
+    assert_eq!(r.verdict, Verdict::Reject);
+}
+
+#[test]
+fn parallel_untyped_nil_is_e4003() {
+    // `a, b := nil, 1` — the nil half is an untyped declaration too.
+    let r = check("fn main() {\n    a, b := nil, 1\n    _ = a\n    _ = b\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for the nil half of `a, b := nil, 1`, got {:?}",
+        cs
+    );
+    assert_eq!(r.verdict, Verdict::Reject);
+}
+
+// ---------------------------------------------------------------------------
+// Every body shape: closure, loop, match arm, if-block — the flat walk and
+// the closure boundary walk both carry the check.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn closure_body_untyped_nil_is_e4003() {
+    let r = check(
+        "fn main() {\n    g := fn() {\n        var x = nil\n        _ = x\n    }\n    g()\n}\n",
+    );
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for a closure-body `var x = nil`, got {:?}",
+        cs
+    );
+}
+
+#[test]
+fn loop_body_untyped_nil_is_e4003() {
+    let r = check("fn main() {\n    for i in 0..3 {\n        var x = nil\n        _ = x\n    }\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for a loop-body `var x = nil`, got {:?}",
+        cs
+    );
+}
+
+#[test]
+fn match_arm_untyped_nil_is_e4003() {
+    let r = check(
+        "fn main() {\n    match 1 {\n        1 => {\n            var y = nil\n            _ = y\n        }\n        _ => {}\n    }\n}\n",
+    );
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for a match-arm `var y = nil`, got {:?}",
+        cs
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Locals named `_` still reject: the emitted Go `var _ = nil` is just as
+// unbuildable.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn blank_untyped_nil_is_e4003() {
+    let r = check("fn main() {\n    var _ = nil\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().any(|c| c == "HYB-E4003"),
+        "expected HYB-E4003 for `var _ = nil`, got {:?}",
+        cs
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Controls that must stay ACCEPTED — the nil HAS a declared home, or is not
+// a declaration at all.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn ascribed_error_nil_stays_legal() {
+    // N1 home #1, ascribed: `var e error = nil` is valid Go and Hybrid.
+    let r = check("fn main() {\n    var e error = nil\n    _ = e\n}\n");
+    assert!(
+        codes(&r).is_empty(),
+        "ascribed error-nil must stay legal, got {:?}",
+        codes(&r)
+    );
+    assert_eq!(r.verdict, Verdict::Accept);
+}
+
+#[test]
+fn bare_nil_arg_stays_legal() {
+    // `f(nil)` — the call site gives nil a type context; not a declaration.
+    let r = check("fn sink(m map[string]int) int { return m[\"k\"] }\n\nfn main() {\n    x := sink(nil)\n    _ = x\n}\n");
+    assert!(
+        codes(&r).iter().all(|c| c != "HYB-E4003"),
+        "bare nil as a call argument is not a declaration; got {:?}",
+        codes(&r)
+    );
+}
+
+#[test]
+fn bare_nil_compare_stays_legal() {
+    // `ch == nil` — a comparison, not a declaration.
+    let r = check("fn main() {\n    ch := make(chan int, 1)\n    if ch == nil {\n        return\n    }\n}\n");
+    assert!(
+        codes(&r).iter().all(|c| c != "HYB-E4003"),
+        "bare nil in a comparison is not a declaration; got {:?}",
+        codes(&r)
+    );
+}
+
+#[test]
+fn zero_value_decl_stays_legal() {
+    // The N3 fix-it route: declare without an initializer.
+    let r = check("fn main() {\n    var ch chan int\n    var s []int\n    var m map[string]int\n    _ = ch\n    _ = s\n    _ = m\n}\n");
+    assert!(
+        codes(&r).is_empty(),
+        "zero-value declarations must stay legal, got {:?}",
+        codes(&r)
+    );
+    assert_eq!(r.verdict, Verdict::Accept);
+}
+
+#[test]
+fn local_const_nil_is_not_e4003() {
+    // Local `const c = nil` is the E6003 constant-expression guard's locus
+    // (issue #640) — E4003 must not double-fire on it. (On main today the
+    // E6003 guard accepts nil literals; the fix lands via issue #640.)
+    let r = check("fn main() {\n    const c = nil\n    _ = c\n}\n");
+    let cs = codes(&r);
+    assert!(
+        cs.iter().all(|c| c != "HYB-E4003"),
+        "local `const c = nil` belongs to the E6003 guard (#640), not E4003; got {:?}",
+        cs
+    );
+}

compiler/crates/hy-diag/data/diagnostics.json

@@ -1,6 +1,6 @@
 {
   "version": 1,
-  "updated": "2026-10-15",
+  "updated": "2026-10-18",
   "format": "HYB-Exxxx registry (SPEC-LANGUAGE.md §9.6; append-only, never renumbered, never reused)",
   "categories": {
     "E0": "parse / lexical",
@@ -484,6 +484,22 @@
       "example": "var e option[int]   // reject: HYB-E4002 — option[T] has no zero value",
       "rule": "N"
     },
+    {
+      "code": "HYB-E4003",
+      "name": "untyped-nil-declaration",
+      "category": "nil-safety",
+      "severity": "error",
+      "title": "an untyped nil cannot declare a binding",
+      "summary": "`var x = nil` / `x := nil` / `let x = nil` leave the binding with no type at all — Go rejects the emitted declaration outright (`use of untyped nil in variable declaration`), so an accepted program would fail `go build`. nil has exactly two homes (N1): `error` and the foreign-Go perimeter, and both must be visible in a declared type.",
+      "fixits": [
+        "declare the nil home explicitly: `var e error = nil` (error's zero value) or `var h Foreign.handle = nil` at the foreign perimeter (N1/N2)",
+        "declare the binding without an initializer — the zero value of the intended type is the value (N3): `var ch chan int`, `var s []int`, `var m map[string]int`",
+        "if absence is the meaning, use `option[T]` — its zero value is `none` (N3)"
+      ],
+      "example": "var x = nil   // reject: HYB-E4003 — Go: use of untyped nil in variable declaration",
+      "rule": "N",
+      "tier0_rule_id": "N1"
+    },
     {
       "code": "HYB-E5001",
       "name": "match-not-exhaustive",

compiler/crates/hy-syntax/tests/parse_all.rs

@@ -1,6 +1,6 @@
 //! Integration test: EVERY must-parse file parses cleanly.
 //!
-//!   * tests/checker-corpus/*.hy            (79 programs — the checker corpus;
+//!   * tests/checker-corpus/*.hy            (80 programs — the checker corpus;
 //!     61-string-escape-fail-closed.hy is the corpus's first PARSE-reject
 //!     fixture and is pinned to fail closed instead)
 //!   * spikes/spike6-ownership/work/*.hy    (10 programs — Tier-0 rewrites)
@@ -49,7 +49,7 @@ fn must_parse(path: &PathBuf) {
 #[test]
 fn checker_corpus_all_parse() {
     let files = hy_files_under("tests/checker-corpus");
-    assert_eq!(files.len(), 79, "expected exactly 79 corpus programs",);
+    assert_eq!(files.len(), 80, "expected exactly 80 corpus programs",);
     // 61-string-escape-fail-closed.hy is the corpus's first PARSE-reject
     // fixture (a malformed LX7 string escape must be named by the lexer,
     // never silently accepted): it is excluded from the must-parse loop

tests/checker-corpus/VERDICTS.md

@@ -800,3 +800,11 @@ reproduction line above is the merged tree.
 - Verdict: REJECT FC, exact diagnostic HYB-E3005. Pins GUARANTEES.md row 11 at a task-spawn check site; scalar-atomic acceptance remains covered by corpus 17.
 - This registers existing fail-closed behavior; no checker rule or existing verdict changes.
 - Verified on the refreshed tree: 79/79 verdict agreement, tripwire not fired; ACCEPT 21 · ACCEPT-MANAGED 2 · REJECT 56.
+
+
+## Additive corpus registration - 2026-10-18: untyped nil declarations
+
+- Program: `untyped-nil-decl-reject.hy` (this change: new HYB-E4003, the N1 untyped leg).
+- Verdict: REJECT N1, exact diagnostic HYB-E4003. `var x = nil` / `x := nil` / `let x = nil` (no ascription) passed the checker with 0 diagnostics and emitted `var x = nil`, which Go rejects outright (`use of untyped nil in variable declaration`) - accepted-but-unbuildable (GUARANTEES row 13, BUILDABLE). nil has exactly two homes (N1): `error` and the foreign-Go perimeter, and both must be visible in a DECLARED type; an untyped nil can never name either.
+- Scope note: distinct from corpus 28 (nils nested in composite literals, which carry their own field/slot type context) and from the ascribed direct-nil E4001 sites (`var s []int = nil` - a declared type exists). Local `const c = nil` is the E6003 constant-expression guard's locus (issue #640; Go: "nil is not constant"), not E4003.
+- Unit pins: `hy-check/tests/untyped_nil_decl.rs` (13 tests: all four spellings, closure/loop/match-arm bodies, blank identifier; controls that stay accepted: ascribed error-nil, bare nil as call argument/compare, zero-value declarations).

tests/checker-corpus/untyped-nil-decl-reject.hy

@@ -0,0 +1,43 @@
+// ============================================================================
+// untyped-nil-decl-reject — N1's UNTYPED leg: `var x = nil` / `x := nil` /
+// `let x = nil` — a local declaration with NO ascription.
+//
+// PURPOSE: pin the checker reject for declarations whose only initializer is
+// an untyped `nil`. The ascribed E4001 sites (`var s []int = nil`) all
+// require a declared type to prove the nil against; with no ascription
+// `shape_of_expr(nil)` is Unknown, the checker used to accept the
+// declaration with 0 diagnostics, and the emitter emitted `var x = nil` —
+// which Go rejects outright (`use of untyped nil in variable declaration`).
+// Accepted-but-unbuildable (GUARANTEES row 13, BUILDABLE). nil has exactly
+// two homes (N1): `error` and the foreign-Go perimeter, and both must be
+// visible in a DECLARED type — an untyped nil can never name either.
+//
+// Distinct from 28-composite-nil-reject (nils NESTED in composite literals,
+// which carry their own field/slot type context) and from the ascribed
+// direct-nil sites (`var s []int = nil` — E4001, a declared type exists).
+// Distinct from local `const c = nil` (the E6003 constant-expression guard,
+// issue #640 — Go: "nil is not constant", a different Go error).
+//
+// Shapes pinned (one active, the rest commented alternates — same verdict):
+//   var ch = nil      /  ch := nil  /  let x = nil  /  a, b := nil, 1
+//   closure-body `var x = nil` (the closure boundary walk carries the check)
+// Controls that must stay ACCEPTED (do not add to this file):
+//   var e error = nil   — ascribed; error is nil's home (E4001 skips it)
+//   f(nil) / ch == nil  — call argument / comparison, not a declaration
+//   var ch chan int     — declare without initializer: the zero value (N3)
+//
+// EXPECTED-VERDICT: REJECT N1
+// EXPECTED-DIAGNOSTIC: HYB-E4003
+// ============================================================================
+
+fn main() {
+  // S1: the short define — Go: `use of untyped nil in variable declaration`.
+  ch := nil
+  _ = ch
+
+  // S2 alternates (same verdict, same code):
+  //   var ch2 = nil
+  //   let x = nil
+  //   a, b := nil, 1
+  //   g := fn() { var y = nil; _ = y }; g()
+}