diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs
index f705cd5..7f9b58b 100644
--- a/crates/ail/src/main.rs
+++ b/crates/ail/src/main.rs
@@ -399,7 +399,16 @@ fn main() -> Result<()> {
                             d.message,
                         );
                     }
-                    std::process::exit(1);
+                    // Iter 19a: only Error-severity diagnostics fail the
+                    // command. Warning-severity diagnostics (e.g. the
+                    // `over-strict-mode` lint) print to stderr but the
+                    // module is still considered to have typechecked.
+                    if diags
+                        .iter()
+                        .any(|d| matches!(d.severity, ailang_check::Severity::Error))
+                    {
+                        std::process::exit(1);
+                    }
                 }
                 let total: usize = ws.modules.values().map(|m| m.defs.len()).sum();
                 println!(
@@ -430,7 +439,13 @@ fn main() -> Result<()> {
                         d.message,
                     );
                 }
-                std::process::exit(1);
+                // Iter 19a: only Error-severity blocks codegen.
+                if diags
+                    .iter()
+                    .any(|d| matches!(d.severity, ailang_check::Severity::Error))
+                {
+                    std::process::exit(1);
+                }
             }
             let ir = ailang_codegen::lower_workspace(&ws)?;
             match out {
@@ -1653,7 +1668,15 @@ fn build_to(
                 d.message,
             );
         }
-        std::process::exit(1);
+        // Iter 19a: only Error-severity blocks the build. Warning-
+        // severity diagnostics (e.g. `over-strict-mode`) print but
+        // do not abort.
+        if diags
+            .iter()
+            .any(|d| matches!(d.severity, ailang_check::Severity::Error))
+        {
+            std::process::exit(1);
+        }
     }
     // Iter 16b.3: run `lift_letrecs` per module on the post-desugar
     // form. Codegen's internal desugar pass is idempotent on a
diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs
index 8c8e02b..ea35bbe 100644
--- a/crates/ailang-check/src/diagnostic.rs
+++ b/crates/ailang-check/src/diagnostic.rs
@@ -46,6 +46,14 @@
 //!   spell the fix in form-A AILang.
 //! - `consume-while-borrowed` — `ctx`: `{"binder": "<n>"}` (Iter 18c.2);
 //!   ditto on `suggested_rewrites`.
+//! - `over-strict-mode` (Iter 19a) — `severity: warning`. Emitted by
+//!   the linearity pass when a fn parameter is annotated `(own T)` but
+//!   the body never consumes it (and never destructures it via
+//!   `match`). `ctx`: `{"binder": "<n>", "current_mode": "own",
+//!   "suggested_mode": "borrow"}`. Carries one
+//!   [`SuggestedRewrite`] whose `replacement` is the relaxed
+//!   `(fn-type ...)` in form-A. Pure advisory; the typechecker still
+//!   accepts the original signature.
 
 use serde::Serialize;
 
@@ -53,15 +61,16 @@ use serde::Serialize;
 ///
 /// Serializes as a lowercase string (`"error"` / `"warning"`) so that
 /// `ail check --json` consumers can branch on it without parsing prose.
-/// The MVP only emits [`Severity::Error`]; [`Severity::Warning`] is
-/// reserved for future lints.
+/// Iter 19a is the first iter to emit [`Severity::Warning`] (via the
+/// linearity-pass `over-strict-mode` lint); pre-19a the variant was
+/// reserved.
 #[derive(Serialize, Debug, Clone, Copy, PartialEq, Eq)]
 #[serde(rename_all = "lowercase")]
 pub enum Severity {
     /// Hard failure. The module did not typecheck.
     Error,
-    /// Non-fatal observation. Reserved; the typechecker does not emit
-    /// warnings yet.
+    /// Non-fatal observation. Module typechecked; the lint is
+    /// advisory.
     Warning,
 }
 
@@ -131,6 +140,22 @@ impl Diagnostic {
         }
     }
 
+    /// Iter 19a: builds a [`Severity::Warning`] diagnostic. Same shape
+    /// as [`Diagnostic::error`] otherwise. Used by lint-style passes
+    /// that report observations rather than hard typecheck failures
+    /// (currently the only emitter is the linearity pass's
+    /// `over-strict-mode` lint).
+    pub fn warning(code: impl Into<String>, message: impl Into<String>) -> Self {
+        Self {
+            severity: Severity::Warning,
+            code: code.into(),
+            message: message.into(),
+            def: None,
+            ctx: serde_json::Value::Object(serde_json::Map::new()),
+            suggested_rewrites: Vec::new(),
+        }
+    }
+
     /// Iter 18c.2: append a [`SuggestedRewrite`]. Builder-style. Used by
     /// the linearity check to attach the form-A fix it computed. Other
     /// diagnostics leave the field empty.
diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs
index cb1baff..0897878 100644
--- a/crates/ailang-check/src/linearity.rs
+++ b/crates/ailang-check/src/linearity.rs
@@ -70,10 +70,38 @@
 //!   the unique consume.
 //! - `consume-while-borrowed` on `Var x`: replacement `(clone <name>)`
 //!   — the author should clone here so the original keeps the borrow.
+//!
+//! ## Iter 19a: `over-strict-mode` lint
+//!
+//! After the linearity walk has finished for a fn whose every param
+//! mode is explicit, we re-inspect each param annotated `(own T)`:
+//!
+//! - The uniqueness pass ([`crate::uniqueness::infer_module`]) gives
+//!   us the param's `consume_count`.
+//! - If `consume_count == 0` AND the body never destructures the
+//!   param via `(match p ...)` (the latter is a *conservative cut* —
+//!   see below), the fn could have been written with `(borrow T)`
+//!   instead and would be cheaper to call (no inc/dec pair, no
+//!   rec-cascade at fn return). Emit `over-strict-mode` as a
+//!   `Severity::Warning` with a suggested fn-type rewrite.
+//!
+//! ### Why the match-scrutinee carve-out is conservative
+//!
+//! The precise rule would be "no consume of any sub-binder of `p`".
+//! Implementing that requires an extra side-table tracking which
+//! pattern-binders trace back to which scrutinee param — non-trivial
+//! and out of scope for 19a. The conservative cut "no `match` with `p`
+//! as scrutinee" is sound (it never warns when the precise rule
+//! wouldn't) but incomplete (it misses some real over-strict fns
+//! whose body matches on `p` but never moves a sub-binder out). The
+//! incompleteness is acceptable because 19a is purely advisory: a
+//! missed warning costs nothing; a spurious warning would be
+//! actively misleading. The precise variant is queued for a follow-up.
 
 use crate::diagnostic::Diagnostic;
+use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable};
 use ailang_core::ast::{Arm, Def, FnDef, Module, ParamMode, Pattern, Term, Type};
-use ailang_surface::term_to_form_a;
+use ailang_surface::{term_to_form_a, type_to_form_a};
 use std::collections::HashMap;
 
 /// Position in which a [`Term::Var`] is being used. See module-level
@@ -125,10 +153,16 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
         }
     }
 
+    // Iter 19a: the over-strict-mode lint reads `consume_count` from
+    // the uniqueness side table. Build it once for the whole module;
+    // reusing the existing pass keeps the "what counts as a consume"
+    // definition in a single place.
+    let uniq = infer_uniqueness(m);
+
     let mut diags = Vec::new();
     for def in &m.defs {
         if let Def::Fn(f) = def {
-            check_fn(f, &globals, &mut diags);
+            check_fn(f, &globals, &uniq, &mut diags);
         }
     }
     diags
@@ -146,7 +180,12 @@ fn strip_forall(t: &Type) -> &Type {
 
 /// Per-fn check. Skips fns whose signature has any `Implicit` param —
 /// see module-level scope rules.
-fn check_fn(f: &FnDef, globals: &HashMap<String, Type>, diags: &mut Vec<Diagnostic>) {
+fn check_fn(
+    f: &FnDef,
+    globals: &HashMap<String, Type>,
+    uniq: &UniquenessTable,
+    diags: &mut Vec<Diagnostic>,
+) {
     let inner = strip_forall(&f.ty);
     let (param_tys, param_modes) = match inner {
         Type::Fn { params, param_modes, .. } => (params.as_slice(), param_modes.as_slice()),
@@ -190,6 +229,39 @@ fn check_fn(f: &FnDef, globals: &HashMap<String, Type>, diags: &mut Vec<Diagnost
     }
 
     checker.walk(&f.body, Position::Consume);
+
+    // Iter 19a: `over-strict-mode` lint. After the linearity walk has
+    // completed (and any errors have been recorded), inspect each
+    // `Own`-annotated param: if `consume_count == 0` AND no `match`
+    // in the body uses the param as scrutinee, the param could be
+    // re-annotated `Borrow`. Emit a Warning with a form-A rewrite.
+    //
+    // Conservative match-scrutinee carve-out: matching on `p` may
+    // move sub-binders out of `p`'s active ctor, in which case
+    // `(borrow T)` would *not* suffice — the callee needs `Own` to
+    // legitimise the sub-consume. The precise rule would inspect the
+    // arm bodies for sub-binder consumes; the conservative rule
+    // skips any fn that matches on the param at all. See
+    // module-level docs for the rationale.
+    for (i, mode) in param_modes.iter().enumerate() {
+        if !matches!(mode, ParamMode::Own) {
+            continue;
+        }
+        let pname = &f.params[i];
+        let consume_count = uniq
+            .get(&(f.name.clone(), pname.clone()))
+            .map(|info| info.consume_count)
+            .unwrap_or(0);
+        if consume_count != 0 {
+            continue;
+        }
+        if body_matches_on(&f.body, pname) {
+            // Conservative cut: a `match` whose scrutinee is `pname`
+            // may move out a sub-binder; staying silent is safe.
+            continue;
+        }
+        diags.push(make_over_strict_mode(&f.name, pname, inner, i));
+    }
 }
 
 /// Per-fn linearity walker.
@@ -610,6 +682,130 @@ fn make_use_after_consume_at_reuse_as(def: &str, binder: &str, body: &Term) -> D
     )
 }
 
+/// Iter 19a: returns `true` if any sub-term of `t` is a
+/// `Term::Match` whose scrutinee is a bare `Var { name: pname }` (or
+/// a `Term::Clone` thereof — clone-then-match is the same shape for
+/// the purposes of the carve-out, since both forms read the binder
+/// without consuming it but expose its sub-binders to the arms).
+///
+/// Used by the over-strict-mode lint as a conservative gate: matching
+/// on `p` *may* move out a sub-binder of `p` — in which case `(own T)`
+/// is genuinely needed and `(borrow T)` would not suffice. We don't
+/// yet inspect the arms to refine the answer; any such match silences
+/// the lint for `pname`.
+fn body_matches_on(t: &Term, pname: &str) -> bool {
+    match t {
+        Term::Lit { .. } | Term::Var { .. } => false,
+        Term::Match { scrutinee, arms } => {
+            if scrutinee_matches_param(scrutinee, pname) {
+                return true;
+            }
+            arms.iter().any(|a| body_matches_on(&a.body, pname))
+                || body_matches_on(scrutinee, pname)
+        }
+        Term::App { callee, args, .. } => {
+            body_matches_on(callee, pname) || args.iter().any(|a| body_matches_on(a, pname))
+        }
+        Term::Let { value, body, .. } => {
+            body_matches_on(value, pname) || body_matches_on(body, pname)
+        }
+        Term::LetRec { body, in_term, .. } => {
+            // The recursive fn's body and the continuation can both
+            // shadow `pname`; we ignore shadowing here — the lint
+            // is allowed to be over-cautious.
+            body_matches_on(body, pname) || body_matches_on(in_term, pname)
+        }
+        Term::If { cond, then, else_ } => {
+            body_matches_on(cond, pname)
+                || body_matches_on(then, pname)
+                || body_matches_on(else_, pname)
+        }
+        Term::Seq { lhs, rhs } => body_matches_on(lhs, pname) || body_matches_on(rhs, pname),
+        Term::Ctor { args, .. } | Term::Do { args, .. } => {
+            args.iter().any(|a| body_matches_on(a, pname))
+        }
+        Term::Lam { body, .. } => body_matches_on(body, pname),
+        Term::Clone { value } => body_matches_on(value, pname),
+        Term::ReuseAs { source, body } => {
+            body_matches_on(source, pname) || body_matches_on(body, pname)
+        }
+    }
+}
+
+/// Iter 19a: a scrutinee "is" `pname` if it's a bare `Var { pname }`
+/// or `Clone(Var { pname })`. Anything else (a fresh App result, a
+/// let-binder, …) does not put `pname` directly in scrutinee
+/// position.
+fn scrutinee_matches_param(scrutinee: &Term, pname: &str) -> bool {
+    match scrutinee {
+        Term::Var { name } => name == pname,
+        Term::Clone { value } => scrutinee_matches_param(value, pname),
+        _ => false,
+    }
+}
+
+/// Iter 19a: build the `over-strict-mode` warning. `inner` is the
+/// fn-type with the original mode; we synthesise a relaxed copy with
+/// `param_modes[i] = Borrow` and render it through
+/// [`type_to_form_a`] to produce the suggested rewrite.
+fn make_over_strict_mode(def: &str, binder: &str, inner: &Type, i: usize) -> Diagnostic {
+    let relaxed = relax_param_to_borrow(inner, i);
+    let replacement = type_to_form_a(&relaxed);
+    Diagnostic::warning(
+        "over-strict-mode",
+        format!(
+            "param `{binder}` is annotated `(own ...)` but the body does not consume it; `(borrow ...)` would suffice"
+        ),
+    )
+    .with_def(def)
+    .with_ctx(serde_json::json!({
+        "binder": binder,
+        "current_mode": "own",
+        "suggested_mode": "borrow",
+    }))
+    .with_suggested_rewrite(
+        format!("relax param `{binder}` mode from `(own ...)` to `(borrow ...)`"),
+        replacement,
+    )
+}
+
+/// Iter 19a: clone of `inner` (assumed `Type::Fn`) with
+/// `param_modes[i]` rewritten to `ParamMode::Borrow`. Other slots
+/// are preserved bit-for-bit. Falls back to returning `inner`
+/// unchanged if `inner` is not a `Type::Fn` (defensive — caller
+/// should have screened this).
+fn relax_param_to_borrow(inner: &Type, i: usize) -> Type {
+    match inner {
+        Type::Fn {
+            params,
+            param_modes,
+            ret,
+            ret_mode,
+            effects,
+        } => {
+            // Materialise param_modes to full length so the relaxed
+            // mode is positioned correctly even when the original
+            // vec was elided to "all-implicit empty" (not the case
+            // here — we only reach this for an `Own` slot — but
+            // defensive).
+            let mut new_modes: Vec<ParamMode> = (0..params.len())
+                .map(|j| param_modes.get(j).copied().unwrap_or(ParamMode::Implicit))
+                .collect();
+            if i < new_modes.len() {
+                new_modes[i] = ParamMode::Borrow;
+            }
+            Type::Fn {
+                params: params.clone(),
+                param_modes: new_modes,
+                ret: ret.clone(),
+                ret_mode: *ret_mode,
+                effects: effects.clone(),
+            }
+        }
+        other => other.clone(),
+    }
+}
+
 /// Build a `consume-while-borrowed` diagnostic for `binder` in `def`.
 /// Suggested rewrite: clone here so the original retains the borrow.
 fn make_consume_while_borrowed(def: &str, binder: &str) -> Diagnostic {
@@ -688,7 +884,11 @@ mod tests {
         assert!(check_module(&m).is_empty());
     }
 
-    /// All-explicit fn that NEVER uses its params: clean.
+    /// All-explicit fn that NEVER uses its params, annotated `Borrow`:
+    /// clean. (Pre-19a this test exercised the same shape with `Own`
+    /// and asserted clean; 19a's `over-strict-mode` lint now fires on
+    /// `Own` + zero-consume — moved into a dedicated positive test
+    /// below. With `Borrow`, the lint does not apply.)
     #[test]
     fn explicit_fn_with_no_uses_is_clean() {
         let m = Module {
@@ -697,7 +897,7 @@ mod tests {
             imports: vec![],
             defs: vec![fn_with_modes(
                 "f",
-                vec![ParamMode::Own],
+                vec![ParamMode::Borrow],
                 Term::Lit { lit: Literal::Int { value: 0 } },
             )],
         };
@@ -772,4 +972,155 @@ mod tests {
         assert_eq!(d.code, "use-after-consume");
         assert_eq!(d.ctx, serde_json::json!({"binder": "p0"}));
     }
+
+    // ---- Iter 19a: over-strict-mode -----------------------------------
+
+    use crate::diagnostic::Severity;
+
+    /// Iter 19a, positive: a fn with `(own T)` whose body merely
+    /// borrows the param via a `Borrow`-mode call → fires
+    /// `over-strict-mode` (Warning) with binder=p0, current=own,
+    /// suggested=borrow, and a non-empty rewrite.
+    #[test]
+    fn over_strict_mode_fires_when_param_only_borrowed() {
+        // Module shape:
+        //   (fn read (params (borrow (con List))) ... ) ; helper, body irrelevant
+        //   (fn f    (params (own    (con List)))     ; over-strict
+        //     body = (app read p0))
+        let read_def = Def::Fn(FnDef {
+            name: "read".into(),
+            ty: Type::Fn {
+                params: vec![Type::Con { name: "List".into(), args: vec![] }],
+                param_modes: vec![ParamMode::Borrow],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Implicit,
+                effects: vec![],
+            },
+            params: vec!["xs".into()],
+            body: Term::Lit { lit: Literal::Int { value: 0 } },
+            doc: None,
+        });
+        let f_body = Term::App {
+            callee: Box::new(Term::Var { name: "read".into() }),
+            args: vec![Term::Var { name: "p0".into() }],
+            tail: false,
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![read_def, fn_with_modes("f", vec![ParamMode::Own], f_body)],
+        };
+        let diags = check_module(&m);
+        // Filter to over-strict-mode in case the helper triggers anything
+        // (it shouldn't — `read` is `Borrow` and param is unused).
+        let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect();
+        assert_eq!(osm.len(), 1, "expected one over-strict-mode, got {diags:?}");
+        let d = osm[0];
+        assert_eq!(d.severity, Severity::Warning);
+        assert_eq!(d.def.as_deref(), Some("f"));
+        assert_eq!(
+            d.ctx,
+            serde_json::json!({
+                "binder": "p0",
+                "current_mode": "own",
+                "suggested_mode": "borrow",
+            })
+        );
+        assert!(
+            !d.suggested_rewrites.is_empty(),
+            "diagnostic should carry a suggested rewrite"
+        );
+        // The replacement is a fn-type, so it does not have to round-trip
+        // through `parse_term` (which parses terms). We only assert it's
+        // a non-empty string that mentions the relaxed `(borrow ...)`.
+        let rep = &d.suggested_rewrites[0].replacement;
+        assert!(
+            rep.contains("(borrow"),
+            "rewrite should mention `(borrow`; got {rep}"
+        );
+        assert!(
+            !rep.contains("(own"),
+            "rewrite should NOT contain the original `(own`; got {rep}"
+        );
+    }
+
+    /// Iter 19a, negative: a fn with `(own T)` whose body consumes
+    /// the param directly does not fire `over-strict-mode`.
+    #[test]
+    fn over_strict_mode_silent_when_body_consumes_param() {
+        // Body: (seq p0 0) — `p0` is consumed in seq.lhs.
+        let body = Term::Seq {
+            lhs: Box::new(Term::Var { name: "p0".into() }),
+            rhs: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "over-strict-mode"),
+            "no over-strict-mode expected; got {diags:?}"
+        );
+    }
+
+    /// Iter 19a, negative: a fn with `(borrow T)` and a borrowing
+    /// body never fires `over-strict-mode` (the lint is gated on
+    /// `Own`).
+    #[test]
+    fn over_strict_mode_silent_when_param_is_borrow() {
+        // Body shape: literal — no use of the param at all.
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_with_modes(
+                "f",
+                vec![ParamMode::Borrow],
+                Term::Lit { lit: Literal::Int { value: 0 } },
+            )],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "over-strict-mode"),
+            "no over-strict-mode expected for borrow-mode param; got {diags:?}"
+        );
+    }
+
+    /// Iter 19a, conservatism marker: a fn with `(own T)` whose body
+    /// is `(match p0 ...)` and never consumes `p0` directly nor any
+    /// of `p0`'s sub-binders does NOT fire `over-strict-mode` in the
+    /// conservative cut. This is a known false-negative; the
+    /// precise variant (which would fire here) is queued for a
+    /// follow-up. Keep this test as a TODO marker — flipping it
+    /// to `assert!(some-warning)` is the signal that the precise
+    /// variant has shipped.
+    #[test]
+    fn over_strict_mode_conservative_skips_match_on_param() {
+        // Body: (match p0 ((pat-wild) 0))
+        // — sub-binders are absent; the param is only read. The
+        //   precise rule would fire here. The conservative rule
+        //   silences any `match` whose scrutinee is the param.
+        let body = Term::Match {
+            scrutinee: Box::new(Term::Var { name: "p0".into() }),
+            arms: vec![Arm {
+                pat: Pattern::Wild,
+                body: Term::Lit { lit: Literal::Int { value: 0 } },
+            }],
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "over-strict-mode"),
+            "conservative cut: no over-strict-mode expected when the body matches on the param; got {diags:?}"
+        );
+    }
 }
diff --git a/crates/ailang-surface/src/lib.rs b/crates/ailang-surface/src/lib.rs
index 663a759..eaedd20 100644
--- a/crates/ailang-surface/src/lib.rs
+++ b/crates/ailang-surface/src/lib.rs
@@ -36,4 +36,4 @@ pub mod parse;
 pub mod print;
 
 pub use parse::{parse, parse_term, ParseError};
-pub use print::{print, term_to_form_a};
+pub use print::{print, term_to_form_a, type_to_form_a};
diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs
index 1f97bb9..ccac716 100644
--- a/crates/ailang-surface/src/print.rs
+++ b/crates/ailang-surface/src/print.rs
@@ -43,6 +43,16 @@ pub fn term_to_form_a(t: &Term) -> String {
     out
 }
 
+/// Iter 19a: render a [`Type`] as form-A. Used by diagnostics that want
+/// to suggest a relaxed signature (e.g. `over-strict-mode` shows the
+/// `(fn-type ...)` with `(borrow T)` in place of `(own T)`). Output is
+/// the same shape that appears as the `type` slot of a `(fn ...)` def.
+pub fn type_to_form_a(t: &Type) -> String {
+    let mut out = String::new();
+    write_type(&mut out, t);
+    out
+}
+
 // ---- helpers --------------------------------------------------------------
 
 fn indent(out: &mut String, level: usize) {
diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md
index 9c6bd64..49d979b 100644
--- a/docs/JOURNAL.md
+++ b/docs/JOURNAL.md
@@ -8591,3 +8591,153 @@ implementation" — it is the literal RED-step that the discipline
 prescribes. The three fixtures shipped here are exactly that:
 each pins one of the three carve-out sites, observable via the
 RC stats line, kept as regression. JOURNAL queue: empty.
+
+## 2026-05-08 — Design: explicit annotations stay mandatory; `over-strict-mode` diagnostic
+
+User pushback on the queue-driven dispatch: the orchestrator
+floated "uniqueness inference replaces fn-signature mode
+annotations" as a candidate direction. Re-read of DESIGN.md
+§ "Decision 10" (lines 685–795) shows that pitch was a
+**Decision-10 reversal**, not an iter within it:
+
+> *"AILang makes it mandatory because the LLM author can carry
+> the cognitive cost trivially, and the compiler gains a precise
+> contract at every call site instead of a probabilistic guess."*
+
+Three reasons mandatory annotations are not redundancy in the
+harmful sense:
+
+  1. **Inference picks weakest-supporting; annotation states
+     intent.** These often coincide today but are conceptually
+     different. The annotation captures what the author committed
+     to, not what the current body needs (e.g. `(own T)` reserved
+     for a planned in-place mutation that hasn't landed).
+  2. **Annotation is a drift-bremse.** Body change that flips
+     the inferred mode → caller-side breakage at remote sites.
+     Annotation enforces the local-conflict-error pattern instead.
+  3. **Forcing function specific to LLM authoring.** Without
+     mandatory annotation, an LLM never has to commit to ownership
+     intent before writing the body — the contract becomes a
+     by-product of local code choice. With it, the contract is a
+     first-order variable the body must satisfy.
+
+The "redundancy" between annotation and body is therefore the
+feature, not the bug — analogous to test code redundantly
+restating implementation behaviour, where the redundancy is what
+catches drift.
+
+### What survives of the original pitch
+
+One narrow but real observation: today, when the author writes
+`(own T)` and the body would compile under `(borrow T)`, the
+typechecker silently accepts. No warning, no diagnostic. The
+runtime cost is real (one inc/dec pair per call, plus potential
+rec-cascade at fn return), but invisible.
+
+The Rust analogue is `clippy::needless_pass_by_value`: an
+informational lint with a suppression mechanism. AILang sharpens
+this to "suppression carries a mandatory reason" — consistent
+with the explicit-intent philosophy.
+
+### Iter scope
+
+Two iters, dispatched separately so 19a's diagnostic frequency
+on real code informs whether 19b's escape hatch is needed at all:
+
+  - **Iter 19a — `over-strict-mode` diagnostic.** Linearity pass
+    detects: `param_modes[i] == Own` + `consume_count(p) == 0` +
+    no consume of any sub-binder of p in the body. Emits
+    `Severity::Warning` (the first warning-level diagnostic the
+    typechecker has emitted; reserves no longer reserved). Carries
+    a `suggested_rewrite` showing the relaxed `(borrow T)`
+    signature. No schema change; pure detection.
+
+  - **Iter 19b — `mode-strict-because` suppression** (deferred
+    pending 19a's signal). Optional schema field on fn defs:
+    `suppress: [{code: String, because: String}]`. `because` is
+    non-empty (schema-validation error otherwise). The suppress
+    mechanism is generic across diagnostic codes but the only
+    consumer initially is `over-strict-mode`.
+
+### Why split
+
+19a alone is shippable: users who see the warning either accept
+the rewrite or live with the noise on intentional-strict fns.
+19b is only worth building if real code surfaces enough
+intentional-strict cases to make the noise unbearable. This lets
+the data drive whether 19b ships at all.
+
+### What this is NOT
+
+Not a relaxation of Decision 10. Annotations stay mandatory.
+Authors cannot omit `param_modes` / `ret_mode`; the compiler
+will not infer them. The diagnostic is purely advisory: "you
+wrote this, here's a tighter alternative." If suppressed (19b),
+the annotation stays exactly as authored.
+
+## 2026-05-08 — Iter 19a: `over-strict-mode` diagnostic shipped
+
+The diagnostic-side of the design entry above. Linearity pass
+gained a post-walk loop over `Own`-annotated params; uniqueness
+side-table provides `consume_count`. When `consume_count == 0`
+*and* the body never destructures the param via match, the lint
+fires with a form-A-rendered fn-type rewrite as `suggested_rewrite`.
+
+### Conservative cut
+
+The precise rule is "no consume of any sub-binder of `p`". The
+shipped check approximates with "no `match` whose scrutinee is
+`pname`" — sound (never false-positive) but incomplete (misses
+match-on-p-without-sub-consume). Documented in `linearity.rs`'s
+module doc and pinned by the test
+`over_strict_mode_conservative_skips_match_on_param`. Acceptable
+because the lint is purely advisory: a missed warning costs
+nothing, a spurious warning would actively mislead. The precise
+variant is queued for a follow-up if real-corpus signal warrants.
+
+### CLI side-effect
+
+This is the first `Severity::Warning` diagnostic the typechecker
+emits. Three CLI exit paths (`Cmd::Check` non-JSON, `Cmd::EmitIr`,
+`build_to`) previously aborted on any non-empty diagnostic list;
+now they only abort when at least one diagnostic is `Severity::Error`.
+The `--json` path was already correct (returns the list, doesn't
+exit). No observable behaviour change for any pre-19a input —
+nothing emitted Warning before this iter — but the gate is now
+in place for future warning-level lints.
+
+### Tests
+
+Four new tests in `linearity.rs::tests`:
+
+  - `over_strict_mode_fires_when_param_only_borrowed` — positive.
+  - `over_strict_mode_silent_when_body_consumes_param` — negative.
+  - `over_strict_mode_silent_when_param_is_borrow` — negative.
+  - `over_strict_mode_conservative_skips_match_on_param` — pins the
+    conservatism; flips to a positive assertion when the precise
+    variant lands.
+
+`ailang-check` test count: 49 → 53. e2e unchanged at 69. Workspace
+build + test green.
+
+### Files touched
+
+  - `crates/ailang-check/src/diagnostic.rs` — registered
+    `over-strict-mode` code, refreshed `Severity::Warning` doc,
+    added `Diagnostic::warning` ctor.
+  - `crates/ailang-check/src/linearity.rs` — module-doc § 19a, the
+    post-walk loop, helpers (`body_matches_on`,
+    `scrutinee_matches_param`, `make_over_strict_mode`,
+    `relax_param_to_borrow`), `check_fn` signature gained a
+    `&UniquenessTable` arg.
+  - `crates/ailang-surface/src/print.rs` — new
+    `pub fn type_to_form_a(&Type) -> String` (re-exported from `lib.rs`).
+  - `crates/ail/src/main.rs` — three exit-on-Error gates.
+
+### What stays queued
+
+  - Iter 19b (`mode-strict-because` suppression): waits for
+    real-corpus signal on whether intentional-strict fns are
+    common enough to warrant the schema field.
+  - Precise sub-binder analysis for the lint: waits for evidence
+    that the conservative cut misses real cases.