diff --git a/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag b/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag index 1582d1d89f2..1065272e04f 100644 --- a/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag +++ b/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag @@ -14,7 +14,7 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode { "RUNG FOUND AT: mitigated on the operator route; below the floor on the value route (the cast's type was dropped, so `x as Q` was Accepted with `Q` declared nowhere). CEILING: structurally guaranteed -- a cast lowers to a value carrying its operand and its target type, or refuses.", "RUNG NOW: mitigated on EVERY route. `v2.compiler.body_lowering_fold` `body_lower_postfix_expr` refuses a postfix chain carrying an as-suffix with `body_lowering_reason_type_annotation_not_carried` located at the authored target type -- the one reason for a type the lowering cannot carry, shared with the let annotation -- and `body_lower_arm_operand_resolved_optional` declines a cast so a let value or an arm reaches that refusal instead of answering the operand. A declared target refuses too: nothing is carried, so nothing is accepted. As an operator operand the cast now refuses with the same reason, because the postfix is folded before the operator reader sees it. CENSUS: the v2-route identity census over the 321-path population (`v2.compiler.reference_conservation_census` `reference_conservation_stratified_sample_paths` plus six) re-derived by `reference_conservation_census_for_paths` over each arm (pair 620ecb0a50f / 4c9f8d326d3): the modules that newly refuse are data rows casting a literal to a refinement and fn bodies casting to String, each refusing whole, and each returns when the trigger below lands.", "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY (the one the refusal above was retired by): a TYPED CAST NODE -- `e as T` lowers to Transform[coerce, e] with `v2.std.type_binder` `` -> T beside its positional children, and that node is SUFFICIENT FOR: resolve binding T in type role through the shared type-role frame (an undeclared T refusing at T); infer admitting the crossing through `v2.std.coercion` (not `std.coercion` `dag_cast_rules`, which is v1's side of `coercion_two_algebras_answer_one_question_stall`) or refusing typed; and translate and eval realizing it or refusing typed -- on every route, for every cast the refusal now stops.", - "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its carrier (`x as Int` from `x: Pos`) REFUSES, loud and typed at the operand, until `v2.std.coercion` admits a refinement-to-declared-carrier crossing as Widened from the type declaration (its existing widening fold needs per-domain integer value sets); it previously admitted only because an unscoped parameter walk bound x to an unrelated `fn positive(x: Int)`. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.", + "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its DECLARED carrier (`x as Int` from `x: Pos`, `type Pos = Int where positive`) is ADMITTED as Widened: `v2.compiler.infer` `refinement_declaration` reads the carrier from the declaration the reference's path reaches, and `v2.std.coercion` `coercion_cast_crossing` composes that carrier edge with the same exact-structural find_witness -- no preservation rule is added and no predicate is evaluated. Only the DECLARED carrier widens, one step: `x as Bool` from x: Pos and `x as Neg` between two refinements of Int REFUSE at the operand; for a refinement of a refinement (`type Pos2 = Pos where ..`) `x as Pos` is Widened and `x as Int` REFUSES (the carrier edge is not walked). The declaration is read through `v2.std.symbol_index` `symbol_index_lookup` on `v2.compiler.resolve` `ResolvedTree` `resolved_declarations` (gunbc#12629: declarations with resolved bodies, so a carrier is the identity resolve bound), and a lookup miss refuses (`bcn_a_refinement_lookup_miss_refuses`). Residue on that arm: the lowered cast's operator names `CoercionCrossing` by the exact rule (`v2.std.compilers.target_model` `canonical_operation_op_coerce`), fixed at lowering, so a Widened crossing is realized under that identity; both are representation-preserving (`OperandUnchanged`), so no emitted program differs. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.", ], evidence: [ @@ -36,7 +36,11 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode { DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_loop_passes_the_resolver_gate", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_foreign_label_on_a_transform_refuses", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_into_a_refinement_refuses_at_infer", field: WholeDeclaration }, - DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_refuses_until_carrier_widening", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_between_sibling_refinements_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_refinement_lookup_miss_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_refinement_of_a_refinement_widens_one_step", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_identity_cast_into_a_refinement_admits", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_as_cast_operand_resolves", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "a_parenthesised_call_operand_resolves", field: WholeDeclaration }, diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index a31cf948c4e..f761f083235 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -15,6 +15,7 @@ import v2.std.compilers.target_model { target_model_canonical_operation_member_declared_type } import v2.compiler.resolve { ResolvedTree } +import v2.std.symbol_index { SymbolIndex, symbol_index_lookup } import v2.compiler.inferred_tree { DerivedGrounding, GroundingNotDerived, @@ -882,7 +883,7 @@ fn infer_product_facts_from_entries( } } -fn infer_node_facts(n: Node, partials: List, kinds: List, tree: Node) -> Outcome { +fn infer_node_facts(n: Node, partials: List, kinds: List, resolved: ResolvedTree) -> Outcome { match infer_bounded_lattice_consumer_gate(consumer: n, partials: partials) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: _, diagnostics: cd } => @@ -929,7 +930,7 @@ fn infer_node_facts(n: Node, partials: List, kinds: List, descent: Holds { value: descent_proof } ) Absent => - match infer_parameter_type_in_scope(tree: tree, reference: n, binding: binding) { + match infer_parameter_type_in_scope(tree: resolved.root, reference: n, binding: binding) { Present { value: domain_ty } => inferred_facts_from_derived_type( node: n, @@ -1172,7 +1173,13 @@ fn infer_arrow_domain_type_for_binding(arrow: Node, binding: Symbol) -> Optional // occurrence identity) and each Arrow on the way back up binds it if its domain names it. // Consumers: infer_node_facts' parameter arm (the grounding every cast, add, application, branch, // match and loop operand reads) and infer_branch_operand_resolved_type_in_tree. -// interim: dissolve-on the SymbolIndex / ResolvedTree.bindings lookup, as before. +// FROZEN, A DECLARED FRONTIER (neat-boar-16 ruling): no new callers and no new arms. A declaration +// reference is answered by v2.std.symbol_index symbol_index_lookup on the ResolvedTree infer receives +// (refinement_declaration), but a frame-bound parameter reference reaches infer as a bare +// canonical_atom with no path (v2.compiler.resolve, the BoundInFrame arm), so this walk still scopes +// it. NEXT TRIGGER, NAMING THE CAPABILITY: resolve emits every frame-bound parameter reference as a +// declaration reference keyed in SymbolIndex, and eval + translate bind through it -- then this search +// and infer_parameter_type_in_scope are deleted. type InferParameterScopeSearch = ParameterReferenceNotHere | ParameterReferenceUnbound @@ -1207,6 +1214,59 @@ fn infer_parameter_type_in_scope(tree: Node, reference: Node, binding: Symbol) - } } +// A REFINEMENT DECLARATION, READ FROM A TYPE REFERENCE THROUGH THE AUTHORITY RESOLUTION USED. A +// resolved reference carries its declaration's qualified path (v2.std.qualified_name +// declaration_reference_path_optional); the declaration is what v2.std.symbol_index +// symbol_index_lookup answers for that path in the DECLARATIONS WITH RESOLVED BODIES +// (v2.compiler.resolve ResolvedTree resolved_declarations, gunbc#12629) -- never symbol_index, which +// holds declarations as authored -- so the carrier is the identity resolve bound: `Int` is the kernel +// binding, `Pos` (as Pos2's carrier) is its declaration reference. No tree is walked and no second +// reference->declaration route exists. `type Pos = Int where positive` is stored as its member `Conj { : Int, +// : clause }` (v2.compiler.body_lowering_fold body_lower_type_variant, the +// head lowered as a type). A MISS IS ABSENT, and Absent never admits: the declared-carrier widening +// runs only after the exact crossing refused, so a lookup that finds nothing leaves that refusal +// standing (v2.test.claim.body_cast_node bcn_a_refinement_lookup_miss_refuses). +// CONSUMERS. .carrier is consumed in this change: refinement_declared_carrier hands it to +// v2.std.coercion coercion_cast_crossing, the declared-carrier widening. .where_clause is a DECLARED +// FRONTIER, not yet consumed: its consumer is the literal-into-refinement cast arm of work item +// adhoc-032c89dc-138 (deep-bee-18), which projects it into resolve's where-predicate bindings. That arm +// lands with the next-rung trigger of gunbc.recurring_failure_mode as_cast_has_no_lowered_form +// (v2.std.coercion deciding a refinement's predicate on the cast operand); it must refuse on Absent +// too, never read a miss as "not a refinement". Absent when the reference is not a declaration +// reference, the index holds no unambiguous declaration at its path, or the declaration carries no +// where clause (it is then not a refinement, and has no carrier to widen to). +type RefinementDeclaration { + carrier: Node + where_clause: Node +} + +fn refinement_declaration(index: SymbolIndex, reference: Node) -> Optional { + match declaration_reference_path_optional(node: reference) { + Absent => Absent + Present { value: path } => + match symbol_index_lookup(index: index, qualified_path: path) { + Absent => Absent + Present { value: decl } => + match find_named_child(root: decl, name: ^dag_surface_where_refinement_clause) { + Rejected { diagnostics: _ } => Absent + Accepted { value: clause, diagnostics: _ } => + match find_named_child(root: decl, name: ^dag_surface_type_expr) { + Rejected { diagnostics: _ } => Absent + Accepted { value: head, diagnostics: _ } => + Present { value: RefinementDeclaration { carrier: head, where_clause: clause } } + } + } + } + } +} + +fn refinement_declared_carrier(index: SymbolIndex, source_type: Node) -> Optional { + match refinement_declaration(index: index, reference: source_type) { + Present { value: d } => Present { value: d.carrier } + Absent => Absent + } +} + // The literal and arrow-domain arms below derive a real type for the operand; the remaining arm // falls through to the operand's own inferred facts. When those facts are the GroundingNotDerived // frontier there is no operand type, and this now refuses (Violates) instead of returning the @@ -1218,7 +1278,7 @@ fn infer_parameter_type_in_scope(tree: Node, reference: Node, binding: Symbol) - fn infer_branch_operand_resolved_type_in_tree( node: Node, facts: InferredFacts, - tree: Node, + resolved: ResolvedTree, ) -> Witness { match dag_canonical_literal_from_node(node: node) { Accepted { value: literal, diagnostics: _ } => @@ -1226,7 +1286,7 @@ fn infer_branch_operand_resolved_type_in_tree( Rejected { diagnostics: _ } => match infer_atom_binding_sym(node: node) { Present { value: binding } => - match infer_parameter_type_in_scope(tree: tree, reference: node, binding: binding) { + match infer_parameter_type_in_scope(tree: resolved.root, reference: node, binding: binding) { Present { value: domain_ty } => Holds { value: domain_ty } Absent => inferred_facts_resolved_type(facts: facts) } @@ -1235,8 +1295,16 @@ fn infer_branch_operand_resolved_type_in_tree( } } +// The operand's type with no enclosing tree: a literal's own type, else the operand's inferred facts. +// It has no parameter arm -- the previous spelling passed the operand as its own tree, where the +// scope search can never bind (the reference is the root), so this states that result directly +// rather than handing a node to a ResolvedTree position it never came from. fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Witness { - infer_branch_operand_resolved_type_in_tree(node: node, facts: facts, tree: node) + match dag_canonical_literal_from_node(node: node) { + Accepted { value: literal, diagnostics: _ } => + infer_binding_value_type_witness(binding: infer_literal_type_binding(literal: literal), at: node) + Rejected { diagnostics: _ } => inferred_facts_resolved_type(facts: facts) + } } fn inferred_facts_from_derived_type( @@ -1608,7 +1676,7 @@ fn infer_match_bool( node: Node, partials: List, entries: List, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { @@ -1632,7 +1700,7 @@ fn infer_match_bool( match infer_branch_operand_resolved_type_in_tree( node: scrutinee_target, facts: scrutinee_facts, - tree: tree + resolved: resolved ) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: scrutinee_type } => @@ -1806,15 +1874,15 @@ fn infer_unify_transform_operand_types( left_facts: InferredFacts, right_node: Node, right_facts: InferredFacts, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { - match infer_branch_operand_resolved_type_in_tree(node: left_node, facts: left_facts, tree: tree) { + match infer_branch_operand_resolved_type_in_tree(node: left_node, facts: left_facts, resolved: resolved) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: left_type } => match infer_branch_operand_resolved_type_in_tree( node: right_node, facts: right_facts, - tree: tree + resolved: resolved ) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: right_type } => @@ -2247,7 +2315,7 @@ fn infer_transform_binary_infix( node: Node, partials: List, entries: List, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { @@ -2280,7 +2348,7 @@ fn infer_transform_binary_infix( left_facts: left_facts, right_node: right_target, right_facts: right_facts, - tree: tree + resolved: resolved ) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: unified_type, diagnostics: ud } => @@ -2443,9 +2511,9 @@ fn infer_gather_match_row_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_match_bool(node: node, partials: partials, entries: entries, tree: tree) { + match infer_match_bool(node: node, partials: partials, entries: entries, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2539,9 +2607,9 @@ fn infer_gather_transform_frontier_on_entries( pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_node_facts(n: node, partials: partials, kinds: kinds, tree: tree) { + match infer_node_facts(n: node, partials: partials, kinds: kinds, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2602,11 +2670,11 @@ fn infer_type_equal_ignoring_provenance(a: Node, b: Node) -> Bool { exact_structural_equality_zip_fold(source_facts: a, candidate: b) } -fn infer_list_element_type(element: Node, entries: List, tree: Node) -> Outcome { +fn infer_list_element_type(element: Node, entries: List, resolved: ResolvedTree) -> Outcome { match lookup_inferred_facts_in_entries(entries: entries, key: element) { Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: element)) Present { value: facts } => - match infer_branch_operand_resolved_type_in_tree(node: element, facts: facts, tree: tree) { + match infer_branch_operand_resolved_type_in_tree(node: element, facts: facts, resolved: resolved) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: t } => outcome_accepted(value: t) } @@ -2618,16 +2686,16 @@ fn infer_list_element_type(element: Node, entries: List, tre fn infer_list_elements_unified_type( elements: List, entries: List, - tree: Node + resolved: ResolvedTree ) -> Optional> { match elements { Empty => Absent Cons { head: first, tail: rest } => Present { - value: bind_outcome(o: infer_list_element_type(element: first, entries: entries, tree: tree), f: fn(t) { + value: bind_outcome(o: infer_list_element_type(element: first, entries: entries, resolved: resolved), f: fn(t) { fold(rest, init: outcome_accepted(value: t), f: fn(acc, element) { bind_outcome(o: acc, f: fn(unified) { - bind_outcome(o: infer_list_element_type(element: element, entries: entries, tree: tree), f: fn(et) { + bind_outcome(o: infer_list_element_type(element: element, entries: entries, resolved: resolved), f: fn(et) { if infer_type_equal_ignoring_provenance(a: unified, b: et) { outcome_accepted(value: unified) } else { @@ -2657,9 +2725,9 @@ fn infer_transform_freemonoid_introduction( node: Node, elements: List, entries: List, - tree: Node + resolved: ResolvedTree ) -> Optional> { - match infer_list_elements_unified_type(elements: elements, entries: entries, tree: tree) { + match infer_list_elements_unified_type(elements: elements, entries: entries, resolved: resolved) { Absent => Absent Present { value: unified } => Present { @@ -2684,15 +2752,15 @@ fn infer_gather_transform_row_on_entries( pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match list_introduction_elements_optional(node: node) { Absent => - infer_gather_application_row_on_entries(node: node, entries: entries, pending: pending, partials: partials, kinds: kinds, tree: tree) + infer_gather_application_row_on_entries(node: node, entries: entries, pending: pending, partials: partials, kinds: kinds, resolved: resolved) Present { value: elements } => - match infer_transform_freemonoid_introduction(node: node, elements: elements, entries: entries, tree: tree) { + match infer_transform_freemonoid_introduction(node: node, elements: elements, entries: entries, resolved: resolved) { Absent => - infer_gather_transform_frontier_on_entries(node: node, entries: entries, pending: pending, partials: partials, kinds: kinds, tree: tree) + infer_gather_transform_frontier_on_entries(node: node, entries: entries, pending: pending, partials: partials, kinds: kinds, resolved: resolved) Present { value: introduced } => match introduced { Rejected { diagnostics: r } => @@ -2740,7 +2808,7 @@ fn infer_gather_application_row_on_entries( pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match infer_application_argument_inhabitance(node: node, entries: entries) { Rejected { diagnostics: r } => @@ -2759,7 +2827,7 @@ fn infer_gather_application_row_on_entries( node: node, partials: partials, entries: entries, - tree: tree, + resolved: resolved, arguments_decided: infer_diagnostics_none(d: id) ) { Present { value: derived } => @@ -2809,7 +2877,7 @@ fn infer_gather_application_row_on_entries( pending: merged_pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } } @@ -2823,7 +2891,7 @@ fn infer_gather_application_row_on_entries( // not derived leaves the check unjudged and the Bind on the counted frontier, as an unannotated Bind // is: the check is neither admitted nor skipped silently. -fn infer_bind_annotation_check(node: Node, entries: List) -> Outcome { +fn infer_bind_annotation_check(node: Node, entries: List, resolved: ResolvedTree) -> Outcome { match type_annotation_optional(n: node) { Absent => outcome_accepted(true) Present { value: annotation } => @@ -2836,7 +2904,12 @@ fn infer_bind_annotation_check(node: Node, entries: List) -> match bound_facts.grounding { GroundingNotDerived { node: _ } => outcome_accepted(true) DerivedGrounding { grounding: g } => - match coercion_cast_crossing(source: g, source_type: g.witness.structural.evidence, target: annotation) { + match coercion_cast_crossing( + source: g, + source_type: g.witness.structural.evidence, + source_declared_carrier: refinement_declared_carrier(index: resolved.resolved_declarations, source_type: g.witness.structural.evidence), + target: annotation + ) { Accepted { value: _, diagnostics: d } => Accepted { value: true, diagnostics: d } Rejected { diagnostics: r } => Rejected { diagnostics: infer_bind_annotation_refusal(annotation: annotation, cause: r) } @@ -2870,9 +2943,9 @@ fn infer_gather_bind_annotation_row_on_entries( pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_bind_annotation_check(node: node, entries: entries) { + match infer_bind_annotation_check(node: node, entries: entries, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2890,7 +2963,7 @@ fn infer_gather_bind_annotation_row_on_entries( pending: diagnostics_merge(outer: pending, inner: d), partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } } @@ -2911,13 +2984,13 @@ fn infer_transform_derived_optional( node: Node, partials: List, entries: List, - tree: Node, + resolved: ResolvedTree, arguments_decided: Bool, ) -> Optional> { if infer_transform_is_binary_infix_int_add_shape(node: node) { - optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, tree: tree)) + optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, resolved: resolved)) } else if infer_transform_is_cast(node: node) { - infer_transform_cast_optional(node: node, entries: entries) + infer_transform_cast_optional(node: node, entries: entries, resolved: resolved) } else if arguments_decided { infer_transform_application_optional(node: node, entries: entries) } else { @@ -2974,7 +3047,7 @@ fn infer_transform_is_cast(node: Node) -> Bool { } } -fn infer_transform_cast_optional(node: Node, entries: List) -> Optional> { +fn infer_transform_cast_optional(node: Node, entries: List, resolved: ResolvedTree) -> Optional> { if !infer_transform_is_cast(node: node) { optional_absent() } else { @@ -2991,7 +3064,12 @@ fn infer_transform_cast_optional(node: Node, entries: List) GroundingNotDerived { node: _ } => optional_absent() DerivedGrounding { grounding: g } => optional_present(value: bind_outcome( - o: coercion_cast_crossing(source: g, source_type: g.witness.structural.evidence, target: target), + o: coercion_cast_crossing( + source: g, + source_type: g.witness.structural.evidence, + source_declared_carrier: refinement_declared_carrier(index: resolved.resolved_declarations, source_type: g.witness.structural.evidence), + target: target + ), f: fn(crossed) { match infer_descent_witness_for_node(n: node) { Violates { diagnostic: d } => Rejected { diagnostics: diagnostics_singleton(d: d) } @@ -3017,14 +3095,14 @@ fn infer_transform_cast_optional(node: Node, entries: List) // added without deciding, at this site, whether it derives its type or joins the counted frontier // -- never defaulted into by omission (DESIGN §4 closed vocabulary, §5 unwritable-by-construction). -fn infer_gather_fold_not_derived(n: Node, partials: List, kinds: List, tree: Node) -> InferGatherFoldAcc { +fn infer_gather_fold_not_derived(n: Node, partials: List, kinds: List, resolved: ResolvedTree) -> InferGatherFoldAcc { infer_gather_transform_frontier_on_entries( node: n, entries: empty_inferred_facts_entry_list(), pending: None, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } @@ -3036,7 +3114,7 @@ fn infer_gather_fold_not_derived(n: Node, partials: List, kinds: List, kinds: List, tree: Node) -> InferGatherFoldAcc { +fn infer_gather_fold_init(n: Node, partials: List, kinds: List, resolved: ResolvedTree) -> InferGatherFoldAcc { match n.kind { ComputationNode { behavior: Branch } => infer_gather_fold_acc_ok( @@ -3071,7 +3149,7 @@ fn infer_gather_fold_init(n: Node, partials: List, kinds: List infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) + ComputationNode { behavior: Value } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) ComputationNode { behavior: Transform } => if length(xs: n.children) == 0 { infer_gather_transform_row_on_entries( @@ -3080,7 +3158,7 @@ fn infer_gather_fold_init(n: Node, partials: List, kinds: List, kinds: List infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) + Absent => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) } - TypeNode { connective: Atom { identity: _ } } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) + TypeNode { connective: Atom { identity: _ } } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) TypeNode { connective: Conj } => match declaration_reference_path_optional(node: n) { - Present { value: _ } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) + Present { value: _ } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) Absent => if infer_type_node_awaits_product_row(kinds: kinds, n: n) { infer_gather_fold_acc_ok( @@ -3126,7 +3204,7 @@ fn infer_gather_fold_init(n: Node, partials: List, kinds: List @@ -3142,7 +3220,7 @@ fn infer_gather_fold_init(n: Node, partials: List, kinds: List if infer_type_node_awaits_product_row(kinds: kinds, n: n) { @@ -3157,10 +3235,10 @@ fn infer_gather_fold_init(n: Node, partials: List, kinds: List infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) - TypeNode { connective: Instantiation } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, tree: tree) + TypeNode { connective: Cardinality } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) + TypeNode { connective: Instantiation } => infer_gather_fold_not_derived(n: n, partials: partials, kinds: kinds, resolved: resolved) } } @@ -3431,7 +3509,7 @@ fn infer_gather_fold_step( child: InferGatherFoldAcc, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { if acc.failed { acc @@ -3442,7 +3520,7 @@ fn infer_gather_fold_step( merged_pending: acc.pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } else if child.failed { infer_gather_fold_acc_failed( @@ -3477,7 +3555,7 @@ fn infer_gather_fold_step( merged_pending: acc.pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } } else if infer_literal_edge_diagnostics_derived(parent: acc.node, edge: edge) { @@ -3499,7 +3577,7 @@ fn infer_gather_fold_step( merged_pending: acc.pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } } else { @@ -3509,7 +3587,7 @@ fn infer_gather_fold_step( merged_pending: diagnostics_merge(outer: acc.pending, inner: child.pending), partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } } @@ -3520,7 +3598,7 @@ fn infer_gather_fold_step_merged( merged_pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { let children_remaining = acc.children_remaining - 1 if acc.await_branch_row && children_remaining == 0 { @@ -3536,7 +3614,7 @@ fn infer_gather_fold_step_merged( entries: merged_entries, pending: merged_pending, partials: partials, - tree: tree + resolved: resolved ) } else if acc.await_loop_row && children_remaining == 0 { infer_gather_loop_row_on_entries( @@ -3552,10 +3630,10 @@ fn infer_gather_fold_step_merged( pending: merged_pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) } else if children_remaining == 0 { - infer_gather_settled_row(acc: acc, merged_entries: merged_entries, merged_pending: merged_pending, partials: partials, kinds: kinds, tree: tree) + infer_gather_settled_row(acc: acc, merged_entries: merged_entries, merged_pending: merged_pending, partials: partials, kinds: kinds, resolved: resolved) } else { infer_gather_fold_acc_ok( node: acc.node, @@ -3579,7 +3657,7 @@ fn infer_gather_settled_row( merged_pending: Diagnostics, partials: List, kinds: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match type_annotation_optional(n: acc.node) { Present { value: _ } => @@ -3589,7 +3667,7 @@ fn infer_gather_settled_row( pending: merged_pending, partials: partials, kinds: kinds, - tree: tree + resolved: resolved ) Absent => if infer_gather_acc_awaits_product_row(node: acc.node, entries: merged_entries) { @@ -3614,13 +3692,13 @@ fn infer_gather_settled_row( } } -fn infer_gather_fold_algebra(partials: List, kinds: List, tree: Node) -> NodeFold { +fn infer_gather_fold_algebra(partials: List, kinds: List, resolved: ResolvedTree) -> NodeFold { NodeFold { init: fn(n0) { - infer_gather_fold_init(n: n0, partials: partials, kinds: kinds, tree: tree) + infer_gather_fold_init(n: n0, partials: partials, kinds: kinds, resolved: resolved) }, step: fn(acc, e, child) { - infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials, kinds: kinds, tree: tree) + infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials, kinds: kinds, resolved: resolved) } } } @@ -3633,7 +3711,7 @@ fn infer_entries_for_tree(tree: ResolvedTree) -> Outcome CandidateSet { CandidateSet { candidates: [target], @@ -372,10 +385,8 @@ fn coercion_cast_target_singleton(target: Node) -> CandidateSet { } } -// source is the operand's grounding (its node is the operand, where a refusal is located) and -// source_type the type that grounding established. -fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: Node) -> Outcome { - match find_witness( +fn coercion_cast_exact_witness(source_type: Node, target: Node) -> Outcome { + find_witness( source_facts: source_type, candidates: coercion_cast_target_singleton(target: target), predicate: PreservationPredicate { @@ -383,7 +394,57 @@ fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: preservation_rule: ^preservation_rule_exact_structural_equality_zip_fold }, multiplicity_policy: UniqueOnly - ) { + ) +} + +fn coercion_cast_refused(source: CanonicalGrounding, upstream: NonEmptyDiagnostics) -> Outcome { + match coercion_wrap_find_witness_rejection(source: source, upstream: upstream) { + Accepted { value: wrapped, diagnostics: _ } => Rejected { diagnostics: wrapped } + Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r } + } +} + +// The Widened arm, reached only after the exact crossing on the source's own type refused; its own +// refusal is discarded for the original one, which is the mismatch the author wrote. +fn coercion_cast_to_declared_carrier( + source: CanonicalGrounding, + source_declared_carrier: Optional, + target: Node, + exact_refusal: NonEmptyDiagnostics, +) -> Outcome { + match source_declared_carrier { + Absent => coercion_cast_refused(source: source, upstream: exact_refusal) + Present { value: carrier } => + match coercion_cast_exact_witness(source_type: carrier, target: target) { + Accepted { value: fw, diagnostics: fw_d } => + Accepted { + value: CoercionResult { + target: fw.candidate, + quality: Widened, + witness: CoercionWitness { + homomorphism: HomomorphismWitness { + rule: ^homomorphism_rule_refinement_declared_carrier, + evidence: coercion_homomorphism_evidence(source: source, fw: fw) + } + } + }, + diagnostics: fw_d + } + Rejected { diagnostics: _ } => coercion_cast_refused(source: source, upstream: exact_refusal) + } + } +} + +// source is the operand's grounding (its node is the operand, where a refusal is located), +// source_type the type that grounding established, and source_declared_carrier the carrier its +// refinement declaration states (Absent when source_type is not a refinement). +fn coercion_cast_crossing( + source: CanonicalGrounding, + source_type: Node, + source_declared_carrier: Optional, + target: Node, +) -> Outcome { + match coercion_cast_exact_witness(source_type: source_type, target: target) { Accepted { value: fw, diagnostics: fw_d } => Accepted { value: CoercionResult { @@ -399,10 +460,12 @@ fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: diagnostics: fw_d } Rejected { diagnostics: r } => - match coercion_wrap_find_witness_rejection(source: source, upstream: r) { - Accepted { value: wrapped, diagnostics: _ } => Rejected { diagnostics: wrapped } - Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r } - } + coercion_cast_to_declared_carrier( + source: source, + source_declared_carrier: source_declared_carrier, + target: target, + exact_refusal: r + ) } } diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index 0733ad2e8df..8c3d10d552a 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -3,16 +3,17 @@ module v2.test.claim.body_cast_node import v2.std.arrow_signature { ApplicationBindingRefused, ApplicationBound, application_binding_plan, declared_signature } import v2.compiler.resolve { ResolvedTree } import std.algebra { Cons, Empty, list_snoc_item } -import v2.std.coercion { NoTargetCandidate } +import v2.std.coercion { CoercionQuality, CoercionResult, NoTargetCandidate, Widened, coercion_cast_crossing } import std.occurrence_identity { OccurrenceSynthetic } import v2.test.claim.type_param_binder_frame { tpb_accepts, tpb_assemble, tpb_refuses_with } import v2.compiler.emit { emit } import v2.compiler.eval { eval, inputs_root_only } -import v2.compiler.infer { InferredFacts, InferredTree, infer } +import v2.compiler.infer { InferredFacts, InferredTree, infer, refinement_declaration } import v2.extdeps.languages.dag { dag_arrow_domain_conj_node, dag_arrow_with_body_node, dag_int_literal_node_from_lexeme, dag_type_atom_node } import v2.extdeps.languages.rust_test { rust_binop_target_model_staging } import v2.extdeps.runtimes.v2_evaluator { v2_evaluator_interpretation } -import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_inferred_facts_from_nodes } +import v2.test.lens_common.infer_fixture { claim_canonical_grounding, claim_inferred_facts_from_nodes, claim_resolved_tree_without_declarations } +import v2.std.qualified_name { QualifiedName, declaration_reference_node } import v2.std.cardinality { termination_proof_witness_for_node } import v2.std.compilers.target_model { canonical_operation_op_coerce, target_model_canonical_operation_wire_node } import v2.std.collection { List } @@ -126,6 +127,41 @@ fn bcn_out_of_refinement() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Int {\n x as Int\n}\n") } +fn bcn_is_widened(q: Optional) -> Bool { + match q { + Present { value: Widened } => true + Present { value: _ } => false + Absent => false + } +} + +// The crossing's quality, from the real assembled tree: the refinement declaration the reference's +// path reaches, and the tree's one cast target. Absent when the tree refuses, the reader finds no +// refinement, the tree does not carry exactly one cast, or the crossing refuses. +fn bcn_crossing_quality(o: Outcome, reference_path: QualifiedName) -> Optional { + match o { + Rejected { diagnostics: _ } => Absent + Accepted { value: root, diagnostics: _ } => + match bcn_cast_targets(n: root.root) { + Cons { head: target, tail: Empty } => + match refinement_declaration(index: root.resolved_declarations, reference: declaration_reference_node(qn: reference_path, occurrence_id: OccurrenceSynthetic)) { + Absent => Absent + Present { value: decl } => + match coercion_cast_crossing( + source: claim_canonical_grounding(type_symbol: ^bcn_refinement_operand, algebra_symbol: ^bcn_refinement_operand), + source_type: declaration_reference_node(qn: reference_path, occurrence_id: OccurrenceSynthetic), + source_declared_carrier: Present { value: decl.carrier }, + target: target + ) { + Accepted { value: crossed, diagnostics: _ } => Present { value: crossed.quality } + Rejected { diagnostics: _ } => Absent + } + } + _ => Absent + } + } +} + fn bcn_refinement_param_as_bool() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Bool {\n x as Bool\n}\n") } @@ -458,17 +494,7 @@ fn bcn_refused_with_mismatch(o: Outcome) -> Bool { } } -// (15) THE CAST OUT OF A REFINEMENT REFUSES, STATED. A parameter is now bound by its ENCLOSING -// Arrow (v2.compiler.infer infer_parameter_type_in_scope), so `x` in `fn f(x: Pos)` grounds as the -// Pos declaration-reference, and Pos is not structurally Int: coercion_cast_crossing refuses with -// its typed mismatch. RED BEFORE: on main at 21f4d0c this row ADMITTED, by the wrong route -- the -// unscoped parameter walk bound f's `x` to the unrelated `fn positive(x: Int)`, and the crossing was -// Int to Int. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: v2.std.coercion admitting a cast from a -// refinement to its DECLARED carrier as Widened, decided from the type declaration; the existing -// coercion_fold_refinement_widening cannot carry it because its predicate needs per-domain integer -// value sets (v2.std.refinement_widening_predicate refinement_widening_value_sets_hold). When that -// lands this row flips to an accepting control asserting the Widened quality. The partner `x as Bool` -// refuses under both groundings. +// A refusal located at the cast's OPERAND (not at the `as` keyword), with coercion's typed mismatch. fn bcn_refused_with_mismatch_at_operand(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false @@ -486,12 +512,105 @@ fn bcn_operand_mismatch(x: Diagnostic) -> Bool { } } -test fn bcn_cast_out_of_a_refinement_refuses_until_carrier_widening() -> Bool { - bcn_refused_with_mismatch(o: bcn_refinement_param_as_bool_inferred()) - && bcn_refused_with_mismatch_at_operand(o: bcn_out_of_refinement_inferred()) +// (15) THE CAST OUT OF A REFINEMENT TO ITS DECLARED CARRIER IS ADMITTED, WIDENED. `x as Int` from +// `x: Pos` (`type Pos = Int where positive`): infer admits it on the production route, and the +// crossing's quality is Widened -- read by v2.compiler.infer refinement_declaration from the SAME +// assembled tree (the declaration reached by the reference's own path) and judged by +// v2.std.coercion coercion_cast_crossing against the SAME tree's cast target. RED BEFORE (main at +// 980761c838): infer refused NoTargetCandidate at the operand, because coercion judged only exact +// structural equality and Pos is not structurally Int. The route is asserted, not only the verdict: +// the quality is Widened, not Exact, so an admission through some other rule cannot green this row. +test fn bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens() -> Bool { + match bcn_out_of_refinement_inferred() { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => + bcn_is_widened(q: bcn_crossing_quality(o: bcn_out_of_refinement(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos, tail: Empty } })) + } } -// (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE. `x as Pos` from `x: Pos`: +// (15b)/(15c) ONLY THE DECLARED CARRIER WIDENS -- at v2.std.coercion's interface, with SUPPLIED +// values (DESIGN section 3, a witness discriminates at one interface): the source is a refinement's +// declaration reference, its declared carrier the node refinement_declaration returns, the target the +// cast's. Row (15) is the inhabitance claim that pairs them: on the production route the reader +// returns the kernel Int atom as Pos's carrier and it meets the tree's own cast target, so the Int +// atom supplied here is the shape the real producer emits. Row (16)'s partner keeps `x as Bool` from +// x: Pos refusing on the production route. +fn bcn_int_type() -> Node { dag_type_atom_node(identity: ^dag_binding_type_int) } +fn bcn_bool_type() -> Node { dag_type_atom_node(identity: ^dag_binding_type_bool) } +fn bcn_ref(leaf: Symbol) -> Node { + declaration_reference_node(qn: Cons { head: ^p, tail: Cons { head: leaf, tail: Empty } }, occurrence_id: OccurrenceSynthetic) +} +fn bcn_supplied_crossing(source_leaf: Symbol, carrier: Node, target: Node) -> Outcome { + coercion_cast_crossing( + source: claim_canonical_grounding(type_symbol: ^bcn_refinement_operand, algebra_symbol: ^bcn_refinement_operand), + source_type: bcn_ref(leaf: source_leaf), + source_declared_carrier: Present { value: carrier }, + target: target + ) +} +fn bcn_supplied_refuses(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => bcn_has_reason(d: d, reason: discriminant(v: NoTargetCandidate)) + } +} +fn bcn_supplied_quality(o: Outcome) -> Optional { + match o { + Accepted { value: crossed, diagnostics: _ } => Present { value: crossed.quality } + Rejected { diagnostics: _ } => Absent + } +} + +// (15b) ONE STEP, AND ONLY THE DECLARED CARRIER. `x as Bool` from x: Pos (carrier Int) refuses. For +// `type Pos2 = Pos where ..` the carrier read from resolved_declarations is the RESOLVED declaration +// reference to Pos (row 15c2 reads it on the production route), so `x as Pos` from x: Pos2 is Widened +// and `x as Int` from x: Pos2 REFUSES: the carrier edge is not walked to a fixed point. Supplied values +// at coercion's interface, in the shape the production route emits. RED if the widening arm admitted a +// non-carrier target or walked the carrier chain. +test fn bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses() -> Bool { + bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos, carrier: bcn_int_type(), target: bcn_bool_type())) + && bcn_is_widened(q: bcn_supplied_quality(o: bcn_supplied_crossing(source_leaf: ^Pos2, carrier: bcn_ref(leaf: ^Pos), target: bcn_ref(leaf: ^Pos)))) + && bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos2, carrier: bcn_ref(leaf: ^Pos), target: bcn_int_type())) +} + +// (15c2) A REFINEMENT OF A REFINEMENT WIDENS ONE STEP ON THE PRODUCTION ROUTE. `x as Pos` from +// `x: Pos2` (`type Pos2 = Pos where positive`): the crossing's quality is Widened, read through the +// production assembly's resolved_declarations, where Pos2's carrier is the resolved reference to Pos, +// against that tree's own cast target. infer's admission of a Widened cast end to end is row (15)'s +// subject; this row's is the resolved carrier, so infer is not re-run here (DESIGN section 3). The +// assembly is a producer rostered warm in v2.workflow.floor_pure_producer_share. RED BEFORE +// gunbc#12629: the carrier was the unresolved atom Pos and the cast refused. +fn bcn_refinement_of_refinement_as_its_carrier() -> Outcome { + tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Pos2 = Pos where positive\n\nfn f(x: Pos2) -> Pos {\n x as Pos\n}\n") +} + +test fn bcn_refinement_of_a_refinement_widens_one_step() -> Bool { + bcn_is_widened(q: bcn_crossing_quality(o: bcn_refinement_of_refinement_as_its_carrier(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos2, tail: Empty } })) +} + +// (15d) A REFINEMENT LOOKUP MISS REFUSES. When v2.compiler.infer refinement_declaration finds no +// declaration -- a tree inferred without resolution (v2.compiler.ingest's bridge supplies an index +// holding no declarations), or an index with no unambiguous entry at the path -- no carrier reaches +// coercion, and `x as Int` from a refinement-typed x keeps the exact crossing's refusal. RED if a +// miss were read as permission (the widening arm admitting with no declared carrier). +test fn bcn_a_refinement_lookup_miss_refuses() -> Bool { + bcn_supplied_refuses(o: coercion_cast_crossing( + source: claim_canonical_grounding(type_symbol: ^bcn_refinement_operand, algebra_symbol: ^bcn_refinement_operand), + source_type: bcn_ref(leaf: ^Pos), + source_declared_carrier: Absent, + target: bcn_int_type() + )) +} + +// (15c) A SIBLING REFINEMENT OVER THE SAME CARRIER IS NOT A CARRIER: `x as Neg` from x: Pos, both +// `Int where ..`, refuses. RED if sharing a carrier admitted a crossing between refinements. +test fn bcn_cast_between_sibling_refinements_refuses() -> Bool { + bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos, carrier: bcn_int_type(), target: bcn_ref(leaf: ^Neg))) +} + +// (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE -- and the required control of +// neat-boar-16's ResolvedTree ruling: `fn positive(x: Int)` beside `fn f(x: Pos)`, where x in f must ground +// as Pos (the frozen parameter scope search), or this cast refuses. `x as Pos` from `x: Pos`: // infer grounds x as the Pos declaration-reference from f's own domain, and coercion_cast_crossing // finds the target structurally equal. The RED beside it: the same operand cast to Bool refuses // (row 15's partner), so this is a judged crossing, not the frontier passing it over. RED BEFORE @@ -537,6 +656,7 @@ test fn bcn_a_foreign_label_on_a_transform_refuses() -> Bool { )) } + // (18b) THE OTHER HALF OF THE SPLIT WALL: a named label that names no parameter of the callee has no // slot, and the one binding authority refuses it -- so no Accepted program holds a foreign label on an // application either. The callee declares `x`; the actual is labelled `bcn_not_a_marker`. diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index fb3850534b4..d853fedcefa 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -519,6 +519,8 @@ import v2.std.collection { List } // THE declaration_graft_assemble PRODUCERS EARN THEIR ROWS ON THE FILL-THAT-CANNOT-LAND (ten on the // receipt below; an eleventh, declaration_graft_where_alias_undeclared_carrier_assembled, is the RED of // the resolved where-head -- one assembly, on the same ground) +// v2.test.claim.body_cast_node bcn_refinement_of_refinement_as_its_carrier is the same ground for the +// Widened cast's one-step row (gunbc#12407): one assembly of a two-refinement module. // GROUND, AND SIX OF THEM ON THE SHARING GROUND AS WELL. Receipt, re-derivable: required-floor // run 35467726264 (gunbc#11574 head 1797ea43bd) reported fourteen of that file's claims // COMPLETED-OVER-COST-REQUIREMENT at 73,857-148,646 eval steps against the 72,300 new-witness @@ -1121,7 +1123,8 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.declaration_graft_assemble.declaration_graft_record_construct_assembled", "v2.test.claim.declaration_graft_assemble.declaration_graft_record_type_only_assembled", "v2.test.claim.declaration_graft_assemble.declaration_graft_flag_and_rec_assembled", - "v2.test.claim.declaration_graft_assemble.declaration_graft_where_alias_undeclared_carrier_assembled" + "v2.test.claim.declaration_graft_assemble.declaration_graft_where_alias_undeclared_carrier_assembled", + "v2.test.claim.body_cast_node.bcn_refinement_of_refinement_as_its_carrier" ] // grammar_relation_row_for_emitted HAS NOW BEEN MEASURED ON THE THIRD CONJUNCT, AND IT PASSES.