F5b: Instantiation::apply substituted concrete pins but ERASED symbolic
Var endpoints back to the fresh var, so a generic threading its own T
(fn wrap<T>(v: T) -> T = identity::<T>(v) — the Alloc::read<T> shape)
synthesized its tail at a stray fresh var and E0722 fired. The law is now
uniform: every binding applies verbatim (rewrite over bindings.get),
no is-Var special case; unpinned vars stay put (E0706 fail-soft kept).

F5a: ckc check <dir> ran NO type checker — a well-resolved, ill-typed
program reported clean while run errored. check now folds the exact
run-path cascade (shared run_type_cascade; app_type_diagnostics), gated
on a resolution-clean app closure exactly as compile_project_object
stages it. --traps stays resolution-only (the corpus trap.md reconcile
contract). Zero goldens re-specified.

New coverage: corpus stone generic_thread (concrete + symbolic pins,
exit 42, freestanding-gated by generic_thread_run.rs; red-proven — the
reversed fix fails it with E0722) and check.rs pinning that check
surfaces E0722 where the resolution-only path must not.

FLAGGED, not touched: ckc check over the injected stdlib surfaces ~150
latent E0702 (true per synthesis-only law: bare literals into width
params) + one suspected E0726 false positive ({}::<Admin> with u) —
the stdlib is codegen-correct but not type-clean; owner follow-up needed.

@@ -60,0 +66,4 @@
+/// (`app::closure_check_diagnostics`) surfaces it; the resolution-only reconcile
+/// path (`app::closure_diagnostics`) must NOT — the two contracts stay distinct.
+#[test]
+fn ckc_check_reports_a_type_error_that_resolution_alone_misses() {

@@ -0,0 +195,4 @@
+        let workspace = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+            .parent()
+            .and_then(Path::parent)
+            .expect("workspace root from ck_driver manifest dir")