ch:type-classes: ch:type-classes

With empty local evidence, the only instance path is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\mathsf{pick}}_{{\mathcal{C}}_0}(\mathsf{Eq}\mathsf{Int})=(\varnothing ,{\pi }_1\mathsf{ordInt})}{{\mathsf{resolve}}_{{\mathcal{C}}_0,\varnothing }(\mathsf{Eq}\mathsf{Int})={\pi }_1\mathsf{ordInt}}}\mathrm{E}-\mathrm{Instance}}{{\mathsf{resolve}}_{{\mathcal{C}}_0,\varnothing }(\mathsf{Eq}(\mathsf{List}\mathsf{Int}))=\mathsf{eqList}({\pi }_1\mathsf{ordInt})}}\mathrm{E}-\mathrm{Instance}}{{\mathsf{resolve}}_{{\mathcal{C}}_0,\varnothing }(\mathsf{Eq}(\mathsf{List}(\mathsf{List}\mathsf{Int})))=\mathsf{eqList}(\mathsf{eqList}({\pi }_1\mathsf{ordInt}))}\mathrm{E}-\mathrm{Instance}.$$ If a second effective declaration has a head unifiable with $\mathsf{Eq}(\mathsf{List}\alpha )$, both freshened heads can match a common instance of the outer request. The effective-head admission check therefore rejects the table rather than choosing between distinct builders. The same check rejects a primitive $\mathsf{Eq}\mathsf{Int}$ clause in the presence of $\mathsf{Ord}\mathsf{Int}$: superclass closure already derives an effective $\mathsf{Eq}\mathsf{Int}$ clause whose builder is ${\pi }_1\mathsf{ordInt}$. Keeping both would destroy the unique selected evidence needed by functionality and coherence.

Without superclass closure, $$\mathsf{nf}\{\mathsf{Ord}(\mathsf{List}\alpha ),\mathsf{Eq}\beta \}=\{\mathsf{Ord}\alpha ,\mathsf{Eq}\beta \}.$$ Under $$\theta =[\mathsf{Int}/\alpha ,\mathsf{List}\mathsf{Int}/\beta ],$$ the raw set succeeds: construct $\mathsf{OrdList}(\mathsf{OrdInt})$, install it, and obtain the required list equality dictionary as $$\mathsf{EqFromOrd}(\mathsf{OrdList}(\mathsf{OrdInt})).$$ The canonical set fails because after constructing $\mathsf{OrdInt}$ it has no instance for $\mathsf{Eq}(\mathsf{List}\mathsf{Int})$. With ${\mathcal{I}}^{\uparrow }$, the derived clause $\mathsf{Ord}a\Rightarrow \mathsf{Eq}(\mathsf{List}a)$ resolves the latter request from $\mathsf{OrdInt}$, so both sets succeed.

For action composition, put $$R=\{\mathsf{Ord}\gamma ,\mathsf{Eq}\beta \},S=[\mathsf{List}\alpha /\gamma ],T=[\mathsf{List}\alpha /\beta ].$$ Without closure, $\mathsf{nf}(SR)=\{\mathsf{Ord}\alpha ,\mathsf{Eq}\beta \}$, so the second action rejects at $\mathsf{Eq}(\mathsf{List}\alpha )$. Direct normalization of $(T\circ S)R$ first constructs $\mathsf{Ord}(\mathsf{List}\alpha )$, installs it, projects the required equality dictionary, and returns $\{\mathsf{Ord}\alpha \}$. With closure, the sequential second action uses the derived clause and returns that same set. Both routes transport the same evidence: $$\mathsf{EqFromOrd}(\mathsf{OrdList}(d_{\mathsf{Ord}})).$$

Explicit type application can select $A=\mathsf{Int}$ and then receive an explicit dictionary. For example, $$f[\mathsf{Int}]\{\mathsf{showDecimal}\}\text{and}f[\mathsf{Int}]\{\mathsf{showHexadecimal}\}$$ may return "10" and "0xa" on the value $10$. At an implicit use, the visible result type is only $\mathsf{String}$; it contains no occurrence of $A$. The type therefore determines neither the instantiation nor the dictionary. This is exactly the failure of $\mathsf{ftv}(Q)\subseteq \mathsf{ftv}(\tau )$.

Give $x$ the fresh type $a$. Fresh instantiations of $\mathsf{nil}:\mathrm{\forall }b.\mathsf{List}b$ and $\mathsf{cons}:\mathrm{\forall }b.b\to \mathsf{List}b\to \mathsf{List}b$ make both singleton lists have type $\mathsf{List}a$. Instantiating $\mathsf{eq}$ at that type contributes $$\mathsf{Eq}(\mathsf{List}a)\Rightarrow \mathsf{List}a\to \mathsf{List}a\to \mathsf{Bool}.$$ The application MGUs identify no further type variables. The normalizer one-way-matches the list instance and records $$\mathsf{eqList}:{\mathsf{Eq}}_D(a)\to {\mathsf{Eq}}_D(\mathsf{List}a),$$ so the residual predicate is $\mathsf{Eq}a$. Abstraction and top-level generalization therefore give $$\mathrm{\forall }a.\mathsf{Eq}a\Rightarrow a\to \mathsf{Bool}.$$

For a rejected right-hand side, place $\mathsf{show}:\mathrm{\forall }b.\mathsf{Show}b\Rightarrow b\to \mathsf{String}$ in the environment and use $\mathsf{show}\mathsf{false}$. W generates the ground request $\mathsf{Show}\mathsf{Bool}$. The selected environment contains only $\mathsf{Show}\mathsf{Int}$, so normalization returns $\mathsf{reject}(\mathsf{Show}\mathsf{Bool})$ before generalization.

In the constructor context $A::\mathsf{Ty}$ and term context $$d:{\mathsf{Eq}}_D(A),x:A,y:A,z:A,$$ the application rules give Discharging $z,y,x,d$ by four uses of T-Lam, and then $A$ by T-TLam, derives $${\mathsf{allSame}\mathsf{3}}^{\mathrm{♯}}:\mathrm{\forall }A::\mathsf{Ty}.{\mathsf{Eq}}_D(A)\to A\to A\to A\to {\mathsf{Bool}}_F.$$

For the displayed run, the outer contractions give Put $e_T={\mathsf{true}}_F[{\mathsf{Bool}}_F]{\mathsf{false}}_F{\mathsf{true}}_F$. The first comparison reduces completely as follows: The second comparison follows the same selected true branch: The final conjunction is The displayed Church false is itself beta-normal, so no redex remains.

For the three failures, take:

1. the overlapping table $$\{(\mathsf{Eq},{\mathsf{Bool}}_F,\mathsf{eqBool}),(\mathsf{Eq},{\mathsf{Bool}}_F,\lambda p:{\mathsf{Bool}}_F.\lambda q:{\mathsf{Bool}}_F.{\mathsf{true}}_F)\};$$ it violates hypothesis 1 of proposition 13.21;

2. the nested declaration $$\mathsf{Eq}A\Rightarrow (\mathsf{Eq}A\Rightarrow s),$$ which creates two dictionaries at the same normalized key and violates hypothesis 3;

3. the two ground entries $$(\mathsf{Tag},{\mathsf{Bool}}_F,\mathsf{0}),(\mathsf{Tag},\mathbb{N},\mathsf{suc}(\mathsf{0})),$$ with $\mathsf{TagD}(A)=\mathbb{N}$. In the scheme $\mathrm{\forall }A.\mathsf{Tag}A\Rightarrow \mathbb{N}$, the constrained variable $A$ does not occur in the normalized visible monotype $\mathbb{N}$. This violates the separate ambiguity/admission check that every constraint variable be determined by that visible monotype, not one of the four numbered coherence hypotheses.

Pair decomposition produces $\mathsf{Int}=\mathsf{Elem}c$ and $a=\mathsf{Bool}$. The latter has most-general substitution $[\mathsf{Bool}/a]$; the former cannot reduce while $c$ is unknown, so $$T=[\mathsf{Bool}/a],U=\{\mathsf{Int}=\mathsf{Elem}c\}.$$

With $c=\mathsf{List}\mathsf{Int}$, the instance equation reduces the right side to $\mathsf{Int}$, and reflexivity discharges $U$. In the chapter’s local target sketch, the method use is $${\mathsf{insert}}^{\mathrm{♯}}[\mathsf{List}\mathsf{Int}][\mathsf{Int}](\mathsf{collectsList}[\mathsf{Int}]\mathsf{eqInt}).$$ The dictionary has type ${\mathsf{Collects}}_D(\mathsf{List}\mathsf{Int},\mathsf{Int})$.

With $c=\mathsf{List}\mathsf{Bool}$, normalization instead produces $\mathsf{Int}=\mathsf{Bool}$. Distinct rigid constructors do not unify, so the inference branch fails. The independently well-typed Boolean method would have target form $${\mathsf{insert}}^{\mathrm{♯}}[\mathsf{List}\mathsf{Bool}][\mathsf{Bool}](\mathsf{collectsList}[\mathsf{Bool}]\mathsf{eqBool}),$$ but it cannot elaborate the source equality constraint demanding element type $\mathsf{Int}$. A valid dictionary term cannot repair a failed static equality.

In $\mathrm{\Delta }=?\mathsf{Int}:x,\alpha ,?\alpha :y$, the query $?\mathsf{Int}$ initially skips the nonmatching $?\alpha$ and selects $x$. After substituting $\mathsf{Int}$ for $\alpha$, nearest-first lookup selects $y$. The evidence terms are therefore exactly $x$ and $y$.

Remove the final assumption $?\alpha :y$. Lookup then reaches $?\mathsf{Int}:x$ directly: no implicit candidate lies between the query and that entry. Consequently the no-match rule is never used, the stability side condition is not invoked, and no valid-substitution premise has become trivial.

The variable $\beta$ is free in the inferred type and not fixed by the environment; $\alpha$ is fixed by the environment. Therefore the maximal split of lemma 11.3 is $$P_1^{\mathsf{g}}=\{\mathsf{Show}\beta \},P_1^{\mathsf{r}}=\{\mathsf{Eq}\alpha \},\sigma =\mathrm{\forall }\beta .\mathsf{Show}\beta \Rightarrow \beta \to \mathsf{Bool}.$$ If the body call returns substitution $S_2$, its factor $T$ is extended on the variables quantified by $\sigma$, while the inherited coordinates obey $$T\star S_1;S_2\star \mathrm{\Gamma }=R\star \mathrm{\Gamma }.$$ This equation fixes the meaning of $\alpha$ in the body exactly as it was fixed in the outer environment. The residual requirement becomes $\mathsf{Eq}\alpha [S_2]$ and is combined with the body’s requirements; by lemma 13.8, final normalization cannot discard an obligation needed by the declarative derivation.

If $\mathsf{Eq}\alpha$ were generalized, the let-bound term could be instantiated at a type unrelated to the outer $\alpha$. That instance would request a dictionary not justified by the outer evidence context, while the residual set would no longer contain $\mathsf{Eq}\alpha$. The displayed environment equation would then fix $\alpha$ on the left but the alleged scheme instance could change it on the right, so the factorization required by theorem 11.5 would fail.

Choose overlap. Add two premise-free declarations $$d_1:\mathsf{Eq}(\mathsf{List}\mathsf{Int}),d_2:\mathsf{Eq}(\mathsf{List}\mathsf{Int})$$ whose Boolean functions disagree on one pair of lists. The closed program $\mathsf{eq}[0][1]$ can then elaborate with either dictionary and has two observable results. The precise failed proof step is the unique-instance case of lemma 11.1; canonical evidence and theorem 11.8 consequently fail as well. A repair would need a displayed deterministic priority in both the declarative and algorithmic systems together with a proof that substitution preserves it. Selecting whichever declaration happens to be encountered first supplies no such invariant.