ch:pattern-compilation: ch:pattern-compilation

After reversing the rows, the matrix is $$\mathsf{choose}(b,n)=\mathsf{suc}(\mathsf{0}),\mathsf{choose}(\mathsf{tt},n)=\mathsf{0}.$$ The first row has no blocking pattern. Ordered priority therefore returns its leaf before inspecting the later constructor row. The case tree is simply $$\mathsf{leaf}(1,\mathsf{suc}(\mathsf{0})).$$ Its one schematic leaf equation is $$\mathsf{choose}(b,n)\equiv \mathsf{suc}(\mathsf{0}).$$ The two closed Boolean instances follow by substitution; no case split is needed. The first row matches every Boolean, so the later constructor row can never be the least matching row and reaches no leaf.

Specializing the vector column against $$\mathsf{vcons}(k,a,xs):\mathsf{Vec}(A,\mathsf{suc}(k))$$ generates $$m=\mathsf{suc}(k).$$ The restricted unifier takes one solution step, producing $$[\mathsf{suc}(k)/m].$$ Hence the index position in this branch is forced to be $\mathsf{suc}(k)$. Suppose instead that the inaccessible pattern contains the written term $k$. Validation then asks for the judgmental equality $$\mathsf{suc}(k)\equiv k,$$ which does not hold. The useful diagnostic is therefore: “inaccessible term mismatch; forced $\mathsf{suc}(k)$, written $k$.” Treating the comparison as another equation would not rescue it: orienting $k=\mathsf{suc}(k)$ reaches the cycle transition of definition 78.9, because the right side contains the variable being solved.

Row count is not a decreasing measure. A variable row is copied into every positive branch, and a row headed by the selected constructor survives in its matching branch; the branch may consequently contain as many rows as the parent.

For the matrix whose two patterns are $$\mathsf{vcons}(k,a,xs)\text{and}z,$$ the measure $\mu$ of lemma 121.13 is initially one: only the outer $\mathsf{vcons}$ is a constructor node. In the $\mathsf{vnil}$ branch the constructor row is deleted and the variable row is copied, so $\mu =0$. In the $\mathsf{vcons}$ branch the outer constructor is consumed; its exposed subpatterns $k,a,xs$ and the copied variable pattern contain no constructor or absurd node, so again $\mu =0$. Thus every recursive branch decreases $\mu$ strictly even though row count need not decrease. This proves the matrix-recursion part of the relative lemma; its separate hypothesis accounts for termination of each scheduled restricted-unifier call.

Splitting the input $v:\mathsf{Vec}(A,m)$ gives two branches. The $\mathsf{vnil}$ branch solves $m=\mathsf{0}$ and reaches the leaf $\star$. In the $\mathsf{vcons}$ branch the unifier solves $m=\mathsf{suc}(k)$, but specialization deletes the sole row. The reported uncovered symbolic pattern is therefore $$[\mathsf{suc}(k)/m,\mathsf{vcons}(k,a,xs)/v],a:A,xs:\mathsf{Vec}(A,k).$$ It is well typed, but if $A:={\mathsf{Id}}_{\mathbf{2}}(\mathsf{tt},\mathsf{ff})$, the internal no-confusion map of example 30.12 sends any candidate $a:A$ to $\mathbf{0}$. Thus, under the separately stated consistency assumption that Timpl has no closed term of $\mathbf{0}$, the symbolic pattern has no closed instance. This argument uses no canonicity theorem, and the coverage theorem itself does not establish that consistency assumption. If $A:=\mathbf{1}$, take $k:=\mathsf{0}$, $a:=\star$, and $xs:=\mathsf{vnil}$. Then $\mathsf{vcons}(\mathsf{0},\star ,\mathsf{vnil}):\mathsf{Vec}(\mathbf{1},\mathsf{suc}(\mathsf{0}))$ is a closed uncovered input.

The leftmost tree first splits $x$. In each resulting branch the second column blocks. Put The complete tree is $$\mathsf{split}(x,\{\mathsf{tt}\mapsto ([\mathsf{tt}/x],{\mathcal{T}}_t),\mathsf{ff}\mapsto ([\mathsf{ff}/x],{\mathcal{T}}_f)\}).$$ Thus the judgmental leaf equations are For example, let Boolean case analysis proves $N(x,y)\to {\mathsf{Id}}_{\mathbb{N}}(g(x,y),\mathsf{suc}(\mathsf{suc}(\mathsf{0})))$: the premise eliminates the $(\mathsf{tt},\mathsf{tt})$ leaf by its first conjunct and both $y=\mathsf{ff}$ leaves by its second, leaving only $(\mathsf{ff},\mathsf{tt})$. In contrast, the unconditional equation $g(x,y)=\mathsf{suc}(\mathsf{suc}(\mathsf{0}))$ suggested by the third source row is false, for instance at $(\mathsf{tt},\mathsf{tt})$.

Write the two vector inputs as $x:\mathsf{Vec}(A,n)$ and $y:\mathsf{Vec}(B,n)$. The complete frontier is $A,B,C,f,n,x,y$; only $x$ and then $y$ block. Splitting $x$ gives $${\sigma }_0=[\mathsf{0}/n,\mathsf{vnil}/x],{\sigma }_s=[\mathsf{suc}(r)/n,\mathsf{vcons}(r,a,as)/x].$$ In the first branch $y:\mathsf{Vec}(B,\mathsf{0})$. The empty-constructor constraint for the second split is $$(\mathsf{0};y){\equiv }_{q:\mathbb{N};\mathsf{Vec}(B,q)}(\mathsf{0};\mathsf{vnil}).$$ Its index component $\mathsf{0}=\mathsf{0}$ is positive because the injectivity transition reduces equal nullary constructor heads to the empty constructor telescope; no reflexive-equation deletion is used. The element component then assigns $y:=\mathsf{vnil}$, giving ${\tau }_{00}=[\mathsf{vnil}/y]$. A $\mathsf{vcons}(q,b,bs)$ alternative gives $\mathsf{0}=\mathsf{suc}(q)$ and is removed by a conflict certificate.

In the successor branch $y:\mathsf{Vec}(B,\mathsf{suc}(r))$. Its empty alternative gives $\mathsf{suc}(r)=\mathsf{0}$ and is negative. Its successor alternative gives $\mathsf{suc}(r)=\mathsf{suc}(q)$; injectivity and solution yield $q:=r$. Here $r$ is an old frontier variable and $q$ is fresh from the second constructor telescope, so the canonical variable–variable orientation preserves $r$ and eliminates $q$. The forced-image matcher then consumes the freshly created $q$-cell: applying $q:=r$ compares its dot $.r$ with the forced image $r$, discharging $r\equiv r$. This gives $${\tau }_{ss}=[r/q,\mathsf{vcons}(r,b,bs)/y].$$ Put $$e_s:=\mathsf{vcons}(r,fab,\mathsf{zipWith}(A,B,C,f,r,as,bs)).$$ Omitting the two negative branches but retaining their certificates, the typed tree is as follows. Each split is keyed by a constructor name; its declared constructor telescope binds the variables used in that branch. Its judgmental leaf equations are the two written source clauses: All seven original telescope positions are therefore present in both leaf instances. The target has the type displayed in the exercise. The recursive call uses $as$, the direct child of the designated first vector; $bs$ is the corresponding second-vector child but is not the termination witness.

Put $D(x):={\mathsf{Id}}_A(a,x)$. Splitting $e:D(a)$ against reflexivity generates the homogeneous telescopic equality $$(a;e){\equiv }_{x:A;D(x)}(a;{\mathsf{refl}}_a).$$ Unfolding one telescope layer first presents the index component $a=a:A$; only after solving it could the dependent tail compare the transported $e$ with ${\mathsf{refl}}_a$. The neutral equation $a=a$ has neither a permitted solution step, since neither side is a unification variable, nor a permitted injectivity or conflict step. Deletion is outside the restricted unifier. The complete run is consequently the zero-step run ending at that same unsolved index component. In particular, it never reaches an assignment $e:={\mathsf{refl}}_a$. Compilation reports stuck unification.

Replacing the reflexivity pattern by $!$ asks the compiler to certify that no constructor is compatible. But ${\mathsf{refl}}_a:D(a)$ is a compatible constructor instance. Its full telescopic constraint is the one displayed above; the stuck neutral component is not a conflict certificate, so the absurd assertion is invalid.

The seven first results are as follows.

1. Complete Boolean negation succeeds: the $\mathsf{tt}$ and $\mathsf{ff}$ constraints are positive, and each specialized matrix has a leaf.

2. The sole $\mathsf{tt}$ clause reports uncovered constructor $\mathsf{ff}$. Its certificate is the positive path choosing $\mathsf{ff}$ together with the resulting empty specialized matrix.

3. The identity-family K clause reports stuck unification at the first component $a=a$ of $(a;e){\equiv }_{x:A;D(x)}(a;{\mathsf{refl}}_a)$.

4. Append with $.k$ reports an unforced inaccessible term. The positive vector constraint forces $\mathsf{suc}(k)$, whereas the row wrote $k$; the failed check is $\mathsf{suc}(k)\equiv k$.

5. The declaration $h(!)$ at $\mathbf{2}$ reports a reachable absurd pattern. Boolean constructors are enumerated in declaration order, so the first result is $\mathsf{badAbsurd}(1,\mathsf{tt},(\mathsf{tt}))$. The $\mathsf{ff}$ branch is positive as well, so no negative certificate required by $!$ exists. The practical corpus’s two-constructor list is an aggregate observation, not the mathematical compiler’s single first diagnostic.

6. The constructor pattern in $E$’s erased Boolean column is blocking, but that column is not a runtime split position. Compilation returns $\mathsf{badRelevance}(1,b)$, where $b$ names the erased binder.

7. For $F$, the first row initially selects the reflexivity column. Its positive unifier orients the old-variable equation as $a:=x$. The second row’s constructor cell $\mathsf{tt}$ at $a$ is therefore paired with the neutral forced image $x$, so the matcher suspends $\mathsf{tt}\mathsf{forcedBy}x$. The first row next selects its final $\mathsf{tt}$ cell. In the $\mathsf{ff}$ branch that row is deleted, the second row becomes first, and retrying the suspended task returns $\mathsf{stuckForce}(2,a,\mathsf{tt},x)$.

The coverage item reports a constructor path rather than a unifier certificate. The remaining failures expose, respectively, the unsolved equation, the forced-versus-written pair, the reachable constructors, the erased blocker, and the neutral forced image with its demanded head.