1.2.2.1 SameType ( s, t )

The abstract operation SameType takes arguments s (a Type Record) and t (a Type Record) and returns a Boolean. It determines whether s and t denote the same type. It performs the following steps when called:

SameType is MUTUAL SUBTYPING. It is therefore reflexive, symmetric, and transitive wherever IsSubtype is reflexive and transitive, which is to say it is an equivalence relation - and callers that de-duplicate, intern, or otherwise treat it as equality may rely on that.

1.2.2.2 SameTypeWithAssumptions ( s, t, assumptions )

The abstract operation SameTypeWithAssumptions takes arguments s (a Type Record), t (a Type Record), and assumptions (a List of Records that have [[First]] and [[Second]] fields) and returns a Boolean. It determines whether s and t denote the same type, treating each pair in assumptions as already established so that comparison of recursive types terminates. It performs the following steps when called:

1.2.2.3 SameTypeStructural ( s, t )

The abstract operation SameTypeStructural takes arguments s (a Type Record) and t (a Type Record) and returns a Boolean.

It performs the following steps when called:

This is a STRICTER relation than SameType. Two Type Records may denote the same values and still differ in construction - most importantly in the metadata they claim - so an implementation that interns Type Objects must use this relation and not SameType. Interning by SameType merges records whose claims differ, and the claim of whichever record is discarded is lost with it.

1.2.2.4 SameTypeList ( a, b, assumptions )

The abstract operation SameTypeList takes arguments a (a List of Type Records), b (a List of Type Records), and assumptions (a List of Records that have [[First]] and [[Second]] fields) and returns a Boolean. It determines whether a and b have the same length and are position-wise the same type under assumptions. It performs the following steps when called:

1.2.2.5 SameArgumentList ( a, b, assumptions )

The abstract operation SameArgumentList takes arguments a (a List), b (a List), and assumptions (a List of Records that have [[First]] and [[Second]] fields) and returns a Boolean. It determines whether a and b have the same length and equal elements, comparing Type Record elements as types under assumptions, Parse Node elements by being the same Parse Node, compound compile-time constants by structural equivalence (1.2.7.2), and other elements with SameValue. It performs the following steps when called:

1.2.2.6 AreDisjoint ( s, t [ , active ] )

The abstract operation AreDisjoint takes arguments s (a Type Record) and t (a Type Record) and optional argument active (a List of Records) and returns a Boolean. It determines whether no value is of both s and t. It performs the following steps when called:

1.2.2.7 CompositeShapesAreDisjoint ( s, t, active )

The abstract operation CompositeShapesAreDisjoint takes arguments s (a Type Record), t (a Type Record), and active (a List of Records) and returns a Boolean. It proves selected contradictions between two composite shapes without evaluating values or treating a membership contract as a construction schema. An unresolved case returns false. It performs the following steps when called:

Record membership permits extra keys by width subtyping. Two conflicting optional properties can both be absent; if either is required, their common value must satisfy both property contracts. Likewise, only tuple positions required at every common admitted length can prove an element conflict. Two array composite shapes can share the empty tuple even when their element types are disjoint; an array shape denotes the variable-length tuple composite. A declared tuple default establishes possible omission without evaluating its initializer. Rest-containing tuple shapes, index-signature interactions and other unresolved shape constraints retain a conservative result unless the kind distinction already proves failure. Repeating an active Type Record pair supplies no proof of disjointness; other independently established conflicts are still checked.

1.2.2.8 CanonicalizeType ( t )

The abstract operation CanonicalizeType takes argument t (a Type Record) and returns a Type Record. It returns the canonical form of t, reading no [[Origin]] (23) in deciding it. Canonical Type Records that denote the same type are the same Record, which is what lets 1.2.2.9 intern them. It performs the following steps when called:

1.2.2.9 GetTypeObject ( t )

The abstract operation GetTypeObject takes argument t (a Type Record) and returns a Type Object. It returns the unique Type Object that denotes the type described by t. It performs the following steps when called:

1.2.3.1 IsSubtype ( s, t, assumptions )

The abstract operation IsSubtype takes arguments s (a Type Record), t (a Type Record), and assumptions (a List of Records that have [[First]] and [[Second]] fields) and returns a Boolean. It determines whether every value of the type s is a value of the type t, treating each pair in assumptions as already established so that comparison of recursive types terminates. The initial call passes an empty List for assumptions. It performs the following steps when called:

Three of the steps above are one relation. A type refines another when it is a parameterized type whose [[Base]] is that type (1.5.20), an enum whose underlying type is that type (1.11.8), or a nominal type whose declaration extends or implements that type's declaration. A type is a subtype of every type it refines and of everything that type is a subtype of; the converse never holds without a crossing, a construction boundary for a parameterization, a validated call for an enum, and nothing at all for a class. The three steps are that rule's cases.

1.2.3.2 IsAssignable ( s, t )

The abstract operation IsAssignable takes arguments s (a Type Record) and t (a Type Record) and returns a Boolean. It determines whether a value of the type s may be assigned where the type t is expected. This is the relation checked at bindings, arguments, and returns. It performs the following steps when called:

1.2.7.1 IsCompileTimeEvaluable ( expr )

The abstract operation IsCompileTimeEvaluable takes argument expr (a Parse Node) and returns a Boolean. It determines whether expr can be evaluated during type checking, reading only values known at that time. It performs the following steps when called:

A compile-time-evaluable function is one whose body reads only its parameters, its own local bindings, immutable bindings whose initializers are compile-time evaluable, and other compile-time-evaluable functions. It may create local state and mutate it. Its body contains no await, no yield, no direct or indirect eval, no use of the Function constructor, and no construction of a Proxy; regular expressions are within the fragment. It performs no input or output and reads no ambient mutable state, none of which it can name under the reading rule above, which is why the discipline is a property of what the code can name rather than a wall around what it does.

A function declaration creates a mutable binding, yet it is the callee this operation exists to admit: the callee of a builder call resolves to a function declaration. Its binding is therefore treated as immutable here where the source text contains no assignment to it and no direct eval. A function the program reassigns is not the function the checker would read, so a call through its name is not evaluable, and a let or var binding is not immutable whether or not the program writes to it.

An import's local immutability does not make the exported binding immutable. This judgment follows the resolved export, including re-exports; a read of an exported let or var remains a read of mutable state. A module namespace member that resolves to an exported binding is subject to the same judgment. The declarations and initializers consulted by this judgment retain their original lexical scopes. In particular, free references in a builder and in its helper functions resolve in the environments of those functions, not in the importing source text or a temporary environment reconstructed from their signatures. A known Static Type is not the value of a binding: a function signature must not stand in for the function, nor may a namespace's structural type stand in for the namespace value. These rules neither initialize an unavailable binding nor execute a dependency body; availability and failure timing remain those of 1.3.8.

1.2.7.2 Deferred Applications

A call whose arguments involve an unbound generic parameter cannot evaluate yet, and is carried as a type: the deferred Type Record of Table 1. The deferred application Type Record of a ComputedType is the deferred Type Record whose [[Operator]] is the function its callee resolves to and whose [[Operands]] holds, for each argument in order, an element that is: the TypeParameter Parse Node where the argument is a reference to an unbound generic parameter; the deferred Type Record where the argument is itself a ComputedType reading one; and otherwise the argument's compile-time value, a Type Object contributing its [[TypeRecord]].

Identity is by that key. SameTypeWithAssumptions compares two deferred Records by operator identity and SameArgumentList, and Type Objects are interned, so two mentions of partial(T) in one generic body are one Type Object before anything is known about T. At specialization, each TypeParameter Parse Node among the [[Operands]] is replaced by the parameter's binding, and the application evaluates by 1.2.7.3.

Two compound compile-time constants, arrays or plain objects of compile-time constants, are structurally equivalent when they have the same shape and their leaves are pairwise SameValue, a Type Object comparing by identity and a RegExp by its source and flags. A compound constant argument contributes to an application's identity by structural equivalence rather than by reference, so pick(User, ['id', 'name']) written twice is one application although the array is a fresh object at each occurrence.

1.2.7.3 EvaluateBuilderCall ( f, args )

The abstract operation EvaluateBuilderCall takes arguments f (a compile-time-evaluable function) and args (a List) and returns either a normal completion containing a Type Object or a throw completion. It evaluates one type-level call, with memoization and a fixpoint for recursion, and checks the contracts of 16 against its result. It performs the following steps when called:

The evaluation memo is a specification-level map from canonical deferred Type Records to successful results, retaining both their Type Objects and their type-result contexts (1.6.5), and the in-flight List tracks the keys under evaluation. Each distinct key evaluates once per program; every later occurrence, in any module, yields the same interned Type Object and selected context. Reuse requires the same determining declaration and captured inputs; equal result Type Objects alone do not identify a reusable context. An implementation may realize both devices in any way that yields these results. An in-flight placeholder supplies no completed context. When fixpoint completion resolves placeholder edges in the result, resolve corresponding edges in its retained context consistently, preserving its binder declarations and captured inputs; no incomplete context is published on failure.

Evaluation of the body of f uses f's ordinary function environment and the applicable parameter binding, generic specialization, receiver and return contracts. Permission to evaluate a function during checking does not remove any of these contracts. An imported name that denotes f denotes that same function for this operation; importing it does not instantiate a new function in the importer's environment. A failed contract or a result that is not a Type Object fails the containing type computation under 1.2.8. Reuse of a memoized result must preserve these requirements and the accounting rules of 1.2.7.5.

1.2.7.4 The Evaluation Budget

Evaluation under this clause is metered by two host-defined limits: a count of evaluation steps and a count of type-construction requests, each per top-level type-position evaluation. Every operation that evaluates a type is metered, the instantiation of a generic type alias among them, since an unmetered one is a way to recurse without spending the budget; so is BindTypeArguments (4.3), and with it the specialization of a declaration over a variadic parameter, since a declaration applying itself to a pack one element longer is the recursion a type alias performs with one more field. For a given source text, two hosts either produce, position for position, the same interned types, or at least one reports a type error: the limits decide whether compilation fails, never what it produces.

The budget bounds a computation, which either completes or is abandoned and reported. A rule requiring a SEARCH — over the types an argument could take, rather than over a fixed evaluation — is not metered by it and is refused where it would otherwise arise (4.13), because truncating a search under a budget yields a wrong answer where truncating a computation yields none.

A limit must be one the implementation can actually reach. An implementation whose own resources — a native stack, a heap — are exhausted before the limit is has not met this clause, whatever the limit's value: the evaluation ends in a way no program can observe and no diagnostic names, which is the outcome this clause exists to prevent. Where an implementation cannot raise its own capacity, it lowers the limit instead. A limit above what an implementation can reach is not a limit.

Exhaustion is not an abrupt completion the evaluated code can observe. No try statement within the evaluation handles it; the evaluation is abandoned, and EvaluateToTypeObject of the containing type-position expression returns a normal completion containing empty, with a diagnostic naming the outermost call and the deepest frames. The containing source check reports a StaticTypeError for evaluation-limit exhaustion. An incidental hook exception or lack of a result after exhaustion does not instead establish an ordinary type mismatch, select an overload fallback, or supply an unknown type.

1.2.7.5 Type Evaluation Accounting Boundaries

The type computation includes propagating retained specialization obligations through declarations: substituting the determining bindings, admitting arguments, and retaining the constraints, predicates, defaults and consumer contracts that an expanded result may erase. These operations are metered when performed during static checking as well as during pre-evaluation; the absence of a builder invocation or a Type Object allocation does not exempt them. Nested propagation shares the enclosing computation's resource state, and an implementation that meters nesting accounts for these logical dependencies even when it processes them with a worklist. This accounting does not require evaluating a default or other expression whose evaluation is deferred by an existing generic rule.

A repeated active obligation with the same declaration-bound inputs may stop propagation of that same obligation. It supplies no completed type, admission proof or waiver of independent obligations. Repeating a declaration with different determining inputs is not the same obligation. If propagation exhausts its allowance, the containing source check reports evaluation-limit exhaustion in the phase that performed the work and publishes no successful checking result. Discard unfinished propagation state on every exit; a later independent check starts without that state. This failure is distinct from return-inference exhaustion and from a proved invalid recursive type.

A type computation includes the complete evaluation it invokes: builder and declared inverse bodies, their callbacks, generic arguments and defaults, object member and tuple element defaults, array extents, refinement predicates, and metadata hooks. Charging only the entry to a user function does not bound that computation. Nested evaluation shares the enclosing computation's resource state and cannot reset its remaining allowance. When an implementation imposes the nesting limit of 1.2.7.4, that limit includes ordinary ECMAScript function-body invocations made during the computation, including mutual recursion and calls through callbacks; tail-call optimization does not remove a logical invocation from this accounting. Suspension retains that state; evaluation by another agent has a distinct state. Evaluating ordinary program code outside such a computation does not consume its allowance.

A type-construction request is an invocation of GetTypeObject while type evaluation is active. Charge one request on entry, before canonicalization, lookup, or allocation, whether the result is already interned or requires a new Type Object. Reading an existing Type Object without invoking this operation is not a construction request. Physical allocation, garbage collection, interning order, and a previously populated intern table do not determine this charge. A tuple candidate enumerated by trial specialization consumes the additional request specified in 17.2, even if that candidate has no materialized Type Object.

Each counter begins at zero. A request whose charge is no greater than the remaining allowance succeeds and reduces that allowance by its charge; a larger request marks the computation exhausted before the requested evaluation proceeds. Exactly consuming the allowance is permitted. Exhaustion is sticky until the outermost computation ends: unwinding a nested call, handling an incidental exception, or returning a fallback does not clear it. A result obtained after exhaustion must not be published as a successful specialization, inverse proposal, resolved type, or successful evaluation-memo entry.

The enclosing checking boundary tests exhaustion before interpreting the computation's result. Exhaustion takes precedence over an incidental hook exception, an absent result, an assignability mismatch, or a candidate-selection failure produced while abandoning that computation. The diagnostic identifies evaluation-limit exhaustion as specified in 1.2.7.4. An implementation failure of its own stack or heap is not evidence that a language type is invalid and must not be translated into an ordinary type-mismatch proof.

1.2.7.6 EvaluateToTypeObject ( expr )

The abstract operation EvaluateToTypeObject takes argument expr (a Parse Node) and returns a normal completion containing either a Type Object or empty. It evaluates expr, which appears in type position, to the Type Object it denotes, or defers it, or returns empty if it does not evaluate to one. It performs the following steps when called:

A successful result retains its type-result context as auxiliary checking evidence for this evaluation occurrence, not as a property of its Type Object or shared source node. An unavailable generic input supplies only the deferred type until its ordinary binding point; failure supplies no context. These requirements do not change the Type Object denoted by the expression.

It is a type error if an expression appears in type position and the value in the normal completion returned by EvaluateToTypeObject is empty (1.2.8). When the empty arises from an abrupt completion whose value is an Error, the type error's diagnostic carries that Error's message, prefixed by the source text of the type-position expression; when it arises from the budget, the diagnostic is the one 1.2.7.4 describes. Diagnostic content is not observable to the evaluated program.

1.2.8.1 Source-Position Class Constructor Evidence

A source class declaration's type denotation and the current constructor value of an ordinary expression are distinct, as specified in 4.8.1. When a checking judgment uses a constructor value's origin, determine the evidence at that expression's evaluation position. A write after a heritage read does not retarget the superclass already selected, and a write during argument evaluation does not replace the constructor or callee already obtained. These rules describe checking evidence; ordinary Evaluation still obtains and uses the actual values once, in its specified order.

The prescribed transparent cases are class creation, initialized unannotated lexical constructor aliases, parentheses, direct identifier assignment, comma evaluation, and conditional or short-circuit selection. Track lexical binding identity, including ordinary shadows and the class's separate inner self binding. An established initialization or assignment transfers its constructor origin to subsequent reads of that binding; a later assignment withdraws or replaces that evidence for subsequent reads only. Preserve any established generic application and its original argument/declaration context. A mutable alias can therefore supply an origin at a particular read without becoming immutable or becoming valid in a type position. An explicit erased or reference view does not acquire a constructor-origin proof by this rule.

For a condition established by the prescribed rules, transfer effects only along the selected evaluation edge. At an unresolved join, retain an origin only if every normally completing incoming edge establishes that same origin. Retain the value captured by an earlier component independently of subsequent state. Check required source forms on skipped or non-completing paths under their existing rules; this is not permission to execute them or to transfer their effects onto another path.

A pattern or iteration write withdraws the origin of each destination binding unless its replacement origin is independently established. A write to a different shadowing binding does not withdraw an outer binding's fact. Account for a loop's possible previous iterations before using a value-origin fact in its body; widen the bindings and dependencies its repeated operations may affect. A catch can observe effects performed before an abrupt completion, and a finally clause retains its ordinary completion ordering. Where a construct has no prescribed transfer establishing an origin, leave that origin unresolved rather than using a syntactic declaration as a substitute.

Potential calls, getters, setters, conversions, iterators, decorator applications and suspension withdraw mutable evidence they may affect. This includes reachable Script-global bindings, imported producer dependencies and bindings writable through captured code or exposed references. Preserve independent immutable captures and local cells that the operation cannot reach. A potentially direct eval additionally affects its visible mutable bindings; in non-strict code, account for declaration injection that can change lookup of an outer name. A bound name spelled eval may still invoke the intrinsic direct eval. Indirect eval and dynamically constructed functions have their ordinary global environment; their spelling alone neither proves purity nor gives them access to an unexposed local cell. Do not parse or execute eval text during this judgment.

Defining a callable does not invoke its body or parameter defaults. Analyze its possible invocation with only the captured facts that remain valid at that entry; perform its default-initializer effects before its body facts. A class evaluates heritage before computed names and static initialization, and its instance initializers and methods run in their separate invocation contexts. A generic application can initialize a specialization, so its permitted effects precede later ordinary reads. Ordinary class decoration retains the exact or bounded replacement-origin rules of 1.11.2, including on exports.

A mutable Script-global constructor read in a deferred body does not capture the constructor present when that body was defined. For established ordinary invocation sites in the checked source, retain a constructor candidate only when the prescribed effect analysis establishes that binding's stability at the actual read, including argument evaluation, parameter defaults and possible repeated activations. This evidence applies to those invocation contexts; it is not a guarantee about future callers. With no established invocation context, the absence of a write in the current source is insufficient: a later Script can replace the global constructor before the body's first invocation. An independent immutable value capture and a class's inner self binding retain their separate origin rules. A property of the global object is not the same binding as a same-spelled Script-global lexical declaration.

Calling a generator creates an iterator and does not establish when its body reads a mutable global constructor. Do not project such a read, or a helper invocation reached from that body, to iterator creation as evidence of binding stability. A suspension retains its effect boundary even when the initial invocation site is known. Unknown invocation or resumption contexts and exhausted evidence withdraw the conditional origin; they do not freeze a global binding or change the constructor denoted by an ordinary expression.

An established violation follows the existing type-error boundary, including a receiving, inherited-member or constructor-signature violation now established through a source-position alias. Unknown effects or ancestry retain runtime admission under 1.2.8.2. This analysis supplies no independent permission to elide checking, to replay an operand after guard failure, or to alter prototype obligations, conversion ordering, storage identity or reference liveness. Optional deeper analysis must not introduce additional mandatory Early Errors or move an inner dynamic-source error before its evaluation.

class Original {}
class Other {}
let Selected = Original;
Selected = Other;
const value: Original = new Selected(); // established mismatch: Early Error

1.2.8.2 Incomplete Nominal Ancestry at Receiving Boundaries

At a binding initialization, assignment, argument or return boundary receiving a source-class nominal type, distinguish an established end of the source's superclass chain from an unavailable superclass origin. A class with no heritage, or with an established null heritage, ends that chain. An unresolved heritage expression does not. Failure to find the target along a chain whose relevant ancestry is unavailable does not establish a type error.

This is a rule about the evidence supporting a receiving judgment, not a change to SameType, IsSubtype or IsAssignable. Retain the source and target contracts, known own member contracts and established declaration identities. Do not replace them with any. A known incompatible argument or identity of an already established application of the target declaration remains incompatible; unavailable ancestry cannot erase that fact. Nor does it erase an independent primitive-category, storage or type-formation error. The existing rules for conversions still apply.

For this judgment, consider source union members independently: a member established to be incompatible still requires the existing type error, while unavailable ancestry in another member supplies no positive proof. A target union admits an established compatible alternative; where none is established compatible but one remains possible because of unavailable ancestry, retain the runtime boundary. A target intersection requires every conjunct; an established incompatible conjunct is not repaired by an unresolved one.

Where ancestry alone prevents resolving the receiving judgment, perform the original evaluation and apply the existing runtime admission to its actual result. Do not select an implicit conversion on the premise that unavailable ancestry proves nominal incompatibility. Preserve lookup, callee capture, argument and constructor effects, their order, and abrupt completions. Do not execute a constructor, getter, initializer or eval source during checking to recover this evidence. Type computations explicitly permitted by 1.2.7 retain their own rules.

Unavailable ancestry never licenses check elision, overload selection or a positive subtype proof. Successful runtime admission retains the ordinary nominal prototype obligations of 1.7.7.2 and all existing storage and reference-liveness checks. A failed admission occurs at the receiving boundary, after the effects that ordinary evaluation has already performed. This clause does not change which declaration a type name denotes.

class V {}
class W extends V {}
const value: V = new W();
eval("1");

1.2.8.3 Proved Library Operations

A proved Map.groupBy result retains the established callback key contract and the source iteration contribution as the element contract of each fresh group array. A proved Object.groupBy result retains the same group contract and the callback result after ToPropertyKey: Symbol keys remain Symbols, while established non-Symbol primitive keys become Strings. These are facts about fresh results, not invariant type stamps placed on ordinary collections. Check a receiving annotation using its normal adoption and conversion rules. No non-empty group is inferred from an empty or unknown source, and unknown callback, key-conversion or iteration effects retain the runtime boundary.

At proved intrinsic String.prototype.replace and replaceAll operations, a callable replacement is checked against each established invocation's actual argument list and undefined receiver. A string search supplies the matched String, its numeric offset and the entire input String; a RegExp or another replacement protocol may supply a different list and requires its own proof. Use ordinary parameter conversion, omission, defaults and rest binding. A proved absence of matches establishes no callback invocation. A custom @@replace method, a replacement method or unknown lookup effects do not inherit the intrinsic contract.

At an established implicit ToString stage of a proved library operation, a participating operand necessarily containing only Symbols is a type error. At an established implicit ToNumber stage of a proved library operation, a participating operand necessarily containing only Symbols, or only BigInts, is likewise a type error: the Math functions and Number convert their arguments with ToNumber, which throws for both, so a Symbol or BigInt given to Math.max fails as surely as one given to parseInt. This includes a string search operand of String.prototype.includes and an Array.prototype.join separator when their preceding stages are established. The examples are not a list: an operation is proved by its origin, so every proved intrinsic that converts an operand with ToString has the stage, among them the search operands of startsWith, endsWith, indexOf, lastIndexOf and localeCompare, each argument of String.prototype.concat, the filler of padStart and padEnd where the target length exceeds the receiver's, and the first argument of parseInt, parseFloat and the URI functions. Array.prototype.join and toString also convert each element after the separator; that stage is established where the receiver's type fixes a length of at least one, as a tuple or an array of fixed extent does, and not for an array that may be empty. Do not replace ToString with a String-only parameter requirement: numeric and other ordinarily convertible primitives remain admitted. The explicit String function's Symbol conversion is unchanged. A proved Object.is is a test whose answer the types may already know: it is a type error where a participating operand's type cannot hold the other operand's value, as a search with a needle its element type cannot hold is (1.14.10, 1.15.4.1). A proved Array.isArray declares a narrowing of its argument (8.2) to the ~array~ and ~tuple~ members of its type, whose every value is an Array and stays one, and away from its primitive members, none of which is one; a proved Number static declares a narrowing to the Number-valued members, answering false for any other value as its existing signature does. Classify the established argument-domain members independently by each proved intrinsic predicate's answer: a true member survives only on the true edge, a false member only on the false edge, and an unknown member on both. In particular, a Number-valued floating domain may still answer false to Number.isInteger. Publish an argument fact only to its preserved captured origin; lexical shadowing or replacement of the intrinsic defeats its origin proof. A test of either is therefore judged by 1.8.5.4. A proved Object.is supplies only SameValue-compatible branch evidence under 1.8.5.1. It is not rewritten as strict equality: zero signs and decimal cohort identity retain their distinct semantics. Unknown earlier protocol effects retain runtime checks.

At a proved typed array or window set operation, read the source as an array-like object, not as an iterable. Establish its length, the converted offset, the destination bounds and the reached indexed reads before checking a copied value against the corresponding destination storage type. An incompatible established store is a type error under the same rules as a direct typed store. An empty copy creates no element obligation; an earlier range failure does not establish a store. Overlap, conversion order, source getters, range errors and reference liveness retain their runtime semantics.

At proved Object.create or Object.setPrototypeOf, a participating prototype argument necessarily outside Object or null is a type error. Preserve Object.setPrototypeOf's preceding RequireObjectCoercible stage and its ordinary handling of non-nullish primitive targets. This is a prototype-argument judgment, not structural adoption or a requirement that the target itself be an Object.

A proved synchronous Array.from result carries the element contract established by the same operation, source and callback proof used for its input checks. With a supplied mapper, use its established result contract; with an omitted or undefined mapper, use the source's established iteration contribution. Check a receiving type against that result at the ordinary conversion boundary. Do not infer elements from mutable indexed storage, infer an incompatible element from an empty source, or turn initial result length into fixed storage extent. An unknown callback result or lost intrinsic proof retains the runtime boundary. This rule introduces no synchronous result contract for Array.fromAsync.

At a proved intrinsic Reflect.apply, check the selected target's callability, the supplied receiver and the forwarded argument list at its ordinary callable contract. Build the list using the operation's array-like positional reads, not iteration; establish the relevant count, entries and effects. Preserve ordinary overload selection, defaults, rest binding and conversions. Reference Values decay under the built-in rule; forwarding does not manufacture references for reference parameters.

At a proved intrinsic Reflect.construct, check the construction capabilities of the target and of an explicitly supplied newTarget independently. Check the established array-like argument list against the target's construct signatures, not newTarget's parameters. Preserve overload selection and ordinary binding. The restriction on directly instantiating an abstract class is not a prohibition on its use as a constructible newTarget or base. A different newTarget does not establish that the result has the target's ordinary instance type. Unknown capabilities, argument reads, specializations or effects remain dynamic. These judgments allocate no instance and change no reference-liveness rule.

A proved selected function contributes its declared generic capability independently of its result signature. Applying explicit type arguments to a function declared nongeneric, such as the original Object.keys, is a type error. Generic statics such as Object.values, Object.entries, Array.from and Array.of retain their declared parameters. A mutable property's spelling does not establish this capability; aliases require the same origin and effect proof.

At a proved intrinsic Promise.all, Promise.race, Promise.any or Promise.allSettled, it is a type error when a participating input's established type cannot satisfy the synchronous iteration protocol the operation requires. Ordinary iterable values are admitted; elements need not themselves be Promises. Preserve every viable or unknown alternative. Where no early proof applies, the original rejection and completion behaviour remains in force.

At proved Array.from, Array.fromAsync, Object.groupBy and Map.groupBy calls, check the supplied callback's callability and each established invocation against its ordinary value-parameter and receiver boundaries, including omission, defaults, rest binding and permitted conversions. An omitted or undefined Array mapper selects identity mapping; a grouping callback is required. A known empty source does not establish an invocation with an incompatible element, although the operation still checks callability. Use the selected operation's own await stages: Array.fromAsync awaits the values it supplies to the mapper and its mapped results. Do not infer iteration from mutable indexed storage. Immutable tuple Composites can establish ordered positions; unknown iteration or callback alternatives retain runtime checks.

The judgments in this clause require establishing the actual selected intrinsic or descriptor and the relevant argument, receiver and storage facts. A spelling or nominal receiver type is insufficient. Account for prior source texts, lexical shadows, own properties, prototype changes, argument evaluation, implicit conversions and other effects that could invalidate a dependency, including concurrent interference where possible. An annotation's boundary is such an effect only where it can run user code for the value that reaches it: checking a construction of the annotated class, a keyed collection constructed empty against type arguments whose checks run no user code, or a literal of plain scalar data against an object type whose members' checks run none, runs no user code. A construction is such an effect unless it runs no user code, as for an intrinsic Map or Set constructed without arguments, or a class of the source text with no heritage, decorators, type parameters or constructor, whose instance fields take scalar initializers or primitive defaults, constructed with scalar arguments. A runtime identity guard cannot justify an Early Error. Unknown dependencies retain runtime checks; checking invokes no ordinary getter, setter, conversion, callback or thread body. Permitted compile-time type evaluation remains governed by its existing rules.

It is a type error to perform an established write to an accessor with no setter, such as the original typed-array capacity or collection size accessor. A fresh receiver with established descriptors may justify the proof; a receiver type alone does not exclude a writable own shadow or a replacement setter. Compound assignments and updates use the same judgment. A logical assignment whose store is skipped performs no write and is not rejected by this rule. Capacity reservation, storage relocation and reference liveness are unchanged.

At a proved intrinsic Function.prototype.call or apply, check the forwarded arguments and receiver at the selected target's ordinary callable contract. apply uses array-like positional reads, not iteration; count, entries and their effects must be established independently. At a proved bind, check the fixed prefix and receiver, without demanding the arguments left for the eventual call, and retain a residual signature only where the remaining mapping is established. Reference Values decay on entry to these built-ins as specified by 2.3; forwarding does not recreate references. Overload and generic argument binding retain their ordinary rules.

At a proved typed Atomics operation, it is a type error if the known target category cannot satisfy 43.6's operation-specific restriction, or an established operand boundary necessarily fails its prescribed conversion. Integer-only operations remain distinct from operations admitting floating-point targets; shared is not an eligibility requirement. The first reference argument retains the Atomics exception to built-in decay. A conditional replacement conversion, such as the replacement of compareExchange, is not established solely by the presence of its argument; a possibly skipped conversion prevents that failure proof. No memory-order, blocking or liveness rule is changed.

At a proved callThread, apply 43.3.2 to established facts, then check the forwarded inputs at the target's callable contract. A non-Object first argument is not an options bag. A first parameter admitting an Object takes precedence over bag classification. If several classifications remain possible, reject only when every relevant mapping fails; otherwise retain the runtime classification. Built-in reference decay remains in force. This judgment launches no work and changes neither Promise settlement nor cancellation.

At a proved Object.assign, Reflect.set, Object.defineProperty, Reflect.defineProperty or Object.defineProperties, an established write to typed own data obeys the ordinary storage boundary. It is a type error when that write necessarily fails. The proof must establish ownness, enumerability, keys, descriptors and the actual receiver as needed by the selected helper. For example, the original Object.assign({ (x: uint8): 0 }, { x: "s" }) has a statically incompatible write. A later source cannot erase an earlier failed write, while duplicate definitions within one source obey ordinary final-property semantics. Structural membership alone does not enumerate copied properties, and a distinct Reflect.set receiver is not assumed to be the target. Unknown getters, proxies, descriptors and explicit any remain dynamic. Reflection gains no ability to replace protected typed storage or extend a reference's lifetime.

Descriptor adapters preserve the selected operation's staging. Reflect.defineProperty does not bypass a typed storage conversion because it returns a Boolean. Object.defineProperties collects and validates the complete descriptor list before applying any definition; a malformed later descriptor or an unknown descriptor getter prevents a proof that an earlier store is reached. Final duplicate-property semantics and each applied definition's order remain unchanged.