Elaboration and Unification

Definition 112.2 — The surface fragment T_ elab¶

The surface fragment $T_{\mathsf{elab}}$ has variables and declared constants; explicit and implicit $\mathrm{\Pi }$-binders, abstractions, and applications; $\mathrm{\Sigma }$-types, pairs, and projections; the nullary and constructor forms of $\mathbf{1}$, $\mathbf{2}$, $\mathbb{N}$, identity, and $\mathsf{Vec}$; strict universe expressions ${\mathcal{U}}_{\ell }$; their motive-annotated eliminators; annotations $(e:A)$; and holes written $\mathrm{\_}$. A fully explicit core term may occur as an annotated atom. Thus every Timpl former is available, while the only information the elaborator reconstructs is:

1. implicit term arguments declared by an implicit $\mathrm{\Pi }$-binder;

2. external universe levels;

3. the type and term demanded by a hole; and

4. annotations forced by an expected type.

A surface $\mathrm{\Pi }$-binder and abstraction record explicitness and relevance. Written application syntax records explicitness; its relevance is copied from the exposed $\mathrm{\Pi }$-head. The $\mathrm{\Sigma }$-binder carries neither bit. Surface recursive clauses are absent from $T_{\mathsf{elab}}$.

Here is the grammar used below. A hatted level or argument may be omitted; $\mathsf{h}$ ranges over the finite Timpl signature card, including its constructors and motive-annotated eliminators. The application marker $ϵ$ is explicit or implicit. In a signature head, omission is permitted exactly at an external level or an implicit argument declared by that head; all motives remain written. A core preterm is the Timpl grammar from convention 112.1, extended only by level metavariables and occurrences $?\alpha [\delta ]$. Thus the grammar does not hide a second class of untyped core nodes.

Definition 112.3 — Contextual metavariables¶

A contextual metavariable declaration has the form $$?\alpha :[\mathrm{\Delta }⊢A],$$ where $\mathrm{\Delta }=x_1:A_1,\dots ,x_k:A_k$ is a well-formed telescope and $\mathrm{\Delta }⊢A\mathsf{type}$. In a context $\mathrm{\Gamma }$, an occurrence has the form $?\alpha [\theta ]$, where $\theta :\mathrm{\Gamma }\to \mathrm{\Delta }$ is a well-typed simultaneous substitution. A definition $?\alpha :=[\mathrm{\Delta }]a$ is legal exactly when $\mathrm{\Delta }⊢a:A$, and replaces every occurrence by $a[\theta ]$. In worked constraint traces only, when $\mathrm{\Delta }=\mathrm{\Gamma }$, the bare notation $?\alpha$ abbreviates the identity occurrence $?\alpha [{\mathrm{id}}_{\mathrm{\Gamma }}]$; declarations and generation rules retain the substitution explicitly.

A metacontext $\mathcal{M}$ is a dependency-ordered list of declarations and definitions. The type and body of an entry may mention only entries to its left. A term metavariable never denotes an external universe level; a level metavariable ranges over level expressions and belongs to a separate finite context $\mathcal{L}$.

Definition 112.4 — Typed meta-substitution and problem-relative generality¶

Let $\mathcal{M}$ and $\mathcal{N}$ be dependency-ordered metacontexts. A typed meta-substitution $\theta :\mathcal{M}\Rightarrow \mathcal{N}$ assigns to every entry $?\alpha :[\mathrm{\Delta }⊢A]$ of $\mathcal{M}$ a term $[\mathrm{\Delta }]a$ well typed at $A$ after the earlier assignments, with free metavariables drawn from $\mathcal{N}$. Its action is postfix: $?\alpha [\delta ][\theta ]$ is $a[\delta ][\theta ]$, and the action extends structurally to contexts, types, terms, and constraints.

If $\rho :\mathcal{N}\Rightarrow \mathcal{P}$, define postfix composition by $$X[\theta ;\rho ]\equiv X[\theta ][\rho ],(\theta ;\rho )(?\alpha ):=\theta (?\alpha )[\rho ].$$ For a finite problem $P$, write $\mathrm{dom}(P)$ for the metavariables present before solving. Solutions ${\theta }_1$ and ${\theta }_2$ are compared only on that domain. Write ${\mathsf{MoreGeneral}}_P({\theta }_1,{\theta }_2)$ when some well-typed $\rho$ satisfies $$?\alpha [{\theta }_2]\equiv ?\alpha [{\theta }_1][\rho ]\text{for every }?\alpha \in \mathrm{dom}(P).$$ Residual fresh metavariables are immaterial: two solutions are identified when a dependency-preserving bijective renaming of those fresh entries makes their actions judgmentally equal on $\mathrm{dom}(P)$. A most general solution is one related by ${\mathsf{MoreGeneral}}_P$ to every solution, modulo that equivalence.

Definition 112.5 — Heterogeneous constraints and solutions¶

An object constraint is either a type equation $$\mathrm{\Gamma }⊢A\doteq B\mathsf{type}$$ or a heterogeneous typed term equation $$\mathrm{\Gamma }⊢(s:S)\doteq (t:T).$$ A type equation requires judgmental equality of two already well-formed types; it does not require them to inhabit a common universe. A solution of a term equation must first make $S$ and $T$ judgmentally equal types and must then, after conversion to either type, make $s$ and $t$ judgmentally equal. We abbreviate the homogeneous case by $\mathrm{\Gamma }⊢s\doteq t:S$. Heterogeneous equations are necessary while dependent indices are still unknown: two constructor spines need not have a common type before their index constraint is solved.

A formation guard has the form $\mathrm{\Gamma }⊢A\dot{\in }{\mathcal{U}}_{\ell }$. It is a suspended, syntax-directed universe-membership task, not an equation, and is never sent to the unifier. After object substitution it is compiled into the exact level premises of the Timpl formation rules by definition 112.11. The component $\mathcal{C}$ stores an ordered equation list and an ordered formation-guard list; concatenation preserves both orders.

A level constraint is either a strict equality $\ell {\doteq }_{\mathsf{L}}{\ell }^{\prime }$ or a formation inequality $\ell +k\le {\ell }^{\prime }$, where $k$ is a meta-level natural number. A constraint state $(\mathcal{L};\mathcal{M};\mathcal{C};\mathcal{U})$ consists of a level context, a metacontext, a finite constraint component $\mathcal{C}$, and a finite list of level constraints.

A solution $(\upsilon ;\theta )$ assigns level expressions to the unknowns in $\mathcal{L}$ and well-typed contextual definitions to the unsolved entries of $\mathcal{M}$. It solves the state when every equation in $\mathcal{C}$ becomes judgmental equality in Timpl, every formation guard compiles without a flexible-head obstruction, and every equality or inequality in $\mathcal{U}$, including those emitted by guard compilation, is valid for all values of the external level parameters. The type-equality and term-equality obligations are both part of solving an object constraint. Once the unique equality-level substitution has been fixed and applied, object solutions are ordered by the problem-relative predicate ${\mathsf{MoreGeneral}}_P$ of definition 112.4; equivalently, ${\theta }_2$ agrees on the original problem domain with ${\theta }_1;\rho$ for a well-typed substitution $\rho$ on the remaining object metavariables in that equality-substituted state. Residual bound-level assignments are not ordered by instantiation. Their order is pointwise: $\nu \le {\nu }^{\prime }$ exactly when $\nu (q)\le {\nu }^{\prime }(q)$ for every bound metavariable $q$ and every valuation of the external parameters.

Definition 112.6 — Generation judgments¶

The judgments respectively synthesize a Timpl type and preterm, check against a supplied Timpl type, or elaborate a well-formed type without asserting that it inhabits one universe. The third mode is necessary because the strict hierarchy of definition 29.1 is not cumulative. The output contexts extend the input contexts, and the returned term, type, and constraints may mention only output declarations. Premises are read left to right: each premise receives the output contexts of its predecessor, and their constraint lists are concatenated in that order. The rules use one fixed fresh-name supply. We also use two auxiliary judgments: The first consumes an ordinary written application spine. The second walks the dependency-ordered argument telescope of a fixed signature head $h$; its input $\overrightarrow{a}$ is the already elaborated prefix. A written argument is $q=e^{ϵ}$. In a signature telescope, every binder additionally has a surface policy $\omega \in \{\mathsf{infer},\mathsf{write}\}$; all motive binders have policy $\mathsf{write}$. List concatenation of independently generated constraints is written with commas and always follows premise order. In long rules only, the abbreviations $${\mathrm{\Xi }}_i:={\mathcal{L}}_i;{\mathcal{M}}_i;\mathrm{\Gamma },{\mathrm{\Omega }}_i:={\mathcal{L}}_i;{\mathcal{M}}_i;{\mathcal{C}}_i;{\mathcal{U}}_i$$ carry no hidden operation: the index on ${\mathrm{\Xi }}_i$ names the level and metacontexts at stage $i$, while the index on ${\mathrm{\Omega }}_i$ names that stage’s output package; an unindexed input in a rule is ${\mathrm{\Xi }}_0$. The sequential package $${\mathrm{\Omega }}_1\diamond {\mathrm{\Omega }}_2:={\mathcal{L}}_2;{\mathcal{M}}_2;({\mathcal{C}}_1,{\mathcal{C}}_2);({\mathcal{U}}_1,{\mathcal{U}}_2)$$ is defined only when the second premise starts in ${\mathrm{\Xi }}_1$, and extends associatively to a finite sequence of threaded packages. Thus $\diamond$ merely prints the state threading and ordered concatenation already required by the judgments. If $g$ is a formation guard, write $\mathrm{\Omega }\oplus g$ for the same package with $g$ appended to the guard projection of its constraint component. This operation does not run a solver. The atomic, checked-hole, direction-changing, and lambda clauses are

Universe membership has its own checking clause:

The displayed inequality is recorded, not solved during generation. It is the exact side condition of U-Hier.

Holes and annotations in synthesis mode, and holes in type mode, are governed by the following rules. These rules fix the declaration order of the fresh level and object metavariables.

Type formation is a separate inductive judgment, not an implicit appeal to a maximum universe. In E-Ty-Vec, ${\mathsf{level}}_{\mathcal{L}}(\hat{\ell })=(\ell ,{\mathcal{L}}_0)$ means $\ell$ is the written well-formed level and ${\mathcal{L}}_0=\mathcal{L}$, or $\ell =?u$ is fresh and ${\mathcal{L}}_0=\mathcal{L},?u$.

Thus the legal input $\mathsf{Vec}[0]((x:\mathbb{N})\to \mathbb{N},\mathsf{0})$ first elaborates its product element type by E-Ty-Pi; the resulting guard is then discharged by U-Pi. No term-synthesis rule for a product is required.

The binding type formers thread the domain output into the opened codomain.

Type-mode rule selection is deterministic. Inspect the outer constructor in this priority order: hole, universe literal, nullary base, identity, vector, product, and Sigma. Rule E-Ty-El is the fallback only for an atom outside those seven syntactic classes whose synthesis exposes a universe. It is therefore never tried after a recognized type-former rule has failed, and no surface type expression selects two type-mode clauses.

Pairs and projections have the following exact clauses. The weak-head premises are tests; failure gives no derivation.

Ordinary application is the least relation generated by E-Syn-App, E-Spine-Done, E-Spine-Insert, and E-Spine-Consume. Rule priority is part of the definition: insertion precedes the explicit case, a written implicit argument precedes insertion, and E-Spine-Done applies only when the written spine is empty and the exposed head is not an implicit product.

A flexible or rigid nonproduct head and an explicitness mismatch have no rule. Consequently this relation inserts one unique consecutive block of implicit arguments and never guesses a relevance bit.

Finally let a signature entry have level parameters $\overrightarrow{u}$, result $R$, and dependency-ordered argument telescope $((x_i:B_i{)}^{{ϵ}_i,{\varrho }_i,{\omega }_i}{)}_{i=1}^n$. Written levels are copied; omitted levels are replaced from left to right by fresh level metavariables. This deterministic operation is written ${\mathsf{levels}}_h(\overrightarrow{\hat{\ell }};\mathcal{L})=(\overrightarrow{\ell };{\mathcal{L}}_0)$. The signature-head and telescope rules are:

There is no omission rule for a $\mathsf{write}$ binder. This is the exact reason an eliminator motive cannot be invented by E-Syn-Head.

Rule E-Chk-Syn emits first-class type equality, so it remains applicable to well-formed mixed-level products that inhabit no common strict universe. When a type equation itself compares ${\mathcal{U}}_r$ with ${\mathcal{U}}_s$, rigid decomposition emits the strict level equality $r{\doteq }_{\mathsf{L}}s$. Separate membership premises emit lower-bound edges through E-Chk-Univ. The type rules never invent a maximum universe: the optional level on a surface vector is a formation witness, while the returned Timpl family is $\mathsf{Vec}(A^{\prime },n^{\prime })$. Every premise receives both output contexts of its predecessor. Lambda, pair, projection, ordinary-spine, and signature-head rules likewise copy their displayed dependency and metadata; a failed head test or marker match has no derivation. In particular a flexible application head is outside this direct generation fragment until an annotation exposes a product with both metadata bits, and no signature rule invents a written motive.

This repeated insertion of consecutive implicit binders is implicit saturation; it stops at the first explicit binder and does not choose among alternative spine shapes.

For a declared head, E-Syn-Head instantiates external levels before the head telescope is traversed. Thus an omitted level of $\mathsf{append}$ or $\mathsf{map}$ is fixed before ordinary implicit saturation, whereas E-Syn-Atom applies only after every external level has already been written.

The displayed rules cover all and only the forms of definition 112.2. In particular, both binding clauses elaborate their codomains in the opened context $\mathrm{\Gamma },x:A^{\prime }$; this is part of the inductive definition rather than an extensibility convention.

Definition 112.9 — Canonical level expressions¶

Fix the declaration order of the external level parameters. A level atom is either a numeral $0+k$ or an expression $p+k$, where $p$ is an external parameter and $k\in \mathbb{N}$. An atom dominates another atom under all natural-number valuations precisely in one of the following cases:

1. they have the same external parameter and the first offset is at least the second;

2. both are numerals and the first numeral is at least the second; or

3. the first is $p+k$, the second is $0+j$, and $k\ge j$.

The canonical level normal form $\mathsf{lnf}(e)$ is the declaration-ordered maximum of atoms obtained by distributing successor over maximum, retaining only the largest offset for each external parameter and deleting every dominated numeral. If no external atom dominates the largest numeral, retain that numeral as the first atom. Repeated atoms and the empty maximum are identified with one copy and $0$, respectively.

Definition 112.11 — Formation-guard compilation¶

After applying every object assignment stored in $\mathcal{M}$, normalize the guarded type to weak-head form and compile $\mathrm{\Gamma }⊢A\dot{\in }{\mathcal{U}}_{\ell }$ by the following exhaustive clauses for the Timpl card: If the weak-head form is a rigid neutral (N) and synthesis gives $\mathrm{\Gamma }⊢N:{\mathcal{U}}_q$, emit the strict equality $\ell {\doteq }_{\mathsf{L}}q$. A still-flexible head returns outside; the compiler never guesses its universe. The base clauses deliberately emit $0\le \ell$, although that inequality is extensionally automatic: when $\ell$ is a fresh omitted vector level, it classifies $\ell$ as a bound metavariable and gives the least choice (0). These clauses are precisely U-Hier, U-Pi, U-Sig, the identity and vector closure rules, and the three base closure rules. Guard compilation therefore emits no object equation and no universe maximum.

Definition 112.12 — Stratified level problems¶

A stratified level problem partitions its level metavariables into equality metavariables and bound metavariables by the following deterministic collection policy. A fresh level metavariable starts unclassified. The first strict equality that orients it to an occurs-free expression classifies it as an equality metavariable; an equality between two unclassified metavariables orients the later declaration to the earlier one. After all strict equalities have been collected and substituted, an unclassified metavariable occurring as the right endpoint of a formation inequality becomes a bound metavariable. Any still-unclassified metavariable is ambiguous, and any strict equality still mentioning a bound metavariable is outside this stratified grammar. Thus classification is generated from constraint roles, not supplied as unexplained input data. Each equality metavariable $q$ has at most one direct assignment $$q{\doteq }_{\mathsf{L}}e,$$ where $e$ is occurs-free and is built from zero, external parameters, and earlier equality metavariables by successor and maximum. Equality assignments are processed in declaration order and substituted through the rest of the problem. No equality metavariable may remain afterward. Normalize a residual rigid equality with $\mathsf{lnf}$; such an equality contains only zero and external parameters. Delete it when the normal forms are identical and reject it otherwise. An equality that still mentions a bound metavariable is outside the stratified grammar.

Before constructing the residual bound graph, normalize every inequality whose right side contains no bound metavariable. Such an inequality is valid for all external-parameter valuations exactly when every atom of the left normal form is dominated, in the sense of definition 112.9, by some atom of the right normal form. Delete a valid rigid inequality and reject an invalid one. The residual bound part is then a finite set of inequalities $$p+k\le q,$$ where $p$ is an external parameter, bound metavariable, or zero; $q$ is a bound metavariable; and $k\in \mathbb{N}$. The two metavariable classes are disjoint. Comparing strict universes ${\mathcal{U}}_r$ and ${\mathcal{U}}_s$ generates a level equality; if it orients toward a fresh equality metavariable, it must fit (112.5). Separately, E-Chk-Univ and formation-guard compilation generate $p+1\le q$ when ${\mathcal{U}}_p$ is checked against ${\mathcal{U}}_q$. Replace $max(p_1,\dots ,p_r)+k\le q$ by its $r$ component inequalities. After the rigid discharge, the upper normal form must be one bound metavariable $q$. An upper maximum containing a bound metavariable is disjunctive rather than a difference-constraint edge and is reported outside this stratified fragment; an upper maximum containing no bound metavariable was already decided by the atomwise test.

Regard (112.6) as an edge $p\stackrel{k}{\to }q$. Adjoin a zero-weight edge $0\stackrel{0}{\to }q$ for every bound metavariable $q$; this records the implicit natural-number lower bound and does not change the set of solutions. Compute strongly connected components of the full nonnegative-weight graph. Reject any component containing a positive-weight edge: within a strongly connected component that edge lies on a positive cycle. Every remaining component has only zero-weight edges; collapse those components. On the resulting acyclic graph, assign to each unknown $q$ the maximum of $p+k$ over all paths from zero or an external parameter $p$ to $q$.

Definition 112.14 — Rigid and flexible weak heads¶

Weak-head normalization reduces head $\beta$-redexes and the computation rule of an eliminator whose scrutinee has constructor head. A weak head is flexible when the head of its neutral spine is an unsolved metavariable, even when applications or stuck eliminators follow that head. It is rigid when the spine head is a bound variable, declared constant, type former, or constructor, or when an eliminator is stuck on such a rigid neutral. Thus $?\alpha [x]y$ is flexible for classification, although it will be outside the direct fragment below.

Before classifying heads, delete any normalized heterogeneous constraint whose two types and whose two terms are respectively judgmentally identical. A remaining constraint is flex–rigid when exactly one term head is flexible, flex–flex when both are flexible, and rigid–rigid otherwise. The types are simplified before the terms; the terms are normalized only far enough to make this classification.

Definition 112.15 — Rigid simplification¶

After weak-head normalization, simplify a heterogeneous rigid–rigid equation as follows.

1. First simplify the equation between its two types. Reject a rigid type clash. Once the types convert, regard the term equation as homogeneous.

2. Delete every normalized reflexive equation, irrespective of whether its common head is rigid or flexible.

3. Decompose two occurrences of the same type former or constructor into equations between corresponding arguments. Dependent spine arguments are processed from left to right, so each earlier equality converts the types of the later pair.

4. Compare two abstractions by extending the context with one variable and comparing their bodies. The normalization interface supplies eta-long forms, so a neutral function at product type is exposed as an abstraction before this clause is used. It also canonicalizes every Unit-typed term to $\star$ and exposes a Sigma-typed neutral as a pair before component comparison.

5. Comparing ${\mathcal{U}}_r$ with ${\mathcal{U}}_s$ emits the strict level equality $r{\doteq }_{\mathsf{L}}s$. Before any suspended term equation is exposed, run the equality stratum of definition 112.12: orient a permitted equality metavariable, substitute its normalized assignment through the entire combined state, and delete a reflexive rigid equality or reject a distinct one. Separately, E-Chk-Univ emits $p+1\le q$ when checking ${\mathcal{U}}_p$ against ${\mathcal{U}}_q$.

6. Reject distinct rigid heads, including distinct constructors of $\mathbf{2}$, $\mathbb{N}$, or $\mathsf{Vec}$.

7. Leave an equation stuck only when at least one side has a flexible head.

The fresh variable in item 4 avoids the free variables of both sides and of the constraint context. For a first-class type equation, skip item 1 and apply items 2–7 directly to the two well-formed type expressions. For a heterogeneous term equation, item 1 is a separate type-equation task and must finish before term-head classification.

Definition 112.17 — Direct contextual-pattern fragment¶

An occurrence is a contextual pattern occurrence when it has the form $?\alpha [x_1,\dots ,x_k]$, the $x_i$ are pairwise distinct, and the displayed substitution is a well-typed variable renaming from the declaration telescope of $?\alpha$. A state is in the direct contextual-pattern fragment when weak-head simplification exposes only such occurrences as an entire flexible side and the following pruning-free conditions hold at every state reached by the fixed strategy. In particular, a metavariable occurrence followed by an application or stuck eliminator is outside this fragment even though its neutral head is flexible for classification. The conditions are:

1. in every flex–rigid constraint $?\alpha [\overrightarrow{x}]\doteq t$, every occurrence of $?\alpha$ and every occurrence of a free ordinary variable outside $\overrightarrow{x}$ is rigid in the sense defined below, while every other metavariable of $t$ can be moved before $?\alpha$ by a dependency-preserving permutation;

2. every flex–flex restriction has a well-formed dependency-closed common telescope and result type;

3. substituting a candidate assignment and weak-head simplifying does not expose a non-pattern occurrence; and

4. after the equality-level substitution, every candidate object body checks at its declared result type without using a residual formation bound or instantiating a bound-level metavariable.

The test is performed before committing each transition. Its possible outcomes are therefore inside, outside the direct fragment, and unsatisfiable. Outside is not a proof of unsatisfiability. The solver does not postpone, prune, imitate, project, or search.

Definition 112.18 — Flex–rigid assignment¶

Consider $$\mathrm{\Gamma }⊢?\alpha [x_1,\dots ,x_k]\doteq t:A.$$ Orient the flexible side to the left. Assign $$?\alpha :=[z_1:A_1,\dots ,z_k:A_k]t^{\mathsf{nf}}[z_1/x_1,\dots ,z_k/x_k]$$ exactly when:

1. $?\alpha$ does not occur in $t^{\mathsf{nf}}$;

2. every free ordinary variable of $t^{\mathsf{nf}}$ is among the $x_i$;

3. every metavariable in $t^{\mathsf{nf}}$ precedes $?\alpha$, after a dependency-preserving permutation of independent declarations; and

4. after applying the equality-level substitution, the candidate body checks against the declared result type of $?\alpha$ without appealing to a residual formation bound or assigning a bound-level metavariable.

Before applying items 1–3, compute the beta-iota normal, eta-long form $t^{\mathsf{nf}}$ supplied by convention 112.1, and use that normal form in both the tests and the displayed assignment. This canonical-form precondition is essential: a variable hidden in a discarded beta argument is not a scope occurrence, and a self-occurrence hidden there is not a cycle. Canonical forms therefore determine the scope and cycle tests rather than merely optimizing them. After assignment, substitute the definition through the remaining state. If item 2 fails only because an out-of-scope variable occurs below another flexible head, report outside the direct fragment; pruning could still produce a solution. A rigid out-of-scope occurrence is an actual scope failure. Failure of item 4 solely because universe membership awaits a residual bound is outside, not unsatisfiable. For example, $?A:[\mathrm{\Gamma }⊢{\mathcal{U}}_q]\doteq {\mathcal{U}}_p$ is deferred by this finite policy when only $p+1\le q$ could license the assignment; the chapter does not claim a principal object substitution before that bound is instantiated.

Definition 112.20 — Flex–flex intersection and insertion¶

For an equation $$?\alpha [x_1,\dots ,x_k]\doteq ?\alpha [y_1,\dots ,y_k],$$ retain exactly those telescope positions $i$ for which $x_i=y_i$, together with every earlier position on which the retained variables’ types and the result type depend. If dependency closure would retain a position with $x_i\ne y_i$, report the state outside the direct fragment. Otherwise create $?\beta :[{\mathrm{\Delta }}^{\prime }⊢A^{\prime }]$ and define both sides through $$?\alpha :=[\mathrm{\Delta }]?\beta [{\pi }_{{\mathrm{\Delta }}^{\prime }}].$$ This rule is reached only after the heterogeneous type task has been solved. Consequently, if a result type itself mentions a mismatched actual parameter, its rigid type equation fails as unsatisfiable before flex–flex intersection. The outside outcome above concerns a dependency-closure failure that remains after the two occurrence types have converted. For distinct metavariables, retain the ordinary variables that occur in both argument lists, ordered as in the ambient context, and close that list under dependencies. Define each metavariable through one fresh $?\beta$ over the retained telescope, provided both declaration telescopes admit the required projections and the two result types are judgmentally equal after restriction. The fixed left-to-right order chooses the fresh name; it does not choose a value for it.

The metacontext operation is part of the rule. First take a dependency-preserving topological permutation that places all declarations needed by ${\mathrm{\Delta }}^{\prime }$ and $A^{\prime }$ before the target declaration or declarations. Insert $?\beta$ immediately before the earliest target, replace each target declaration by the displayed definition through $?\beta$, and substitute those definitions through every later declaration, definition, and constraint. Recheck the resulting suffix. If a target is a prerequisite of the fresh declaration, or if two targets cannot be brought to this position without reversing a dependency, the state is outside the direct fragment.