diff --git a/dag/gunbc/defork_type_name_census.dag b/dag/gunbc/defork_type_name_census.dag index fe44e045c75..cdfe333c583 100644 --- a/dag/gunbc/defork_type_name_census.dag +++ b/dag/gunbc/defork_type_name_census.dag @@ -204,8 +204,8 @@ data defork_census_rows: List = [ names: ["Int8", "Int16", "Int32", "Int64", "Int128", "UInt8", "UInt16", "UInt32", "UInt64", "UInt128"], reading: AuthoredResolutionReading { dag_side: "→ `std.machine_constraints` `Compose` / `MachineWidth` + `std.integer` `Int`/`UInt`", - v2_side: "→ `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth` + `v2.std.integer` `Int`/`UInt`", - class: "same concept, every referent divergent" + v2_side: "→ `std.machine_constraints` `Compose` / `MachineWidth` + `v2.std.integer` `Int`/`UInt`", + class: "same concept, Int/UInt referent divergent" }, disposition: ForkNeedsDecisionRecord { family: "integer family" } }, @@ -213,17 +213,8 @@ data defork_census_rows: List = [ names: ["IntPlatform", "UIntPlatform"], reading: AuthoredResolutionReading { dag_side: "→ `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth`", - v2_side: "→ `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth`/`PointerWidth`", - class: "text near-identical, every referent divergent" - }, - disposition: ForkNeedsDecisionRecord { family: "integer family" } - }, - SharedTypeNameRow { - names: ["Compose", "MachineWidth"], - reading: AuthoredResolutionReading { - dag_side: "`std.machine_constraints` — phantom composition / width over `WidthResolution`", - v2_side: "`v2.std.integer` / `v2.std.machine` — opaque, unconstrained parameter", - class: "same concept, divergent constraint" + v2_side: "→ `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth`", + class: "text near-identical, Int/UInt referent divergent" }, disposition: ForkNeedsDecisionRecord { family: "integer family" } }, @@ -248,6 +239,11 @@ data defork_census_rows: List = [ ] data defork_census_resolved: List = [ + ResolvedSharedTypeName { + names: ["Compose", "MachineWidth"], + resolution: ResolvedByDeletingV2 { reason: "N7-2 root B: v2 gained kinded type parameters (`v2.std.type_binder` `type_application_conformance`), so the kinded `std.machine_constraints` `MachineWidth` normalizes on the native route; `v2.std.machine` `MachineWidth`/`PointerWidth` and `v2.std.integer` `Compose` are deleted and `v2.std.integer` imports them from `std.machine_constraints` (its `MachineWidth` rows were kind-wrong and now read `MachineWidth`)" }, + change: 13038 + }, ResolvedSharedTypeName { names: ["String"], resolution: ResolvedByDeletingDag { reason: "operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling)" }, diff --git a/dag/gunbc/recurring_failure_mode/a_binding_position_recorded_as_a_declaring_identity.dag b/dag/gunbc/recurring_failure_mode/a_binding_position_recorded_as_a_declaring_identity.dag index 3dd6c973b74..9829fd077eb 100644 --- a/dag/gunbc/recurring_failure_mode/a_binding_position_recorded_as_a_declaring_identity.dag +++ b/dag/gunbc/recurring_failure_mode/a_binding_position_recorded_as_a_declaring_identity.dag @@ -11,6 +11,7 @@ data a_binding_position_recorded_as_a_declaring_identity: RecurringFailureMode = "HARM. One declaration acquires one identity PER RELAY it is reached through, so the map that exists to make identity single-valued is the thing that forks it. Nothing refuses: every path resolves, and the reference is Accepted. It surfaces downstream as a wrong answer with no diagnostic -- a target that spells a declaration by its module emits a path into the relay module, which declares nothing and therefore has no item to name, so the emitted program refers to something that was never written.", "DISTINGUISHING FACTS. refusal_reason_minted_as_canonical_identity is a value minted from the WRONG VOCABULARY (a diagnostic reason standing in a name's place); this row is a value from the RIGHT vocabulary read at the WRONG LAYER -- a real qualified path, naming a real position, that is a binding rather than a declaration. The recognition rule is a question, not a spelling: when a field is named for a DECLARATION, ask whether every writer of it can only have written a declaration there, and follow one re-export before answering. An index whose lookup succeeds at a relay will answer that question wrong and stay green.", "RECEIPT (2026-09-22, fierce-wren-487, found by review 70003 on gunbc#12048). Uninhabited until resolution began CARRYING the declaring path: while a resolved reference was a bare leaf the recorded declaring path reached no consumer, so the fork existed in the index and was unobservable. The enrolled chain claim could not see it either -- it asserted only that the chain RESOLVES, and an index that stops at the relay resolves perfectly well. Repaired by chasing one step through symbol_index_claimants_at, which already answers who declares what lives at a position; a relay's own row was chased the same way when it bound, so one step reaches the home. Enrolled: v2.test.claim.namespace_xl0.cross_module_reference_resolution a_re_export_resolves_to_the_home_not_the_relay_holds, whose NEGATIVE conjunct is the discriminator -- measured FAIL before the chase and PASS after, with the sibling same-leaf row PASS in both runs.", + "RECEIPT, SECOND WRITER (2026-10-03, sunny-lynx-759, gunbc#13038). v2.compiler.symbol_index_fill symbol_index_fill_unique_variant_aliases writes a module-unique variant TWICE as an ENTRY: once at its declaring path under its coproduct (p.Resolution.Pointer, symbol_index_fill_containment_node) and again at the module-level binding position (p.Pointer), over the same arm node, through symbol_index_insert rather than a binding row. So symbol_index_declaring_path_of answers p.Pointer for p.Pointer -- the binding position is its own declaring identity, and the chase this row's first repair added cannot reach the home. MINIMAL REPRODUCER: `module p` / `type Resolution = Static | Pointer` / `type Width` / `type UsesPointer = Width`. The bare `Pointer` resolves to declaration_reference p.Pointer; comparing it by declaring path against the kind's variant p.Resolution.Pointer judged a conforming argument OUTSIDE its kind (resolve_reason_type_argument_kind_not_inhabited, measured on the gunbc#13038 branch before the workaround). gunbc#13038 compares the indexed declaration NODE instead (v2.compiler.resolve resolve_path_declares_node), which is a consumer-side workaround and not the repair; v2.test.claim.type_application_kind tak_kinded_parameter_accepts_a_variant_of_its_kind is the control that went red. THE REPAIR this receipt names: the variant alias is a BINDING to its declaring path (recorded so symbol_index_claimants_at answers p.Resolution.Pointer), not a second entry, after which resolve_path_declares_node can be replaced by a declaring-path comparison.", "RUNG FOUND AT: outside the ladder -- silent wrongness.", "CEILING: structurally impossible. A binding position and a declaring position are different concepts sharing one carrier (QualifiedName), so either can be written where the other is owed. The wall is the type: a declaring identity a binding path cannot inhabit, which is the same wall refusal_reason_minted_as_canonical_identity names from its own direction.", "NEXT-RUNG TRIGGER: a declaration-identity carrier distinct from the qualified path of an arbitrary position, so that symbol_index_bind_at cannot be handed a binding position at all; until then the enrolled row above is the wall, and it is a permanent regression control rather than an expecting-red probe.", @@ -19,5 +20,8 @@ data a_binding_position_recorded_as_a_declaring_identity: RecurringFailureMode = DeclarationRef { module_path: "v2.compiler.symbol_index_fill", decl_name: "symbol_index_bind_pending_round", field: WholeDeclaration }, DeclarationRef { module_path: "v2.std.symbol_index", decl_name: "symbol_index_declaring_path_of", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.cross_module_reference_resolution", decl_name: "a_re_export_resolves_to_the_home_not_the_relay_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.compiler.symbol_index_fill", decl_name: "symbol_index_fill_unique_variant_aliases", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.compiler.resolve", decl_name: "resolve_path_declares_node", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.type_application_kind", decl_name: "tak_kinded_parameter_accepts_a_variant_of_its_kind", field: WholeDeclaration }, ], } diff --git a/docs/plans/dag-v2-defork-audit.md b/docs/plans/dag-v2-defork-audit.md index db01d33d5b2..392be138ef9 100644 --- a/docs/plans/dag-v2-defork-audit.md +++ b/docs/plans/dag-v2-defork-audit.md @@ -192,15 +192,14 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a ## 2D. The shared type-name census (the one list): the population is derived, the dispositions are authored -**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **20 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`. +**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **18 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`. | name(s) | declared in (derived) | dag/std side (authored reading) | src/v2/std side (authored reading) | class (authored) | disposition | | --- | --- | --- | --- | --- | --- | | `NonNegativeInt`, `PositiveInt` | `dag/std/integer.dag`, `src/v2/std/refinement.dag` | `std.integer` — `= Nat` / `= Nat where gt_zero` (refinement of `std.nat` `Nat`) | `v2.std.refinement` — record `refined: Refined` (smart-constructor over `v2.std.integer` `Int`), consumed by the formatter extdeps | MEANING FORK | OPEN — next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`) | | `Int`, `UInt` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.nat` `Nat` (via `std.algebra` `GroupCompletion`) | → `v2.std.nat` `Nat` | same concept, divergent referent | NEEDS A DECISION RECORD (integer family) | -| `Int8`, `Int16`, `Int32`, `Int64`, `Int128`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, `UInt128` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose` / `MachineWidth` + `std.integer` `Int`/`UInt` | → `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth` + `v2.std.integer` `Int`/`UInt` | same concept, every referent divergent | NEEDS A DECISION RECORD (integer family) | -| `IntPlatform`, `UIntPlatform` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | → `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth`/`PointerWidth` | text near-identical, every referent divergent | NEEDS A DECISION RECORD (integer family) | -| `Compose`, `MachineWidth` | `dag/std/machine_constraints.dag`, `src/v2/std/integer.dag`, `src/v2/std/machine.dag` | `std.machine_constraints` — phantom composition / width over `WidthResolution` | `v2.std.integer` / `v2.std.machine` — opaque, unconstrained parameter | same concept, divergent constraint | NEEDS A DECISION RECORD (integer family) | +| `Int8`, `Int16`, `Int32`, `Int64`, `Int128`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, `UInt128` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose` / `MachineWidth` + `std.integer` `Int`/`UInt` | → `std.machine_constraints` `Compose` / `MachineWidth` + `v2.std.integer` `Int`/`UInt` | same concept, Int/UInt referent divergent | NEEDS A DECISION RECORD (integer family) | +| `IntPlatform`, `UIntPlatform` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | text near-identical, Int/UInt referent divergent | NEEDS A DECISION RECORD (integer family) | | `TerminationProof` | `dag/std/termination.dag`, `src/v2/std/cardinality.dag` | `std.termination` — `dimensions: List` | `v2.std.cardinality` — `non_increasing: List`, `strict: RankingComponent` | same question, divergent model | NEEDS A DECISION RECORD (termination) | | `Unit` | `dag/std/types.dag`, `src/v2/std/cardinality.dag` | `std.types` — empty record | `v2.std.cardinality` — empty record | one concept, two declarations | NEEDS A DECISION RECORD (unit) | @@ -208,6 +207,7 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a | name(s) | resolution | change | | --- | --- | --- | +| `Compose`, `MachineWidth` | v2 side deleted — N7-2 root B: v2 gained kinded type parameters (`v2.std.type_binder` `type_application_conformance`), so the kinded `std.machine_constraints` `MachineWidth` normalizes on the native route; `v2.std.machine` `MachineWidth`/`PointerWidth` and `v2.std.integer` `Compose` are deleted and `v2.std.integer` imports them from `std.machine_constraints` (its `MachineWidth` rows were kind-wrong and now read `MachineWidth`) | #13038 | | `String` | dag side deleted — operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling) | #13089 | | `Nat` | v2 side deleted — operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance | #12846 | | `Float` | both sides deleted; the concept is homed at `extdeps.standards.ieee_754_2019 binary64` — IEEE 754-2019 §3.6 (operator ruling relayed 2026-09-28): `std.float` (Float = Float64, uncited) and `v2.std.float` (Float = Binary64) both deleted; kernel Float's meaning is the `std.kernel_type_denotation` row, not a std alias | #12547 | diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 983b8baaac0..964f5dfb486 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -117,10 +117,13 @@ import v2.std.symbol_index { symbol_index_global_unique_lookup, symbol_index_declaring_path_of, symbol_index_lexical_lookup, + symbol_index_declared_binders_at, symbol_index_lookup, symbol_index_renaming_alias_at } import v2.std.node { + BinderTypeEdge, + core_edge, Cardinality, MapLiteralEntriesEdge, labeled_core_is, @@ -178,7 +181,7 @@ import v2.std.node { ArrowBodyEdge, BinderDefaultEdge, } -import v2.std.type_binder { GenericTypeDecl, PlainTypeDecl, type_decl_view, edge_is_cast_target, edge_is_type_annotation, edge_is_type_params, type_binder_first_mislabelled, type_binder_labels_conform, type_param_names } +import v2.std.type_binder { ArgumentInhabitsKind, ArgumentLiteralUnjudged, ArgumentOutsideKind, ArgumentTypeParameterUnjudged, KindInhabitance, KindUnresolved, TypeApplicationArityMismatch, TypeApplicationConformance, TypeApplicationConforms, TypeApplicationKindNotInhabited, TypeApplicationKindUnresolved, TypeApplicationBinderOrderMalformed, type_application_conformance, type_binder_atom_identity_optional, type_param_kind_optional, GenericTypeDecl, PlainTypeDecl, type_decl_view, edge_is_cast_target, edge_is_type_annotation, edge_is_type_params, type_binder_first_mislabelled, type_binder_labels_conform, type_param_names } import v2.std.node_query { field_projection_edge_field_optional, field_projection_optional, @@ -3365,6 +3368,8 @@ fn resolve_node_walk_entered( } } } + TypeNode { connective: Instantiation } => + resolve_type_application(ctx: ctx, walked: resolve_children_homogeneous_scope(ctx: ctx, n: n)) TypeNode { connective: _ } => resolve_children_homogeneous_scope(ctx: ctx, n: n) ComputationNode { behavior: _ } => @@ -3372,6 +3377,167 @@ fn resolve_node_walk_entered( } } +// A TYPE APPLICATION BINDS ITS DECLARATION'S TYPE PARAMETERS IN EXACT BIJECTION, AND EACH ARGUMENT +// INHABITS ITS PARAMETER'S KIND. Checked here, at the head->declaration join, once the head and +// arguments have resolved: the head names a corpus declaration by path, the index carries that +// declaration's binders (v2.std.symbol_index symbol_index_declared_binders_at), and the verdict is +// v2.std.type_binder type_application_conformance's -- the one authority. A refusal is located at the +// application for arity and at the argument for kind, as v1 04_resolve type_param_kind_diagnostics +// locates it. +// +// POPULATION, STATED. A head that is not a corpus declaration reference -- a kernel canonical atom, or a +// type parameter applied as a head -- has no indexed binders, so it is outside this check rather than +// passed by it; a head whose path the index does not hold is contested, and resolve refuses that +// ambiguity where the head resolved. +fn resolve_type_application(ctx: ResolveContext, walked: ResolveNodeWalk) -> ResolveNodeWalk { + match walked { + ResolveWalkAccepted { value: resolved, diagnostics: _, lexical: _ } => + match resolve_type_application_refusal_optional(ctx: ctx, n: resolved) { + Absent => walked + Present { value: d } => resolve_walk_refused_one(chain: diagnostics_singleton(d: d)) + } + ResolveWalkRefused { first: _, rest: _, observation: _ } => walked + } +} + +fn resolve_type_application_refusal_optional(ctx: ResolveContext, n: Node) -> Optional { + match node_positional_child_targets(node: n) { + Empty => optional_absent() + Cons { head: head, tail: arguments } => + match declaration_reference_path_optional(node: head) { + Absent => optional_absent() + Present { value: path } => + match symbol_index_lookup(index: ctx.namespace.symbol_index, qualified_path: path) { + Absent => optional_absent() + Present { value: _ } => + resolve_type_application_verdict( + n: n, + verdict: type_application_conformance( + binders: resolve_declared_binders_or_none(ctx: ctx, path: path, at: n), + arguments: arguments, + inhabits: fn(argument, kind) { resolve_kind_inhabitance(ctx: ctx, declaration: path, argument: argument, kind: kind) } + ) + ) + } + } + } +} + +// A declaration that binds no type parameters is applied to none: its binders are the empty Conj. +fn resolve_declared_binders_or_none(ctx: ResolveContext, path: QualifiedName, at: Node) -> Node { + match symbol_index_declared_binders_at(index: ctx.namespace.symbol_index, qualified_path: path) { + Present { value: b } => b + Absent => node_with_occurrence_id(kind: TypeNode { connective: Conj }, children: [], occurrence_id: at.occurrence_id) + } +} + +fn resolve_type_application_verdict(n: Node, verdict: TypeApplicationConformance) -> Optional { + match verdict { + TypeApplicationConforms => optional_absent() + TypeApplicationArityMismatch { declared: _, supplied: _ } => + optional_present(value: resolve_type_application_diagnostic(reason: ^resolve_reason_type_application_arity_mismatch, at: n)) + TypeApplicationKindNotInhabited { argument: a, kind: _ } => + optional_present(value: resolve_type_application_diagnostic(reason: ^resolve_reason_type_argument_kind_not_inhabited, at: a)) + TypeApplicationKindUnresolved { argument: a, kind: _ } => + optional_present(value: resolve_type_application_diagnostic(reason: ^resolve_reason_type_parameter_kind_unresolved, at: a)) + TypeApplicationBinderOrderMalformed => + optional_present(value: resolve_type_application_diagnostic(reason: ^resolve_reason_type_parameter_order_malformed, at: n)) + } +} + +fn resolve_type_application_diagnostic(reason: Symbol, at: Node) -> Diagnostic { + Diagnostic { reason: reason, at: node_locus(node: at), correction: Unavailable { reason: UserInputBoundary } } +} + +// WHETHER A RESOLVED ARGUMENT INHABITS A KIND AS AUTHORED ON `declaration`'s BINDER. The kind is the +// lowered binder's own node, so its name resolves from the DECLARATION's position, never the use's; +// it must name a coproduct, and an argument inhabits it exactly when the argument resolves to one of +// that coproduct's variants -- by the DECLARATION the index holds, never by leaf spelling. A unique +// variant referenced bare resolves to its module-level path (p.Pointer), which +// v2.compiler.symbol_index_fill symbol_index_fill_unique_variant_aliases files as a second ENTRY over +// the same arm node rather than as a binding to p.Resolution.Pointer, so +// symbol_index_declaring_path_of cannot relate the two paths; the arm node they share can. A Nat literal and a type +// parameter of an enclosing declaration are not judged (v2.std.type_binder KindInhabitance). +fn resolve_kind_inhabitance(ctx: ResolveContext, declaration: QualifiedName, argument: Node, kind: Node) -> KindInhabitance { + if dag_node_is_int_literal_atom(node: argument) { + ArgumentLiteralUnjudged + } else if resolve_argument_is_type_parameter(ctx: ctx, argument: argument) { + ArgumentTypeParameterUnjudged + } else { + match resolve_kind_variant_paths_optional(ctx: ctx, declaration: declaration, kind: kind) { + Absent => KindUnresolved + Present { value: variants } => + match declaration_reference_path_optional(node: argument) { + Absent => ArgumentOutsideKind + Present { value: arg_path } => + match symbol_index_lookup(index: ctx.namespace.symbol_index, qualified_path: arg_path) { + Absent => ArgumentOutsideKind + Present { value: arg_decl } => + if any(xs: variants, predicate: fn(v) { resolve_path_declares_node(ctx: ctx, path: v, declared: arg_decl) }) { ArgumentInhabitsKind } else { ArgumentOutsideKind } + } + } + } + } +} + +fn resolve_argument_is_type_parameter(ctx: ResolveContext, argument: Node) -> Bool { + match type_binder_atom_identity_optional(n: argument) { + Absent => false + Present { value: id } => + resolve_scope_binds_type_parameter(s: ctx.type_scope, name: id) || resolve_scope_binds_type_parameter(s: ctx.scope, name: id) + } +} + +fn resolve_scope_binds_type_parameter(s: Scope, name: Symbol) -> Bool { + match lookup_chain(s: s, name: name) { + Accepted { value: found, diagnostics: _ } => + match found { + BoundInFrame { canonical: _, kind: k } => + match k { + TypeParameterFrame => true + ParameterFrame { arrow_path: _ } => false + LexicalFrame { binders: _ } => false + } + BoundAtRoot { canonical: _ } => false + ScopeUnbound => false + } + Rejected { diagnostics: _ } => false + } +} + +fn resolve_path_declares_node(ctx: ResolveContext, path: QualifiedName, declared: Node) -> Bool { + match symbol_index_lookup(index: ctx.namespace.symbol_index, qualified_path: path) { + Present { value: n } => n == declared + Absent => false + } +} + +// The variant paths of the coproduct a kind atom names, looked up lexically from the declaration. +fn resolve_kind_variant_paths_optional(ctx: ResolveContext, declaration: QualifiedName, kind: Node) -> Optional> { + match type_binder_atom_identity_optional(n: kind) { + Absent => optional_absent() + Present { value: kind_name } => + match symbol_index_lexical_lookup(index: ctx.namespace.symbol_index, position: declaration, name: kind_name) { + LexicalHit { node: kind_decl, path: kind_binding } => + let kind_path = symbol_index_declaring_path_of(index: ctx.namespace.symbol_index, target: kind_binding) + match kind_decl.kind { + TypeNode { connective: Disj } => + optional_present(value: fold(kind_decl.children, init: Empty, f: fn(acc, e) { + match e.label { + Authored { name: v } => list_snoc_item(xs: acc, item: qualified_name_snoc(qn: kind_path, segment: v)) + StructuralLabel { label: _ } => acc + Positional => acc + } + })) + TypeNode { connective: _ } => optional_absent() + ComputationNode { behavior: _ } => optional_absent() + } + LexicalAmbiguous { candidates: _ } => optional_absent() + LexicalUnbound => optional_absent() + } + } +} + // A LOOP RESOLVES ITS EDGES AS ANY NODE DOES, EXCEPT TWO. The domain and body walk through // resolve_child_edge as ordinary expressions. ^loop_realized_declaration_edge (v2.std.node // LoopRealizedDeclaration) is a CLAIM made by a desugaring about which declaration the author's head @@ -3761,7 +3927,7 @@ fn resolve_type_param_binder(ctx: ResolveContext, binder: Node) -> ResolveNodeWa match resolve_atom(ctx: ctx, n: binder, identity: id) { Rejected { diagnostics: d } => if diagnostics_fatal_reason(d: d) == ^resolve_reason_unbound_symbol { - ResolveWalkAccepted { value: canonical_atom(identity: id, occurrence_id: binder.occurrence_id), diagnostics: None, lexical: [] } + resolve_type_param_binder_kind(ctx: ctx, binder: binder, identity: id) } else { resolve_walk_refused_one(chain: diagnostics_singleton(d: type_param_shadows_visible_name_diagnostic(binder: binder))) } @@ -3772,9 +3938,39 @@ fn resolve_type_param_binder(ctx: ResolveContext, binder: Node) -> ResolveNodeWa } } +// AN ADMITTED BINDER KEEPS ITS KIND, RESOLVED. The kind is an ordinary type expression in the +// declaration's scope (v2.std.type_binder type_param_kind_optional), so it resolves as any type +// position does and a kind that names nothing refuses here, at the kind. +fn resolve_type_param_binder_kind(ctx: ResolveContext, binder: Node, identity: Symbol) -> ResolveNodeWalk { + match type_param_kind_optional(binder: binder) { + Absent => + ResolveWalkAccepted { value: canonical_atom(identity: identity, occurrence_id: binder.occurrence_id), diagnostics: None, lexical: [] } + Present { value: kind } => + match resolve_node_walk(ctx: ctx, n: kind) { + ResolveWalkAccepted { value: resolved_kind, diagnostics: d, lexical: l } => + ResolveWalkAccepted { + value: node_with_occurrence_id( + kind: TypeNode { connective: Atom { identity: identity } }, + children: [core_edge(marker: BinderTypeEdge, target: resolved_kind)], + occurrence_id: binder.occurrence_id + ), + diagnostics: d, + lexical: l + } + ResolveWalkRefused { first: f, rest: r, observation: o } => ResolveWalkRefused { first: f, rest: r, observation: o } + } + } +} + +// The set's declared-order edge is label metadata (v2.std.node type_binder_conj_conforms), not a +// binder: it is carried through unchanged, never resolved as one. fn resolve_type_params_conj(ctx: ResolveContext, conj: Node) -> ResolveNodeWalk { child_walk_node(n: conj, w: fold(conj.children, init: child_walk_init(), f: fn(acc, e) { - child_walk_step(w: acc, e: e, r: resolve_type_param_binder(ctx: ctx, binder: e.target)) + if edge_is_core(e: e, marker: ArrowSignatureOrderEdge) { + child_walk_step(w: acc, e: e, r: ResolveWalkAccepted { value: e.target, diagnostics: None, lexical: [] }) + } else { + child_walk_step(w: acc, e: e, r: resolve_type_param_binder(ctx: ctx, binder: e.target)) + } })) } diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 0a5a90fc384..b4a230aeb7c 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -874,7 +874,8 @@ fn infer_declaration_wrapper_facts_from_entries( // already gives a type-denoting binding (the dag_binding_denotation arm of infer_node_facts): // TypeDenotationKind. That grants no member, construction or representation-sensitive coercion, and // for a generic declaration (`type MachineWidth`) it says only that the declaration names a type -// constructor -- a use's arity stays the binder authority's to check. It is not the empty product: an +// constructor -- a use's arity and kinds are checked at resolve by the binder authority +// (v2.std.type_binder type_application_conformance). It is not the empty product: an // authored empty record is a member, and forms through product introduction. fn infer_opaque_declaration_facts(node: Node, partials: List) -> Outcome { match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) { diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index ce5cedaed6e..1a523f1ad36 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -139,6 +139,7 @@ import v2.std.symbol_index { import v2.std.node { node_subtree_nodes, ArrowEffectClaimsEdge, + BinderTypeEdge, ArrowExecutionModeClaimEdge, ArrowResourceRequirementsEdge, MapLiteralEntryEdge, @@ -184,7 +185,7 @@ import v2.std.node { core_edge_label, edge_is_core, } -import v2.std.type_binder { cast_target_edge, type_alias_wrapper, type_decl_wrapper, type_opaque_wrapper, type_param_names, type_params_edge } +import v2.std.type_binder { type_binder_set_children, cast_target_edge, type_alias_wrapper, type_decl_wrapper, type_opaque_wrapper, type_param_names, type_params_edge } import v2.std.arrow_contract { effect_claim_label, hermetic_claim_label } import std.effects { EffectClaim, ReadonlyClaim, IdempotentClaim } import v2.std.node_query { @@ -3055,25 +3056,61 @@ fn body_lower_decl_generic_params_slot_optional(captured: Node) -> Optional, } +// generic_param is seq(name, optional(seq(`:`, kind))); an absent kind captures as the empty Conj. fn body_lower_generic_param_binder_optional(item: Node) -> Optional { - match body_lower_param_binding_atom_optional(node: body_lower_deep_unwrap_optional(node: item)) { + match sugar_sequence_pair_optional(node: body_lower_deep_unwrap_optional(node: item)) { + Absent => optional_absent() + Present { value: name_then_kind } => + let suffix = body_lower_deep_unwrap_optional(node: name_then_kind.right) + if is_empty_conj_root(n: suffix) { + body_lower_generic_param_named_optional(item: item, name_node: name_then_kind.left, kind: optional_absent()) + } else { + match sugar_sequence_pair_optional(node: suffix) { + Absent => optional_absent() + Present { value: colon_then_kind } => + match body_lower_type_expr_lowered_optional(node: colon_then_kind.right) { + Absent => optional_absent() + Present { value: kind } => body_lower_generic_param_named_optional(item: item, name_node: name_then_kind.left, kind: optional_present(value: kind)) + } + } + } + } +} + +fn body_lower_generic_param_named_optional(item: Node, name_node: Node, kind: Optional) -> Optional { + match body_lower_param_binding_atom_optional(node: body_lower_deep_unwrap_optional(node: name_node)) { Absent => optional_absent() Present { value: binder } => match node_atom_identity_optional(node: binder) { Absent => optional_absent() - Present { value: name } => optional_present(value: BodyLowerGenericBinder { item: item, binder: binder, name: name }) + Present { value: name } => optional_present(value: BodyLowerGenericBinder { item: item, binder: binder, name: name, kind: kind }) } } } +// The binder Atom, carrying the kind as its one BinderTypeEdge when the parameter declares one +// (v2.std.node type_binder_conforms). fn body_lower_generic_param_edge_of(b: BodyLowerGenericBinder) -> Edge { - Edge { label: Authored { name: b.name }, target: body_lower_param_ref_atom(source: b.item, identity: b.name) } + let atom = body_lower_param_ref_atom(source: b.item, identity: b.name) + match b.kind { + Absent => Edge { label: Authored { name: b.name }, target: atom } + Present { value: k } => + Edge { + label: Authored { name: b.name }, + target: node_with_occurrence_id(kind: atom.kind, children: [core_edge(marker: BinderTypeEdge, target: k)], occurrence_id: atom.occurrence_id) + } + } } // The repeat tail of comma_list(item): each element is seq(opt(comma), item). @@ -3185,11 +3222,11 @@ fn body_lower_decl_type_params(captured: Node) -> DeclTypeParams { Absent => TypeParamsUnreadable Present { value: edges } => TypeParams { - conj: node_lowered_from( + conj: close_lowered_image(root: node_lowered_from( kind: TypeNode { connective: Conj }, - children: edges, + children: type_binder_set_children(binders: edges, source: generic_params), source: generic_params - ) + )) } } } @@ -5329,7 +5366,7 @@ fn body_lower_function_value_arrow( let type_param_edges: List = match type_params { Empty => no_edges Cons { head: _, tail: _ } => - [type_params_edge(conj: node_lowered_from(kind: TypeNode { connective: Conj }, children: type_params, source: shell))] + [type_params_edge(conj: close_lowered_image(root: node_lowered_from(kind: TypeNode { connective: Conj }, children: type_binder_set_children(binders: type_params, source: shell), source: shell)))] } outcome_with_diagnostics( value: body_lower_callable_arrow( diff --git a/src/v2/compiler/symbol_index_fill.dag b/src/v2/compiler/symbol_index_fill.dag index b4ce19440da..92f6037bea0 100644 --- a/src/v2/compiler/symbol_index_fill.dag +++ b/src/v2/compiler/symbol_index_fill.dag @@ -92,21 +92,31 @@ data symbol_index_containment_disposition: Disposition = Scaffold { // declarations of the alias, and a binder is never a declared identity. // The node a declared name binds to, and the member the index descends into when the declaration // declares members -- one dispatch on the view for both. -// type_params: a GENERIC declaration binds its member, which cannot carry its binders, so they ride -// beside it (v2.std.symbol_index symbol_index_mark_declared_type_params). Empty for every other arm: -// an alias or bodyless declaration binds its wrapper, which still carries them. +// binders: a GENERIC declaration binds its member, which cannot carry its binders, so they ride +// beside it (v2.std.symbol_index symbol_index_mark_declared_type_params). An alias or bodyless +// declaration binds its wrapper and its binders are recorded beside it too, so every declaration that +// binds type parameters answers v2.std.symbol_index symbol_index_declared_binders_at the same way -- +// the read resolve's type-application check (v2.std.type_binder type_application_conformance) takes. +// Absent only for a plain member, which binds none. type SymbolIndexDeclared { bound: Node members: Optional - type_params: List + binders: Optional } fn symbol_index_declared(target: Node) -> SymbolIndexDeclared { match type_decl_view(target: target) { - GenericTypeDecl { binders: _, member: m } => SymbolIndexDeclared { bound: m, members: optional_present(value: m), type_params: type_param_names(n: target) } - TypeAlias { binders: _, aliased: _ } => SymbolIndexDeclared { bound: target, members: optional_absent(), type_params: Empty } - OpaqueTypeDecl { binders: _ } => SymbolIndexDeclared { bound: target, members: optional_absent(), type_params: Empty } - PlainTypeDecl { member: m } => SymbolIndexDeclared { bound: m, members: optional_present(value: m), type_params: Empty } + GenericTypeDecl { binders: b, member: m } => SymbolIndexDeclared { bound: m, members: optional_present(value: m), binders: optional_present(value: b) } + TypeAlias { binders: b, aliased: _ } => SymbolIndexDeclared { bound: target, members: optional_absent(), binders: optional_present(value: b) } + OpaqueTypeDecl { binders: b } => SymbolIndexDeclared { bound: target, members: optional_absent(), binders: optional_present(value: b) } + PlainTypeDecl { member: m } => SymbolIndexDeclared { bound: m, members: optional_present(value: m), binders: optional_absent() } + } +} + +fn symbol_index_mark_declared_binders(index: SymbolIndex, qualified_path: QualifiedName, binders: Optional) -> SymbolIndex { + match binders { + Present { value: b } => symbol_index_mark_declared_type_params(index: index, qualified_path: qualified_path, params: b) + Absent => index } } @@ -115,14 +125,14 @@ fn symbol_index_fill_declared_child(index: SymbolIndex, path: QualifiedName, seg let child_path = qualified_name_snoc(qn: path, segment: segment) let declared = symbol_index_declared(target: symbol_index_binder_type_or_target(target: edge.target)) let with_binding = symbol_index_mark_namespace_body_if( - index: symbol_index_mark_declared_type_params( + index: symbol_index_mark_declared_binders( index: symbol_index_insert( index: index, qualified_path: child_path, resolved: declared.bound ), qualified_path: child_path, - params: declared.type_params + binders: declared.binders ), qualified_path: child_path, target: edge.target diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 506232a2bd6..0c1c3938d58 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -904,12 +904,30 @@ fn dag_grammar_generic_params_expr() -> GrammarExpr { dag_grammar_sequence( left: dag_grammar_terminal(token_class: ^dag_token_lt), right: dag_grammar_sequence( - left: dag_grammar_comma_list_expr(item: dag_grammar_ident_or_type_decl_modifier_name()), + left: dag_grammar_comma_list_expr(item: dag_grammar_generic_param_expr()), right: dag_grammar_terminal(token_class: ^dag_token_gt) ) ) } +// ONE TYPE PARAMETER: a name, optionally bounded by a KIND (`type MachineWidth`), +// as v1 02_parse parse_optional_type_param_kind reads it. Left-factored as seq(name, optional(suffix)), +// the shape the other optional-suffix rules share (dag_grammar_typed_param_expr): an absent kind +// captures as (name, ), so no ordered choice re-reads the name. The kind lowers onto the +// binder (v2.compiler.body_lowering_fold body_lower_generic_param_edge_of) and is enforced at each +// application (v2.std.type_binder type_application_conformance). +fn dag_grammar_generic_param_expr() -> GrammarExpr { + dag_grammar_sequence( + left: dag_grammar_ident_or_type_decl_modifier_name(), + right: dag_grammar_optional( + element: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_colon), + right: dag_grammar_nonterminal(production: ^dag_production_type_expr) + ) + ) + ) +} + // A PARAMETER MAY REFINE ITS TYPE WITH A WHERE CLAUSE AND MAY CARRY A DEFAULT (`lifetime_seconds: Int // where range(min: 1, max: 3600) = 3600`), as v1 02_parse parse_param reads it. ONE ALTERNATIVE, // LEFT-FACTORED: `name: T` is the shared prefix and the tail is optional, so no choice is made on a diff --git a/src/v2/std/integer.dag b/src/v2/std/integer.dag index 010eff9feb6..c0fba422c7e 100644 --- a/src/v2/std/integer.dag +++ b/src/v2/std/integer.dag @@ -20,22 +20,13 @@ import v2.std.node_query { find_named_child } import std.integer { Signedness, Signed, Unsigned } import std.content_hash { Fnv1a64Structural, content_hash_atom, content_hash_tagged_structural } import std.types { NonEmptyStr, List } -import v2.std.machine { - Byte, - MachineWidth, - PointerWidth, - Word8, - Word16, - Word32, - Word64, - Word128 -} +import v2.std.machine { Byte } +import std.machine_constraints { Compose, MachineWidth, PointerWidth } import std.nat { Nat, Zero, Succ, NatQuotient, nat_div_rem_by_succ } import v2.std.text { Char, CharAbsent, CharFound, String, string_head, string_tail } import std.bit { Word64 } type Int = GroupCompletion type UInt = Nat -type Compose type Representation = TwosComplement @@ -44,17 +35,17 @@ type Representation type OverflowDisposition = Wrapping | Saturating | UndefinedBehavior | Trapping -type Int8 = Compose> -type Int16 = Compose> -type Int32 = Compose> -type Int64 = Compose> -type Int128 = Compose> - -type UInt8 = Compose> -type UInt16 = Compose> -type UInt32 = Compose> -type UInt64 = Compose> -type UInt128 = Compose> +type Int8 = Compose> +type Int16 = Compose> +type Int32 = Compose> +type Int64 = Compose> +type Int128 = Compose> + +type UInt8 = Compose> +type UInt16 = Compose> +type UInt32 = Compose> +type UInt64 = Compose> +type UInt128 = Compose> type IntPlatform = Compose> type UIntPlatform = Compose> diff --git a/src/v2/std/machine.dag b/src/v2/std/machine.dag index 3034657a969..063c4166075 100644 --- a/src/v2/std/machine.dag +++ b/src/v2/std/machine.dag @@ -2,5 +2,3 @@ module v2.std.machine import std.bit { Bit, Byte, Word8, Word16, Word32, Word64, Word128 } -type MachineWidth -type PointerWidth diff --git a/src/v2/std/node.dag b/src/v2/std/node.dag index 96f396ec4c4..c31071412ee 100644 --- a/src/v2/std/node.dag +++ b/src/v2/std/node.dag @@ -849,13 +849,16 @@ fn arrow_named_edge_is_non_binder(e: Edge) -> Bool { } } -// WHETHER AN EDGE IS AN ARROW'S DECLARED ORDER: label metadata (the domain's binder labels), not a value -// the Arrow is built from. The one classification every reader that walks values through an Arrow asks -// -- v2.compiler.infer (its gather fold and product evidence) and std.kind's roster-kind index -- so -// no reader keeps its own list of metadata labels. +// WHETHER AN EDGE IS A DECLARED ORDER: label metadata (binder labels), not a value the parent is built +// from. Two parents carry one: an Arrow (its domain's order) and a type-parameter binder set +// (type_binder_conj_conforms). A Conj can carry the core marker only as a binder set -- no authored +// label spells a core marker -- so the Conj arm answers for exactly those. The one classification +// every reader that walks values through either asks -- v2.compiler.infer (its gather fold and product +// evidence) and std.kind's roster-kind index -- so no reader keeps its own list of metadata labels. fn arrow_signature_order_edge(parent: Node, edge: Edge) -> Bool { match parent.kind { TypeNode { connective: Arrow } => edge_is_core(e: edge, marker: ArrowSignatureOrderEdge) + TypeNode { connective: Conj } => edge_is_core(e: edge, marker: ArrowSignatureOrderEdge) _ => false } } @@ -1078,27 +1081,74 @@ fn arrow_first_positional_target(children: List) -> FirstPositionalTarget // the Conj (v2.std.type_binder) rather than by a second node kind. The same Conj rides on an Arrow for // `fn f` and on a type declaration's member for `type Box`; a binder whose target is not its own // Atom is unwritable here rather than refused downstream. +// +// A KINDED TYPE PARAMETER (`type MachineWidth`) carries its kind the way a value +// binder carries its type: one BinderTypeEdge, here on the binder's own Atom, so the identity the +// binder declares is unchanged and an unkinded binder is exactly the leaf it was. Any other child is +// unwritable. v2.std.type_binder type_param_kind_optional is the one reader of the edge. fn type_binder_conforms(e: Edge) -> Bool { match e.label { Positional => false StructuralLabel { label: _ } => false Authored { name: sym } => match e.target.kind { - TypeNode { connective: Atom { identity: id } } => (id == sym) && (count(e.target.children) == 0) + TypeNode { connective: Atom { identity: id } } => (id == sym) && type_binder_children_conform(children: e.target.children) _ => false } } } +fn type_binder_children_conform(children: List) -> Bool { + match children { + Empty => true + Cons { head: k, tail: Empty } => edge_is_core(e: k, marker: BinderTypeEdge) + Cons { head: _, tail: Cons { head: _, tail: _ } } => false + } +} + +// A BINDER SET CARRIES ITS DECLARED ORDER, the way an Arrow's domain does. The Conj's binder edges are +// labelled, and content hashing sorts labelled edges, so `type Pair` and `type Pair` would +// otherwise be one identity and an application's arguments would pair with binders in LABEL order. So +// a set that binds any name carries exactly one ^arrow_signature_order_edge -- the carrier a declared +// signature already uses (v2.std.arrow_signature signature_order_edge), read by the same parser +// (arrow_signature_order_read) -- whose labels are exactly a permutation of the binder labels; a set +// that binds none carries no order. Any other edge is unwritable here. fn type_binder_conj_conforms(t: Node) -> Bool { match t.kind { TypeNode { connective: Conj } => all_names_distinct(children: t.children) - && fold(t.children, init: true, f: fn(acc, e) { acc && type_binder_conforms(e: e) }) + && fold(t.children, init: true, f: fn(acc, e) { acc && type_binder_set_edge_conforms(e: e) }) + && type_binder_order_conforms(children: t.children) _ => false } } +fn type_binder_set_edge_conforms(e: Edge) -> Bool { + match e.label { + Authored { name: _ } => type_binder_conforms(e: e) + StructuralLabel { label: _ } => edge_is_core(e: e, marker: ArrowSignatureOrderEdge) + Positional => false + } +} + +fn type_binder_labels_of(children: List) -> List { + fold(children, init: Empty, f: fn(acc, e) { + match e.label { + Authored { name: sym } => list_snoc_item(xs: acc, item: sym) + StructuralLabel { label: _ } => acc + Positional => acc + } + }) +} + +fn type_binder_order_conforms(children: List) -> Bool { + match arrow_signature_order_read(children: children) { + OrderAbsent => count(type_binder_labels_of(children: children)) == 0 + OrderUnreadable => false + OrderLabels { labels: labels } => symbols_are_one_distinct_set(a: labels, b: type_binder_labels_of(children: children)) + } +} + type NamedEdgeTargetLookup = Found { target: Node } | Ambiguous diff --git a/src/v2/std/symbol_index.dag b/src/v2/std/symbol_index.dag index 44ee2b51fa5..dc0105e4a1f 100644 --- a/src/v2/std/symbol_index.dag +++ b/src/v2/std/symbol_index.dag @@ -28,7 +28,7 @@ import v2.std.optional { } import v2.std.diagnostic { Accepted, Rejected } import v2.std.node { Node, Symbol } -import v2.std.type_binder { AliasRenaming, NotARenaming, PureRenamingOf, type_alias_renaming } +import v2.std.type_binder { AliasRenaming, NotARenaming, PureRenamingOf, binder_conj_names, type_alias_renaming } import v2.std.qualified_name { QualifiedName, qualified_name_init, @@ -86,7 +86,7 @@ type SymbolIndex { bound_declarings: Map> declared_payloads: Map renaming_aliases: Map - declared_type_params: Map> + declared_type_params: Map declared_resources: Map namespace_bodies: Map } @@ -372,7 +372,7 @@ fn symbol_index_declares_resource_at(index: SymbolIndex, qualified_path: Qualifi } } -fn symbol_index_mark_declared_type_params(index: SymbolIndex, qualified_path: QualifiedName, params: List) -> SymbolIndex { +fn symbol_index_mark_declared_type_params(index: SymbolIndex, qualified_path: QualifiedName, params: Node) -> SymbolIndex { SymbolIndex { entries: index.entries, global_bare: index.global_bare, @@ -386,12 +386,18 @@ fn symbol_index_mark_declared_type_params(index: SymbolIndex, qualified_path: Qu } fn symbol_index_declared_type_params_at(index: SymbolIndex, qualified_path: QualifiedName) -> List { - match map_lookup(m: index.declared_type_params, key: qualified_path) { - Present { value: params } => params + match symbol_index_declared_binders_at(index: index, qualified_path: qualified_path) { + Present { value: binders } => binder_conj_names(conj: binders) Absent => Empty } } +// THE BINDER CONJ A DECLARATION BINDS, kinds included (v2.std.type_binder type_param_kind_optional). +// Absent for a declaration that binds no type parameters. +fn symbol_index_declared_binders_at(index: SymbolIndex, qualified_path: QualifiedName) -> Optional { + map_lookup(m: index.declared_type_params, key: qualified_path) +} + fn symbol_index_global_unique_lookup(index: SymbolIndex, name: Symbol) -> GlobalBareLookup { match v2.std.collection.map_get(index.global_bare, name) { Accepted { value: opt, diagnostics: _ } => match opt { diff --git a/src/v2/std/type_binder.dag b/src/v2/std/type_binder.dag index 9fdddaa4a77..5aeb6546722 100644 --- a/src/v2/std/type_binder.dag +++ b/src/v2/std/type_binder.dag @@ -2,8 +2,10 @@ module v2.std.type_binder import std.types { List } import std.algebra { Cons, Empty, list_snoc_item } +import v2.std.algebra { zip_map } import v2.std.optional { Optional, Present, Absent, optional_present, optional_absent } import v2.std.arrow_contract { arrow_contract_conforms } +import v2.std.arrow_signature { signature_order_edge, arrow_signature_order_head_is_list_introduction } import v2.std.node_query { binder_node_parts } import v2.std.node { MatchArmScopeExitEdge, @@ -38,6 +40,12 @@ import v2.std.node { TypeAnnotationEdge, TypeBodyEdge, TypeParamsEdge, + BinderTypeEdge, + arrow_signature_order_read, + OrderAbsent, + OrderLabels, + OrderUnreadable, + edge_is_core, core_edge_label, ArrowBodyEdge, ArrowSignatureOrderEdge, @@ -133,8 +141,9 @@ fn type_alias_wrapper(binders: Node, aliased: Node) -> Node { // `type MachineWidth` declares binders and no body: Conj { : Conj { bits: bits } }. // Not an empty member: an empty Conj body would assert a record with no fields, a different fact. The -// binders are carried because a use's arity (`MachineWidth<64>`) is checked against them. THE ONE -// PRODUCER of the opaque wrapper. +// binders are carried because a use (`MachineWidth<64>`) is checked against them -- arity and kind -- +// by type_application_conformance at v2.compiler.resolve resolve_type_application. Until that consumer +// landed this sentence claimed a check nothing performed. THE ONE PRODUCER of the opaque wrapper. fn type_opaque_wrapper(binders: Node) -> Node { node_synthetic( kind: TypeNode { connective: Conj }, @@ -248,14 +257,150 @@ fn type_param_names(n: Node) -> List { } } +// THE KIND A TYPE PARAMETER DECLARES, read off its binder Atom: `bits: WidthResolution` lowers its +// binder to Atom{bits} carrying one BinderTypeEdge -> WidthResolution (v2.std.node +// type_binder_conforms admits exactly that child). Absent for an unkinded parameter. +fn type_param_kind_optional(binder: Node) -> Optional { + fold(binder.children, init: optional_absent(), f: fn(acc, e) { + if edge_is_core(e: e, marker: BinderTypeEdge) { optional_present(value: e.target) } else { acc } + }) +} + +// WHETHER AN APPLIED TYPE ARGUMENT INHABITS A PARAMETER'S KIND, as the caller can establish it. The +// judgment needs the declarations the kind and argument resolve to, which only resolve holds, so it +// is supplied; the PAIRING it is applied over is decided here and nowhere else. ArgumentLiteralUnjudged +// is the language-level Nat literal rule: a literal is admitted in any kinded position and is NOT +// judged against the kind's roster. ArgumentTypeParameterUnjudged is an argument that is itself a type +// parameter of an enclosing declaration (`MachineWidth` inside a generic over bits): its +// instances are judged where that declaration is applied, not here. Both ADMIT without crediting +// inhabitance, and this module records no count of them: nothing would consume one. The honest +// record of what stays unjudged is the declared frontier std.machine_constraints +// machine_width_literal_roster_frontier, which states the rung this position sits at. +type KindInhabitance + = ArgumentInhabitsKind + | ArgumentLiteralUnjudged + | ArgumentTypeParameterUnjudged + | ArgumentOutsideKind + | KindUnresolved + +// A TYPE APPLICATION AGAINST ITS DECLARATION'S BINDERS. Exact bijection first: arguments pair with +// binders by position only once their counts agree, so a kind is never judged against an argument an +// arity error has shifted. Then each kinded binder's argument is judged in order and the first that +// is not inhabited refuses AT THAT ARGUMENT. An unkinded binder admits any argument, as before. +type TypeApplicationConformance + = TypeApplicationConforms + | TypeApplicationArityMismatch { declared: Int, supplied: Int } + | TypeApplicationKindNotInhabited { argument: Node, kind: Node } + | TypeApplicationKindUnresolved { argument: Node, kind: Node } + | TypeApplicationBinderOrderMalformed + +// THE ONE AUTHORITY for checking an applied type against the binders it instantiates, consumed by +// v2.compiler.resolve at the head->declaration join (resolve_type_application_conformance). Before it, +// this module's wrapper notes said a use's arity "is checked against" the binders while nothing +// performed the check. +fn type_application_conformance( + binders: Node, + arguments: List, + inhabits: fn(Node, Node) -> KindInhabitance +) -> TypeApplicationConformance { + match type_param_order(binders: binders) { + TypeParamOrderMalformed => TypeApplicationBinderOrderMalformed + TypeParamOrderDeclared { labels: labels } => + if count(labels) != count(arguments) { + TypeApplicationArityMismatch { declared: count(labels), supplied: count(arguments) } + } else { + fold(zip_map(a: labels, b: arguments, f: fn(l, arg) { TypeParamArgument { name: l, argument: arg } }), + init: TypeApplicationConforms, + f: fn(acc, pa) { type_application_step(acc: acc, binders: binders, pa: pa, inhabits: inhabits) }) + } + } +} + +type TypeParamArgument { + name: Symbol + argument: Node +} + +fn type_application_step(acc: TypeApplicationConformance, binders: Node, pa: TypeParamArgument, inhabits: fn(Node, Node) -> KindInhabitance) -> TypeApplicationConformance { + match acc { + TypeApplicationConforms => + match type_binder_target_of(binders: binders, name: pa.name) { + Absent => TypeApplicationBinderOrderMalformed + Present { value: binder } => + match type_param_kind_optional(binder: binder) { + Absent => acc + Present { value: kind } => + match inhabits(pa.argument, kind) { + ArgumentInhabitsKind => acc + ArgumentLiteralUnjudged => acc + ArgumentTypeParameterUnjudged => acc + ArgumentOutsideKind => TypeApplicationKindNotInhabited { argument: pa.argument, kind: kind } + KindUnresolved => TypeApplicationKindUnresolved { argument: pa.argument, kind: kind } + } + } + } + TypeApplicationArityMismatch { declared: _, supplied: _ } => acc + TypeApplicationKindNotInhabited { argument: _, kind: _ } => acc + TypeApplicationKindUnresolved { argument: _, kind: _ } => acc + TypeApplicationBinderOrderMalformed => acc + } +} + +// THE DECLARED ORDER OF A BINDER SET, read once. A set binds its names in AUTHORED order, carried by +// the set's one ^arrow_signature_order_edge (v2.std.node type_binder_conj_conforms) -- never by the +// stored sequence of its labelled edges, which content hashing sorts. A set binding no name has the +// empty order. Malformed is a set v2.std.node refuses; resolve refuses it before any reader runs +// (type_binder_labels_conform), so a reader meeting it here answers nothing rather than guessing. +type TypeParamOrder + = TypeParamOrderDeclared { labels: List } + | TypeParamOrderMalformed + +fn type_param_order(binders: Node) -> TypeParamOrder { + if !type_binder_conj_conforms(t: binders) { + TypeParamOrderMalformed + } else { + match arrow_signature_order_read(children: binders.children) { + OrderAbsent => TypeParamOrderDeclared { labels: Empty } + OrderUnreadable => TypeParamOrderMalformed + OrderLabels { labels: labels } => + if arrow_signature_order_head_is_list_introduction(arrow: binders) { TypeParamOrderDeclared { labels: labels } } else { TypeParamOrderMalformed } + } + } +} + +// The names a binder set declares, IN DECLARED ORDER: every positional reader of type parameters +// (an application's pairing, an alias renaming, infer's instance zip through +// v2.std.symbol_index symbol_index_declared_type_params_at) reads them here. fn binder_conj_names(conj: Node) -> List { - fold(conj.children, init: Empty, f: fn(acc, e) { + match type_param_order(binders: conj) { + TypeParamOrderDeclared { labels: labels } => labels + TypeParamOrderMalformed => Empty + } +} + +// THE ONE MINT OF A BINDER SET'S EDGES: the binder edges as authored, plus -- when any name is bound -- +// the order edge built from those same edges by the declared-signature carrier +// (v2.std.arrow_signature signature_order_edge), so the set and its order are one fact from one list. +// The caller wraps the result in its own located Conj. +fn type_binder_set_children(binders: List, source: Node) -> List { + let names = fold(binders, init: Empty, f: fn(acc, e) { match e.label { Authored { name: sym } => list_snoc_item(xs: acc, item: sym) StructuralLabel { label: _ } => acc Positional => acc } }) + if count(names) == 0 { binders } else { list_snoc_item(xs: binders, item: signature_order_edge(order: names, source: source)) } +} + +fn type_binder_target_of(binders: Node, name: Symbol) -> Optional { + fold(binders.children, init: optional_absent(), f: fn(acc, e) { + match e.label { + Authored { name: sym } => if sym == name { optional_present(value: e.target) } else { acc } + StructuralLabel { label: _ } => acc + Positional => acc + } + }) } // THE EDGE THAT CARRIES A CAST'S TARGET TYPE. `e as T` lowers to Transform[coerce, e] with this 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 db91cf4696b..95c03c0e07c 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 @@ -27,7 +27,7 @@ import v2.std.diagnostic { diagnostics_has_reason } import std.algebra { list_snoc_item } -import v2.std.type_binder { type_params_edge } +import v2.std.type_binder { type_binder_set_children, type_params_edge } import v2.std.optional { Absent, Optional, Present } import v2.std.node_query { binder_edge } import v2.std.node { @@ -117,12 +117,12 @@ fn inhabitance_generic_formal_tree() -> Node { item: type_params_edge( conj: node_synthetic( kind: TypeNode { connective: Conj }, - children: [ + children: type_binder_set_children(binders: [ Edge { label: Authored { name: ^inhabitance_type_param_t }, target: dag_type_atom_node(identity: ^inhabitance_type_param_t) } - ] + ], source: dag_type_atom_node(identity: ^inhabitance_type_param_t)) ) ) ) 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 index 31cb180e3c0..e5c36224250 100644 --- 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 @@ -20,7 +20,7 @@ import v2.std.list_introduction { list_introduction_head_path, lower_list_introd 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.type_binder { type_params_edge } +import v2.std.type_binder { type_binder_set_children, type_params_edge } import std.algebra { list_snoc_item } import v2.std.node_query { binder_edge } import v2.std.node { @@ -101,9 +101,9 @@ fn dr_generic_arrow(type_param: Symbol, return_type: Node, body: Node) -> Node { item: type_params_edge( conj: node_synthetic( kind: TypeNode { connective: Conj }, - children: [ + children: type_binder_set_children(binders: [ Edge { label: Authored { name: type_param }, target: dag_type_atom_node(identity: type_param) } - ] + ], source: dag_type_atom_node(identity: type_param)) ) ) ) diff --git a/src/v2/test/claim/manual/infer_ground_add.dag b/src/v2/test/claim/manual/infer_ground_add.dag index 1ee4d5f6d5a..d4644b997bc 100644 --- a/src/v2/test/claim/manual/infer_ground_add.dag +++ b/src/v2/test/claim/manual/infer_ground_add.dag @@ -365,8 +365,8 @@ fn infer_descent_witness_contract_node(n: Node) -> Outcome { data case_infer_add_compiles: InferReceiptCase = InferCompilesReceiptCase { label: "manual/infer: infer(fixture_add_resolved_tree) derives descent and accepts", input_symbol: ^infer_receipt_input_infer_add, - input: fixture_add_resolved_tree(), - expected_value: fixture_add_resolved_tree() + input: fixture_add_resolved_tree().root, + expected_value: fixture_add_resolved_tree().root } data subject_infer_add_compiles: TestClaimEvalSubject = infer_receipt_subject(case: case_infer_add_compiles) diff --git a/src/v2/test/claim/manual/solve_constraints_add.dag b/src/v2/test/claim/manual/solve_constraints_add.dag index 24e440eb490..b9c02b8ca85 100644 --- a/src/v2/test/claim/manual/solve_constraints_add.dag +++ b/src/v2/test/claim/manual/solve_constraints_add.dag @@ -29,7 +29,7 @@ import v2.std.verification { } fn fixture_add_constraint_graph() -> ConstraintGraph { - ConstraintGraph { root: fixture_add_resolved_tree() } + ConstraintGraph { root: fixture_add_resolved_tree().root } } fn anchor_solve_constraints_add() -> Outcome { @@ -42,9 +42,9 @@ fn anchor_solve_constraints_add() -> Outcome { data witness_solve_constraints_add_accepts: Bool = match anchor_solve_constraints_add() { Accepted { value: g, diagnostics: d } => - (g.node == fixture_add_resolved_tree()) + (g.node == fixture_add_resolved_tree().root) && (g.witness.structural.property == ^preservation_rule_constraint_satisfaction) - && (g.witness.structural.evidence == fixture_add_resolved_tree()) + && (g.witness.structural.evidence == fixture_add_resolved_tree().root) && (g.witness.closedness.property == ^constraint_property_candidate_set_closedness) && (d == None) Rejected { diagnostics: _ } => false diff --git a/src/v2/test/claim/match_binder/match_binder_typing_test.dag b/src/v2/test/claim/match_binder/match_binder_typing_test.dag index 7729029f87a..de171d5c36c 100644 --- a/src/v2/test/claim/match_binder/match_binder_typing_test.dag +++ b/src/v2/test/claim/match_binder/match_binder_typing_test.dag @@ -32,6 +32,7 @@ import v2.std.node { core_edge_label } import v2.std.node_query { binder_node, construct_node, field_projection_optional } +import v2.std.type_binder { type_binder_set_children } import v2.std.symbol_index { SymbolIndex, empty_symbol_index, @@ -592,7 +593,7 @@ fn mbt_index() -> SymbolIndex { resolved: mbt_parse_artifact_declaration() ), qualified_path: mbt_qn(segs: [^p, ^Outcome]), - params: [^T] + params: mbt_conj(fields: type_binder_set_children(binders: [Edge { label: Authored { name: ^T }, target: Node { kind: TypeNode { connective: Atom { identity: ^T } }, children: [], occurrence_id: OccurrenceSynthetic } }], source: mbt_conj(fields: []))) ) } diff --git a/src/v2/test/claim/type_application_kind_test.dag b/src/v2/test/claim/type_application_kind_test.dag new file mode 100644 index 00000000000..85e5e04ae90 --- /dev/null +++ b/src/v2/test/claim/type_application_kind_test.dag @@ -0,0 +1,185 @@ +module v2.test.claim.type_application_kind + +import v2.compiler.resolve { ResolvedTree } +import extdeps.communication.medium { Lossless, Medium } +import v2.compiler.name_resolve { Admission, ResolutionSubject } +import v2.compiler.program_assembly { assemble_program_from_ingest } +import v2.compiler.source_authority { DagSourceReadWitness } +import v2.extdeps.languages.dag { dag_language_model } +import std.algebra { Cons, Empty } +import v2.std.cross_tree.import_model { V2Tree } +import v2.std.artifact { Artifact, SourceFile } +import v2.std.diagnostic { Accepted, Outcome, Rejected, diagnostics_fatal_reason } +import std.occurrence_identity { OccurrenceSynthetic } +import v2.std.node { Atom, Authored, BinderTypeEdge, Conj, Edge, Node, Positional, StructuralLabel, Symbol, TypeNode, core_edge } +import v2.std.type_binder { ArgumentInhabitsKind, ArgumentLiteralUnjudged, ArgumentOutsideKind, KindInhabitance, TypeApplicationArityMismatch, TypeApplicationConforms, TypeApplicationKindNotInhabited, type_application_conformance, type_binder_set_children } +import std.types { List } + +// A TYPE APPLICATION AGAINST ITS DECLARATION'S BINDERS (v2.std.type_binder type_application_conformance, +// consumed by v2.compiler.resolve resolve_type_application). Each specimen is one inline source over the +// real assembly route; the kinded declaration mirrors std.machine_constraints MachineWidth, whose +// `` is the corpus's use. Controls: a conforming kinded argument, a literal and an +// unkinded parameter are accepted; a non-conforming argument refuses at the argument; an application whose +// argument count differs from its declaration's binders refuses -- including one applied to a declaration +// that binds none. +data tak_artifact: Artifact = Artifact { + kind: SourceFile, + id: ^type_application_kind_artifact, + file_path: "src/v2/pilot/type_application_kind_pilot.dag" +} + +fn tak_assemble(src: String) -> Outcome { + assemble_program_from_ingest( + ingest: Cons { + head: DagSourceReadWitness { + source: Medium { carried: src, fidelity: Lossless }, + artifact: tak_artifact, + compilation_unit: ^type_application_kind_cu, + source_root: V2Tree + }, + tail: Empty + }, + admission: Admission { subject: ResolutionSubject { name: Cons { head: ^p, tail: Empty } }, imports: Empty }, + lm: dag_language_model() + ) +} + +fn tak_accepts(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn tak_refuses_with(o: Outcome, reason: Symbol) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == reason + } +} + +fn tak_prelude() -> String { + "module p\n\ntype Resolution\n = Static\n | Pointer\n\ntype Other\n = Foreign\n | Alien\n\ntype Width\n\ntype Plain\n\ntype ZKind\n = | Zk\n\ntype AKind\n = | Ak\n\ntype Pair\n\n" +} + +fn tak_kind_conforms() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type UsesPointer = Width\n")) } +fn tak_kind_literal() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type UsesEight = Width<8>\n")) } +fn tak_kind_foreign_variant() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type UsesForeign = Width\n")) } +fn tak_kind_kernel_type() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type UsesInt = Width\n")) } +fn tak_unkinded() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type UsesPlain = Plain\n")) } +fn tak_arity_over() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type TooMany = Plain\n")) } +// Parameter names that sort OPPOSITE to their authored order, each with its own kind: a binder Conj is +// canonicalized by label, so pairing through its stored edges would judge Zk against AKind. +fn tak_order_authored() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type InOrder = Pair\n")) } +fn tak_order_swapped() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type Swapped = Pair\n")) } +fn tak_arity_nongeneric() -> Outcome { tak_assemble(src: concat(tak_prelude(), "type NotGeneric = Other\n")) } + +test fn tak_kinded_parameter_accepts_a_variant_of_its_kind() -> Bool { + tak_accepts(o: tak_kind_conforms()) +} + +test fn tak_kinded_parameter_accepts_a_nat_literal_unjudged() -> Bool { + tak_accepts(o: tak_kind_literal()) +} + +test fn tak_kinded_parameter_refuses_a_variant_of_another_coproduct() -> Bool { + tak_refuses_with(o: tak_kind_foreign_variant(), reason: ^resolve_reason_type_argument_kind_not_inhabited) +} + +test fn tak_kinded_parameter_refuses_a_kernel_type() -> Bool { + tak_refuses_with(o: tak_kind_kernel_type(), reason: ^resolve_reason_type_argument_kind_not_inhabited) +} + +test fn tak_arguments_pair_with_parameters_in_authored_order() -> Bool { + tak_accepts(o: tak_order_authored()) +} + +test fn tak_arguments_swapped_against_authored_order_refuse() -> Bool { + tak_refuses_with(o: tak_order_swapped(), reason: ^resolve_reason_type_argument_kind_not_inhabited) +} + +test fn tak_unkinded_parameter_is_unchanged() -> Bool { + tak_accepts(o: tak_unkinded()) +} + +test fn tak_application_with_more_arguments_than_binders_refuses() -> Bool { + tak_refuses_with(o: tak_arity_over(), reason: ^resolve_reason_type_application_arity_mismatch) +} + +test fn tak_application_of_a_non_generic_declaration_refuses() -> Bool { + tak_refuses_with(o: tak_arity_nongeneric(), reason: ^resolve_reason_type_application_arity_mismatch) +} + +// THE VERDICT AT ITS OWN INTERFACE, over supplied binders and a supplied judgment (DESIGN section 3: a +// witness discriminates at one interface; the specimens above are this boundary's inhabitance claims on +// the real route). A literal the judgment leaves unjudged is admitted, never refused -- the frontier +// std.machine_constraints machine_width_literal_roster_frontier declares -- and an arity mismatch is +// decided before any kind is judged. +fn tak_atom(id: Symbol) -> Node { + Node { kind: TypeNode { connective: Atom { identity: id } }, children: [], occurrence_id: OccurrenceSynthetic } +} + +fn tak_binder(name: Symbol, kind: Symbol) -> Edge { + Edge { + label: Authored { name: name }, + target: Node { kind: TypeNode { connective: Atom { identity: name } }, children: [core_edge(marker: BinderTypeEdge, target: tak_atom(id: kind))], occurrence_id: OccurrenceSynthetic } + } +} + +fn tak_set(binders: List) -> Node { + Node { kind: TypeNode { connective: Conj }, children: type_binder_set_children(binders: binders, source: tak_atom(id: ^binders)), occurrence_id: OccurrenceSynthetic } +} + +fn tak_kinded_binders() -> Node { + tak_set(binders: [tak_binder(name: ^bits, kind: ^Resolution)]) +} + +// `` with its binder edges STORED IN LABEL ORDER (a, z) -- what content hashing's +// canonical sequence is -- and the declared order (z, a) minted from the authored list. Built by +// taking the authored set's order edge and re-sequencing only the binder edges. +fn tak_pair_binders_label_sorted() -> Node { + let authored = tak_set(binders: [tak_binder(name: ^z, kind: ^ZKind), tak_binder(name: ^a, kind: ^AKind)]) + let order_edges = fold(authored.children, init: Empty, f: fn(acc, e) { + match e.label { + Authored { name: _ } => acc + StructuralLabel { label: _ } => concat(acc, [e]) + Positional => acc + } + }) + Node { kind: TypeNode { connective: Conj }, children: concat([tak_binder(name: ^a, kind: ^AKind), tak_binder(name: ^z, kind: ^ZKind)], order_edges), occurrence_id: OccurrenceSynthetic } +} + +// The supplied judgment: an argument inhabits a kind exactly when it is that kind's one variant. +fn tak_pair_judge(argument: Node, kind: Node) -> KindInhabitance { + let expected = if kind == tak_atom(id: ^ZKind) { tak_atom(id: ^Zk) } else { tak_atom(id: ^Ak) } + if argument == expected { ArgumentInhabitsKind } else { ArgumentOutsideKind } +} + + +test fn tak_unjudged_literal_argument_is_admitted() -> Bool { + match type_application_conformance(binders: tak_kinded_binders(), arguments: [tak_atom(id: ^eight)], inhabits: fn(a, k) { ArgumentLiteralUnjudged }) { + TypeApplicationConforms => true + _ => false + } +} + +test fn tak_pairing_follows_declared_order_not_stored_sequence() -> Bool { + match type_application_conformance(binders: tak_pair_binders_label_sorted(), arguments: [tak_atom(id: ^Zk), tak_atom(id: ^Ak)], inhabits: fn(a, k) { tak_pair_judge(argument: a, kind: k) }) { + TypeApplicationConforms => true + _ => false + } +} + +test fn tak_arguments_swapped_against_declared_order_refuse_at_the_interface() -> Bool { + match type_application_conformance(binders: tak_pair_binders_label_sorted(), arguments: [tak_atom(id: ^Ak), tak_atom(id: ^Zk)], inhabits: fn(a, k) { tak_pair_judge(argument: a, kind: k) }) { + TypeApplicationKindNotInhabited { argument: _, kind: _ } => true + _ => false + } +} + +test fn tak_arity_is_decided_before_kind() -> Bool { + match type_application_conformance(binders: tak_kinded_binders(), arguments: [tak_atom(id: ^a), tak_atom(id: ^b)], inhabits: fn(a, k) { ArgumentOutsideKind }) { + TypeApplicationArityMismatch { declared: d, supplied: s } => (d == 1) && (s == 2) + _ => false + } +} diff --git a/src/v2/test/claim/type_param_binder_frame_test.dag b/src/v2/test/claim/type_param_binder_frame_test.dag index 165cde8cd02..69c9046a5e8 100644 --- a/src/v2/test/claim/type_param_binder_frame_test.dag +++ b/src/v2/test/claim/type_param_binder_frame_test.dag @@ -47,6 +47,7 @@ import v2.std.node { import v2.std.text { String } import v2.std.optional { Absent, Present } import v2.std.type_binder { + type_binder_set_children, OpaqueTypeDecl, TypeAlias, GenericTypeDecl, @@ -264,7 +265,7 @@ fn tpb_generic_arrow(type_params: List, formals: List) -> Node { label: core_edge_label(marker: TypeParamsEdge), target: node_synthetic( kind: TypeNode { connective: Conj }, - children: fold(type_params, init: [], f: fn(acc, p) { concat(acc, [tpb_binder_edge(name: p)]) }) + children: type_binder_set_children(binders: fold(type_params, init: [], f: fn(acc, p) { concat(acc, [tpb_binder_edge(name: p)]) }), source: node_synthetic(kind: TypeNode { connective: Conj }, children: [])) ) }, Edge { label: core_edge_label(marker: ArrowBodyEdge), target: dag_int_literal_fixture_one() } @@ -378,7 +379,7 @@ fn tpb_with_type_param(decl: Node) -> Node { kind: e.target.kind, children: concat(e.target.children, [Edge { label: core_edge_label(marker: TypeParamsEdge), - target: node_synthetic(kind: TypeNode { connective: Conj }, children: [tpb_binder_edge(name: ^T)]) + target: tpb_t_binders() }]) ) }]) @@ -521,7 +522,7 @@ fn tpb_box_disj() -> Node { } fn tpb_t_binders() -> Node { - node_synthetic(kind: TypeNode { connective: Conj }, children: [tpb_binder_edge(name: ^T)]) + node_synthetic(kind: TypeNode { connective: Conj }, children: type_binder_set_children(binders: [tpb_binder_edge(name: ^T)], source: node_synthetic(kind: TypeNode { connective: Conj }, children: []))) } // The declaration target the real lowering writes (v2.std.type_binder type_decl_wrapper) for a @@ -847,3 +848,5 @@ test fn tpb_generic_nullary_coproduct_classifies_as_nullary() -> Bool { count(tpb_generic_member(o: tpb_type_decl_nullary_tag())) == 1 && fold(tpb_generic_member(o: tpb_type_decl_nullary_tag()), init: true, f: fn(acc, m) { acc && tpb_member_is_nullary_enum(m: m) }) } + + diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 377b8aab8fc..907b6f2183d 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -1099,6 +1099,15 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.where_predicate_binding.wpb_resolved_undeclared", "v2.test.claim.where_predicate_binding.wpb_resolved_labelled_then_undeclared", "v2.test.claim.where_predicate_binding.wpb_resolved_labelled_and_marker", + "v2.test.claim.type_application_kind.tak_kind_conforms", + "v2.test.claim.type_application_kind.tak_kind_literal", + "v2.test.claim.type_application_kind.tak_kind_foreign_variant", + "v2.test.claim.type_application_kind.tak_kind_kernel_type", + "v2.test.claim.type_application_kind.tak_unkinded", + "v2.test.claim.type_application_kind.tak_arity_over", + "v2.test.claim.type_application_kind.tak_arity_nongeneric", + "v2.test.claim.type_application_kind.tak_order_authored", + "v2.test.claim.type_application_kind.tak_order_swapped", "v2.test.claim.type_param_binder_frame.tpb_identity", "v2.test.claim.type_param_binder_frame.tpb_colliding", "v2.test.claim.type_param_binder_frame.tpb_used_outside",