ch:typed-metaprogramming: ch:typed-metaprogramming

Let the caller’s printed $x$ carry scope set $S$. Expansion allocates fresh stamps $s_1,s_2\notin S$ and produces $$\mathsf{let}{x}^{S\cup \{s_1\}}=e_1\mathsf{in}\mathsf{let}{x}^{S\cup \{s_2\}}=e_2\mathsf{in}(x^{S\cup \{s_2\}},x^{S\cup \{s_1\}}).$$ Identifiers copied from $e_1,e_2$ retain their caller scopes. A free $x^S$ inside $e_1$ therefore resolves to the caller declaration: neither introduced binder has a scope set contained in $S$. The two generated references resolve respectively to the unique declarations whose scope sets are $S\cup \{s_2\}$ and $S\cup \{s_1\}$. Maximal-subset resolution is unique in all three cases.

For ${\mathrm{\Gamma }}_0=(c:\mathsf{Code}(\mathbb{N})@0)$, the complete tree is $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{(c:\mathsf{Code}(\mathbb{N})@0)\in {\mathrm{\Gamma }}_0}{{\mathrm{\Gamma }}_0{⊢}_{0}c:\mathsf{Code}(\mathbb{N})}}\mathrm{Q}-\mathrm{Var}}{{\mathrm{\Gamma }}_0{⊢}_1\mathsf{splice}(c):\mathbb{N}}}\mathrm{Q}-\mathrm{Splice}\\ {\displaystyle \frac{}{{\mathrm{\Gamma }}_0{⊢}_{1}1:\mathbb{N}}}\mathrm{Nat}\end{array}}{{\mathrm{\Gamma }}_0{⊢}_1\mathsf{splice}(c)+1:\mathbb{N}}}\mathrm{Add}}{{\mathrm{\Gamma }}_0{⊢}_0\mathsf{quote}(\mathsf{splice}(c)+1):\mathsf{Code}(\mathbb{N})}\mathrm{Q}-\mathrm{Quote}.$$ For ${\mathrm{\Gamma }}_1=(d:\mathsf{Code}(\mathbb{N})@1)$, the nested tree is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{(d:\mathsf{Code}(\mathbb{N})@1)\in {\mathrm{\Gamma }}_1}{{\mathrm{\Gamma }}_1{⊢}_{1}d:\mathsf{Code}(\mathbb{N})}}\mathrm{Q}-\mathrm{Var}}{{\mathrm{\Gamma }}_1{⊢}_2\mathsf{splice}(d):\mathbb{N}}}\mathrm{Q}-\mathrm{Splice}}{{\mathrm{\Gamma }}_1{⊢}_1\mathsf{quote}(\mathsf{splice}(d)):\mathsf{Code}(\mathbb{N})}}\mathrm{Q}-\mathrm{Quote}}{{\mathrm{\Gamma }}_1{⊢}_0\mathsf{quote}(\mathsf{quote}(\mathsf{splice}(d))):\mathsf{Code}(\mathsf{Code}(\mathbb{N}))}\mathrm{Q}-\mathrm{Quote}.$$ The phases are therefore $1$ at the variable premise, $2$ at the splice conclusion, $1$ at the inner quotation conclusion, and $0$ at the outer quotation conclusion. Finally, ${\mathrm{\Gamma }}_x=(x:\mathbb{N}@0)$ contains no declaration $x:\mathbb{N}@1$. Hence the attempted addition premise ${\mathrm{\Gamma }}_x{⊢}_{1}x:\mathbb{N}$ has no Q-Var derivation, so neither ${\mathrm{\Gamma }}_x{⊢}_{1}x+1:\mathbb{N}$ nor ${\mathrm{\Gamma }}_x{⊢}_0\mathsf{quote}(x+1):\mathsf{Code}(\mathbb{N})$ is derivable.

The analytical Boolean macro has the two clauses $$\mathsf{unliftBool}⟨\mathsf{tt}⟩\Rightarrow \mathsf{tt},\mathsf{unliftBool}⟨\mathsf{ff}⟩\Rightarrow \mathsf{ff}.$$ The first pattern judgment checks the quoted pattern at code type $\mathsf{Code}\mathbf{2}$ and returns the empty pattern environment; the second has the same input and output. Consequently both branches check at $\mathbf{2}$, so the whole match has result type $\mathbf{2}$. A pattern $⟨\lfloor y\rfloor ⟩$ is rejected because its body contains the splice form itself, whereas the pattern judgment matches only the simply typed fragment with $\mathsf{fix}$, not quotation or splicing forms. No pattern rule can derive a judgment for that body, regardless of the type assigned to $y$. Admitting it would require extending the pattern grammar, pattern reduction, and the source’s preservation proof.