Qualified types and dictionary evidence

For ${\mathrm{QTC}}_0$, The finite superclass graph is acyclic. Each primitive instance head begins with a constructor. Every premise is headed by a proper subterm of the result head. Resolution uses the finite effective table ${\mathcal{I}}^{\uparrow }$: for each primitive clause and each reachable superclass it contains the clause obtained by following the fixed shortest superclass path. Its builder is the primitive constructor followed by that path’s dictionary projection. For each requested class, all effective result heads must be pairwise nonunifiable. This check is performed after closure, so a direct $\mathsf{Eq}\mathsf{Int}$ clause is rejected when it would overlap the projection derived from $\mathsf{Ord}\mathsf{Int}$. An evidence context has distinct canonical keys. The fixed partial selector ${\mathsf{best}}_{\mathrm{\Delta }}$ chooses exact local evidence first. Otherwise it chooses the uniquely ordered shortest superclass projection. Resolution consists of exactly

${\mathsf{best}}_{\mathrm{\Delta }}(K\tau )=d$

${\mathsf{resolve}}_{\mathcal{C},\mathrm{\Delta }}(K\tau )=d$

${\mathsf{best}}_{\mathrm{\Delta }}(K\tau )\uparrow$${\mathsf{pick}}_{\mathcal{C}}(K\tau )=(P,b)$${\mathsf{resolve}}_{\mathcal{C},\mathrm{\Delta }}(p)=d_p(p\in P)$

${\mathsf{resolve}}_{\mathcal{C},\mathrm{\Delta }}(K\tau )=b{\overline{d}}_p$

The partial function $\mathsf{pick}$ freshens and one-way-matches the unique effective candidate; it is not symmetric unification.

Normalization ${\mathsf{nf}}_{\mathcal{C}}$ uses one fixed-priority agenda. It processes exact or projected local evidence before instances; allocates a fresh hole only for an unresolved variable-headed request; and expands an unresolved constructor request through its unique one-way-matching instance. Completed constructor frames install their evidence for later agenda requests. Duplicate goals share the first recorded evidence, and a retained subclass hole discharges its superclass holes. A missing constructor-headed instance rejects immediately. Its total result is $$\mathsf{reject}(p)\text{or}\mathsf{ok}(Q,\eta ),$$ where $Q$ is the ordered irredundant variable-headed hole set and $\eta$ reconstructs every input request jointly from those holes. The open sets $P$ and $Q$ have the same solvable ground instances. More exactly, if normalization returns $\mathsf{ok}(Q,\eta )$, then for every substitution $S$, normalizing $SP$ and $SQ$ rejects together or returns the same canonical set with commuting evidence templates. If canonical $R$ entails $SP$, then it entails $SQ$; this is the factorization direction used by principality. A source judgment is formed only with canonical $P$ and canonical, unambiguous schemes in $\mathrm{\Gamma }$. Its four rules are

$x:\sigma \in \mathrm{\Gamma }$$\sigma \succcurlyeq (Q\Rightarrow \tau )$$\mathcal{C};P⊩Q$

$\mathcal{C};P;\mathrm{\Gamma }⊢x:\tau$

$\mathcal{C};P;\mathrm{\Gamma },x:{\tau }_1⊢e:{\tau }_2$

$\mathcal{C};P;\mathrm{\Gamma }⊢\lambda x.e:{\tau }_1\to {\tau }_2$

$\mathcal{C};P_1;\mathrm{\Gamma }⊢e_1:{\tau }_1\to {\tau }_2$$\mathcal{C};P_2;\mathrm{\Gamma }⊢e_2:{\tau }_1$${\mathsf{nf}}_{\mathcal{C}}(P_1\cup P_2)=\mathsf{ok}(P,\eta )$

$\mathcal{C};P;\mathrm{\Gamma }⊢e_1{e}_2:{\tau }_2$

$\mathcal{C};P_1;\mathrm{\Gamma }⊢e_1:{\tau }_1$${\mathsf{Gen}}_{\mathcal{C}}(\mathrm{\Gamma };P_1;{\tau }_1)=(P_r,\sigma ,\zeta )$$\mathcal{C};P_2;\mathrm{\Gamma },x:\sigma ⊢e_2:{\tau }_2$${\mathsf{nf}}_{\mathcal{C}}(P_r\cup P_2)=\mathsf{ok}(P,\eta )$

$\mathcal{C};P;\mathrm{\Gamma }⊢\mathbf{let}x=e_1\mathbf{in}{e}_2:{\tau }_2$

Here generalization quantifies exactly the variables of the normalized predicates and result type that are not fixed by $\mathrm{\Gamma }$, retains the other canonical predicates as $P_r$, records the template $\zeta$, and requires $\mathsf{ftv}(Q)\subseteq \mathsf{ftv}({\tau }_1)$. Type substitution acts on an environment through the partial canonical action $S\star \mathrm{\Gamma }$: it freshens bound variables, substitutes only free variables, renormalizes each predicate interface, and records the induced evidence transport. Substitution naturality of normalization gives $T\star S\star \mathrm{\Gamma }=T\circ S\star \mathrm{\Gamma }$ up to fresh binders whenever both sides are defined, with alpha-equivalent composite evidence transports.

Qualified inference returns $W_{\mathcal{C}}(\mathrm{\Gamma },e)=(P,S,\tau )$. Writing ${\mathsf{cnf}}_{\mathcal{C}}(P)=Q$ for the successful canonical predicate component, its four clauses are:

1. a fresh instance $(Q^{\prime },{\tau }^{\prime })$ of $\mathrm{\Gamma }(x)$ returns $({\mathsf{cnf}}_{\mathcal{C}}(Q^{\prime }),\mathsf{id},{\tau }^{\prime })$;

2. an abstraction chooses fresh $a$, recursively obtains $(P,S,\tau )$ in $\mathrm{\Gamma },x:a$, and returns $(P,S,S(a)\to \tau )$;

3. an application obtains $(P_1,S_1,{\tau }_1)$, then $(P_2,S_2,{\tau }_2)$ in $S_1\star \mathrm{\Gamma }$, sets $U=\mathsf{mgu}(S_2{\tau }_1,{\tau }_2\to a)$, and returns $$({\mathsf{cnf}}_{\mathcal{C}}(U(S_2{P}_1\cup P_2)),U\circ S_2\circ S_1,U(a));$$

4. a let obtains $(P_1,S_1,{\tau }_1)$, generalizes it in $S_1\star \mathrm{\Gamma }$ to $(P_r,\sigma ,\zeta )$, then obtains $(P_2,S_2,{\tau }_2)$ in $S_1\star \mathrm{\Gamma },x:\sigma$, and returns $$({\mathsf{cnf}}_{\mathcal{C}}(S_2{P}_r\cup P_2),S_2\circ S_1,{\tau }_2).$$

Every failed normalization or ambiguity check rejects at its displayed clause; evidence templates are uniquely recomputed from the recorded W derivation rather than hidden in a fourth return component.

The evidence-explicit target core adds type and dictionary abstraction and application: The dictionary forms are typed by

$\mathrm{\Gamma },d:D⊢u:T$

$\mathrm{\Gamma }⊢\lambda \{d:D\}.u:D\to T$

$\mathrm{\Gamma }⊢u:D\to T$$\mathrm{\Gamma }⊢\delta :D$

$\mathrm{\Gamma }⊢u\{\delta \}:T$

Superclass edges and instances contribute For canonical $P$, let ${\mathrm{\Delta }}_P=d_p:p_D$ in canonical order. An evidence template $\eta$ acts by hole replacement $\eta \cdot u$, and a type substitution acts on core syntax and templates by $S^{†}u$. Elaboration is indexed by the successful W derivation $\mathcal{W}$. Its complete family is

$x:(\mathrm{\forall }\overline{\alpha }.Q\Rightarrow {\tau }_0;{\kappa }_x)\in \mathrm{\Gamma }$${\mathsf{resolve}}_{\mathcal{C},{\mathrm{\Delta }}_P}(\theta q)={\delta }_q(q\in Q)$

$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}x:\theta {\tau }_0⇝x[\theta \overline{\alpha }]\{({\theta }^{†}{\kappa }_x)({\overline{\delta }}_q)\}$

$a\text{ fresh}{W}_{\mathcal{C}}(\mathrm{\Gamma },x:a,e)=(P,S,\tau )$$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma },x:a{⊢}_D^{{\mathcal{W}}_0}e:\tau ⇝u$

$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}\lambda x.e:S(a)\to \tau ⇝\lambda x:|S(a)|.u$

$W_{\mathcal{C}}(\mathrm{\Gamma },e_1)=(P_1,S_1,{\tau }_1)\mathcal{C};{\mathrm{\Delta }}_{P_1};\mathrm{\Gamma }{⊢}_D^{{\mathcal{W}}_1}{e}_1:{\tau }_1⇝u_1$$W_{\mathcal{C}}(S_1\star \mathrm{\Gamma },e_2)=(P_2,S_2,{\tau }_2)\mathcal{C};{\mathrm{\Delta }}_{P_2};S_1\star \mathrm{\Gamma }{⊢}_D^{{\mathcal{W}}_2}{e}_2:{\tau }_2⇝u_2$$U=\mathsf{mgu}(S_2{\tau }_1,{\tau }_2\to a){\mathsf{nf}}_{\mathcal{C}}(U(S_2{P}_1\cup P_2))=\mathsf{ok}(P,\eta )$

$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}{e}_1{e}_2:U(a)⇝(\eta {|}_{U(S_2{P}_1)}\cdot U^{†}{S_2}^{†}{u}_1)(\eta {|}_{U(P_2)}\cdot U^{†}{u}_2)$

For let, if $\zeta :{\mathrm{\Delta }}_{P_r},{\mathrm{\Delta }}_Q{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{P_1}$ is the generalization template and $\eta :{\mathrm{\Delta }}_P{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{S_2{P}_r},{\mathrm{\Delta }}_{P_2}$, write ${\eta }_r,{\eta }_2$ for its restrictions and define

$W_{\mathcal{C}}(\mathrm{\Gamma },e_1)=(P_1,S_1,{\tau }_1)\mathcal{C};{\mathrm{\Delta }}_{P_1};\mathrm{\Gamma }{⊢}_D^{{\mathcal{W}}_1}{e}_1:{\tau }_1⇝u_1$${\mathsf{Gen}}_{\mathcal{C}}(S_1\star \mathrm{\Gamma };P_1;{\tau }_1)=(P_r,\mathrm{\forall }\overline{a}.Q\Rightarrow {\tau }_1,\zeta )$$W_{\mathcal{C}}(S_1\star \mathrm{\Gamma },x:\mathrm{\forall }\overline{a}.Q\Rightarrow {\tau }_1,e_2)=(P_2,S_2,{\tau }_2)$$\mathcal{C};{\mathrm{\Delta }}_{P_2};S_1\star \mathrm{\Gamma },x:\mathrm{\forall }\overline{a}.Q\Rightarrow {\tau }_1{⊢}_D^{{\mathcal{W}}_2}{e}_2:{\tau }_2⇝u_2$${\mathsf{nf}}_{\mathcal{C}}(S_2{P}_r\cup P_2)=\mathsf{ok}(P,\eta )$

$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}\mathbf{let}x=e_1\mathbf{in}{e}_2:{\tau }_2⇝u_{\mathsf{let}}$

The target environment is $|S\star \mathrm{\Gamma }|$, where $S$ is the substitution returned by $\mathcal{W}$. The exact top-level closure is $${\mathsf{close}}_{\mathcal{C}}(e)=\mathrm{\Lambda }\overline{a}.\lambda \{{\overline{d}}_Q:|Q|\}.\zeta \cdot u$$ when W at the empty environment succeeds, generalization returns no residual predicates, and $u$ is the displayed W-indexed elaboration. Missing ground evidence or ambiguity rejects closure. The evidence-core roots are ordinary, type, dictionary, and let beta under call-by-value compatible closure. Brace erasure has forward step simulation and existential reverse lifting; it is not injective.

For the explicitly typed ground compatibility exercises, retain the annotated forms $$s::=\cdots \mid \mathsf{eq}[A](s_1,s_2)\mid (KA\Rightarrow s)\mid s⟨K,A⟩.$$ They specialize the preceding ${\mathrm{QTC}}_0$ elaboration rather than forming a second inference calculus. A finite ground table $\mathrm{\Sigma }$ and a local evidence map $\mathrm{\Psi }$ each contain at most one entry per normalized class/type key, and ${\mathsf{resolve}}_{\mathrm{\Psi },\mathrm{\Sigma }}$ tries the local map before the table. The three annotated rules are

${\mathsf{resolve}}_{\mathrm{\Psi },\mathrm{\Sigma }}(\mathsf{Eq},A)=d$$\mathrm{\Psi };\mathrm{\Sigma }⊢s_i⇝e_i(i=1,2)$

$\mathrm{\Psi };\mathrm{\Sigma }⊢\mathsf{eq}[A](s_1,s_2)⇝d{e}_1{e}_2$

$d\text{ fresh}$$\mathrm{\Psi }[(K,A)\mapsto d];\mathrm{\Sigma }⊢s⇝e$

$\mathrm{\Psi };\mathrm{\Sigma }⊢(KA\Rightarrow s)⇝\lambda d:K_D(A).e$

$\mathrm{\Psi };\mathrm{\Sigma }⊢s⇝e$${\mathsf{resolve}}_{\mathrm{\Psi },\mathrm{\Sigma }}(K,A)=d$

$\mathrm{\Psi };\mathrm{\Sigma }⊢s⟨K,A⟩⇝ed$

The bounded associated-type extension ${\mathrm{ATS}}_0$ adds saturated synonym applications and equality constraints: Entailment $\mathrm{\Theta }⊩\pi$ includes class specialization and modus ponens together with reflexivity, symmetry, transitivity, and congruence for equality. The distinctive rules and algorithmic judgment are $$\frac{\mathrm{\Theta }⊩\mathsf{Collects}\tau }{\mathrm{\Theta }⊢\mathsf{Elem}\tau \mathsf{type}}\mathrm{AT}-\mathrm{WF}\frac{\begin{array}{c}\mathrm{\Theta }\mid \mathrm{\Gamma }⊢e:{\tau }_1\\ \mathrm{\Theta }⊩{\tau }_1={\tau }_2\end{array}}{\mathrm{\Theta }\mid \mathrm{\Gamma }⊢e:{\tau }_2}\mathrm{AT}-\mathrm{Conv},$$ $$\mathrm{\Theta },U\mid T\mathrm{\Gamma }{⊢}_{\mathsf{W}}e:\tau .$$ The last judgment returns class constraints, pending equality constraints, a substitution, and a monotype. Its imported soundness endpoint is theorem 13.23; no completeness or principality result is attached to this extension. Its exact admission conditions also require specific nonoverlapping constructor-headed instances, decreasing contexts, saturated synonym applications, the designated variable-headed form for programmer equality constraints, and the two fixed-variable checks stated in section 13.4. The source paper omits its evidence rules; the displayed dictionary/type-passing instance in the chapter is the book’s local target sketch.

The separately imported COCHIS comparison uses predicative types, monotypes, terms, and contexts Only monotypes instantiate $\mathrm{\forall }$. Its resolution judgments are The load-bearing recursive rules are

$\mathsf{tyvars}(\mathrm{\Delta });\mathrm{\Delta }{⊢}_{\mathsf{f}}[\rho ]⇝E$

$\mathrm{\Delta }{⊢}_{\mathsf{r}}\rho ⇝E$

$A;\mathrm{\Delta },?{\rho }_1:z{⊢}_{\mathsf{f}}[{\rho }_2]⇝E$$z\text{ fresh}$

$A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[{\rho }_1\Rightarrow {\rho }_2]⇝\lambda z:|{\rho }_1|.E$

$A;\mathrm{\Delta };[\mathrm{\Delta }]{⊢}_{\mathsf{l}}\tau ⇝E$

$A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[\tau ]⇝E$

$\mathrm{\Delta };[\rho ];x{⊢}_{\mathsf{m}}\overline{\rho };\overline{z};\tau ⇝E$$A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[\overline{\rho }]⇝\overline{E}$

$A;\mathrm{\Delta };[{\mathrm{\Delta }}^{\prime },?\rho :x]{⊢}_{\mathsf{l}}\tau ⇝E[\overline{E}/\overline{z}]$

$\mathsf{stable}(A;\mathrm{\Delta };\rho ;x;\tau )$$A;\mathrm{\Delta };[{\mathrm{\Delta }}^{\prime }]{⊢}_{\mathsf{l}}\tau ⇝E$

$A;\mathrm{\Delta };[{\mathrm{\Delta }}^{\prime },?\rho :x]{⊢}_{\mathsf{l}}\tau ⇝E$

$\mathrm{\Delta };[\tau ];x{⊢}_{\mathsf{m}}\varnothing ;\varnothing ;\tau ⇝x$

$\mathrm{\Delta },?{\rho }_1:z;[{\rho }_2];xz{⊢}_{\mathsf{m}}\overline{\rho };\overline{z};\tau ⇝E$$z\text{ fresh}$

$\mathrm{\Delta };[{\rho }_1\Rightarrow {\rho }_2];x{⊢}_{\mathsf{m}}{\rho }_1,\overline{\rho };z,\overline{z};\tau ⇝E$

$\mathrm{\Delta }⊢\sigma$$\mathrm{\Delta };[\rho [\sigma /\alpha ]];x[\sigma ]{⊢}_{\mathsf{m}}\overline{\rho };\overline{z};\tau ⇝E$

$\mathrm{\Delta };[\mathrm{\forall }\alpha .\rho ];x{⊢}_{\mathsf{m}}\overline{\rho };\overline{z};\tau ⇝E$

Quantifier matching instantiates $[\mathrm{\forall }\alpha .\rho ];x$ to $[\rho [\sigma /\alpha ]];x[\sigma ]$ when $\mathrm{\Delta }⊢\sigma$, then continues matching. The unambiguity predicate is The valid-substitution judgment $\mathsf{valid}(A;\mathrm{\Delta };\theta )$ extends by the singleton substitution $[\sigma /\alpha ]$ only when $\alpha \in A$, $\mathrm{\Delta }={\mathrm{\Delta }}_0,\alpha ,{\mathrm{\Delta }}_1$, $\sigma$ is well scoped in ${\mathrm{\Delta }}_0$, and the remainder is valid in $({\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1)[\sigma /\alpha ]$. Finally, $\mathsf{stable}(A;\mathrm{\Delta };\rho ;x;\tau )$ excludes every such valid substitution under which the skipped $\rho$ would match $\tau$. This card reproduces the comparison’s recursive evidence plumbing; the complete systems and remaining premises are source-cited to Figs. 2 and 6–10 in the chapter.