diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs
index 75b2db5..42a23f4 100644
--- a/crates/ail/tests/e2e.rs
+++ b/crates/ail/tests/e2e.rs
@@ -93,6 +93,20 @@ fn list_map_doubles_then_prints() {
     assert_eq!(lines, vec!["2", "4", "6"]);
 }
 
+/// Iter 14a: end-to-end exercise of parameterised ADTs through a
+/// polymorphic higher-order fn. `data List a` plus
+/// `map : forall a b. ((a) -> b, List<a>) -> List<b>` recursive,
+/// instantiated at `(Int, Int)`. Guards: forall with two type vars +
+/// recursive call inside its own body + ctor construction with
+/// substituted field types + match-arm bindings flowing into an
+/// effectful tail call.
+#[test]
+fn list_map_poly_inc_then_prints() {
+    let stdout = build_and_run("list_map_poly.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["2", "3", "4"]);
+}
+
 /// Iter 11 dogfood: insertion sort over an 11-element IntList.
 /// Exercises `<=`, `if`, mutual-leaf recursion (`insert` and `sort`),
 /// nested ctor construction, and the Iter 10 seq operator inside
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index 4a196ff..c30c2f3 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/crates/ailang-codegen/src/lib.rs
@@ -2076,18 +2076,27 @@ impl<'a> Emitter<'a> {
                 for (exp, actual) in cref.ail_fields.iter().zip(arg_tys.iter()) {
                     unify_for_subst(exp, actual, &var_set, &mut subst)?;
                 }
-                // Vars not pinned by ctor args (e.g. `None` for
-                // `Maybe a`) are filled with `Type::unit()` as a
-                // placeholder. That's harmless for monomorphic call
-                // sites — codegen never instantiates a polymorphic fn
-                // off this un-pinned shape because the typechecker
-                // would have rejected an under-determined call —
-                // and keeps the function total for the well-formed
-                // ones (e.g. `Some(7)` pins `a` from the arg).
+                // Vars not pinned by ctor args (e.g. `Nil` for `List a`,
+                // `None` for `Maybe a`) are filled with a synth-only
+                // wildcard `Type::Var { name: "$u" }`. The `$u`-prefix
+                // is reserved here (mirrors the checker's `$m` for
+                // metavars) and is treated as a match-anything wildcard
+                // by `unify_for_subst` on the arg side. This matters
+                // when a nullary ctor like `Nil` is nested inside a
+                // parent ctor whose other args pin the same type var
+                // concretely — e.g. `Cons(Int, Nil) : List<a>` must
+                // pin `a = Int` from the head and let the tail's
+                // unconstrained `a` defer rather than collide on
+                // `Type::unit()` as it would have pre-fix.
                 let resolved: Vec<Type> = cref
                     .type_vars
                     .iter()
-                    .map(|v| subst.get(v).cloned().unwrap_or_else(Type::unit))
+                    .map(|v| {
+                        subst
+                            .get(v)
+                            .cloned()
+                            .unwrap_or_else(|| Type::Var { name: "$u".into() })
+                    })
                     .collect();
                 Ok(Type::Con {
                     name: type_name.clone(),
@@ -2237,6 +2246,18 @@ fn unify_for_subst(
     vars: &BTreeSet<&str>,
     subst: &mut BTreeMap<String, Type>,
 ) -> Result<()> {
+    // Iter 14a fix: an arg-side `$u`-prefixed var is a synth-only
+    // wildcard produced by `synth_arg_type` for nullary ctors of a
+    // parameterised ADT (e.g. `Nil : List<$u>`). It carries no real
+    // constraint — accept without binding so a sibling arg can pin
+    // the type var instead. Without this, `Cons(Int, Nil)` synth
+    // would unify `a = Int` (from head) and then `a = $u` (from
+    // tail's recursive `List<a>` slot) and falsely error.
+    if let Type::Var { name } = arg {
+        if name.starts_with("$u") {
+            return Ok(());
+        }
+    }
     match (param, arg) {
         (Type::Var { name }, _) if vars.contains(name.as_str()) => {
             if let Some(prev) = subst.get(name) {
diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md
index 955b6dd..a510dc3 100644
--- a/docs/JOURNAL.md
+++ b/docs/JOURNAL.md
@@ -1407,3 +1407,109 @@ budget at the start of 14a is tight, alternative is 14b
 (GC/arena scaffolding) or 14c (poly fn as value); both have
 real design questions that need an orchestrator design pass
 first, so 14a stays the default.
+
+## Iter 14a — polymorphic `List a` end-to-end + monomorphisation bug fixed
+
+The dogfood payoff for parameterised ADTs (13a/b/c). Prior
+to this iter, the only programs exercising the feature were
+`box.ail.json` (single `MkBox(42)` round-trip) and
+`maybe_int.ail.json` (single `or_else` call). That is a thin
+slice — neither program builds a recursive parameterised ADT
+nor calls a polymorphic higher-order fn. 14a closes that gap
+with `data List a` + `map : forall a b. ((a) -> b, List<a>) ->
+List<b>` recursive, then prints the result.
+
+Three-agent run (tester → debugger → no implementer needed):
+
+1. **Tester** wrote `examples/list_map_poly.ail.json` (5 defs:
+   `List`, `inc`, `map`, `print_list`, `main`) and a new e2e
+   test `list_map_poly_inc_then_prints` that asserts stdout
+   `["2", "3", "4"]`. Typecheck passed, build crashed:
+   `internal: monomorphisation: var \`a\` bound to two
+   distinct types`. Tester correctly stopped — fixture
+   encodes the contract; bug is in the compiler — and
+   reported with a hypothesis (recursion / shared
+   substitution slot in `map`).
+
+2. **Debugger** refuted the hypothesis with a non-recursive
+   repro (`Cons(7, Nil)` triggers the same crash without
+   `map` in the picture at all). Real cause was much smaller:
+   in `synth_arg_type` (codegen, ~line 2087) for `Term::Ctor`,
+   any type var of the parent ADT that the ctor's args
+   couldn't pin was filled with `Type::unit()` as a
+   placeholder. For nullary ctors of a parameterised ADT
+   (`Nil : List<a>`, `None : Maybe<a>`) that placeholder
+   leaked upward. Inside a parent like `Cons(Int, Nil) :
+   List<a>`, `unify_for_subst` would walk
+   `cref.ail_fields = [Var{a}, Con{List,[Var{a}]}]` against
+   `[Int, Con{List,[Unit]}]`, bind `a = Int` from the head,
+   then collide with `a = Unit` from the tail. The recursive
+   `map` fixture surfaced it because it is the first program
+   to nest a nullary ctor of a parameterised ADT inside a
+   parent ctor — the existing 13b regressions never did. The
+   tester's hypothesis was reasonable from the symptom but
+   wrong on mechanism; refuting it via a smaller repro is
+   exactly the discipline the debugger role is for.
+
+3. **Fix** (`crates/ailang-codegen/src/lib.rs`, +30/-9 LOC,
+   no new variant, no API change):
+   - Replace `Type::unit()` placeholder with a synth-only
+     wildcard `Type::Var { name: "$u" }`. The `$u` prefix is
+     a reserved-namespace convention that mirrors the
+     checker's `$m<id>` for instantiation metavars — same
+     trick (source-level identifiers can't start with `$`),
+     same goal (extra semantics without schema change).
+   - `unify_for_subst` short-circuits on a `$u`-prefixed
+     **arg-side** var: accept without binding, let a sibling
+     arg pin the type var instead. Param-side semantics
+     untouched. `derive_substitution`'s "var not pinned"
+     check still fires for genuinely under-determined calls
+     (those would have failed typechecking, so codegen never
+     sees them, but the safety net stands).
+
+**Tests:** 25/25 e2e (was 24, +1 new poly test). All five
+named regressions stayed green: `list_map_doubles_then_prints`,
+`parameterised_box_round_trip`, `parameterised_maybe_match`,
+`polymorphic_id_at_int_and_bool`, `polymorphic_apply_with_fn_param`.
+Insertion sort still green. `cargo doc --no-deps`: 0 warnings
+(workspace invariant from 13d/e/f preserved). `cargo build
+--workspace` green.
+
+**Process note: tester→debugger→done in one iter.** No
+implementer dispatch needed — the debugger's mandate covers
+"propose **and apply** a minimally invasive fix" once the
+diagnosis is solid. 30 LOC across two sites in one file is
+inside the role's scope (the role doc says "stop and report"
+only on >50 LOC across multiple files). The orchestrator-side
+work was the design (the source program), the scoped briefs,
+and verification. This is the cleanest agent-flow shape so
+far: each agent did exactly its job, the tester's wrong
+hypothesis didn't propagate because the debugger tested it,
+and the orchestrator never wrote compiler code.
+
+**Findings flagged** (judgement deferred, not fixed):
+
+- `CodegenError::Internal` (the catch-all string variant the
+  docwriter flagged in 13f) is now used by one more invariant
+  — the `$u` short-circuit could in principle be reached by a
+  malformed input; it's currently silent because typecheck
+  rejects under-determined calls upstream. Worth splitting
+  into typed variants the next time codegen tests get a real
+  rewrite. (Same finding as 13f, now reinforced by another
+  use site.)
+- The `$u` / `$m` reserved-prefix convention (`$u` for
+  codegen synth wildcards, `$m<id>` for checker metavars)
+  is undocumented as a project-wide naming rule. Two
+  prefixes is fine; if a third appears, this should be
+  promoted to a DESIGN.md note.
+
+**Next.** Parameterised ADTs are now genuinely usable for
+real programs. The standard library starter set (an
+`examples/std_*` series with `List`, `Maybe`, `Either`,
+basic combinators `length`, `filter`, `fold`, `concat`)
+becomes worthwhile in a way it wasn't pre-14a — that's a
+plausible 14b alternative, smaller than GC/arena, and would
+itself surface more dogfood bugs. The original 14b
+(GC/arena) and 14c (poly fn as value) remain on the queue
+but have not had a design pass.
+
diff --git a/examples/list_map_poly.ail.json b/examples/list_map_poly.ail.json
new file mode 100644
index 0000000..19f375c
--- /dev/null
+++ b/examples/list_map_poly.ail.json
@@ -0,0 +1,230 @@
+{
+  "schema": "ailang/v0",
+  "name": "list_map_poly",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "type",
+      "name": "List",
+      "vars": ["a"],
+      "doc": "Polymorphic singly-linked list.",
+      "ctors": [
+        { "name": "Nil", "fields": [] },
+        {
+          "name": "Cons",
+          "fields": [
+            { "k": "var", "name": "a" },
+            {
+              "k": "con",
+              "name": "List",
+              "args": [{ "k": "var", "name": "a" }]
+            }
+          ]
+        }
+      ]
+    },
+    {
+      "kind": "fn",
+      "name": "inc",
+      "type": {
+        "k": "fn",
+        "params": [{ "k": "con", "name": "Int" }],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": ["x"],
+      "doc": "Add 1 to an Int.",
+      "body": {
+        "t": "app",
+        "fn": { "t": "var", "name": "+" },
+        "args": [
+          { "t": "var", "name": "x" },
+          { "t": "lit", "lit": { "kind": "int", "value": 1 } }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "map",
+      "type": {
+        "k": "forall",
+        "vars": ["a", "b"],
+        "body": {
+          "k": "fn",
+          "params": [
+            {
+              "k": "fn",
+              "params": [{ "k": "var", "name": "a" }],
+              "ret": { "k": "var", "name": "b" },
+              "effects": []
+            },
+            {
+              "k": "con",
+              "name": "List",
+              "args": [{ "k": "var", "name": "a" }]
+            }
+          ],
+          "ret": {
+            "k": "con",
+            "name": "List",
+            "args": [{ "k": "var", "name": "b" }]
+          },
+          "effects": []
+        }
+      },
+      "params": ["f", "xs"],
+      "doc": "Polymorphic map: apply f to every element, recursing on the tail.",
+      "body": {
+        "t": "match",
+        "scrutinee": { "t": "var", "name": "xs" },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "Nil", "fields": [] },
+            "body": {
+              "t": "ctor",
+              "type": "List",
+              "ctor": "Nil",
+              "args": []
+            }
+          },
+          {
+            "pat": {
+              "p": "ctor",
+              "ctor": "Cons",
+              "fields": [
+                { "p": "var", "name": "h" },
+                { "p": "var", "name": "t" }
+              ]
+            },
+            "body": {
+              "t": "ctor",
+              "type": "List",
+              "ctor": "Cons",
+              "args": [
+                {
+                  "t": "app",
+                  "fn": { "t": "var", "name": "f" },
+                  "args": [{ "t": "var", "name": "h" }]
+                },
+                {
+                  "t": "app",
+                  "fn": { "t": "var", "name": "map" },
+                  "args": [
+                    { "t": "var", "name": "f" },
+                    { "t": "var", "name": "t" }
+                  ]
+                }
+              ]
+            }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "print_list",
+      "type": {
+        "k": "fn",
+        "params": [
+          {
+            "k": "con",
+            "name": "List",
+            "args": [{ "k": "con", "name": "Int" }]
+          }
+        ],
+        "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": ["xs"],
+      "doc": "Print each Int on its own line.",
+      "body": {
+        "t": "match",
+        "scrutinee": { "t": "var", "name": "xs" },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "Nil", "fields": [] },
+            "body": { "t": "lit", "lit": { "kind": "unit" } }
+          },
+          {
+            "pat": {
+              "p": "ctor",
+              "ctor": "Cons",
+              "fields": [
+                { "p": "var", "name": "h" },
+                { "p": "var", "name": "t" }
+              ]
+            },
+            "body": {
+              "t": "seq",
+              "lhs": {
+                "t": "do",
+                "op": "io/print_int",
+                "args": [{ "t": "var", "name": "h" }]
+              },
+              "rhs": {
+                "t": "app",
+                "fn": { "t": "var", "name": "print_list" },
+                "args": [{ "t": "var", "name": "t" }]
+              }
+            }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "doc": "Map inc over [1,2,3] via polymorphic List, then print: 2,3,4.",
+      "body": {
+        "t": "app",
+        "fn": { "t": "var", "name": "print_list" },
+        "args": [
+          {
+            "t": "app",
+            "fn": { "t": "var", "name": "map" },
+            "args": [
+              { "t": "var", "name": "inc" },
+              {
+                "t": "ctor",
+                "type": "List",
+                "ctor": "Cons",
+                "args": [
+                  { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+                  {
+                    "t": "ctor",
+                    "type": "List",
+                    "ctor": "Cons",
+                    "args": [
+                      { "t": "lit", "lit": { "kind": "int", "value": 2 } },
+                      {
+                        "t": "ctor",
+                        "type": "List",
+                        "ctor": "Cons",
+                        "args": [
+                          { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+                          {
+                            "t": "ctor",
+                            "type": "List",
+                            "ctor": "Nil",
+                            "args": []
+                          }
+                        ]
+                      }
+                    ]
+                  }
+                ]
+              }
+            ]
+          }
+        ]
+      }
+    }
+  ]
+}