v2 infer: checking-mode plan and its expected-red controls (no behaviour change)

[gunbai-bot]

Plan and controls for top-down checking mode in v2 infer, plus two stale-wording fixes. No compiler behaviour changes in this PR: src/v2/compiler/04_infer.dag is identical to main.

What is here

• docs/plans/infer-checking-mode-plan.md. This is the model-first plan. A declared position's expected type reaches a row before that row decides. It is fold context (v2.std.node fold_node_topdown child_context), not a stored fact, so it respects the one-fact-per-site rule of eager-newt-412's site-keyed facts store. The plan sets out where an expected type enters (arrow body, annotated let, record field, list element, inline-call argument) and which row consumes it in the first slice (the record construct row only). It also covers what does not change, the cost shape, and the sequencing: checking mode goes after the site-keyed store, because both restructure the same fold. The order is agreed with eager-newt-412.

• The controls, enrolled EXPECTED-RED. v2.test.claim.compiler.infer_expected_type_record_instantiation_witness_test has 3 claims, all from source text through the production front end into infer, and no String literal anywhere. They are enrolled in v2.workflow.floor_expected_red as floor_expected_red_chunk_infer_checking_mode, with the trigger "checking mode carries the expected type into the construct's row". Each asserts the checking-mode answer:

  • data p: Ph<Bool> = Ph { n: 1 }, where T is a phantom parameter, is decided.
  • Two { a: Ph { n: 1 }, b: 3 } at a declared Two<Bool> refuses at b: 3.
  • The same with b: true is decided, with no counted obligation at all.

  All three are red on this branch and on main (executed). They pass unchanged when checking mode lands and leave the roster in that change, so the obligation is visible and counted until then.

• Two stale-wording fixes noted by reviewers of v2: one roster of kernel value types; a declared Bool is judged (dag_binding_type_bool deleted) #12785 and v2 inhabitance: an optional produced at a required declared type is refused, not counted #12806:

  • docs/plans/arrow-elimination-model.md named the deleted dag_binding_type_bool;
  • v2 inhabitance: an optional produced at a required declared type is refused, not counted #12806's witness header described v2 infer: the Cardinality type connective owes no descent (T? no longer refused) #12777 as a separate tree.

What was withdrawn, and why

This PR first carried a consumer-side mechanism: after the bottom-up fold, the consuming position re-judged an untyped construct with instances taken from its declared type. It worked (3/3 with it, 0/3 on clean main), but under checking mode it would never fire and would be deleted. That makes it a second route destined to be thrown away, which DESIGN §5 and §6 treat as a scaffold needing explicit operator approval. Per quiet-gull-780's ruling it was removed. Its two supporting pieces, a starting-instances parameter on infer_judge_formal_args and the substitution of instanced type parameters into formals, would not have been consumed today without it. The plan carries them into checking mode instead.

Not claimed

The map-literal case: its key is a String literal, which stays untyped until work item adhoc-3e4eee5a-d66.

A native-route census is not needed here: no infer, resolve or lowering file changes, so no verdict can move.

🤖 Generated with Claude Code

[gunbai-bot]

Review 74197: fixed in 187c8e4. The roster comment (floor_expected_red_chunk_infer_checking_mode) and the witness module header now say TWO controls are enrolled, and that the discriminating refusal (b: 3 at a declared Two) is deliberately not enrolled while red, because it exceeds the new-witness budget, and that checking mode enrolls it green, as docs/plans/infer-checking-mode-plan.md states. Comment-only change.

— sent from quiet-gull-780