v2: a parameter's type may carry a where refinement; it parses and the fn refuses at the clause until a carrier exists

dag/gunbc/recurring_failure_mode/parameter_refinement_has_no_carrier.dag

@@ -0,0 +1,21 @@
+module gunbc.recurring_failure_mode.parameter_refinement_has_no_carrier
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data parameter_refinement_has_no_carrier: RecurringFailureMode = RecurringFailureMode {
+  identity: "parameter_refinement_has_no_carrier" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: a fn parameter's type is refined by a where clause (`lifetime_seconds: Int where range(min: 1, max: 3600)`), which v1 reads (`v1` `02_parse` `parse_param`), and v2 has no way to carry the refinement on a lowered parameter: the one where-clause reader (`v2.compiler.body_lowering_fold` `body_lower_kept_where_clause`) serves a type variant, and a parameter's type is read by `body_lower_type_expr_lowered_optional`, whose sequence fallback keeps the base type and drops the clause.",
+    "HARM: a parameter lowered without its refinement admits every value of the base type at the call boundary the author narrowed, silently -- the refinement is the parameter's contract.",
+    "CONTAINED, NOT SILENT: the grammar parses the refinement (`v2.extdeps.languages.dag` `dag_grammar_typed_param_expr`, the refined arm taken only where a clause is written) and body lowering refuses the fn on both arms, located at the clause, as `body_lowering_reason_parameter_refinement_unmodeled` (`body_lower_param_refinement_refusal_optional`). The module refuses at normalize.",
+    "RUNG FOUND AT: mitigated (typed, located refusal). CEILING: structurally impossible -- a parameter's refinement is part of its lowered type. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: a parameter's lowered type carries its where-clause refinement, read through the one where-clause reader type variants use rather than a second one, so `body_lowering_reason_parameter_refinement_unmodeled` has no producer.",
+  ],
+
+  evidence: [
+    DeclarationRef { module_path: "v2.test.claim.parse.parameter_refinement", decl_name: "a_refined_parameter_parses_holds", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.parse.parameter_refinement", decl_name: "a_refined_parameter_refuses_at_its_clause_holds", field: WholeDeclaration },
+  ],
+}

src/v2/compiler/body_lowering_fold.dag

@@ -3590,7 +3590,29 @@ fn body_lower_pattern_generics_optional(captured: Node) -> Optional<Node> {
 fn body_lower_first_signature_refusal_optional(captured: Node) -> Optional<Outcome<Node>> {
   match body_lower_pattern_form_refusal_optional(captured: captured) {
     Present { value: refused } => optional_present(value: refused)
-    Absent => body_lower_fn_uses_refusal_optional(captured: captured)
+    Absent =>
+      match body_lower_param_refinement_refusal_optional(captured: captured) {
+        Present { value: refused } => optional_present(value: refused)
+        Absent => body_lower_fn_uses_refusal_optional(captured: captured)
+      }
+  }
+}
+
+// A PARAMETER WHOSE TYPE IS REFINED BY A WHERE CLAUSE REFUSES, LOCATED AT THE CLAUSE. The only
+// reader of a where clause (body_lower_kept_where_clause) serves a type variant; a parameter's type
+// is read by body_lower_type_expr_lowered_optional, which would keep the base type and drop the
+// refinement. So until a parameter's type can carry its refinement the fn refuses
+// (gunbc.recurring_failure_mode parameter_refinement_has_no_carrier). The clause is searched only
+// inside this declaration's own param_list.
+fn body_lower_param_refinement_refusal_optional(captured: Node) -> Optional<Outcome<Node>> {
+  match body_lower_find_captured(root: captured, emitted: ^dag_surface_param_list) {
+    ParseSubtreeAbsent => optional_absent()
+    ParseSubtreeFound { captured: param_list } =>
+      match body_lower_find_production_shell_optional(root: param_list, emitted: ^dag_surface_where_refinement_clause) {
+        Absent => optional_absent()
+        Present { value: clause } =>
+          optional_present(value: outcome_rejected(d: body_lower_diagnostic(reason: ^body_lowering_reason_parameter_refinement_unmodeled, n: clause)))
+      }
   }
 }
 

src/v2/extdeps/languages/dag.dag

@@ -804,12 +804,31 @@ fn dag_grammar_generic_params_expr() -> GrammarExpr {
   )
 }
 
+// A PARAMETER MAY REFINE ITS TYPE WITH A WHERE CLAUSE (`lifetime_seconds: Int where range(min: 1,
+// max: 3600)`), as v1 02_parse parse_param reads it. The refined form is the FIRST arm and requires
+// the clause, so it is taken only where one is written; an unrefined parameter falls to the second
+// arm, whose shape is exactly the one every parameter reader already reads. A refined parameter
+// does not lower yet: v2.compiler.body_lowering_fold refuses the fn at the clause
+// (body_lowering_reason_parameter_refinement_unmodeled) rather than reading the type and dropping
+// the refinement.
 fn dag_grammar_typed_param_expr() -> GrammarExpr {
-  dag_grammar_sequence(
-    left: dag_grammar_binding_name_terminal(),
+  dag_grammar_choice(
+    left: dag_grammar_sequence(
+      left: dag_grammar_binding_name_terminal(),
+      right: dag_grammar_sequence(
+        left: dag_grammar_terminal(token_class: ^dag_token_colon),
+        right: dag_grammar_sequence(
+          left: dag_grammar_nonterminal(production: ^dag_production_type_expr),
+          right: dag_grammar_nonterminal(production: ^dag_production_where_refinement_clause)
+        )
+      )
+    ),
     right: dag_grammar_sequence(
-      left: dag_grammar_terminal(token_class: ^dag_token_colon),
-      right: dag_grammar_nonterminal(production: ^dag_production_type_expr)
+      left: dag_grammar_binding_name_terminal(),
+      right: dag_grammar_sequence(
+        left: dag_grammar_terminal(token_class: ^dag_token_colon),
+        right: dag_grammar_nonterminal(production: ^dag_production_type_expr)
+      )
     )
   )
 }

src/v2/test/claim/parse/parameter_refinement_test.dag

@@ -0,0 +1,57 @@
+module v2.test.claim.parse.parameter_refinement
+
+import v2.compiler.reference_conservation_admission { conservation_subject_of_text }
+import v2.extdeps.languages.dag { parse_production_emitted_identity_optional }
+import v2.std.diagnostic { Accepted, NodeLocus, Rejected, diagnostics_fatal }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.std.logic { Bool }
+import v2.std.optional { Absent, Present }
+import v2.std.text { String }
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// A PARAMETER MAY REFINE ITS TYPE WITH A WHERE CLAUSE (v2.extdeps.languages.dag
+// dag_grammar_typed_param_expr), as v1 reads it. It PARSES; the fn REFUSES at the clause
+// (body_lowering_reason_parameter_refinement_unmodeled, gunbc.recurring_failure_mode
+// parameter_refinement_has_no_carrier) rather than lowering the base type and dropping the
+// refinement. An unrefined parameter is untouched.
+data refined_source: String = "module probe.param_refine\n\nfn wait(seconds: Int where range(min: 1, max: 3600)) -> Int {\n  seconds\n}\n"
+data plain_source: String = "module probe.param_refine\n\nfn wait(seconds: Int) -> Int {\n  seconds\n}\n"
+
+// Each outcome is computed ONCE as a nullary value, enrolled WARM in
+// v2.workflow.floor_pure_producer_share, and each claim reads it.
+fn refined_parsed() -> Bool {
+  match conservation_subject_of_text(path: "probe_refined.dag", text: refined_source).parsed {
+    Accepted { value: _, diagnostics: _ } => true
+    Rejected { diagnostics: _ } => false
+  }
+}
+
+fn refined_refused_at_clause() -> Bool {
+  match conservation_subject_of_text(path: "probe_refined.dag", text: refined_source).normalized {
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: d } =>
+      diagnostics_fatal(d: d).reason == ^body_lowering_reason_parameter_refinement_unmodeled
+        && match diagnostics_fatal(d: d).at {
+             NodeLocus { anchor: a } =>
+               match parse_production_emitted_identity_optional(node: a.at) {
+                 Present { value: id } => id == ^dag_surface_where_refinement_clause
+                 Absent => false
+               }
+             _ => false
+           }
+  }
+}
+
+fn plain_normalized() -> Bool {
+  match conservation_subject_of_text(path: "probe_plain.dag", text: plain_source).normalized {
+    Accepted { value: _, diagnostics: _ } => true
+    Rejected { diagnostics: _ } => false
+  }
+}
+
+test fn a_refined_parameter_parses_holds() -> Bool { refined_parsed() }
+
+test fn a_refined_parameter_refuses_at_its_clause_holds() -> Bool { refined_refused_at_clause() }
+
+test fn an_unrefined_parameter_still_normalizes_holds() -> Bool { plain_normalized() }

src/v2/workflow/compile_door_cause_ownership.dag

@@ -156,6 +156,12 @@ data known_frontier_causes: List<CauseOwnership> = [
     lane: SharedSelfHostCriticalPath,
     flip_trigger: "a `pattern` declaration shares the one fn_decl production but v1 admits it only without generic params and with a block body (dag syntax dag_item_forms: has_type_params false, body_kind BlockBody); a pattern-headed declaration writing generic params or an `= expr` body refuses located at what it wrote (v2.compiler.body_lowering_fold body_lower_pattern_form_refusal_optional). This is a fidelity wall, not a frontier: it retires only if the grammar can express the narrower pattern form without changing the fn_decl spine depth the positional readers walk, so the form becomes unwritable rather than refused"
   },
+  CauseOwnership {
+    cause: ^body_lowering_reason_parameter_refinement_unmodeled,
+    grain: FatalGrain,
+    lane: SharedSelfHostCriticalPath,
+    flip_trigger: "a fn parameter whose type is refined by a where clause parses and refuses at the clause on both lowering arms (v2.compiler.body_lowering_fold body_lower_param_refinement_refusal_optional), because the only where-clause reader serves a type variant and a parameter's type reader would drop the refinement. Flips when a parameter's lowered type carries its refinement -- the parameter type read through the one where-clause reader that type variants use -- so the reason has no producer (gunbc.recurring_failure_mode parameter_refinement_has_no_carrier)"
+  },
   CauseOwnership {
     cause: ^body_lowering_reason_uses_clause_unmodeled,
     grain: FatalGrain,

src/v2/workflow/floor_pure_producer_share.dag

@@ -1110,6 +1110,9 @@ data floor_cross_claim_pure_producers_warm: List<String> = [
   "v2.test.claim.parse.where_clause_required_comma.alias_then_service_parsed",
   "v2.test.claim.parse.where_clause_required_comma.two_predicates_parsed",
   "v2.test.claim.parse.where_clause_required_comma.adjacent_predicates_parsed",
+  "v2.test.claim.parse.parameter_refinement.refined_parsed",
+  "v2.test.claim.parse.parameter_refinement.refined_refused_at_clause",
+  "v2.test.claim.parse.parameter_refinement.plain_normalized",
   "v2.test.claim.occurrence_role.occurrence_role.binders_fixture_outcome",
   "v2.test.claim.occurrence_role.occurrence_role.mixed_param_list_parsed",
   "v2.test.claim.occurrence_role.occurrence_role.mixed_param_list_planted",