TY3 v0 — generic instantiation:
- ck_types::lift: GenericParam + GenericParamMap; a path-head whose name
  matches a generic-parameter binder lifts to Ty::Var instead of falling
  through to the nominal lookup.
- ck_types::signature: FnSignature.type_params; SignatureTable.next_var
  forks the per-call instantiation counter so fresh Vars never alias
  signature Vars; FnDecl::generic_params() (ck_syntax::bodies) enumerates
  the <A, B> binders.
- ck_types::instantiate (new): Instantiation { fresh, rename, bindings },
  try_bind, collect_from_match (structural match into Var/Nominal/Fn),
  close_var_chains (Var→Var chain closure), apply.
- ck_types::check: synth_generic_call orchestrator + helpers
  (instantiate_signature, collect_arg_bindings, report_generic_conflicts,
  report_generic_unbound, check_args_post_subst); softens residual Vars
  to Unknown so the E0702 cascade is suppressed when E0706 already named
  the unpinned slot.
- E0706 "cannot determine type argument" — primary on the call, secondary
  on the type-param's declaration.
- E0707 "conflicting bindings for `T`" — N binding-source secondaries,
  distinct from E0702 per the locked 2026-05-28 design entry.
- Gating fixtures: tests/types/infer_from_args.cktest (the happy path),
  tests/types/unpinnable_variable.cktest (E0706 only), tests/types/
  conflicting_bindings.cktest (E0707 + post-subst E0702).

Synthesis-only docs lock (2026-05-28):
- docs/impl/type-system/inference.md: rewritten — one mode (synthesis),
  no checking-mode propagation, no expected-type parameter. Lambdas
  synthesize from their annotated parameters. Generic args come from
  exactly two sources (turbofish first, arguments second); no third
  source from the surrounding context.
- docs/impl/type-system/TY3-generics-and-instantiation.md: explicit
  "no expected-return source" entry; locked open items (Var→Var chain
  closure, all-or-nothing turbofish, distinct E0707, recursive interner,
  effect-row carry-through, TY8 existential interaction).
- docs/impl/type-system/TY2-bidirectional-core.md: status note —
  bidirectional mode removed; "check" reads as the assignability
  assertion at every declared boundary. Numeric width-narrowing rule
  retired (bare literal always synthesizes its default; turbofish at the
  site is the only path to a fixed-width).
- docs/impl/type-system/type-representation.md: widening section renamed
  ("…lives at the assignment boundary"); payload-free variants flow via
  tag-membership (case 2), never via inference.
- docs/syntax.md: turbofish made universal — variant refs, empty list,
  empty map, numeric literals. No `_type` suffix sugar.
- docs/impl/type-system/README.md: cascade row updated.
- Dead-link sweep: anchors in 03-parser.md / slices.md /
  TY2-bidirectional-core.md / TY7-exhaustive-match-and-narrowing.md /
  errors-and-narrowing.md retargeted at the renamed headings.

Note: this commit still carries the ExpectedReturn binding source in
ck_types::instantiate and the expected: Option<&Ty> parameter through
synth_call / synth_uncached / synth_block / synth_with_expected. Both
are removed in the immediately-following synthesis-only delta commit
(Delta A in the coordinated landing). Landing TY3 v0 and the doc lock
as one commit keeps the moving parts together; the Delta A commit
brings the impl in line with the doc lock.

@@ -0,0 +253,4 @@
+    /// `Var` in the side-table matches TY2's fail-soft invariant (downstream
+    /// stages see a real, if incomplete, shape).
+    #[must_use]
+    pub fn apply(&self, ty: &Ty) -> Ty {