Vocabulary concepts and the generic type metatype

When a vocabulary metatype is in scope, its name introduces a concept:

// A declaration is terminated by exactly ONE of: its `{ }` body, its `{ }`
// cover, or — when it has NEITHER — a REQUIRED ';' (the same item-termination
// rule as Rust: `struct Foo;` vs `struct Foo { … }`). A missing terminator on
// the bodyless form is `OE0011 MissingTerminator`.
concept-decl    ::= attribute* 'pub'? <metatype-name> Ident generic-params?
                     supertype? refinement-clause? ( cover | body | ';' )
supertype       ::= specialization? instantiation?
specialization  ::= '<:' TypeExpr (',' TypeExpr)*
instantiation   ::= ':' TypeExpr (',' TypeExpr)*
cover           ::= '{' variant (',' variant)* ','? '}' // bare-ident members; self-terminating
body            ::= '{' (field-decl | instance-value) (',' …)* ','? '}'   // self-terminating — no ';'
instance-value  ::= Ident '=' expr                     // see body modes below

A cover and a field/instance body share the { … } surface; the member shape distinguishes them. A cover’s members are bare concept names (a brace whose first entry is an Ident followed by , or }), matching enum’s { Circle, Square } and the complete Parent { A, B } group axiom; a body’s first entry carries a : (a field name: Type), :: (a per-target axis override), or = (an instance-value).

The leading identifier (type, or a vocabulary name like kind, subkind, role, phase, category, …) is contextually a concept-introducing keyword — resolved per Name resolution against the pub metatype declarations visible in scope: declared in this package, or imported from a vocabulary package. type is not ambient — it is the std::core baseline, brought into scope by use std::core::{type} or a [package].prelude entry (RFD 0038). An introducer that resolves to no visible pub metatype is refused with OE0605 UnknownMetatype at ox check and ox build.

use std::core::{type};   // the no-commitment baseline, brought into scope (RFD 0038)
pub type Document { title: String, body: String }

// Vocabulary-classified concepts: the vocabulary must be IN SCOPE.
// Here it is declared in-package (the external-vocabulary-package
// pattern — a real UFO package would ship these declarations and be
// imported instead; nothing UFO-related ships with Argon):
pub metatype kind = { };
pub metatype subkind = { };
pub metatype category = { };

pub kind Person { name: String, age: Nat }
pub subkind Adult <: Person iff { self.age >= 18 };   // defined class: auto-classified (Refinement)
pub category Animal;

// Concept with a cover — the fields attach to each variant via subkind hierarchy.
pub kind Vehicle { Car, Truck, Motorcycle }
pub subkind Car         <: Vehicle { license_plate: String }
pub subkind Truck       <: Vehicle { license_plate: String, cargo_kg: Nat }
pub subkind Motorcycle  <: Vehicle { license_plate: String, weight: Real }

Supertype clauses. <: T declares specialization (intra-classification subtyping): Adult <: Person says every adult is a person. : T declares iof-instantiation: pub kind USD : Currency says USD is an instance of the higher-order type Currency. Both clauses are general substrate features — neither commits to any specific higher-order theory. Higher-order theories like MLT (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) interpret the order arithmetic over :; the substrate itself only enforces that iof is well-founded and acyclic.

Multiple parents on either axis. Both clauses admit a comma-separated list, and both can co-occur on a single declaration:

pub subkind Penguin
    <: FlyingAnimal, AquaticAnimal              // specializes two kinds at order n
    :  Vertebrate_Species, Endangered_Species   // instance of two categories at order n+1
{
    name: String,
    body_plan   = "tetrapod",
    iucn_status = IucnStatus::Vulnerable,
}

When both clauses are present the canonical order is <: then :, mirroring the order arithmetic (specialization parents at the concept’s own order, instantiation parents one above). The order is a style convention, not a rule: both clauses are independent (parents are an unordered set on each axis), so either source order parses and means the same thing — writing : before <: is accepted with the OW0010 style warning (never an error), and oxfmt normalizes it to the canonical order. All parents in a single <: clause must be at the same order; all parents in a single : clause must be at one order above. Unprivileged theory packages (e.g. mlt) enforce additional cross-parent constraints over the iof DAG.

Diamond resolution. When multiple parents (on either axis) declare a field with the same name, the elaborator rejects the declaration with OE0208 AmbiguousFieldFromMultipleParents. The modeler resolves the ambiguity by qualifying the field with its parent:

pub category Vertebrate_Species { habitat: String }
pub category Endangered_Species { habitat: HabitatProtectionZone }

pub subkind Penguin : Vertebrate_Species, Endangered_Species {
    Vertebrate_Species::habitat = "Antarctic coast",
    Endangered_Species::habitat = HabitatProtectionZone::IUCN_II,
}

Field access from instances follows the same qualification when ambiguous: bar.habitat is rejected with OE0208; the modeler writes bar.Vertebrate_Species::habitat to disambiguate. The substrate offers no automatic merge, override-by-position, or last-wins behavior — every collision is resolved explicitly. (This is consistent with how Argon’s trait system handles method-name collisions; see Trait atom.)

Body modes when : T is present. When a concept is declared as an iof-instance of another (pub kind USD : Currency { … }), the body admits two statement kinds:

• field = value — sets the value of a field defined on the target T. This is the kind-as-instance facet: USD is filling in fields that Currency declared on its instances.
• field: Type — declares an instance-level field that the kind itself will carry forward to its own instances. This is the kind-as-kind facet: every USD bill will have its own serial_number.

pub category Currency {
    #[intrinsic] iso_code: String,
    #[intrinsic] decimal_places: Nat,
    symbol: String,
}

pub kind USD : Currency {
    iso_code       = "USD",        // value for the Currency-defined field
    decimal_places = 2,
    symbol         = "$",

    serial_number: String,         // instance-level field on bills
    denomination:  Nat,
}

let my_twenty = USD { serial_number: "L12345678A", denomination: 20 };

#[intrinsic] on a field declares it must be set at kind level by every iof-instance. Cross-level binding diagnostics: OE1901 InstantiationFieldNotInTarget (a = binding names a field absent from the target metatype), OE1902 InstantiationFieldShadows (a : field shadows an inherited one), OE1908 IntrinsicPropertyMissing (a required #[intrinsic] field is left unbound), and OE0208 AmbiguousFieldFromMultipleParents (a field declared by multiple parents, unqualified). Theory-specific cross-level constraints (e.g., MLT’s categorization / partition / subordination / powertype rules) are not compiler diagnostics: a higher-order theory ships as an unprivileged package (e.g. mlt, Higher-order modeling) and authors those constraints as its own rules/checks over the neutral substrate; see appendix C.

Field access through the iof chain. For an instance bar: SomeKind where SomeKind : SomeCat and SomeCat declares field x, the access bar.x is resolved by walking up the iof chain:

1. Instance fields first. If bar has x declared as an instance-level field (via x: Type in SomeKind’s body), return bar’s own value.
2. Kind-level values next. Otherwise, look at meta(bar) = SomeKind. If SomeKind set x = value at its kind level, return that value.
3. Walk further up. If SomeKind itself does not bind x, continue: meta(meta(bar)), etc., until either x is found or the chain bottoms out at an entity with no further : parent.
4. Not found. Error: OE0101 UnresolvedName (or a more specific field-not-found variant).

Three equivalent surface forms reach the same value when x lives at the kind level:

Shadowing across levels. If x is bound at both an instance level and a higher kind level — different types, or the same type with different values — the elaborator rejects the declaration with OE1902 InstantiationFieldShadows. Modelers either rename, or accept the shadow explicitly by writing meta(bar).x / SomeKind.x when they need the kind-level value. There is no implicit override.