ch:elaboration: ch:elaboration

The first equation orients to $$?\alpha :=[x:\mathbb{N}]x.$$ The body has type $\mathbb{N}$ in the declaration telescope $x:\mathbb{N}$, so substitution at the occurrence gives $x$ as required. For the third equation, typing the right side in the full declaration telescope gives $$?\beta :=[x:\mathbb{N},y:\mathbf{2}]x.$$ A legal contextual definition may ignore a telescope variable; its premise is typing in the whole telescope, not occurrence of every variable in the body.

The middle equation does not orient. Its right-hand side is well typed at $\mathbb{N}$ in the ambient context, but its Boolean scrutinee is the free variable $y$. Hence it is not a term of type $\mathbb{N}$ in the smaller telescope $x:\mathbb{N}$. The failed premise of definition 112.3 is $x:\mathbb{N}⊢a:\mathbb{N}$ for the proposed body $a$; equivalently, this is a scope failure, not an occurs failure.

Pair checking first checks $\mathsf{0}$ against $\mathbb{N}$. Substituting the returned core term for $n$ makes the second expected type $${\mathsf{Id}}_{\mathbb{N}}(n,\mathsf{0})[\mathsf{0}/n]={\mathsf{Id}}_{\mathbb{N}}(\mathsf{0},\mathsf{0}).$$ Thus $\mathsf{refl}(\mathsf{0})$ checks, and the original pair is accepted.

With first component $\mathsf{suc}(\mathsf{0})$, the second expected type is instead $${\mathsf{Id}}_{\mathbb{N}}(\mathsf{suc}(\mathsf{0}),\mathsf{0}).$$ The introduction $\mathsf{refl}(\mathsf{0})$ has native type ${\mathsf{Id}}_{\mathbb{N}}(\mathsf{0},\mathsf{0})$. Rigid decomposition of the required type equality reaches the endpoint constraint $$\mathsf{suc}(\mathsf{0})\doteq \mathsf{0}:\mathbb{N}.$$ Its heads are distinct natural-number constructors, so rigid simplification rejects it.

The incoming bounds at $r$ give $$r=max(u+1,v).$$ The bounds at $s$ then give These are least because every solution must dominate every path weight into the corresponding vertex, and the displayed maxima attain all four bounds.

After adding $s+1\le r$, the edges $$r\stackrel{1}{\to }s\stackrel{1}{\to }r$$ form a cycle of total weight $2$. Summing its inequalities yields $r+2\le r$, an impossible inequality of natural levels. This is the positive-cycle certificate.

Left-to-right heterogeneous decomposition first equates the outer types, $$\mathsf{Vec}(A,\mathsf{suc}(?p[\pi ]))\doteq \mathsf{Vec}(A,\mathsf{suc}(m)):{\mathcal{U}}_u.$$ Rigid decomposition and successor injectivity emit $$?p[\pi ]\doteq m:\mathbb{N}.$$ The direct contextual assignment is $?p:=[{\mathrm{\Gamma }}_0]m$. After substitution, both constructor results have type $\mathsf{Vec}(A,\mathsf{suc}(m))$, and the two head entries are the same term $a:A$, so their equation deletes reflexively. Before comparing the final arguments, use the solved index equation to convert $$xs:\mathsf{Vec}(A,?p[\pi ])\text{to}xs:\mathsf{Vec}(A,m).$$ The tail equation is therefore the homogeneous judgment $$xs\doteq ys:\mathsf{Vec}(A,m).$$ If the tails were compared first, their available types would be $\mathsf{Vec}(A,?p[\pi ])$ and $\mathsf{Vec}(A,m)$. Those are not yet judgmentally the same type, so no homogeneous typed equation could be formed. The earlier index equation supplies exactly the context conversion needed by the later component.

The pattern assignment is $$?\alpha :=[x:\mathbb{N},y:\mathbf{2}](x,\mathsf{suc}(x)).$$ In that telescope, $x:\mathbb{N}$ and $\mathsf{suc}(x):\mathbb{N}$. Consequently the pair has type $\sum _{n:\mathbb{N}}\mathbb{N}$, and instantiating the abstraction at $[x,y]$ beta-reduces to the right-hand side of the constraint. The pattern condition asks that the occurrence apply $?\alpha$ to a variable renaming of its telescope. It does not require the solution body to depend on every formal parameter, so the unused $y$ is harmless.

For the first equation, only the first argument position agrees. Introduce $?\beta :[r:\mathbb{N}⊢\mathbb{N}]$ and set $$?\alpha :=[r:\mathbb{N},s:\mathbb{N}]?\beta [r].$$ Both sides reduce to $?\beta [x]$, so the retained telescope is $r:\mathbb{N}$. For the second equation, only the second position agrees. With $?\gamma :[s:\mathbb{N}⊢\mathbb{N}]$, set $$?\alpha :=[r:\mathbb{N},s:\mathbb{N}]?\gamma [s].$$ Both sides now reduce to $?\gamma [y]$, and the retained telescope is $s:\mathbb{N}$. The factorization argument of lemma 112.23 makes these solutions most general: any solution must ignore precisely the formal position varied independently across the two occurrences.

If the result type is $\mathsf{Vec}(\mathbb{N},y)$, the first constraint is heterogeneous: its occurrence types are $\mathsf{Vec}(\mathbb{N},y)$ and $\mathsf{Vec}(\mathbb{N},z)$. Type-first simplification reaches the rigid equation $y\doteq z:\mathbb{N}$, so the solver returns unsatisfiable before attempting an intersection. The second constraint gives identical occurrence types $\mathsf{Vec}(\mathbb{N},y)$; it reaches flex–flex intersection, retains the second parameter, and introduces a fresh metavariable of result type $\mathsf{Vec}(\mathbb{N},s)$.

For the signature with base type $o$ and sole constant $c:o$, two solutions of $?F[c]\doteq c:o$ are $$?F:=[x:o]x\text{and}?F:=[x:o]c.$$ Neither unifier is an instance of the other. Later substitutions affect only residual metavariables. They cannot turn the bound occurrence $x$ in the first body into the rigid constant $c$, or turn the rigid constant in the second body into $x$.

There is no third unifier above both. Normalize its body at type $o$ in context $x:o$. With no eliminator or other constant, its canonical forms are $x$, $c$, or a neutral headed by a residual metavariable. Replacing $x$ by $c$ turns the first two into $c$, while a residual neutral stays neutral and cannot solve the equation without an additional constraint. Hence the two displayed bodies are the complete set of unifiers, modulo judgmental equality and residual renaming, and neither is most general.

The flex–rigid proof abstracts along a bijective variable renaming of the declaration telescope. The argument $c$ is rigid, not that renaming, so equality at the observed input gives no equality of abstractions. This is a proof of non-unitarity; undecidability of unrestricted higher-order unification is a separate source result.

Bare $\mathsf{vnil}$ does not synthesize: its omitted element type and level receive no determining equation. It checks against an expected vector type whose index is zero, for example $$\mathsf{vnil}\Leftarrow \mathsf{Vec}(\mathbb{N},\mathsf{0}),$$ or synthesizes after the level-explicit annotation $(\mathsf{vnil}:\mathsf{Vec}[0](\mathbb{N},\mathsf{0}))$.

The abstraction $\lambda x.x$ also does not synthesize, because its domain is absent. It checks against $\mathbb{N}\to \mathbb{N}$, or synthesizes after the annotation $(\lambda x.x:\mathbb{N}\to \mathbb{N})$.

The pair $(\mathsf{0},\mathrm{\_})$ does not synthesize, since pair introduction is checking-directed. Against $\sum _{n:\mathbb{N}}\mathbb{N}$, the first component checks and the second hole is assigned expected type $\mathbb{N}$, but its term metavariable remains unsolved. Thus it remains ambiguous even while checking. No type annotation can choose a term for that hole under definition 112.25; a minimal repair must also fill it, for example $$((\mathsf{0},\mathsf{0}):\sum _{n:\mathbb{N}}\mathbb{N}).$$ This last case is the boundary between missing type information, repaired by an expected type, and missing program information, repaired by a term.

In the $\mathsf{cons}$ branch the constructor indices give $$A:{\mathcal{U}}_u,x:A,xs:\mathsf{Nest}(A\times A).$$ The written polymorphic scheme may be instantiated independently at each recursive occurrence. The call on $xs$ selects the instance $$\mathsf{size}\{A\times A\}:\mathsf{Nest}(A\times A)\to \mathbb{N},$$ so its domain is exactly the known type of $xs$.

Under the monomorphic provisional assumption $\mathsf{size}:\mathsf{Nest}(?X)\to \mathbb{N}$, checking the defining function at the constructor pattern gives $xs:\mathsf{Nest}(?X\times ?X)$. Checking that recursive argument against the provisional domain generates $$?X\doteq ?X\times ?X.$$ An attempt to orient this equation would define the type metavariable using a type that contains it. The occurs check rejects the cycle.

Contextual pattern assignment cannot help. Its flexible heads are term metavariables at a fixed declared type, applied to variable renamings. Here the missing object is a quantified type scheme whose two instances have different monotypes. No rule in the direct fragment introduces that quantifier, so the problem lies outside the solver rather than furnishing a failed pattern equation.

Freshening polymorphic self-application gives the instances $\mathsf{pid}[\ell ]$ and $\mathsf{pid}[\kappa ]$. The second occurrence is an argument to the first, so the universe containing its type must be below the first occurrence’s universe: If one monomorphic level were reused, the result would instead contain a strict cycle. UniCoq may distinguish flexible from rigid universe instances; Timpl has only the stratified equality-and-bound problems of definition 112.12. The example therefore illustrates a richer source language, not a failure of the proved graph solver.

For list membership, rigid decomposition first reduces the overloaded goal to $$\mathsf{luntag}(\mathsf{list}\mathsf{\_}\mathsf{of}(?f))\doteq [y_1]++[y_2].$$ There is no direct canonical key pairing $\mathsf{luntag}$ with append, so the default key selects $\mathsf{rightTag}$. The residual equation has a $\mathsf{list}\mathsf{\_}\mathsf{of}$ projector against a $\mathsf{rightTag}$-headed term; that key selects $\mathsf{right}\mathsf{\_}\mathsf{proof}$, after which fresh metavariables are generated for the instance’s arguments. Timpl has no canonical-structure database or overloading search. Its theorem is conditional on one fixed signature head and deterministic insertion, so this search trace is outside its statement.

In the guard example, write the published local bindings as The equality for $p$ forces $?X_1:={\mathsf{id}}_{\mathbb{N}\to \mathbf{0}}$. Applying this substitution to the provisional body gives $$hfx⟼{\mathsf{id}}_{\mathbb{N}\to \mathbf{0}}fx⟶fx.$$ The recursive argument is still $x$, not a structural subterm of $x$. Conversion of the unification endpoints survives, but the CIC kernel’s syntactic guard check rejects the instantiated fixpoint. The exact archived plugin replay in appendix D confirms the source tests, but does not turn this counterexample into a metatheorem. Timpl excludes recursive clauses and fixpoint unification in convention 112.1; its successful output is instead independently checked against the displayed nonrecursive signature. Thus the published counterexample refutes a natural correctness conjecture for the richer procedure and leaves this chapter’s soundness and bounded completeness claims untouched.

Use the implicit declaration In a context containing $A:{\mathcal{U}}_u$, $B:{\mathcal{U}}_v$, $n:\mathbb{N}$, $f:A\to B$, and $xs:\mathsf{Vec}(A,n)$, implicit saturation creates, in order, the level context $$?{\ell }_A,?{\ell }_B$$ and then the contextual term metacontext $$?X:[\mathrm{\Gamma }⊢{\mathcal{U}}_{?{\ell }_A}],?Y:[\mathrm{\Gamma }⊢{\mathcal{U}}_{?{\ell }_B}],?p:[\mathrm{\Gamma }⊢\mathbb{N}].$$ The initial core spine is $\mathsf{map}[?{\ell }_A,?{\ell }_B]\{?X\}\{?Y\}\{?p\}$. Checking $f$ against $?X\to ?Y$ rigidly decomposes its known type $A\to B$, giving the two term equations $$?X\doteq A,?Y\doteq B.$$ Orienting $?X:=A$ and $?Y:=B$ checks each body against its contextual metavariable’s declared universe. Decomposing those universe equations emits the strict level equations $$?{\ell }_A{\doteq }_{\mathsf{L}}u,?{\ell }_B{\doteq }_{\mathsf{L}}v.$$ Before applying that substitution, the vector argument generates $$\mathsf{Vec}(?X,?p)\doteq \mathsf{Vec}(A,n),$$ whose rigid components are $?X\doteq A$ and $?p\doteq n$; after the function constraints have been substituted, only $?p\doteq n$ is new. The normalized strict level assignments are therefore $u$ and $v$. The type-formation judgment establishes the mixed-level declaration without assigning the whole product to an enclosing universe. The metavariable-free result is $$\mathsf{map}[u,v]\{A\}\{B\}\{n\}fxs:\mathsf{Vec}(B,n).$$ The object equations fix $?X,?Y,?p$, while the strict level equations fix $?{\ell }_A,?{\ell }_B$. No choice remains.

The following four constraints are well typed in the indicated metacontexts.

1. $\mathsf{0}\doteq \mathsf{suc}(\mathsf{0}):\mathbb{N}$ is a rigid-head clash.

2. For $?\alpha :[x:\mathbb{N}⊢\mathbb{N}]$, $?\alpha [x]\doteq \mathsf{suc}(?\alpha [x]):\mathbb{N}$ triggers the occurs check.

3. In $x:\mathbb{N},y:\mathbb{N}$, for $?\alpha :[x:\mathbb{N}⊢\mathbb{N}]$, $?\alpha [x]\doteq y:\mathbb{N}$ is a scope escape.

4. For $?F:[x:o⊢o]$ in the signature with the sole constant $c:o$, $?F[c]\doteq c:o$ is a non-pattern application.

The first has no solution because distinct canonical constructors of $\mathbb{N}$ cannot be judgmentally equal. A solution of the second would be a finite acyclic term equal to a term containing itself as a proper subterm; constructor inversion would reproduce the same demand below one $\mathsf{suc}$, so no such contextual definition exists. A legal solution of the third must be typed in the telescope $x:\mathbb{N}$, but the rigid ambient variable $y$ is not in that telescope and substitution cannot remove it. Hence no scoped solution exists.

The fourth has the two solutions $?F:=[x]x$ and $?F:=[x]c$. They are incomparable because residual instantiation cannot replace a bound variable by a rigid constant or conversely. They are also complete: a beta-normal, eta-long body of type $o$ in context $x:o$ is $x$, $c$, or a residual neutral; after substituting $c$, a residual neutral cannot become the rigid canonical form $c$. Thus the problem is non-unitary. The direct solver therefore reports the problem outside its fragment; this protects the stated principality boundary without asserting that either solution is unsound. Unrestricted higher-order undecidability is a separate, stronger source theorem.

Represent a rigid first-order term by a node of a finite acyclic directed graph. A node is labelled by an ordinary variable, a metavariable leaf, or a rigid symbol $F$ together with an ordered vector of child nodes of the symbol’s arity. Sharing is permitted. A state consists of this graph, a union–find partition, and a queue of node pairs still to be equated.

For a substitution $\theta$ of the metavariable leaves, write $G,n{\Downarrow }_{\theta }t$ when recursively unfolding node $n$, replacing each metavariable leaf by its $\theta$-image, yields the tree term $t$. Say that $\theta$ solves a graph state when it gives equal unfolded terms to every pair in the queue and to every pair of nodes in one union–find class. This relation records the mathematical content of a class; path compression and representative choice are absent from it.

Consider one work item $(n,m)$ with equal rigid labels $F$ and child vectors $(n_1,\dots ,n_k)$ and $(m_1,\dots ,m_k)$. The graph step unions the classes of $n,m$, removes $(n,m)$, and enqueues every $(n_i,m_i)$. We prove preservation in both directions. If $\theta$ solves the old state, then $$F(t_1,\dots ,t_k)=F(u_1,\dots ,u_k),G,n_i{\Downarrow }_{\theta }{t}_i,G,m_i{\Downarrow }_{\theta }{u}_i.$$ Rigid injectivity gives $t_i=u_i$ for every $i$. Thus every new child pair and the new parent class are satisfied. Conversely, if $\theta$ solves the new state, every $t_i=u_i$; congruence gives equality of the two parent unfoldings, so the removed work item is satisfied. All untouched classes and work items have identical interpretations. The step therefore preserves exactly the tree solutions. Different rigid labels instead give the empty solution set by rigid-head disjointness.

This is a refinement lemma for one merge. It supplies neither the global algorithm nor the Paterson–Wegman bound: the latter additionally requires its specific graph representation, scheduling, and constant-time machine operations.