feat(check): mir.1a — typed-MIR types + post-mono lower_to_mir + elaborate_workspace (additive)

First half of spec iteration mir.1 (docs/specs/0060-typed-mir.md,
plan docs/plans/0114-mir.1a-mir-infrastructure.md). Purely additive: a
new leaf crate plus a post-mono lowering walk plus the front-end entry.
Nothing consumes MIR yet — codegen and the CLI are untouched — so the
whole existing suite stays green (102 test-result-ok lines, 0 failed;
the one ignored is the #49 pin, which lifts at mir.4). mir.1b flips
codegen to consume MIR and deletes the synth_with_extras mirror.

What lands:
- `ailang-mir` (new leaf crate, depends only on ailang-core): MTerm /
  MArg / MArm / MLoopBinder / MNewArg / Callee / Mode / StrRep / MirDef
  / MirModule / MirWorkspace, structurally complete over all 17 Term
  variants plus the dedicated Str split (MTerm::Str{lit,rep}). Every
  later-iteration annotation field exists now at a mir.1 default
  (App.callee = Indirect, MArg.mode/consume_count = Owned/1, Str.rep =
  Static, New.elem = None); the struct shape will not change across
  mir.2–mir.5, only the values. MTerm::ty() reads the carried type.
- `ailang-check::lower_to_mir`: the post-mono walk. Carries no second
  type engine — it calls the canonical `synth` per node with fresh
  throwaway inference scaffolding (subst/counter/residuals/…), applies
  the substitution, and threads only the lexical locals/loop_stack,
  maintained by the same push/pop rules synth uses (Let, Loop, Lam,
  LetRec, and Match via synth's own type_check_pattern). This is the
  "one engine, not two" property the milestone buys, on the producer
  side.
- `ailang-check::elaborate_workspace`: the single front-end entry —
  check (diagnostics gate) → desugar+lift → monomorphise → lower_to_mir
  — transcribed from the CLI build path. check_workspace stays for the
  diagnostics-only callers.
- Three ty-fill pins (crates/ailang-check/tests/lower_to_mir_ty.rs)
  load the #51/#53/#49 witnesses as fixtures and elaborate the whole
  workspace, so lower_to_mir is exercised over the full prelude+kernel,
  not just the tiny witness. Two new witness fixtures
  (examples/new_{rawbuf_size_only,counter_user_adt}.ail); #49 reuses the
  existing loop_recur_str_binder_no_leak_pin.ail.

Deviations from the plan, all forced by ground truth and verified
against the live code before commit:
- FnDef.export is Option<String>, not bool — dropped from MirDef (the
  plan's note allowed this fallback). Codegen reads FnDef.export
  directly, unaffected.
- fn_param_types did not exist — lifted the param-type extraction into
  a shared pub(crate) fn and rewired both mono.rs sites
  (collect_mono_targets, collect_rewrite_targets) to it, so the
  param-type source cannot drift between mono and lower_to_mir. The
  helper unwraps a top-level Forall then reads Type::Fn.params —
  identical to the inner_ty extraction it replaces; the early-return
  non-fn guard is preserved at both sites. Behaviour-preserving (whole
  suite green; this is the only edit to existing mono behaviour).
- lower_module mirrors two more mono.rs scaffolding rules the plan
  under-transcribed: skip intrinsic-bodied fns (they are
  signature-only; lowering them would hit synth's Term::Intrinsic
  guard) and seed env.current_module + env.globals + env.imports per
  module so synth's Var lookup resolves post-mono specialisations
  (e.g. compare__Int) in the prelude.
- The #53 pin asserts the lowered (new Counter 42) init carries ty
  Counter, not that it is an MTerm::New: a monomorphic `new` over a
  user ADT is desugared to a dotted call `(app Counter.new 42)` before
  lower_to_mir runs (desugar.rs:1078-1098), so it lowers to MTerm::App.
  MTerm::New survives only for a polymorphic `new` carrying a written
  NewArg::Type (the #51 RawBuf path, covered by the rawbuf pin). The
  pin's intent — ty-fill correctness — is preserved; the structural
  variant is mir.2/mir.5 territory.
- ailang-mir uses workspace-inherited Cargo fields for consistency with
  the existing crates (added it to [workspace.dependencies]).

refs #49

crates/ailang-check/tests/lower_to_mir_ty.rs

@@ -0,0 +1,99 @@
+//! mir.1a: `lower_to_mir` fills `ty` on every node from the canonical
+//! `synth`, and routes string literals to `MTerm::Str { rep: Static }`.
+//! Loads the boundary witnesses as workspace fixtures (prelude +
+//! kernel injected by `load_workspace`) and elaborates the whole
+//! workspace, so the walk is exercised over the full prelude. These
+//! pins protect the producer; codegen consumption arrives in mir.1b.
+
+use ailang_check::elaborate_workspace;
+use ailang_mir::{MTerm, MirWorkspace, StrRep};
+use ailang_surface::load_workspace;
+use std::path::{Path, PathBuf};
+
+/// `<repo>/examples` — resolved from this crate's manifest dir,
+/// cwd-independent (same pattern as `method_collision_pin.rs`).
+fn examples_dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR"))
+        .parent().expect("crates/ailang-check has parent crates/")
+        .parent().expect("crates/ has parent repo root")
+        .join("examples")
+}
+
+/// Load a witness fixture (prelude injected) and elaborate it to MIR.
+fn elaborate_fixture(module: &str) -> MirWorkspace {
+    let entry = examples_dir().join(format!("{module}.ail"));
+    let ws = load_workspace(&entry).expect("fixture loads (prelude injected)");
+    elaborate_workspace(&ws).expect("witness elaborates to MIR")
+}
+
+/// A def's lowered body in the elaborated workspace.
+fn body<'a>(mir: &'a MirWorkspace, module: &str, def: &str) -> &'a MTerm {
+    &mir.modules[module]
+        .defs
+        .iter()
+        .find(|d| d.name == def)
+        .expect("def present")
+        .body
+}
+
+#[test]
+fn str_literal_lowers_to_static_str_node() {
+    // #49 witness: the loop seed "x" is a Str literal → MTerm::Str,
+    // rep = Static at mir.1 (mir.4 flips loop seeds to Heap).
+    let m = "loop_recur_str_binder_no_leak_pin";
+    let mir = elaborate_fixture(m);
+    assert!(
+        find_static_str_seed(body(&mir, m, "main")),
+        "loop seed \"x\" must lower to MTerm::Str {{ rep: Static }}"
+    );
+}
+
+#[test]
+fn new_over_user_adt_carries_node_types() {
+    // #53 witness: every node has a filled `ty`; the lowered
+    // `(new Counter 42)` node's type is the user ADT `Counter`.
+    //
+    // A *monomorphic* `new` (no leading type-arg) is desugared to a
+    // type-scoped call `(app Counter.new 42)` before lower_to_mir runs
+    // (desugar.rs:1083-1098) — so the let-init lowers to `MTerm::App`,
+    // not `MTerm::New`. `MTerm::New` survives only for a *polymorphic*
+    // `new` carrying a written `NewArg::Type` (the #51 RawBuf case).
+    // What this pin protects is the ty-fill: the lowered init node
+    // carries the checker-proved result type `Counter`.
+    let m = "new_counter_user_adt";
+    let mir = elaborate_fixture(m);
+    let MTerm::Let { init, .. } = body(&mir, m, "main") else {
+        panic!("main body is a let");
+    };
+    let ty_str = ailang_core::pretty::type_to_string(&init.ty());
+    assert!(
+        ty_str.contains("Counter"),
+        "lowered (new Counter 42) init node ty is Counter, got {ty_str}"
+    );
+}
+
+#[test]
+fn rawbuf_size_only_elaborates() {
+    // #51 witness: a RawBuf read only for size — must elaborate clean
+    // (the element type carried only by the author's annotation does
+    // not block lowering).
+    let mir = elaborate_fixture("new_rawbuf_size_only");
+    assert!(mir.modules.contains_key("new_rawbuf_size_only"));
+}
+
+/// Recursively search for a `MTerm::Str { rep: Static }` reachable
+/// from a loop binder init (the seed).
+fn find_static_str_seed(t: &MTerm) -> bool {
+    match t {
+        MTerm::Loop { binders, body, .. } => {
+            binders.iter().any(|b| matches!(
+                &b.init,
+                MTerm::Str { rep: StrRep::Static, .. }
+            )) || find_static_str_seed(body)
+        }
+        MTerm::Let { init, body, .. } => {
+            find_static_str_seed(init) || find_static_str_seed(body)
+        }
+        _ => false,
+    }
+}