Qualified Types, Type Classes, and Coherent Dictionary Elaboration

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A class names a collection of operations indexed by a type; its operations are its methods. An instance implements those operations at a particular type constructor. At run time the implementation is carried by a dictionary, an ordinary record of method values. A superclass edge requires every dictionary for the subclass to carry a dictionary for the superclass. These meanings govern the motivating example as well as the calculus below.

The term $$\mathsf{same}:=\lambda x.\mathsf{eq}xx$$ is the smallest obstruction. Hindley–Milner can assign $\mathrm{\forall }A.A\to \mathsf{Bool}$ when eq is itself assigned the scheme $\mathrm{\forall }A.A\to A\to \mathsf{Bool}$. Parametricity then makes that assignment too strong: a parametric function at the latter scheme is constant. Given $(a_1,a_2)\in A^2$ and $(b_1,b_2)\in B^2$, use the relation $R=\{(a_1,b_1),(a_2,b_2)\}$; parametricity relates the two Boolean results by Boolean equality. Since both pairs were arbitrary, all results agree. Real equality is not constant. Conversely, if a caller may silently choose either the usual integer equality dictionary or a dictionary that always returns false, same 0 has two answers. A useful account of overloading must therefore say both where an operation comes from and why its choice is stable.

One finite qualified-type calculus

Typing $\mathsf{same}$ generates a class request $\mathsf{Eq}\alpha$; entailment constructs the dictionary passed to $\mathsf{eq}$. These class requests are distinct from the row lacks predicates of chapter 4.

For example, a superclass edge from $\mathsf{Ord}$ to $\mathsf{Eq}$ requires every $\mathsf{Ord}$ dictionary to contain an $\mathsf{Eq}$ dictionary. Thus an $\mathsf{Ord}\mathsf{Int}$ instance determines both integer order and integer equality; the projections below make that containment explicit.

Call the calculus ${\mathrm{QTC}}_0$. Its monotypes, predicates, and schemes are Class names are unary. Predicate sets are finite, not multisets. A class environment $\mathcal{C}=(\mathcal{S},\mathcal{I})$ contains

1. a finite acyclic superclass graph $\mathcal{S}$; and

2. finitely many primitive instance clauses $P\Rightarrow K(C\overline{\tau })$, where $C$ is a type constructor, every premise is headed by a proper subterm of $C\overline{\tau }$, and no two instance heads for the same class unify.

Without superclass closure, substitution can change which dictionary should be selected. If $\mathsf{Ord}$ has superclass $\mathsf{Eq}$ and the only primitive clauses are $$\mathsf{Ord}\mathsf{Int},\mathsf{Ord}\alpha \Rightarrow \mathsf{Ord}(\mathsf{List}\alpha ),$$ then substituting $\alpha :=\mathsf{Int}$ turns an $\mathsf{Eq}(\mathsf{List}\alpha )$ request into a projection from a constructible $\mathsf{Ord}$ dictionary, although the unclosed table has no matching $\mathsf{Eq}$ clause. The missing derived projection is the reason for closing the table before resolution.

Resolution uses the finite effective table ${\mathcal{I}}^{\uparrow }$. Fix a total order on class names and, at each class, on its outgoing superclass edges. Paths are ordered first by length and then lexicographically by those edge orders. For every primitive clause $i:P\Rightarrow K^{\prime }(C\overline{\tau })$ and every superclass $K$ reachable from $K^{\prime }$, including $K^{\prime }$ itself, choose the fixed shortest class/path-order path and add $$i^K:P\Rightarrow K(C\overline{\tau }).$$ Its evidence builder is the primitive constructor followed by the path projection, made explicit below. The empty path is the identity. After this closure, no two effective result heads for the same requested class may unify. Checking nonoverlap only in the primitive table is insufficient: a direct $\mathsf{Eq}\mathsf{Int}$ clause would overlap the derived projection of an $\mathsf{Ord}\mathsf{Int}$ clause. Rejecting that pair, rather than choosing between possibly different dictionaries, is what makes normalization substitution-stable without assuming class laws. Superclass closure is finite because the class graph and primitive table are finite.

There are no variable-headed instances, uncontrolled overlap, local instances, or class defaults. These restrictions are a termination and coherence policy: for one source program, every selected elaboration constructs the same evidence up to alpha-equivalence. This is not a claim about production Haskell. Our running environment ${\mathcal{C}}_0$ is In particular, it has no $\mathsf{Show}\mathsf{Bool}$ instance. The two source methods have the schemes $$\mathsf{eq}:\mathrm{\forall }\alpha .\mathsf{Eq}\alpha \Rightarrow \alpha \to \alpha \to \mathsf{Bool},\mathsf{show}:\mathrm{\forall }\alpha .\mathsf{Show}\alpha \Rightarrow \alpha \to \mathsf{String}.$$

Entailment constructs evidence

For each class, fix an ordinary target dictionary type. The examples use For the running table, fix target constants $$\mathsf{ordInt}:{\mathsf{Ord}}_D(\mathsf{Int}),\mathsf{eqList}:\mathrm{\forall }A.{\mathsf{Eq}}_D(A)\to {\mathsf{Eq}}_D(\mathsf{List}A).$$ If primitive instance $i$ has constructor $c_i$ and the chosen path runs from subclass $K^{\prime }$ to superclass $K$, write ${\pi }_{K,K^{\prime }}:K_D^{\prime }(A)\to K_D(A)$ for its dictionary projection. The effective candidate’s builder is $$b_{i^K}\overline{d}={\pi }_{K,K^{\prime }}(c_i\overline{d}).$$ For the empty path, ${\pi }_{K,K}$ is the identity. For the displayed product representation of ${\mathsf{Ord}}_D$, the abstract projection ${\pi }_{\mathsf{Eq},\mathsf{Ord}}$ is the ordinary first projection ${\pi }_1$. Thus ${\pi }_1\mathsf{ordInt}$ and $\mathsf{eqList}({\pi }_1\mathsf{ordInt})$ are not additional resolution oracles: they are the two instance builders just declared.

Proof of Lemma 11.1 — Resolution terminates and is functional

Proof. Every recursive resolution call is an effective-instance-premise call. Its type is a proper subterm of the matched head because superclass closure changes only the result class and evidence builder, never the primitive premises. Type size therefore decreases strictly. The selector ${\mathsf{best}}_{\mathrm{\Psi }}$ computes a superclass path by a finite scan of the finite acyclic hierarchy; it does not make a recursive resolution call. Hence neither phase admits an infinite call chain.

For functionality, ${\mathsf{best}}_{\mathrm{\Psi }}$ is a partial function: exact lookup is unique because $\mathrm{\Psi }$ has distinct keys, and the fixed length/class/path order selects one superclass projection. Its definedness also makes E-Local and E-Instance mutually exclusive. Otherwise ${\mathsf{pick}}_{\mathcal{C}}$ is a partial function because the fully closed effective heads do not unify. One-way matching is preserved by type substitution. The induction hypotheses uniquely determine all premise evidence. Evidence typing follows in the same induction: a projection has the declared superclass dictionary type, and each effective builder is a well-typed projection of a primitive instance constructor consuming exactly its premise dictionaries. ◻

Canonical predicates, generalization, and ambiguity

Proof of Lemma 11.2 — Canonicalization

Proof. Termination and determinism. Every premise placed below a constructor frame has a proper-subterm type, so frame depth is bounded by the size of its root request. The initial set and every premise list are finite; consequently the agenda is finite. Nonunifiability of the fully closed effective heads gives one candidate and matcher. The fixed agenda and sibling orders remove every remaining choice. Thus the procedure returns one success or the first fixed-priority rejection.

Replay soundness. Induct on the height of the finite completed-frame tree, visiting children before their parent. If a completed frame $F$ has retained holes $Q_F$, the induction property is: for every request $p$ in the subtree rooted at $F$ there is a selected term $${\mathrm{\Delta }}_{Q_F}⊢{\eta }_F(p):p_D,{\eta }_F(p)[S][\overline{d}/Q_F[S]]{=}_{\alpha }{\mathsf{replay}}_{F[S]}(p[S]).$$ Applying $S$ and replacing each substituted hole by its recorded evidence therefore gives exactly the replayed evidence. The property is simultaneous for all recorded requests. A fresh variable-headed hole is its own evidence. A completed constructor frame is derivable from its recorded premise evidence; installing it in $\mathrm{\Psi }$ merely shares that derivation with later goals. In the superclass case, suppose the selected effective clause comes from $i:P\Rightarrow K^{\prime }(C\overline{\tau })$ and path projection ${\pi }_{K,K^{\prime }}$. For premise evidence $\overline{d}$, both direct replay and replay after substitution construct ${\pi }_{K,K^{\prime }}(i\overline{d}):K_D(C\overline{\tau })$. Effective nonoverlap is stable under substitution, so replay cannot change the selected clause. Duplicate sharing preserves the conjunction, and superclass-hole removal preserves it because a retained subclass dictionary projects to the removed superclass dictionary. Composing the recorded builders and projections gives $\eta$ and proves $\mathcal{C};Q⊩P$.

Naturality. For naturality, induct simultaneously on the two replay trees for $P[S]$ and $Q[S]$, using the maximum remaining height. A substituted variable-headed hole either remains a hole or becomes a constructor request; in the latter case both runs select the same effective clause. A constructor frame replays that clause and applies the induction hypotheses to its proper-subterm premises. If substitution merges two formerly distinct holes, duplicate sharing maps both occurrences to the first recorded evidence, so no lockstep bijection between old holes is required. Finally, if one substituted hole becomes a superclass consequence of another, the fixed projection replaces it on both runs. When the subclass dictionary is $i\overline{d}$, both runs record ${\pi }_{K,K^{\prime }}(i\overline{d})$ from the same primitive premises. These cases also show that a missing constructor candidate occurs on both sides. Hence both runs reject together or finish with the same ordered holes $R$, and their evidence templates commute as stated. With a grounding substitution and empty evidence context, this is ground equivalence.

Irredundancy and rejection. At the end, distinct members of $Q$ are variable-headed and no member is a superclass consequence of the others. Effective instances cannot match a variable-headed request. Therefore removing any member leaves that request underivable from the remainder. In the rejection case, the absence of a selected effective constructor-headed candidate leaves neither a global derivation nor an admissible constructor-headed local assumption. ◻

Proof of Lemma 13.8 — Canonical factorization

Proof. Fix selected entailment derivations of every root request in $P[S]$ from $R_0$. Descend each completed frame tree from its root toward its retained holes, inducting on the maximum remaining frame height. At a constructor frame, the root request cannot be discharged by an exact entry of the canonical set $R_0$, whose entries are variable headed. If it were discharged by a superclass projection from such an entry, its head would still be variable headed. Its selected derivation must therefore use an effective instance clause. Nonoverlap forces that clause to be the one recorded in the frame; invert the selected derivation to obtain selected derivations of the proper-subterm premises, and continue downward. At a retained hole, the selected derivation reached by this inversion is evidence for the corresponding member of $Q[S]$. If $S$ identifies two holes, duplicate sharing keeps the first selected derivation and directs both occurrences to it. Every retained hole is therefore entailed by $R_0$, which is the displayed entailment. ◻

Without superclass closure, naturality and canonical factorization are false. Let $\mathsf{Ord}$ have superclass $\mathsf{Eq}$ and take only the primitive instances $$\mathsf{Ord}\mathsf{Int},\mathsf{Ord}\alpha \Rightarrow \mathsf{Ord}(\mathsf{List}\alpha ).$$ Normalizing $\{\mathsf{Ord}(\mathsf{List}\alpha ),\mathsf{Eq}\beta \}$ without the derived projected clause retains $\{\mathsf{Ord}\alpha ,\mathsf{Eq}\beta \}$. After $\alpha :=\mathsf{Int}$ and $\beta :=\mathsf{List}\mathsf{Int}$, the original set is jointly solvable by constructing $\mathsf{Ord}(\mathsf{List}\mathsf{Int})$ and projecting, while the retained set is not. In ${\mathcal{I}}^{\uparrow }$ the derived clause $$\mathsf{Ord}\alpha \Rightarrow \mathsf{Eq}(\mathsf{List}\alpha )$$ builds the missing projection, so both sides succeed.

Let $\mathsf{ftv}$ denote free type variables. Given $\mathrm{\Gamma }$, $P$, and $\tau$, first compute ${\mathsf{nf}}_{\mathcal{C}}(P)$. If it rejects, generalization rejects at the same request; in particular, $\mathsf{Show}\mathsf{Bool}$ cannot become a silent residual. Otherwise let the result be $\mathsf{ok}(P^0,\eta )$ and put $$A=\mathsf{ftv}(P^0,\tau )\setminus \mathsf{ftv}(\mathrm{\Gamma }).$$ Every member of $P^0$ has the form $K\alpha$, so place it in $P_g$ when $\alpha \in A$ and in $P_r$ otherwise. This gives the disjoint, exhaustive split $P^0=P_g\uplus P_r$. Define Because $P_g$ is a subset of the already canonical variable-headed set $P^0$, this second normalization returns $Q=P_g$ and the identity template. It is retained deliberately so every generalization boundary calls the same checked interface, rather than relying on an unchecked invariant in an implementation. Here $\zeta$ composes the two normalization templates and witnesses $$\mathcal{C};P_r,Q⊩P.$$ The residual $P_r$ remains at the enclosing binding. A scheme is unambiguous when $$\mathsf{ftv}(Q)\subseteq \mathsf{ftv}(\tau ).$$ Thus the first scheme below is rejected because its result does not determine $A$; the second is unambiguous: $$\mathrm{\forall }A.\mathsf{Show}A\Rightarrow \mathsf{String},\mathrm{\forall }A.\mathsf{Eq}A\Rightarrow A\to \mathsf{Bool}.$$ The final step of ${\mathsf{Gen}}_{\mathcal{C}}$ checks this inclusion and rejects the binding when it fails.

Canonicality is checked when a binding enters an environment; it is not a claim that raw textual substitution preserves a predicate list. We use the global postfix action $\tau [S]$ and left-to-right composition $S;T$, characterized by $\tau [S;T]=\tau [S][T]$. Define the canonical action $S\star \mathrm{\Gamma }$ pointwise. Freshen a binding $x:\mathrm{\forall }\overline{a}.P\Rightarrow \tau$ away from $S$, apply $S$ only to its free variables, and compute $${\mathsf{nf}}_{\mathcal{C}}(P[S])=\mathsf{ok}(Q,{\kappa }_x).$$ The resulting binding is $x:\mathrm{\forall }\overline{a}.Q\Rightarrow \tau [S]$, annotated by the transport ${\kappa }_x:{\mathrm{\Delta }}_Q{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{P[S]}$. The action is undefined if normalization or the ambiguity check rejects. For example, specializing $x:\mathsf{Eq}\alpha \Rightarrow \alpha \to \mathsf{Bool}$ at $\alpha :=\mathsf{Int}$ removes the predicate and records the global Eq Int evidence projected from Ord Int; it does not leave a noncanonical ground predicate in the environment. One wants $T\star S\star \mathrm{\Gamma }$ and $S;T\star \mathrm{\Gamma }$ the same intended composite, but determinism alone does not prove that claim. We use $S\star \mathrm{\Gamma }$ only when this action succeeds. Its target translation $(S\star \mathrm{\Gamma }{)}^D$ retains the substituted prior interface $P[S]\Rightarrow \tau [S]$ for each free target variable; ${\kappa }_x$ converts evidence for the canonical source view $Q$ to that interface at each use.

Proof of Lemma 13.9 — Canonical environment actions compose

Proof. Work bindingwise after one common freshening of its quantified variables. If normalizing $P[S]$ yields $Q$ with transport $\kappa$, the substitution clause of lemma 11.2 says that normalizing $Q[T]$ and normalizing $P[S;T]$ return the same canonical predicate set. Its commuting template clause equates the sequential transport with the direct transport. Ordinary type components agree because substitution composes. Repeating this argument over the finite environment proves the result; the ambiguity checks inspect the same final scheme and therefore agree as well. ◻

Qualified typing and inference

The source term grammar is the HM grammar. Its declarative judgment is $$\mathcal{C};P;\mathrm{\Gamma }⊢e:\tau .$$ It is formed only when ${\mathsf{nf}}_{\mathcal{C}}(P)=\mathsf{ok}(P,\mathsf{id})$ and each scheme was admitted canonically and unambiguously when its binding entered $\mathrm{\Gamma }$. Subsequent type substitution acts through $S\star \mathrm{\Gamma }$, not by raw substitution, using convention 13.6. The structural rules for variables, abstractions, applications, and let are as follows. $$\frac{\begin{array}{c}x:\sigma \in \mathrm{\Gamma }\\ \sigma \succcurlyeq (Q\Rightarrow \tau )\\ \mathcal{C};P⊩Q\end{array}}{\mathcal{C};P;\mathrm{\Gamma }⊢x:\tau }\mathrm{Q}-\mathrm{Var}$$ $$\frac{\mathcal{C};P;\mathrm{\Gamma },x:{\tau }_1⊢e:{\tau }_2}{\mathcal{C};P;\mathrm{\Gamma }⊢\lambda x.e:{\tau }_1\to {\tau }_2}\mathrm{Q}-\mathrm{Lam}$$ $$\frac{\begin{array}{c}\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 )\end{array}}{\mathcal{C};P;\mathrm{\Gamma }⊢e_1{e}_2:{\tau }_2}\mathrm{Q}-\mathrm{App}$$ $$\frac{\begin{array}{c}\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 )\end{array}}{\mathcal{C};P;\mathrm{\Gamma }⊢\mathbf{let}x=e_1\mathbf{in}{e}_2:{\tau }_2}\mathrm{Q}-\mathrm{Let}.$$ In Q-Var, $\sigma \succcurlyeq (Q\Rightarrow \tau )$ means instantiate the quantified variables and then discharge the instantiated scheme predicates from $Q$. Thus this chapter-local occurrence has a qualified type on the right, unlike the HM monotype-instance relation of chapter 3. The three-place occurrence $\mathcal{C};P⊩Q$ is likewise the class-environment-indexed evidence relation defined above, not the two-place row entailment. For a concrete derivation, take $${\mathrm{\Gamma }}_0(\mathsf{eq})=\mathrm{\forall }\alpha .\mathsf{Eq}\alpha \Rightarrow \alpha \to \alpha \to \mathsf{Bool}.$$ Identify a monotype $\alpha$ in $\mathrm{\Gamma }$ with the scheme $\mathrm{\forall }\varnothing .\varnothing \Rightarrow \alpha$. Then the first new judgment is exercised in full: $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\mathrm{\Gamma }}_0(\mathsf{eq})=\mathrm{\forall }\beta .\mathsf{Eq}\beta \Rightarrow \beta \to \beta \to \mathsf{Bool}\\ (\mathsf{Eq}\beta \Rightarrow \beta \to \beta \to \mathsf{Bool})[\alpha /\beta ]=\mathsf{Eq}\alpha \Rightarrow \alpha \to \alpha \to \mathsf{Bool}\\ {\mathcal{C}}_0;\{\mathsf{Eq}\alpha \}⊩\{\mathsf{Eq}\alpha \}\end{array}}{{\mathcal{C}}_0;\{\mathsf{Eq}\alpha \};{\mathrm{\Gamma }}_0,x:\alpha ⊢\mathsf{eq}:\alpha \to \alpha \to \mathsf{Bool}}}\mathrm{Q}-\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}x:(\varnothing \Rightarrow \alpha )\in {\mathrm{\Gamma }}_0,x:\alpha \\ {\mathcal{C}}_0;\varnothing ⊩\varnothing \end{array}}{{\mathcal{C}}_0;\varnothing ;{\mathrm{\Gamma }}_0,x:\alpha ⊢x:\alpha }}\mathrm{Q}-\mathrm{Var}\end{array}}{{\mathcal{C}}_0;\{\mathsf{Eq}\alpha \};{\mathrm{\Gamma }}_0,x:\alpha ⊢\mathsf{eq}x:\alpha \to \mathsf{Bool}}}\mathrm{Q}-\mathrm{App}\\ {\displaystyle \frac{\begin{array}{c}x:(\varnothing \Rightarrow \alpha )\in {\mathrm{\Gamma }}_0,x:\alpha \\ {\mathcal{C}}_0;\varnothing ⊩\varnothing \end{array}}{{\mathcal{C}}_0;\varnothing ;{\mathrm{\Gamma }}_0,x:\alpha ⊢x:\alpha }}\mathrm{Q}-\mathrm{Var}\end{array}}{{\mathcal{C}}_0;\{\mathsf{Eq}\alpha \};{\mathrm{\Gamma }}_0,x:\alpha ⊢\mathsf{eq}xx:\mathsf{Bool}}}\mathrm{Q}-\mathrm{App}}{{\mathcal{C}}_0;\{\mathsf{Eq}\alpha \};{\mathrm{\Gamma }}_0⊢\lambda x.\mathsf{eq}xx:\alpha \to \mathsf{Bool}}\mathrm{Q}-\mathrm{Lam}.$$

Qualified Algorithm W

Qualified inference returns predicates as well as an HM substitution and type: $$W_{\mathcal{C}}(\mathrm{\Gamma },e)=(P,S,\tau ).$$ It uses the same most-general unifier as chapter 3. Its clauses use the postfix action and left-to-right composition fixed above. The brackets $A[B/\alpha ]$ still denote one capture-avoiding substitution. Write ${\mathsf{cnf}}_{\mathcal{C}}(P)=Q$ when ${\mathsf{nf}}_{\mathcal{C}}(P)=\mathsf{ok}(Q,\eta )$ for the uniquely determined $\eta$; if normalization rejects, W rejects at that clause. The mathematical W triple discards $\eta$; its derivation records the normalization call, and the elaborator below recomputes the unique template.

1. For $x$, fresh-instantiate $\mathrm{\Gamma }(x)=\mathrm{\forall }\overline{\alpha }.Q\Rightarrow \tau$ to $(Q^{\prime },{\tau }^{\prime })$ and return $({\mathsf{cnf}}_{\mathcal{C}}(Q^{\prime }),\mathsf{id},{\tau }^{\prime })$.

2. For $\lambda x.e$, choose fresh $a$, compute $W_{\mathcal{C}}(\mathrm{\Gamma },x:a,e)=(P,S,\tau )$, and return $(P,S,a[S]\to \tau )$.

3. For $e_1{e}_2$, compute $(P_1,S_1,{\tau }_1)$ for $e_1$, then $(P_2,S_2,{\tau }_2)$ for $e_2$ in $S_1\star \mathrm{\Gamma }$. With fresh $a$, let $U=\mathsf{mgu}({\tau }_1[S_2],{\tau }_2\to a)$ and return $$({\mathsf{cnf}}_{\mathcal{C}}((P_1[S_2]\cup P_2)[U]),S_1;S_2;U,a[U]).$$

4. For $\mathbf{let}x=e_1\mathbf{in}{e}_2$, compute $(P_1,S_1,{\tau }_1)$, then ${\mathsf{Gen}}_{\mathcal{C}}(S_1\star \mathrm{\Gamma };P_1;{\tau }_1)=(P_r,\sigma ,\zeta )$, and $(P_2,S_2,{\tau }_2)$ for $e_2$ in $S_1\star \mathrm{\Gamma },x:\sigma$. Return $$({\mathsf{cnf}}_{\mathcal{C}}(P_r[S_2]\cup P_2),S_1;S_2,{\tau }_2).$$

The earlier example follows the first three clauses: eq contributes $\mathsf{Eq}a\Rightarrow a\to a\to \mathsf{Bool}$; each occurrence of x unifies with $a$; canonicalization leaves $\{\mathsf{Eq}a\}$; abstraction returns $\mathsf{Eq}a\Rightarrow a\to \mathsf{Bool}$.

Proof of Lemma 11.3 — The generalization split is maximal

Proof. The set $A$ contains exactly the variables not fixed by $\mathrm{\Gamma }$. Successful normalization leaves only variable-headed requirements, removing the empty-variable case. Hence every residual is exactly $K\alpha$, with $\alpha \in A$ or $\alpha \in \mathsf{ftv}(\mathrm{\Gamma })$. The two comprehensions are therefore disjoint, exhaustive, and forced. ◻

Proof of Lemma 13.11 — Declarative typing is stable under canonical substitution

Proof. Induct on the displayed typing derivation. In Q-Var, substitute the scheme instance and its selected entailment. Naturality of lemma 11.2 and lemma 13.8 replace the substituted predicate lists by their canonical forms. The abstraction case extends the canonical action by $x:{\tau }_1[S]$. In Q-App, apply the induction hypotheses to both premises and normalize the union; naturality identifies this result with $Q$. In Q-Let, apply the first induction hypothesis, then canonicalize and factor its generalized predicate list to rebuild the substituted scheme. Apply the second induction hypothesis under that scheme, canonicalize the residual list, and use naturality to identify the combined normal form with $Q$; Q-Let then rebuilds the conclusion. Freshening the quantified variables away from $S$ preserves the free-variable side condition. These are all four rules. ◻

Proof of Theorem 11.4 — Inference soundness

Proof. By induction on $e$. For a variable, fresh instantiation and canonicalization give exactly Q-Var. For an abstraction, the induction hypothesis types the body under $S\star \mathrm{\Gamma },x:a[S]$; Q-Lam discharges $x$. For an application, apply lemma 13.11 with $U$ to both induction hypotheses. The MGU equation ${\tau }_1[S_2][U]=({\tau }_2\to a)[U]$ says both operands have the common domain ${\tau }_2[U]$; Q-App combines the transported predicates. For let, the induction hypothesis for $e_1$ and lemma 11.3 justify the exact scheme and residual predicates used by Q-Let; the second induction hypothesis types $e_2$, and final canonicalization combines $P_r[S_2]$ with $P_2$. ◻

Say that $Q\Rightarrow \rho$ is a qualified instance of $P\Rightarrow \tau$ when some substitution $T$ satisfies $\tau [T]=\rho$ and $\mathcal{C};Q⊩P[T]$.

Proof of Theorem 11.5 — Success and principality for QTC_0

Proof. Induct on the declarative typing derivation, generalized over the base environment $\mathrm{\Gamma }$ and its action $R$. The induction claim includes success: W terminates at the corresponding syntax and returns $(P,S,\tau )$; there is then a substitution $T$ satisfying all three displayed conclusions. Thus an induction hypothesis licenses the next recursive call rather than assuming that call has returned.

Canonicalization needs a direction not carried by its output template. If W normalizes an input predicate set $P_{\mathrm{in}}$ to $P$, the template gives $P⊩P_{\mathrm{in}}$. Principality instead needs to derive $P[T]$ from a declarative entailment of $P_{\mathrm{in}}[T]$. Every use below of a final normalization therefore invokes lemma 13.8.

Variable. Fresh instantiation always returns. Rename its variables away from the declarative instance. The substitution witnessing the declarative instance factors through that fresh renaming; canonical factorization proves the returned predicate entailment. Its restriction to the environment variables is $R$, so the canonical environments agree.

Abstraction. The premise induction hypothesis makes the body call succeed. Extend its factor by sending W’s fresh argument variable to the declarative domain. This gives the arrow equality, leaves the predicate entailment unchanged, and the extended canonical-environment equation discharges the bound variable.

Application. Inversion gives premise types $B\to \rho$ and $B$. The two induction hypotheses make W’s calls return $(P_1,S_1,{\tau }_1)$ and $(P_2,S_2,{\tau }_2)$. The ordinary HM factorization-extension calculation of lemma 4.45 aligns their residual substitutions on the variables inherited from $\mathrm{\Gamma }$. Extend the aligned substitution to W’s fresh result variable $a$ by $a\mapsto \rho$; call the result $V$. Then $${\tau }_1[S_2][V]=({\tau }_2\to a)[V]=B\to \rho .$$ Hence W’s unification call succeeds. Most-generality gives a $T$ such that, on every variable in this equation and in the inherited environment, $$V=U;T,a[U][T]=\rho ,T\star S_1;S_2;U\star \mathrm{\Gamma }=R\star \mathrm{\Gamma }.$$ The two premise entailments, transported through this equality, give $$\mathcal{C};Q⊩(P_1[S_2]\cup P_2)[U][T].$$ Canonical factorization for W’s final normalization gives $\mathcal{C};Q⊩P[T]$.

Let. The first induction hypothesis makes the right-hand-side call return $(P_1,S_1,{\tau }_1)$. Write its deterministic split as $$X=\mathrm{ftv}(P_1,{\tau }_1)\setminus \mathrm{ftv}(S_1\star \mathrm{\Gamma }),P_1=P_1^{\mathsf{g}}\cup P_1^{\mathsf{r}},\sigma =\mathrm{\forall }X.P_1^{\mathsf{g}}\Rightarrow {\tau }_1.$$ By lemma 11.3, the declarative generalized scheme factors through $\sigma$, while $P_1^{\mathsf{r}}$ remains an outer requirement. After extending both equal canonical environments by the factored scheme, the body induction hypothesis makes the second call return $(P_2,S_2,{\tau }_2)$. The HM factorization-extension lemma extends the body factor on variables generalized at the first call; let $T$ be the resulting common factor. Then $${\tau }_2[T]=\rho ,T\star S_1;S_2\star \mathrm{\Gamma }=R\star \mathrm{\Gamma },\mathcal{C};Q⊩(P_1^{\mathsf{r}}[S_2]\cup P_2)[T].$$ Canonical factorization for the last normalization yields $\mathcal{C};Q⊩P[T]$.

Every recursive and unification call has now been shown to succeed. A normalization rejection contradicts the corresponding declarative entailment by canonical factorization. For a closed term, generalization quantifies every free result variable, and the factorization just proved is qualified-scheme generality. ◻

The theorem does not cover ambiguous schemes, overlapping effective heads, higher-rank annotations, or defaulting. It also assumes the usual completeness and most-generality theorem for the HM unifier rather than reproving it.

Dictionary elaboration and execution

Write ${\tau }^D$ for source-type translation, ${\mathrm{\Gamma }}^D$ for pointwise context translation, and $\mathsf{DictTel}(Q)$ for the ordered dictionary telescope. The map $\mathrm{erase}(u)$ erases dictionary braces from a target term and applies the corresponding erasure to every context or telescope entry.

The target signature is part of the admitted class environment. Each superclass edge and instance declaration contributes, respectively, An effective candidate contributes no new primitive constant: its builder is the displayed primitive $c_i$ followed by its declared superclass projection. The method interface is explicit as well: $${\mathsf{eq}}^{\mathrm{♯}}:\mathrm{\forall }\alpha .{\mathsf{Eq}}_D(\alpha )\to \alpha \to \alpha \to \mathsf{Bool},{\mathsf{eq}}^{\mathrm{♯}}:=\mathrm{\Lambda }\alpha .\lambda \{d:{\mathsf{Eq}}_D(\alpha )\}.d.$$

For canonical $P$, let ${\mathrm{\Delta }}_P$ be the ordered telescope $d_p:p_D$. If an evidence template $\eta$ has domain $R$, write $\eta \cdot u$ for simultaneous replacement of the holes $d_r$ in $u$. A type substitution also acts on core type annotations, type applications, dictionary types, and evidence templates; write this action $S^{†}v$. Holes are keyed by their predicates, and $$S^{†}{d}_p=d_{p[S]}.$$ The image telescope contains one binder for each distinct predicate in $P[S]$, in canonical order. Thus if $p[S]=p^{\prime }[S]$, the two occurrences become references to the same binder rather than two colliding declarations. The following normalizer template then replaces those image holes by evidence over the canonical result telescope. The annotation on a binding in $S\star \mathrm{\Gamma }$ remembers the template that converts dictionaries for its canonical predicates to dictionaries expected by the binding’s previous target interface. These annotations compose when $-\star -$ composes.

Proof of Lemma 13.15 — Target substitution is scoped under merging

Proof. Induct on the target typing derivation. The hole case uses the key equation above; coalescing changes two declarations into repeated uses of their one common declaration. All type and term constructors are homomorphic. The second claim is simultaneous evidence substitution, using the typing of the normalizer template from lemma 11.2. ◻

Elaboration is indexed by the successful W derivation $\mathcal{W}$: $$\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}e:\tau ⇝u.$$ Here $\mathrm{\Gamma }$ is W’s input environment. The derivation $\mathcal{W}$ records W’s semantic result $(P,S,\tau )$: $S$ transports the input environment, $P$ is the residual predicate set, and $\tau$ is the inferred source type. The conclusion adds the elaborated target term $u$, typed under $S\star \mathrm{\Gamma }$ and ${\mathrm{\Delta }}_P$. The elaboration judgment has cases for variables, abstractions, applications, and lets. A variable occurrence uses exactly the instantiation $\theta$ recorded by W. Its ${\kappa }_x$ is the binding’s accumulated canonical-environment transport; it is the identity for a binding that has not been transported. For a template $\eta$ and a subset $R$ of its domain, $\eta {|}_R$ is the simultaneous evidence substitution restricted to holes whose keys lie in $R$. $$\frac{\begin{array}{c}x:(\mathrm{\forall }\overline{\alpha }.Q\Rightarrow {\tau }_0;{\kappa }_x)\in \mathrm{\Gamma }\\ {\mathsf{resolve}}_{\mathcal{C},\mathsf{store}({\mathrm{\Delta }}_P)}(q[\theta ])={\delta }_q(q\in Q)\end{array}}{\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}x:{\tau }_0[\theta ]⇝x[\overline{\alpha }[\theta ]]\{({\theta }^{†}{\kappa }_x)({\overline{\delta }}_q)\}}\mathrm{D}-\mathrm{Var}$$ $$\frac{\begin{array}{c}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\end{array}}{\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}\lambda x.e:a[S]\to \tau ⇝\lambda x:(a[S]{)}^D.u}\mathrm{D}-\mathrm{Lam}$$ $$\frac{\begin{array}{c}{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}({\tau }_1[S_2],{\tau }_2\to a){\mathsf{nf}}_{\mathcal{C}}((P_1[S_2]\cup P_2)[U])=\mathsf{ok}(P,\eta )\end{array}}{\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}{e}_1{e}_2:a[U]⇝(\eta {|}_{P_1[S_2][U]}\cdot U^{†}{S_2}^{†}{u}_1)(\eta {|}_{P_2[U]}\cdot U^{†}{u}_2)}\mathrm{D}-\mathrm{App}$$ For let, generalization records a template $\zeta :{\mathrm{\Delta }}_{P_r},{\mathrm{\Delta }}_Q{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{P_1}$ reconstructing the right-hand side requirements. After $S_2$, if $\eta :{\mathrm{\Delta }}_P{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{P_r[S_2]},{\mathrm{\Delta }}_{P_2}$ is the final normalization template, write ${\eta }_r,{\eta }_2$ for its restrictions and put $$\frac{\begin{array}{c}{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}}(P_r[S_2]\cup P_2)=\mathsf{ok}(P,\eta )\end{array}}{\mathcal{C};{\mathrm{\Delta }}_P;\mathrm{\Gamma }{⊢}_D^{\mathcal{W}}\mathbf{let}x=e_1\mathbf{in}{e}_2:{\tau }_2⇝u_{\mathsf{let}}}\mathrm{D}-\mathrm{Let}$$ For a nonidentity let transport, take $$\mathbf{let}f=\lambda xs.\mathsf{eq}xsxs\mathbf{in}f{\mathsf{nil}}_{\mathsf{Int}}.$$ The right-hand side initially requests $P_1=\{\mathsf{Eq}(\mathsf{List}a)\}$. Generalization retains $Q=\{\mathsf{Eq}a\}$ and records the nonidentity template $$\zeta (d_a)=\mathsf{eqList}(d_a):{\mathsf{Eq}}_D(\mathsf{List}a).$$ Consequently D-Let emits the generalized binding Here $\zeta$ performs the instance decomposition and the body occurrence of $f$ uses the nontrivial instantiation recorded by D-Var.

Here $\mathsf{DictTel}(Q)$ is the ordered telescope just defined. The mathematical W answer remains $(P,S,\tau )$; $\mathcal{W}$ stores its choices, while the unique $\eta$ and $\zeta$ are recomputed by the total normalizer. In the application rule, $S_2$ and $U$ act on $P_1,u_1$, $U$ acts on $P_2,u_2$, and $S_1\star -$ acts on the argument environment. In the let rule, $S_2$ acts on $P_r,\zeta ,u_1$ before final canonicalization.

Top-level closure is a separate, deterministic operation. If $$\begin{array}{c}{W}_{\mathcal{C}}(\varnothing ,e)=(P,S,\tau ),{\mathsf{Gen}}_{\mathcal{C}}(\varnothing ;P;\tau )=(\varnothing ,\mathrm{\forall }\overline{a}.Q\Rightarrow \tau ,\zeta ),\\ \mathcal{C};{\mathrm{\Delta }}_P;\varnothing {⊢}_D^{\mathcal{W}}e:\tau ⇝u,\end{array}$$ then $${\mathsf{close}}_{\mathcal{C}}(e)=\mathrm{\Lambda }\overline{a}.\lambda \{{\overline{d}}_Q:\mathsf{DictTel}(Q)\}.\zeta \cdot u.$$ The empty residual is forced at the empty source environment; missing ground evidence or ambiguity makes closure reject. A bar over type or dictionary application denotes the corresponding repeated unary forms in canonical order.

For example, the complete evidence-directed elaboration of the opening term is as follows. Here ${\mathrm{\Gamma }}_0$ binds the source name $\mathsf{eq}$ to the target constant ${\mathsf{eq}}^{\mathrm{♯}}$ with its displayed qualified scheme. At both applications, $S_2$, $U$, the normalizer template $\eta$, and every accumulated environment transport are identities. To keep the proof tree legible, its internal nodes suppress the unchanged indices ${\mathcal{C}}_0;d:{\mathsf{Eq}}_D(\alpha );{\mathrm{\Gamma }}_0$ and their types; each node is an instance of the indexed judgment just defined. $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathsf{eq}⇝{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]\{d\}\\ x⇝x\end{array}}{\mathsf{eq}x⇝{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]\{d\}x}}\mathrm{D}-\mathrm{App}\\ x⇝x\end{array}}{\mathsf{eq}xx⇝{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]\{d\}xx}}\mathrm{D}-\mathrm{App}}{{\mathcal{C}}_0;d:{\mathsf{Eq}}_D(\alpha );{\mathrm{\Gamma }}_0{⊢}_D^{\mathcal{W}}\lambda x.\mathsf{eq}xx:\alpha \to \mathsf{Bool}⇝\lambda x:\alpha .{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]\{d\}xx}\mathrm{D}-\mathrm{Lam}.$$ Generalizing closes it as $$\mathrm{\Lambda }\alpha .\lambda \{d:{\mathsf{Eq}}_D(\alpha )\}.\lambda x:\alpha .{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]\{d\}xx.$$

Proof of Theorem 11.6 — Target type preservation

Proof. Induct on D-Var, D-Lam, D-App, and D-Let. Variable evidence has the required dictionary type by lemma 11.1; target type and dictionary applications therefore instantiate its translated scheme. More precisely, $${\theta }^{†}{\kappa }_x:{\mathrm{\Delta }}_{Q[\theta ]}{\Rightarrow }_{\mathsf{e}}{\mathrm{\Delta }}_{Q_0[\theta ]},$$ where $Q_0$ is the predicate interface stored with $x$. Applying this transport to the selected ${\overline{\delta }}_q$ gives the dictionary arguments expected by $x[\overline{\alpha }[\theta ]]$. For abstraction the body induction hypothesis is under $S\star \mathrm{\Gamma },x:a$, so its ordinary binder has type $a[S{]}^D$. At application, ${S_2}^{†}-$ and $U^{†}-$ transport both induction hypotheses by lemma 13.15 to $U\star S_2\star S_1\star \mathrm{\Gamma }$; the MGU gives the common domain. Applying $\eta$ to both normalized predicate sets gives the same dictionary telescope, so source and target applications use the same dictionary parameters. At let, the generalization split determines exactly the type and dictionary abstractions; ${S_2}^{†}\zeta$ transports the right-hand side, while residual dictionaries remain in ${\mathrm{\Delta }}_P$. Canonicalization evidence is well typed by lemma 11.2, so every reconstructed dictionary application typechecks. For erasure, the dictionary-abstraction case sends $\lambda \{d:D\}.u$ to $\lambda d:D.\mathrm{erase}(u)$ and uses the body induction hypothesis. The dictionary-application case sends $u\{\delta \}$ to $\mathrm{erase}(u)\mathrm{erase}(\delta )$ and uses ordinary application. All remaining constructors use their homomorphic System F rule. ◻

Erase dictionary braces from $U$ to System F by All other clauses are homomorphic. Instance constants and superclass projections retain their displayed signatures. Define surface evaluation by evidence insertion and top-level closure: Thus an implicit surface program executes through its unique evidence core; there is no second raw reduction relation that guesses dictionaries.

Proof of Lemma 13.17 — Core–target step correspondence

Proof. Inspect the root rule. Ordinary beta, type beta, let beta, products, base operations, instance constructors, and superclass projections are homomorphic. Dictionary beta maps to ordinary target beta. Conversely, a target root and the typed outer constructor of the given $u$ select a corresponding core root; evaluation contexts lift structurally. The lift need not be unique because brace erasure is not injective: for example, an ordinary lambda and a dictionary lambda may erase to the same System F lambda. Induction on a step sequence gives forward simulation and existential reverse lifting for reflexive-transitive closure. ◻

Proof of Lemma 13.18 — Core dynamic preservation and value reflection

Proof. For clause 1, inspect the root contraction and close the result under the evaluation contexts. Ordinary beta, type beta, let beta, and dictionary beta use the corresponding substitution lemma. A primitive equation preserves the type because its two sides were checked at the same type in the same free-variable context; substituting its value arguments preserves that typing. For clause 2, inspect the two value grammars. Erasure changes a dictionary abstraction into an ordinary abstraction and otherwise preserves the outer constructor. Conversely, a core term whose erasure has a value outer constructor is an ordinary abstraction, type abstraction, dictionary abstraction, value pair, base value, or saturated dictionary constructor, so it is a core value. ◻

Proof of Theorem 11.7 — Forward operational simulation

Proof. Resolution, normalization, W, and the four elaboration rules are functional, so $u$ is unique up to renaming. Unfold the definition of $e{\Downarrow }_{\mathcal{C}}w$. Forward simulation gives the first clause. Repeated reverse lifting gives a core endpoint $w$ erasing to $V$. Value reflection in lemma 13.18 makes that endpoint a core value, giving the second clause. The endpoint is existential rather than fixed because erasure forgets the brace distinction. In particular, the displayed D-Let accounts for type/dictionary administrative redexes; the proof never identifies generalized surface let substitution with one homomorphic target step. ◻

For instance, erasing braces from the preceding core term gives the System F calculation $$(\mathrm{\Lambda }\alpha .\lambda d.\lambda x.{\mathsf{eq}}^{\mathrm{♯}}[\alpha ]dxx)[\mathsf{Int}]({\pi }_1\mathsf{ordInt})0{⟶}^{\ast }({\pi }_1\mathsf{ordInt})00{⟶}^{\ast }\mathsf{true}.$$

Proof of Theorem 11.8 — Algorithmic coherence

Proof. Fresh type variables and dictionary binders may differ only by renaming. The HM MGU is unique up to such renaming; canonical predicate order is fixed; and lemma 11.1 proves that each request has at most one selected evidence term. An induction over D-Var, D-Lam, D-App, and D-Let therefore determines every core constructor and subterm. Homomorphic erasure preserves alpha-equivalence, and alpha-equivalent System F terms are contextually equivalent. ◻

Thus the result is determinism of the selected algorithm, not a coherence theorem for the declarative system.

The annotated ground compatibility slice

For the explicitly typed ground exercises in appendix A, use the distinct Church-Boolean dictionary notation These are annotations on ${\mathrm{QTC}}_0$ elaboration: bind, use, and discharge one displayed dictionary. They are not a second inference calculus. The symbols ${\mathsf{Bool}}_F,{\mathsf{true}}_F,{\mathsf{false}}_F$ are the Church encoding from definition 5.15; they are recalled here because the following dictionary returns that encoding rather than the primitive $\mathsf{Bool}$ used above. Let

Proof of Proposition 13.21 — Ground-table specialization

Proof. Type normalization fixes the lookup key. The local map contains at most one entry; if it contains none, the table contains at most one. Structural induction on the annotated term then forces the elaboration clause and all subterms. The proposition is also the premise-free closed-type specialization of theorem 11.8. ◻

Associated type synonyms: one bounded extension

The principal calculus above resolves a predicate but never lets that resolution determine a type. Collections expose the missing dependency: $$\begin{array}{l}\mathsf{class}\mathsf{Collects}c\mathsf{where}\mathsf{type}\mathsf{Elem}c;\\ \mathsf{empty}:c;\mathsf{insert}:\mathsf{Elem}c\to c\to c;\mathsf{toList}:c\to \mathsf{List}(\mathsf{Elem}c).\end{array}$$ The class predicate says that the operations exist. The associated synonym $\mathsf{Elem}c$ says which element type those operations share. It is a partial, saturated type-level function: the application is admitted only when $\mathsf{Collects}c$ is entailed.

This section is a bounded import, called ${\mathrm{ATS}}_0$. It does not strengthen the principality theorem for ${\mathrm{QTC}}_0$. Extend the predicate and instance environments by Class declarations give an arity and kind to $S$. An instance gives both a class clause and an equality scheme. For example, $$\begin{array}{l}\mathsf{instance}\mathsf{Eq}a\Rightarrow \mathsf{Collects}(\mathsf{List}a)\mathsf{where}\\ \mathsf{type}\mathsf{Elem}(\mathsf{List}a)=a;\cdots \end{array}$$ contributes $$\mathrm{\forall }a.\mathsf{Eq}a\Rightarrow \mathsf{Collects}(\mathsf{List}a),\mathrm{\forall }a.\mathsf{Elem}(\mathsf{List}a)=a.$$ The equality scheme itself is unqualified, but its left side is well formed only where the associated class predicate is entailed. The instance checker verifies the right-hand side using the superclass environment and the instance premises, while the paired class clause supplies those premises whenever the reduction is applicable. This pairing prevents synonym reduction from exposing a type whose class precondition was never established.

Write $\mathrm{\Theta }⊩\pi$ for entailment by class and equality schemes. In addition to specialization and modus ponens, equality has reflexivity, symmetry, transitivity, and congruence. The two distinctive typing rules 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}.$$ Thus $\mathsf{Elem}c$ is not well formed merely because $c$ is a type. For instance, the annotation $\mathsf{Elem}c\to c$ must carry a premise $\mathsf{Collects}c$.

Evidence and type passing.

The source paper says that its typing rules admit the conventional type-directed evidence translation, but deliberately omits those extended rules [CKPJ05]. The following ground instance is therefore a local target sketch, not an imported elaboration theorem. Class predicates elaborate to ordinary dictionaries, the associated type is an explicit target type parameter, and equality solving chooses and normalizes that parameter at compile time. For the running class, use $${\mathsf{Collects}}_D(C,E):=C\times (E\to C\to C)\times (C\to \mathsf{List}E).$$ The method and list instance have target types Consequently the ground source call at $\mathsf{List}\mathsf{Int}$ elaborates to $${\mathsf{insert}}^{\mathrm{♯}}[\mathsf{List}\mathsf{Int}][\mathsf{Int}](\mathsf{collectsList}[\mathsf{Int}]\mathsf{eqInt}).$$ The equation $\mathsf{Elem}(\mathsf{List}\mathsf{Int})=\mathsf{Int}$ justifies the second type argument. It contributes no run-time proof object to this System-F-style target. An open pending equality remains in the source constraint set until later instantiation makes a rewrite possible.

Well-formed programs require constructor-headed, specific, nonoverlapping instance heads; decreasing instance contexts; saturated associated applications; and a confluent, terminating synonym rewrite system. Programmer-written equality constraints have a variable in the designated class-index position. Define the fixed variables by Thus variables beneath an associated application do not count as fixed, whereas variables in the ordinary right-hand side of an equality constraint do. If $\mathrm{\forall }\overline{a}.P\Rightarrow \tau$ is a method signature in class $K\beta$, require $$\beta \notin \mathsf{FV}(P)\text{and}\beta \in \mathsf{Fixv}(\mathrm{\forall }\overline{a}.P\Rightarrow \tau ).$$ Every annotation $e::\mathrm{\forall }\overline{a}.\rho$ also requires $\overline{a}\cap \mathsf{FV}(\rho )\subseteq \mathsf{Fixv}(\rho )$. These are the source’s admission conditions, not conclusions of inference.

Proof of Theorem 13.23 — Soundness of associated-type inference—imported

Proof. This is exactly Chakravarty, Keller, and Peyton Jones’s Theorem 2, under the well-formed-program hypotheses and judgment roles fixed above [CKPJ05]. Their proof factors through a syntax-directed declarative system; soundness of type reduction, one-step unification, its closure, and subsumption discharge the non-syntactic equality cases. Those lemmas are imported with the theorem, not reproved for ${\mathrm{QTC}}_0$. ◻

The imported source states completeness and principality only as beliefs [CKPJ05]. This chapter therefore imports neither. It also makes no claim for open type families, overlap, injectivity annotations, roles, dependent equality, or unrestricted modern GHC instance programs.

Source boundary.

The class examples and dictionary translation are from [WB89]; that paper’s larger principal-typing statement is explicitly conjectural [WB89]. The separation of qualified typing from evidence translation follows [HHPJW96], whose metatheorems are only outlined there and are not imported as proofs. Predicate entailment, context reduction, generalization, and ambiguity follow the executable specification in [Jon99]; that source is an implementation specification, not a mechanized metatheory. The finite superclass-closed effective table, full effective-head nonoverlap policy, normalization naturality, and factorization lemma are the book’s explicit bounded repair; they are not attributed to those larger systems. The proofs in this chapter are therefore for the explicitly restricted ${\mathrm{QTC}}_0$ above. They do not claim principality for Haskell’s full class system.

Stable and coherent implicits

COCHIS begins from a smaller failure than a large type-class program. Its contexts grow to the right, so the final implicit below is nearest: $$\mathrm{\Delta }=\beta ,?\beta :x,\alpha ,?\alpha :y.$$ Before substituting $\beta$ for $\alpha$, the query $?\beta$ skips $?\alpha$ and returns $x$. After substitution, the nearer assumption has type $?\beta$ and the same query returns $y$. Equivalently, type application changes the evidence selected by $$\lambda ?\beta .(\mathrm{\Lambda }\alpha .\lambda ?\alpha .?\beta )\beta$$ when compared with its type-beta reduct. Resolution that is merely deterministic is therefore not necessarily stable under substitution.

The comparison uses the paper’s exact predicative syntax. From here through the end of the comparison, $\sigma$ ranges over COCHIS monotypes, not the qualified schemes of ${\mathrm{QTC}}_0$, and $\mathrm{\Delta }$ is COCHIS’s full typing context, not the evidence-only context used above: Only monotypes $\sigma$ may instantiate $\mathrm{\forall }$. Besides typing $\mathrm{\Delta }⊢e:\rho$, the deterministic specification has these judgment signatures: These are, respectively, main resolution, focusing, nearest-first lookup, matching with returned goals and evidence placeholders, and permission to skip one candidate. The main rule sets $A=\mathsf{tyvars}(\mathrm{\Delta })$; focusing strips $\mathrm{\forall }$ and rule premises until a simple head remains; lookup scans ${\mathrm{\Delta }}^{\prime }$ from right to left. It commits to the first match and may skip a candidate only when the displayed stability judgment holds. Concretely, $\mathsf{stable}(A;\mathrm{\Delta };\rho ;x;\tau )$ means that no substitution valid for $A;\mathrm{\Delta }$ makes the candidate $\rho$ match the query $\tau$; validity and matching are defined immediately after the rules.

Here is the load-bearing fragment of that resolution, including the recursive evidence plumbing. Write $A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[\overline{\rho }]⇝\overline{E}$ for the pointwise resolution of a sequence of goals. Matching a candidate returns both recursive goals $\overline{\rho }$ and fresh placeholders $\overline{z}$; the lookup rule resolves those goals in the full environment and substitutes the resulting evidence into the candidate evidence. The notation $|\rho |$ in this imported fragment is its own source-to-target type translation; it is unrelated to $\mathsf{DictTel}$, $(-{)}^D$, and $\mathrm{erase}(-)$ above.

$\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$

The simplest lookup uses four of the rules immediately. For either $\theta =\mathsf{id}$ or $\theta =[\mathsf{Int}/\beta ]$, $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\mathrm{\Delta };[\beta [\theta ]];x{⊢}_{\mathsf{m}}\varnothing ;\varnothing ;\beta [\theta ]⇝x}}\mathrm{C}-\mathrm{M}-\mathrm{Simp}\\ A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[\varnothing ]⇝\varnothing \end{array}}{A;\mathrm{\Delta };[?\beta [\theta ]:x]{⊢}_{\mathsf{l}}\beta [\theta ]⇝x}}\mathrm{C}-\mathrm{L}-\mathrm{Match}}{A;\mathrm{\Delta }{⊢}_{\mathsf{f}}[\beta [\theta ]]⇝x}}\mathrm{C}-\mathrm{R}-\mathrm{Simp}}{\mathrm{\Delta }{⊢}_{\mathsf{r}}\beta [\theta ]⇝x}\mathrm{C}-\mathrm{R}-\mathrm{Main}.$$ Thus the same lookup derivation selects $x$ before and after the ground substitution. The complete source typing and valid-substitution systems are Figs. 2 and 6 of [SdSOWM19]; its resolution, algorithm, unification, and termination systems are Figs. 7–10 on pp. 30–35.

Unambiguity is the inductive predicate $\mathsf{UA}(A;\rho )$: Write $\mathsf{unamb}(\rho )$ for $\mathsf{UA}(\varnothing ;\rho )$; implicit binders and queries require it.

The valid-substitution judgment is $\mathsf{valid}(A;\mathrm{\Delta };\theta )$. The empty substitution is valid. Its only extension clause admits $[\sigma /\alpha ]\cdot \theta$ when $\alpha \in A$, the environment splits as ${\mathrm{\Delta }}_0,\alpha ,{\mathrm{\Delta }}_1$, the monotype $\sigma$ is well scoped in the prefix ${\mathrm{\Delta }}_0$, and $$\mathsf{valid}(A\setminus \{\alpha \};[\sigma /\alpha ]({\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1);\theta ).$$ Finally, $\mathsf{stable}(A;\mathrm{\Delta };\rho ;x;\tau )$ says that there is no such valid $\theta$ under which the skipped $\theta \rho$ matches the query $\theta \tau$. This is the exact side condition that rejects the witness above; ordinary deterministic lookup alone would accept it.

Recursive rules are admitted only when each premise head is structurally smaller than the result head and every type variable occurs no more often in the premise than in the result. This is the comparison’s one selected mechanism: stable implicit resolution, not a second extension of ${\mathrm{QTC}}_0$.

Proof of Theorem 11.10 — Imported COCHIS boundary

Imported proof. Source. Items 1–6 import Theorems 5.1–5.6 and Lemmas 5.1–5.3 of [SdSOWM19] for exactly the calculus and side conditions frozen above. The paper’s mutual inductions provide the weakening, substitution, resolution, and translation lemmas; its structural measure proves termination of recursive resolution. System F strong normalization and the operational simulation give item 6. No COCHIS principality theorem, result for arbitrary lexical implicits, or result for ${\mathrm{QTC}}_0$ is imported. ◻

The contrast is now precise. ${\mathrm{QTC}}_0$ obtains coherence by an admissible superclass-closed instance environment with fixed candidate priority, canonical constraints, and functional evidence construction. COCHIS admits lexical implicit evidence, so it needs unambiguity and valid substitutions to make resolution stable as types change.