diff --git a/dag/gunbc/recurring_failure_mode/annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation.dag b/dag/gunbc/recurring_failure_mode/annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation.dag new file mode 100644 index 00000000000..a4a6c27ad59 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation.dag @@ -0,0 +1,26 @@ +module gunbc.recurring_failure_mode.annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation: RecurringFailureMode = RecurringFailureMode { + identity: "annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation" as NonEmptyStr, + + receipts: [ + "INVALID STATE: v2 answers one question -- does this produced value inhabit this declared type? -- through two relations chosen by position. An argument at its formal and a fn body at its declared return build a DeclaredTypeObligation and consult v2.std.inhabitance declared_type_inhabitance; an annotated let (`let x: T = e`) is judged by v2.compiler.infer infer_bind_annotation_check through v2.std.coercion coercion_cast_crossing, the fold a cast's crossing asks.", + + "HARM: a meaning fork at the relation layer (DESIGN section 3). The two relations are different procedures -- coercion selects a target-language inhabitant spelling under a TargetSelectionPolicy with its own mismatch vocabulary, inhabitance is find_witness over the declared singleton -- so one produced/declared pair can be admitted at a let and refused at an argument or a return, or refused under two different reason vocabularies. v2.std.inhabitance declared_type_inhabitance already records why routing an inhabitance question through coercion_fold would nickname target selection as typechecking; the let position does exactly that.", + + "DISTINGUISHING FACTS: an ascription converts nothing (infer_bind_annotation_check uses only the verdict, never a crossed value), so the let question is inhabitance, not a cast. DeclaredTypePosition names PositionDirectCallArgument and PositionDeclaredReturn and has no let arm; v1's DeclaredTypePosition carries PositionLetAnnotation, so the seed already models the let as a declared-type position of the one relation.", + + "RECOGNITION RULE: a DeclaredTypePosition-shaped question (produced type at an authored declared type) answered anywhere other than declared_type_inhabitance. Found 2026-09-27 while wiring the PositionDeclaredReturn producer (brief node adhoc-0e837314-c3c), and kept out of that change by the lane manager's ruling so the return producer lands on the relation its frontier named.", + + "RUNG FOUND AT: mitigatable on the let path (a mismatch coercion recognises refuses, located at the annotation, infer_reason_bound_value_does_not_inhabit_annotation); the fork itself is unrefused by any gate and held only by review.", + + "CEILING: structurally impossible -- one relation, positions as data. Decidable and fully modeled: the relation and the position vocabulary both exist.", + + "NEXT-RUNG TRIGGER: a PositionLetAnnotation arm on v2.std.inhabitance DeclaredTypePosition with infer_bind_annotation_check building a DeclaredTypeObligation and consulting declared_type_inhabitance, and coercion_cast_crossing no longer imported by that check, sufficient that every declared-type position in v2.compiler.infer reaches one relation; the let's discriminating RED and positive control re-enrolled on that route.", + ], + + evidence: [], +} diff --git a/dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag b/dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag index bc216cd5468..7c28c4d5e9d 100644 --- a/dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag +++ b/dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag @@ -15,7 +15,7 @@ data argument_type_obligation_absent_while_the_route_advances: RecurringFailureM "RECOGNITION RULE: an application whose argument type is derived and a distinct constructor from the formal is Accepted. The discriminating RED is v2.test.claim.compiler.infer_application_argument_inhabitance_witness_test infer_incompatible_argument_refuses_holds (Bool at an Int formal). Positive control: infer_compatible_argument_admits_holds.", - "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). A TypeNode Cardinality formal is not yet that counted frontier on infer: connective_multiplicity maps Cardinality to RequiresTerminationProof, so infer_node_facts Rejects before application inhabitance runs. infer_descent_witness_for_node remaps the upstream cardinality_descent_not_proven diagnostic to infer_descent_not_derived; that is the reason on the Outcome (infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.", + "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. Since 2026-09-27 GenericFormal means a formal that MENTIONS one of the callee's declared type variables (DeclaredTypeObligation.type_variables, read off the Arrow by v2.std.type_binder type_param_names); an Instantiation whose constructor and arguments are all established is decided by the same structural zip, so a `List` formal is judged rather than counted (a product argument at it now refuses, inhabitance_product_produced_at_a_collection_formal_refuses_holds). The declared side is read at its denotation (v2.extdeps.languages.dag dag_binding_denotation over each atom), and a bare declared atom that join does not denote is counted FormalUnresolved. The same relation now has a second producer, PositionDeclaredReturn: v2.compiler.infer infer_arrow_declared_return_check judges each Arrow body at its declared return and REPLACED the inline equality check #12379 had put on arrow introduction (infer_arrow_body_inhabits_declared_return, deleted; its reason arrow_body_does_not_inhabit_declared_return is kept, located at the body). Before the replacement a return that join did not denote was admitted with no diagnostic; it is now counted. Witnesses: v2.test.claim.compiler.infer_declared_return_inhabitance_witness_test (RED declared_return_int_with_a_bool_body_refuses_holds, controls declared_return_int_with_an_int_body_admits_holds and declared_return_bool_with_a_bool_body_admits_holds) and v2.test.claim.compiler.infer_arrow_elimination_witness_test. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). A TypeNode Cardinality formal is not yet that counted frontier on infer: connective_multiplicity maps Cardinality to RequiresTerminationProof, so infer_node_facts Rejects before application inhabitance runs. infer_descent_witness_for_node remaps the upstream cardinality_descent_not_proven diagnostic to infer_descent_not_derived; that is the reason on the Outcome (infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.", "RUNG FOUND AT, source to native emission: unclaimed. Native emission stays a declared frontier until v2.std.inhabitance is in the native 04_infer closure and infer_incompatible_argument_refuses_holds refuses on the emitted binary.", @@ -25,7 +25,7 @@ data argument_type_obligation_absent_while_the_route_advances: RecurringFailureM "NEXT-RUNG TRIGGER, widening: a producer supplies integer value-set evidence on produced and declared; then declared_type_inhabitance consumes preservation_rule_refinement_widening on that algebra.", - "NEXT-RUNG TRIGGER, unjudgeable applications: operator Arrow from ResolvedTree.bindings, argument type derivation, generic instantiation, and an honest TypeNode Cardinality / Optional multiplicity that does not dissolve RequiresTerminationProof without a replacement RED, sufficient that inhabitance OptionalCarrier is counted on infer (not Outcome Rejected for descent) and the InhabitanceUndecidable frontier count over reached applications is zero on both routes. The v2 arm of this class retires only when that count is zero on both routes.", + "NEXT-RUNG TRIGGER, unjudgeable applications: operator Arrow from ResolvedTree.bindings, argument type derivation (including an application's RESULT type, which infer leaves GroundingNotDerived, so a call producing `Outcome` at an `Outcome` formal or return is counted rather than decided), generic instantiation, and an honest TypeNode Cardinality / Optional multiplicity that does not dissolve RequiresTerminationProof without a replacement RED, sufficient that inhabitance OptionalCarrier is counted on infer (not Outcome Rejected for descent) and the InhabitanceUndecidable frontier count over reached applications is zero on both routes. The v2 arm of this class retires only when that count is zero on both routes.", "THIS IS NOT rest_ok_over_uninhabiting_body: that class is HTTP 200 mapped as RestOk over an uninhabiting body. This class is a compiler application-argument obligation absent while the route advances.", ], diff --git a/dag/gunbc/recurring_failure_mode/function_type_evidence_carries_its_body.dag b/dag/gunbc/recurring_failure_mode/function_type_evidence_carries_its_body.dag index 14ea96eba17..42b485c01a4 100644 --- a/dag/gunbc/recurring_failure_mode/function_type_evidence_carries_its_body.dag +++ b/dag/gunbc/recurring_failure_mode/function_type_evidence_carries_its_body.dag @@ -19,7 +19,7 @@ data function_type_evidence_carries_its_body: RecurringFailureMode = RecurringFa "CEILING: structurally impossible, since the Arrow's type node can be constructed as domain to codomain only.", - "NEXT-RUNG TRIGGER: a function-type introduction rule in v2.compiler.infer that derives an Arrow's type from its domain and declared return alone, with the body judged against the return (infer_arrow_body_inhabits_declared_return) instead of composed into the type, and a fixture constructor carrying the return once. It must be sufficient that two Arrows differing only in body derive equal types.", + "NEXT-RUNG TRIGGER: a function-type introduction rule in v2.compiler.infer that derives an Arrow's type from its domain and declared return alone, with the body judged against the return (v2.compiler.infer infer_arrow_declared_return_check) instead of composed into the type, and a fixture constructor carrying the return once. It must be sufficient that two Arrows differing only in body derive equal types.", ], evidence: [], diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index a31cf948c4e..e4af23c92a6 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -60,7 +60,7 @@ import v2.std.optional { optional_present } import v2.std.qualified_name { declaration_reference_node, declaration_reference_path_optional } -import v2.std.node { arrow_signature_order_label, edge_label_of } +import v2.std.node { Ambiguous, Found, arrow_body_target_lookup, arrow_signature_order_label, edge_label_of } import v2.std.list_introduction { list_introduction_elements_optional, list_introduction_head_path } import v2.std.arrow_signature { ApplicationBindingRefused, @@ -82,6 +82,7 @@ import v2.std.constraints { import v2.std.inhabitance { DeclaredType, DeclaredTypeObligation, + DeclaredTypePosition, DeclaredTypeVariable, TypeVariableInstance, inhabitance_formal_declaration, @@ -97,6 +98,7 @@ import v2.std.inhabitance { declared_type_inhabitance, inhabitance_node_undecidable_reason, inhabitance_undecidable_diagnostic, + position_declared_return, position_direct_call_argument, undecidable_argument_type_not_derived, undecidable_formal_unresolved @@ -702,51 +704,6 @@ fn infer_formation_child_evidence_edges( ) } -// ARROW INTRODUCTION: A BODIED ARROW'S BODY MUST INHABIT THE RETURN IT DECLARES. Asked only once every -// child of the Arrow is derived (the product row above), so the body's type is known. The body's -// value type must equal the declared return's denotation, structurally with provenance stripped -// (infer_type_equal_ignoring_provenance, the list rule's authority); otherwise the Arrow refuses, -// located at the body. An Arrow with no body edge, or whose return is not a binding the language -// join denotes, is not judged here -- and arrow elimination derives nothing from such a return. -fn infer_arrow_body_does_not_inhabit_declared_return_diagnostic(body: Node) -> Diagnostic { - Diagnostic { - reason: ^arrow_body_does_not_inhabit_declared_return, - at: node_locus(node: body), - correction: Unavailable { reason: ExternalContractUnknown } - } -} - -fn infer_arrow_body_inhabits_declared_return(node: Node, entries: List) -> Outcome { - match node.kind { - TypeNode { connective: Arrow } => - match arrow_body_target_lookup(children: node.children) { - Ambiguous => outcome_rejected(infer_canonical_grounding_incoherent_diagnostic(node: node)) - Found { target: body } => - match infer_arrow_declared_return_type(arrow: node) { - Absent => outcome_accepted(value: true) - Present { value: declared } => - match lookup_inferred_facts_in_entries(entries: entries, key: body) { - Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: body)) - Present { value: body_facts } => - match inferred_facts_resolved_type(facts: body_facts) { - Violates { diagnostic: d } => outcome_rejected(d) - Holds { value: body_type } => - if infer_type_equal_ignoring_provenance(a: declared, b: body_type) { - outcome_accepted(value: true) - } else { - outcome_rejected( - infer_arrow_body_does_not_inhabit_declared_return_diagnostic(body: body) - ) - } - } - } - } - _ => outcome_accepted(value: true) - } - _ => outcome_accepted(value: true) - } -} - // WHICH FORMATION A SETTLED TYPE NODE TAKES, decided once. A type-declaration wrapper is NOT a // product even though its carrier is a Conj (v2.std.type_binder type_decl_view says which it is), so it // never reaches product introduction: an alias or generic member forms its own evidence with the binder @@ -860,22 +817,17 @@ fn infer_product_facts_from_entries( ) ) Present { value: evidence_edges } => - bind_outcome( - o: infer_arrow_body_inhabits_declared_return(node: node, entries: entries), - f: fn(_checked) { - bind_outcome_accepted( - od: cd, - inner: inferred_facts_from_derived_type( - node: node, - derived_type: Node { - kind: node.kind, - children: evidence_edges, - occurrence_id: OccurrenceSynthetic - }, - descent: Holds { value: descent_proof } - ) - ) - } + bind_outcome_accepted( + od: cd, + inner: inferred_facts_from_derived_type( + node: node, + derived_type: Node { + kind: node.kind, + children: evidence_edges, + occurrence_id: OccurrenceSynthetic + }, + descent: Holds { value: descent_proof } + ) ) } } @@ -2010,16 +1962,92 @@ fn infer_judge_application_argument( application: Node, entries: List, formal: InhabitanceFormal, - arg: Node + arg: Node, + type_params: List ) -> Outcome { - match inhabitance_node_undecidable_reason(n: formal.declared) { + infer_judge_declared_position( + position: position_direct_call_argument(), + application: application, + entries: entries, + formal: formal, + produced_at: arg, + type_params: type_params + ) +} + +// ONE JUDGE FOR EVERY DECLARED POSITION. An argument at its formal and an Arrow body at its declared +// return ask the same question -- does the type derived at `produced_at` inhabit `formal.declared`? -- +// so both build a DeclaredTypeObligation here and hand it to the one relation, +// v2.std.inhabitance declared_type_inhabitance. Only the position differs, and it rides on the +// obligation into the refusal. A position whose produced type is not derived stays the counted +// frontier (UndecidableArgumentTypeNotDerived), never an admission. +// +// The declared side is compared at its DENOTATION, the value type the produced side is derived in: +// a type-name atom as written (`Bool`) is not the value type a `true` derives (v2.std.logic +// bool_node), so each atom goes through the one binding->value-type join, +// v2.extdeps.languages.dag dag_binding_denotation, before the relation reads it. A declared type +// that is a bare atom the join does not denote, and not one of the type variables, is not a type +// this relation can compare: it is counted UndecidableFormalUnresolved, never refused for the +// spelling and never admitted silently. +fn infer_declared_position_undecidable_reason( + declared: Node, + type_params: List +) -> Optional { + match inhabitance_node_undecidable_reason(n: declared, type_variables: type_params) { + Present { value: reason } => optional_present(value: reason) + Absent => + match declared.kind { + TypeNode { connective: Atom { identity: id } } => + match dag_binding_denotation(sym: id) { + Present { value: _ } => Absent + Absent => optional_present(value: undecidable_formal_unresolved()) + } + _ => Absent + } + } +} + +fn infer_declared_type_denotation(declared: Node) -> Node { + fold_node( + n: declared, + algebra: NodeFold { + init: fn(self) { + match self.kind { + TypeNode { connective: Atom { identity: id } } => + match dag_binding_denotation(sym: id) { + Present { value: denoted } => denoted + Absent => Node { kind: self.kind, children: [], occurrence_id: self.occurrence_id } + } + _ => Node { kind: self.kind, children: [], occurrence_id: self.occurrence_id } + } + }, + step: fn(acc, edge, sub) { + Node { + kind: acc.kind, + children: list_snoc_item(xs: acc.children, item: Edge { label: edge.label, target: sub }), + occurrence_id: acc.occurrence_id + } + } + } + ) +} + +fn infer_judge_declared_position( + position: DeclaredTypePosition, + application: Node, + entries: List, + formal: InhabitanceFormal, + produced_at: Node, + type_params: List +) -> Outcome { + match infer_declared_position_undecidable_reason(declared: formal.declared, type_params: type_params) { Present { value: reason } => infer_inhabitance_undecidable_accepted( application: application, reason: reason ) Absent => - match lookup_inferred_facts_in_entries(entries: entries, key: arg) { + match lookup_inferred_facts_in_entries(entries: entries, key: produced_at) { Absent => infer_inhabitance_undecidable_accepted( application: application, @@ -2034,11 +2062,12 @@ fn infer_judge_application_argument( ) Holds { value: produced } => let obligation = DeclaredTypeObligation { - position: position_direct_call_argument(), + position: position, parameter_identity: formal.parameter_identity, - declared: formal.declared, + declared: infer_declared_type_denotation(declared: formal.declared), produced: produced, - application: application + application: application, + type_variables: type_params } match declared_type_inhabitance(obligation: obligation) { Inhabits { homomorphism: _ } => Accepted { value: true, diagnostics: None } @@ -2081,7 +2110,7 @@ fn infer_judge_application_argument_instantiating( ) -> Outcome> { match inhabitance_formal_declaration(declared: formal.declared, type_params: type_params) { DeclaredType { declared: _ } => - match infer_judge_application_argument(application: application, entries: entries, formal: formal, arg: arg) { + match infer_judge_application_argument(application: application, entries: entries, formal: formal, arg: arg, type_params: type_params) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: _, diagnostics: d } => Accepted { value: instances, diagnostics: d } } @@ -2092,7 +2121,8 @@ fn infer_judge_application_argument_instantiating( application: application, entries: entries, formal: InhabitanceFormal { parameter_identity: formal.parameter_identity, declared: instance }, - arg: arg + arg: arg, + type_params: type_params ) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: _, diagnostics: d } => Accepted { value: instances, diagnostics: d } @@ -3592,6 +3622,75 @@ fn infer_gather_settled_row( tree: tree ) Absent => + match infer_arrow_declared_return_check(node: acc.node, entries: merged_entries) { + Rejected { diagnostics: r } => + infer_gather_fold_acc_failed( + node: acc.node, + pending: rejected_with_pending(pending: merged_pending, rejected: r), + await_branch_row: false, + await_match_row: false, + await_loop_row: false, + await_transform_row: false, + children_remaining: 0 + ) + Accepted { value: _, diagnostics: rd } => + infer_gather_settled_unannotated_row( + acc: acc, + merged_entries: merged_entries, + merged_pending: diagnostics_merge(outer: merged_pending, inner: rd), + partials: partials + ) + } + } +} + +// AN ARROW'S BODY IS JUDGED AT ITS DECLARED RETURN. A fn lowers to an Arrow whose second positional +// child is the declared return and whose ^arrow_body_edge is the body +// (v2.compiler.body_lowering_fold body_lower_fn_decl_arrow). By the Arrow's settled row every child +// has folded, so the body's derived type is in `entries`, and the body is judged at the declared +// return through the same judge -- and so the same relation -- an argument meets at its formal. The +// Arrow's own type parameters are the obligation's type variables: a return that mentions one stays +// UndecidableGenericFormal, counted. An Arrow with no body is a signature (a fn type, a census-grade +// declaration) and owes nothing here; one with two bodies, or a body but no declared return, is a +// malformed Arrow and refuses. +fn infer_arrow_declared_return_check(node: Node, entries: List) -> Outcome { + match node.kind { + TypeNode { connective: Arrow } => + match arrow_body_target_lookup(children: node.children) { + Ambiguous => outcome_rejected(infer_arrow_declared_return_shape_diagnostic(node: node)) + Found { target: body } => + match list_at_optional(xs: node_positional_child_targets(node: node), index: 1) { + Absent => outcome_rejected(infer_arrow_declared_return_shape_diagnostic(node: node)) + Present { value: declared } => + infer_judge_declared_position( + position: position_declared_return(), + application: body, + entries: entries, + formal: InhabitanceFormal { parameter_identity: ^declared_return, declared: declared }, + produced_at: body, + type_params: type_param_names(n: node) + ) + } + _ => outcome_accepted(true) + } + _ => outcome_accepted(true) + } +} + +fn infer_arrow_declared_return_shape_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: ^infer_arrow_declared_return_shape_invalid, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn infer_gather_settled_unannotated_row( + acc: InferGatherFoldAcc, + merged_entries: List, + merged_pending: Diagnostics, + partials: List, +) -> InferGatherFoldAcc { if infer_gather_acc_awaits_product_row(node: acc.node, entries: merged_entries) { infer_gather_product_row_on_entries( node: acc.node, @@ -3611,7 +3710,6 @@ fn infer_gather_settled_row( children_remaining: 0 ) } - } } fn infer_gather_fold_algebra(partials: List, kinds: List, tree: Node) -> NodeFold { diff --git a/src/v2/std/inhabitance.dag b/src/v2/std/inhabitance.dag index c2a5f43020a..4c00b493fcd 100644 --- a/src/v2/std/inhabitance.dag +++ b/src/v2/std/inhabitance.dag @@ -18,19 +18,16 @@ import v2.std.find_witness { find_witness } import v2.std.node { - Arrow, Atom, Cardinality, - ComputationNode, Conj, - Disj, Edge, - Instantiation, Named, Node, Positional, Symbol, TypeNode, + node_subtree_nodes, node_synthetic } import v2.std.optional { Absent, Optional, Present, optional_present } @@ -85,12 +82,16 @@ type DeclaredTypePosition = PositionDirectCallArgument | PositionDeclaredReturn +// type_variables are the declaring Arrow's type parameters (v2.std.type_binder type_param_names): +// the only atoms in `declared` that name no type, and so the only thing that keeps an +// Instantiation from being decided structurally. type DeclaredTypeObligation { position: DeclaredTypePosition parameter_identity: Symbol declared: Node produced: Node application: Node + type_variables: List } type InhabitanceFormal { @@ -109,14 +110,17 @@ type InhabitanceVerdict | InhabitanceRefused { find_witness_reason: Symbol } | InhabitanceUndecidable { reason: InhabitanceUndecidableReason } -// PositionDeclaredReturn is the second coproduct arm so DeclaredTypePosition is not a one-arm -// alias. This fold only constructs PositionDirectCallArgument. Declared frontier: a return-type -// inhabitance obligation (produced body type vs declared return) at the same declared_type_inhabitance -// consumer, trigger = that producer landing in v2.compiler.infer. +// Two producers, one relation: v2.compiler.infer builds PositionDirectCallArgument per argument of +// an application and PositionDeclaredReturn per Arrow body against its declared return, and both +// hand the obligation to declared_type_inhabitance. fn position_direct_call_argument() -> DeclaredTypePosition { PositionDirectCallArgument } +fn position_declared_return() -> DeclaredTypePosition { + PositionDeclaredReturn +} + fn inhabitance_position_symbol(position: DeclaredTypePosition) -> Symbol { match position { PositionDirectCallArgument => ^position_direct_call_argument @@ -143,29 +147,51 @@ fn inhabitance_cardinality_type(inner: Node) -> Node { ) } +// A TYPE MENTIONS A TYPE VARIABLE WHEN ANY ATOM IN IT IS SPELLED AS ONE. v2.compiler.resolve refuses +// a type parameter that shadows a visible name, so inside the declaring Arrow that spelling means +// the binder and nothing else -- whether it stands bare (`x: T`) or as an Instantiation's head +// or argument (`Box`, `T` lowered as Instantiation[T]). +fn inhabitance_node_mentions_type_variable(n: Node, type_variables: List) -> Bool { + fold(node_subtree_nodes(root: n), init: false, f: fn(acc, m) { + acc || (match m.kind { + TypeNode { connective: Atom { identity: id } } => + fold(type_variables, init: false, f: fn(found, v) { found || (v == id) }) + _ => false + }) + }) +} + +// A TYPE IS DECIDED UNLESS IT MENTIONS A TYPE VARIABLE. An applied type whose constructor and +// arguments are all established (`Outcome`) is a type node like any other, and +// exact_structural_equality_zip_fold compares it argument by argument, so `Outcome` at +// `Outcome` refuses. A type that mentions one of the declaring Arrow's type variables -- bare +// (`-> T`) or inside an Instantiation (`Box`) -- stays UndecidableGenericFormal: this relation +// holds no instance for the variable, and comparing its spelling against a concrete type would +// refuse for the wrong reason. The check reads the variable first, so no connective arm can decide +// a type that carries one. fn inhabitance_node_undecidable_reason( - n: Node + n: Node, + type_variables: List ) -> Optional { - match n.kind { - TypeNode { connective: Cardinality } => - optional_present(value: UndecidableOptionalCarrier) - TypeNode { connective: Instantiation } => - optional_present(value: UndecidableGenericFormal) - TypeNode { connective: Atom { identity: _ } } => Absent - TypeNode { connective: Conj } => Absent - TypeNode { connective: Disj } => Absent - TypeNode { connective: Arrow } => Absent - ComputationNode { behavior: _ } => Absent + if inhabitance_node_mentions_type_variable(n: n, type_variables: type_variables) { + optional_present(value: UndecidableGenericFormal) + } else { + match n.kind { + TypeNode { connective: Cardinality } => + optional_present(value: UndecidableOptionalCarrier) + _ => Absent + } } } fn inhabitance_pair_undecidable_reason( declared: Node, - produced: Node + produced: Node, + type_variables: List ) -> Optional { - match inhabitance_node_undecidable_reason(n: declared) { + match inhabitance_node_undecidable_reason(n: declared, type_variables: type_variables) { Present { value: reason } => optional_present(value: reason) - Absent => inhabitance_node_undecidable_reason(n: produced) + Absent => inhabitance_node_undecidable_reason(n: produced, type_variables: type_variables) } } @@ -186,7 +212,8 @@ fn inhabitance_pair_undecidable_reason( fn declared_type_inhabitance(obligation: DeclaredTypeObligation) -> InhabitanceVerdict { match inhabitance_pair_undecidable_reason( declared: obligation.declared, - produced: obligation.produced + produced: obligation.produced, + type_variables: obligation.type_variables ) { Present { value: reason } => InhabitanceUndecidable { reason: reason } Absent => @@ -216,9 +243,23 @@ fn inhabitance_no_candidate_application_reason() -> Symbol { ^application_argument_does_not_inhabit } -fn inhabitance_application_refusal_reason(find_witness_reason: Symbol) -> Symbol { +fn inhabitance_no_candidate_return_reason() -> Symbol { + ^arrow_body_does_not_inhabit_declared_return +} + +fn inhabitance_no_candidate_reason(position: DeclaredTypePosition) -> Symbol { + match position { + PositionDirectCallArgument => inhabitance_no_candidate_application_reason() + PositionDeclaredReturn => inhabitance_no_candidate_return_reason() + } +} + +fn inhabitance_application_refusal_reason( + position: DeclaredTypePosition, + find_witness_reason: Symbol +) -> Symbol { if find_witness_reason == ^find_witness_reason_no_candidate { - inhabitance_no_candidate_application_reason() + inhabitance_no_candidate_reason(position: position) } else { find_witness_reason } @@ -312,7 +353,10 @@ fn application_argument_does_not_inhabit_diagnostic( find_witness_reason: Symbol ) -> Diagnostic { Diagnostic { - reason: inhabitance_application_refusal_reason(find_witness_reason: find_witness_reason), + reason: inhabitance_application_refusal_reason( + position: obligation.position, + find_witness_reason: find_witness_reason + ), at: node_locus(node: obligation.application), correction: Suggested { node: Node { diff --git a/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag b/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag index 247d9321fef..e492529a28f 100644 --- a/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag +++ b/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag @@ -22,6 +22,8 @@ import v2.std.diagnostic { diagnostics_has_reason } import v2.std.logic { Bool } +import std.algebra { list_snoc_item } +import v2.std.type_binder { type_params_edge } import v2.std.optional { Absent, Present } import v2.std.node { ComputationNode, @@ -77,8 +79,12 @@ fn inhabitance_call_tree(arg: Node) -> Node { ) } +// THE FORMAL MENTIONS A TYPE VARIABLE THE CALLEE DECLARES. `T` is bound by the Arrow's own type +// parameter list (v2.std.type_binder type_params_edge), so the relation holds no instance for it and +// the obligation is counted UndecidableGenericFormal. An Instantiation that mentions no declared type +// variable is decided structurally instead (inhabitance_ground_instantiation_* below). fn inhabitance_generic_formal_tree() -> Node { - inhabitance_apply( + let arrow = dag_arrow_with_body_node( domain: inhabitance_named_conj_domain( parameter: ^inhabitance_param_t, declared: node_synthetic( @@ -91,7 +97,34 @@ fn inhabitance_generic_formal_tree() -> Node { ] ) ), - arg: dag_int_literal_fixture_one() + return_type_binding: ^dag_binding_type_int, + body: dag_int_literal_fixture_one() + ) + node_synthetic( + kind: ComputationNode { behavior: Transform }, + children: [ + Edge { + label: Positional, + target: node_synthetic( + kind: arrow.kind, + children: list_snoc_item( + xs: arrow.children, + item: type_params_edge( + conj: node_synthetic( + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^inhabitance_type_param_t }, + target: dag_type_atom_node(identity: ^inhabitance_type_param_t) + } + ] + ) + ) + ) + ) + }, + Edge { label: Positional, target: dag_int_literal_fixture_one() } + ] ) } @@ -200,7 +233,8 @@ test fn inhabitance_cardinality_type_is_optional_carrier_holds() -> Bool { match inhabitance_node_undecidable_reason( n: inhabitance_cardinality_type( inner: dag_type_atom_node(identity: ^dag_binding_type_int) - ) + ), + type_variables: [] ) { Absent => false Present { value: reason } => @@ -251,19 +285,18 @@ test fn infer_atom_operator_is_counted_formal_unresolved_holds() -> Bool { // preservation_rule_exact_structural_equality_zip_fold, which reads BOTH sides -- so the seed's // repair does not transfer and the cell had to be measured rather than assumed. // -// WHAT IS MEASURED (captured diagnostics, not inferred from the classifier): neither direction -// reaches that fold, and the two directions stop at DIFFERENT earlier boundaries. With the -// product declared and the collection supplied as the argument, the argument is a type node with -// no derived value type, so the obligation is counted as UndecidableArgumentTypeNotDerived -// (alongside infer_grounding_not_derived) before the formal is classified. With the collection -// declared, `inhabitance_node_undecidable_reason` classifies the Instantiation formal as -// UndecidableGenericFormal. Either way this path does not silently answer Inhabits the way the -// seed did -- it counts the obligation as undecidable and the route advances, which is exactly -// the standing of gunbc.recurring_failure_mode argument_type_obligation_absent_while_the_route_advances -// and not a second class. The next-rung trigger is that row's: an argument whose value type is -// derived as an APPLIED collection type, and a classifier that distinguishes an applied type whose -// constructor and arguments are all established from a type variable, which it cannot do today -// because both are Instantiation. +// WHAT IS MEASURED (captured diagnostics, not inferred from the classifier): the two directions +// stop at DIFFERENT boundaries. With the product declared and the collection supplied as the +// argument, the argument is an Instantiation with no derived value type, so the obligation is +// counted UndecidableArgumentTypeNotDerived before the relation is asked. With the collection +// declared, the formal `List` mentions no declared type variable, so it is decided +// (inhabitance_node_undecidable_reason reads the declaring Arrow's type parameters since the +// declared-return producer landed); the product argument derives its formation evidence, and the +// relation REFUSES it at the formal, application_argument_does_not_inhabit. Neither direction answers +// Inhabits the way the seed did. The first direction keeps the standing of +// gunbc.recurring_failure_mode argument_type_obligation_absent_while_the_route_advances; its +// next-rung trigger is that row's: an argument whose value type is derived as an APPLIED collection +// type. fn inhabitance_collection_type_node() -> Node { node_synthetic( kind: TypeNode { connective: Instantiation }, @@ -318,18 +351,18 @@ test fn inhabitance_collection_produced_at_a_product_formal_is_counted_frontier_ } } -test fn inhabitance_product_produced_at_a_collection_formal_is_counted_frontier_holds() -> Bool { +test fn inhabitance_product_produced_at_a_collection_formal_refuses_holds() -> Bool { match infer( tree: claim_resolved_tree_without_declarations(root: inhabitance_declared_formal_tree( declared: inhabitance_collection_type_node(), arg: inhabitance_nominal_product_type_node() )) ) { - Rejected { diagnostics: _ } => false - Accepted { value: _, diagnostics: d } => + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: nds } => diagnostics_has_reason( - d: d, - reason: ^inhabitance_undecidable_generic_formal + d: Some { diagnostics: nds }, + reason: ^application_argument_does_not_inhabit ) } } diff --git a/src/v2/test/claim/compiler/infer_declared_return_inhabitance_witness_test.dag b/src/v2/test/claim/compiler/infer_declared_return_inhabitance_witness_test.dag new file mode 100644 index 00000000000..8398fb4204b --- /dev/null +++ b/src/v2/test/claim/compiler/infer_declared_return_inhabitance_witness_test.dag @@ -0,0 +1,287 @@ +module v2.test.claim.compiler.infer_declared_return_inhabitance_witness_test + +import v2.compiler.infer { infer } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } +import v2.std.inhabitance { + DeclaredTypeObligation, + InhabitanceRefused, + InhabitanceUndecidable, + Inhabits, + declared_type_inhabitance, + inhabitance_undecidable_reason_symbol, + position_declared_return +} +import v2.extdeps.languages.dag { + dag_int_literal_fixture_one, + dag_type_atom_node +} +import v2.std.arrow_signature { declared_signature } +import v2.std.list_introduction { list_introduction_head_path, lower_list_introduction } +import v2.std.qualified_name { declaration_reference_node } +import std.occurrence_identity { OccurrenceSynthetic } +import v2.std.diagnostic { Accepted, Rejected, Some, diagnostics_has_reason } +import v2.std.logic { Bool } +import v2.std.type_binder { type_params_edge } +import std.algebra { list_snoc_item } +import v2.std.node { + Arrow, + Conj, + Edge, + Instantiation, + Named, + Node, + Positional, + Symbol, + TypeNode, + node_synthetic +} + +// WHAT THIS FILE ESTABLISHES: a fn's body is judged at its declared return. v2.compiler.infer +// infer_arrow_declared_return_check builds a DeclaredTypeObligation at PositionDeclaredReturn for +// every Arrow carrying an ^arrow_body_edge and hands it to v2.std.inhabitance +// declared_type_inhabitance -- the relation an argument meets at its formal, so there is one +// relation and two producers. Each red here has a positive control that differs from it only in +// the body (or the declared return), so a red cannot be satisfied by a check that refuses +// everything. +// +// WHY TREES AND NOT SOURCE TEXT. The fixtures are the Arrow body lowering produces +// (v2.compiler.body_lowering_fold body_lower_fn_decl_arrow: domain, return, return, declared order, +// body), handed to `infer`. A source-text v2 acceptance harness that admits the fixture's peer +// roots does not exist yet (test.claim.named_argument_binding_two_route_witness_test records that +// v2's standalone driver refuses its own positive control); that harness is this file's next-rung +// trigger, at which point these arms gain source-text twins. +// +// WHY THE GENERIC DISCRIMINATOR AT INFER IS A LIST LITERAL. The only Instantiation-typed value v2 +// infer derives is the FreeMonoid introduction (v2.compiler.infer infer_freemonoid_type_of); an +// application's result type stays GroundingNotDerived, so a body `Outcome` produced by a +// call is counted UndecidableArgumentTypeNotDerived at the return, not decided. The +// `Outcome` / `Outcome` pair is therefore established on the relation directly, and +// through infer with `List` declared against a `[1]` body. + +fn dr_empty_domain() -> Node { + node_synthetic(kind: TypeNode { connective: Conj }, children: []) +} + +// ONE DECLARED PARAMETER, NOT NONE. Every node here is OccurrenceSynthetic, and a childless product +// derives the childless synthetic node as its evidence -- itself -- so an empty domain is refused +// grounding_evidence_is_source (v2.std.constraints canonical_grounding_from_derived_type) before any +// return is judged. A lowered domain carries its fn's occurrence id and cannot meet that state; this +// fixture is shaped like test.claim.compiler.infer_arrow_elimination_witness_test ae_domain instead. +fn dr_domain() -> Node { + node_synthetic( + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Named { name: ^dr_param_x }, target: dag_type_atom_node(identity: ^dag_binding_type_int) } + ] + ) +} + +fn dr_arrow(return_type: Node, body: Node) -> Node { + let signature = declared_signature(params: dr_domain().children, source: dr_domain()) + node_synthetic( + kind: TypeNode { connective: Arrow }, + children: [ + signature.domain, + Edge { label: Positional, target: return_type }, + Edge { label: Positional, target: return_type }, + signature.order, + Edge { label: Named { name: ^arrow_body_edge }, target: body } + ] + ) +} + +fn dr_generic_arrow(type_param: Symbol, return_type: Node, body: Node) -> Node { + let arrow = dr_arrow(return_type: return_type, body: body) + node_synthetic( + kind: arrow.kind, + children: list_snoc_item( + xs: arrow.children, + item: type_params_edge( + conj: node_synthetic( + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Named { name: type_param }, target: dag_type_atom_node(identity: type_param) } + ] + ) + ) + ) + ) +} + +fn dr_int() -> Node { + dag_type_atom_node(identity: ^dag_binding_type_int) +} + +fn dr_bool() -> Node { + dag_type_atom_node(identity: ^dag_binding_type_bool) +} + +fn dr_bool_literal() -> Node { + dag_type_atom_node(identity: ^dag_token_kw_true) +} + +fn dr_applied(head: Node, argument: Node) -> Node { + node_synthetic( + kind: TypeNode { connective: Instantiation }, + children: [ + Edge { label: Positional, target: head }, + Edge { label: Positional, target: argument } + ] + ) +} + +fn dr_list_of(element: Node) -> Node { + dr_applied( + head: declaration_reference_node(qn: list_introduction_head_path(), occurrence_id: OccurrenceSynthetic), + argument: element + ) +} + +fn dr_outcome_of(argument: Node) -> Node { + dr_applied(head: dag_type_atom_node(identity: ^dr_type_outcome), argument: argument) +} + +fn dr_refuses_at_return(tree: Node) -> Bool { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: nds } => + diagnostics_has_reason(d: Some { diagnostics: nds }, reason: ^arrow_body_does_not_inhabit_declared_return) + } +} + +fn dr_admits(tree: Node) -> Bool { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +test fn declared_return_int_with_a_bool_body_refuses_holds() -> Bool { + dr_refuses_at_return(tree: dr_arrow(return_type: dr_int(), body: dr_bool_literal())) +} + +test fn declared_return_int_with_an_int_body_admits_holds() -> Bool { + dr_admits(tree: dr_arrow(return_type: dr_int(), body: dag_int_literal_fixture_one())) +} + +test fn declared_return_bool_with_an_int_body_refuses_holds() -> Bool { + dr_refuses_at_return(tree: dr_arrow(return_type: dr_bool(), body: dag_int_literal_fixture_one())) +} + +test fn declared_return_list_of_bool_with_an_int_list_body_refuses_holds() -> Bool { + dr_refuses_at_return( + tree: dr_arrow( + return_type: dr_list_of(element: dr_bool()), + body: lower_list_introduction(elements: [dag_int_literal_fixture_one()], source: dr_empty_domain()) + ) + ) +} + +test fn declared_return_list_of_int_with_an_int_list_body_admits_holds() -> Bool { + dr_admits( + tree: dr_arrow( + return_type: dr_list_of(element: dr_int()), + body: lower_list_introduction(elements: [dag_int_literal_fixture_one()], source: dr_empty_domain()) + ) + ) +} + +// THE DECLARED SIDE IS READ AT ITS DENOTATION. `Bool` as written is not the value type `true` +// derives (v2.std.logic bool_node); comparing the spelling would refuse every Bool-returning fn. +test fn declared_return_bool_with_a_bool_body_admits_holds() -> Bool { + dr_admits(tree: dr_arrow(return_type: dr_bool(), body: dr_bool_literal())) +} + +test fn declared_return_list_of_bool_with_a_bool_list_body_admits_holds() -> Bool { + dr_admits( + tree: dr_arrow( + return_type: dr_list_of(element: dr_bool()), + body: lower_list_introduction(elements: [dr_bool_literal()], source: dr_empty_domain()) + ) + ) +} + +// A RETURN THE BINDING JOIN DOES NOT DENOTE IS COUNTED, NOT REFUSED AND NOT SILENT. Before this +// relation judged returns, such an Arrow was admitted with no diagnostic at all. +test fn declared_return_undenoted_atom_is_counted_formal_unresolved_holds() -> Bool { + match infer(tree: claim_resolved_tree_without_declarations(root: dr_arrow(return_type: dag_type_atom_node(identity: ^dr_type_undenoted), body: dr_bool_literal()))) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: d } => + diagnostics_has_reason(d: d, reason: ^inhabitance_undecidable_formal_unresolved) + } +} + +// A RETURN SPELLED AS THE FN'S OWN TYPE VARIABLE IS COUNTED, NOT COMPARED. `fn f() -> T { 1 }` +// must not refuse because the Atom `T` is not the Atom `Int`; the relation holds no instance for T, +// so the obligation is UndecidableGenericFormal on the Accepted path. +test fn declared_return_type_variable_is_counted_generic_formal_holds() -> Bool { + match infer( + tree: claim_resolved_tree_without_declarations( + root: dr_generic_arrow( + type_param: ^dr_type_param_t, + return_type: dag_type_atom_node(identity: ^dr_type_param_t), + body: dag_int_literal_fixture_one() + ) + ) + ) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: d } => + diagnostics_has_reason(d: d, reason: ^inhabitance_undecidable_generic_formal) + } +} + +fn dr_return_obligation(declared: Node, produced: Node, type_variables: List) -> DeclaredTypeObligation { + DeclaredTypeObligation { + position: position_declared_return(), + parameter_identity: ^declared_return, + declared: declared, + produced: produced, + application: dr_empty_domain(), + type_variables: type_variables + } +} + +// THE CLASS #12441 REPAIRS ON THE SEED, DECIDED BY THE ONE v2 RELATION: two instantiations of one +// generic coproduct at distinct type arguments are distinct types. +test fn relation_refuses_outcome_of_record_at_outcome_of_node_holds() -> Bool { + match declared_type_inhabitance( + obligation: dr_return_obligation( + declared: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_node)), + produced: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_record)), + type_variables: [] + ) + ) { + InhabitanceRefused { find_witness_reason: _ } => true + Inhabits { homomorphism: _ } => false + InhabitanceUndecidable { reason: _ } => false + } +} + +test fn relation_admits_outcome_of_node_at_outcome_of_node_holds() -> Bool { + match declared_type_inhabitance( + obligation: dr_return_obligation( + declared: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_node)), + produced: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_node)), + type_variables: [] + ) + ) { + Inhabits { homomorphism: _ } => true + InhabitanceRefused { find_witness_reason: _ } => false + InhabitanceUndecidable { reason: _ } => false + } +} + +test fn relation_counts_outcome_of_a_type_variable_as_generic_formal_holds() -> Bool { + match declared_type_inhabitance( + obligation: dr_return_obligation( + declared: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_param_t)), + produced: dr_outcome_of(argument: dag_type_atom_node(identity: ^dr_type_node)), + type_variables: [^dr_type_param_t] + ) + ) { + InhabitanceUndecidable { reason: reason } => + inhabitance_undecidable_reason_symbol(reason: reason) == ^inhabitance_undecidable_generic_formal + Inhabits { homomorphism: _ } => false + InhabitanceRefused { find_witness_reason: _ } => false + } +}