ch:modular-type-classes: ch:modular-type-classes

The monomorphic choice fixes the available module at the definition site: $$A.f⇝\lambda x:\mathsf{Int}.\mathsf{EqInt}\mathsf{.}\mathsf{eq}(x,x+2).$$ Hence $$B.y⇝\mathsf{EqInt}\mathsf{.}\mathsf{eq}(3,5)=\mathsf{false}.$$ The constrained-polymorphic choice exports the evidence parameter: $$A.f⇝\mathrm{\Lambda }X:\mathsf{EQ}.\lambda x:X.t.X.\mathsf{eq}(x,x+2).$$ At the use in $B$, inference may instantiate $X$ with $\mathsf{EqParity}$, giving $$B.y⇝\mathsf{EqParity}\mathsf{.}\mathsf{eq}(3,5)=\mathsf{true}.$$ The boundary of $A$ must decide whether $f$ is exported at the monomorphic signature $\mathsf{Int}\to \mathsf{Bool}$ or at the constrained-polymorphic signature $\mathrm{\forall }X:\mathsf{EQ}.X.t\to \mathsf{Bool}$. Instance scope alone cannot determine that exported interface.

The evidence tree is $$\mathsf{ShowList}⟨\mathsf{ShowPair}⟨\mathsf{ShowBool},\mathsf{ShowInt}⟩⟩.$$ Its proper evidence subterms have types Applying $\mathsf{ShowList}$ to the last subterm gives $$\mathsf{ShowList}⟨\mathsf{ShowPair}⟨\mathsf{ShowBool},\mathsf{ShowInt}⟩⟩:\mathsf{SHOW}[\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int}))].$$

The two accepted declarations have result heads $$(\mathsf{SHOW},\mathsf{Int})\text{and}(\mathsf{SHOW},\mathsf{List}).$$ Both heads are absent from the original environment, so lemma 16.4 applies to $\mathsf{ShowInt}$ and to $\mathsf{ShowList}$.

For $\mathsf{EqNever}$, the result head is $(\mathsf{EQ},\mathsf{Int})$, already occupied by $\mathsf{EqInt}$. The non-overlap premise fails. If the adoption were allowed, the same request would have two derivations, $$\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Int}]{\Downarrow }_{\mathsf{res}}\mathsf{EqInt}\text{and}\mathrm{\Theta }⊢\mathsf{EQ}[\mathsf{Int}]{\Downarrow }_{\mathsf{res}}\mathsf{EqNever},$$ with observably different equality operations.

Depth-first, left-to-right resolution visits these keys: The first three lookups find $\mathsf{EqList}$, $\mathsf{EqPair}$, and $\mathsf{EqInt}$. The fourth finds no declaration, so the first reported error is $$\mathsf{missing}(\mathsf{EQ},\mathsf{Bool}).$$ There is no possible R-Base conclusion for the Boolean request. Thus the second premise needed for the R-Functor application of $\mathsf{EqPair}$ cannot be completed; the enclosing $\mathsf{EqList}$ premise consequently fails as well.

Put $$V:=\mathsf{ShowList}⟨\mathsf{ShowPair}⟨\mathsf{ShowBool},\mathsf{ShowInt}⟩⟩.$$ Resolution gives $$\mathrm{\Theta }⊢\mathsf{SHOW}[\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int}))]{\Downarrow }_{\mathsf{res}}V.$$ The source elaborates to $$\lambda z:\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int})).V.\mathsf{show}z.$$ Let $${\mathrm{\Gamma }}_z:=z:\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int})).$$ Evidence typing gives $$\mathrm{\Theta }⊢V:\mathsf{SHOW}[\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int}))].$$ Target weakening therefore gives the same judgment under ${\mathrm{\Gamma }}_z;\mathrm{\Theta }$, and signature projection gives $${\mathrm{\Gamma }}_z;\mathrm{\Theta }⊢V.\mathsf{show}:\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{Int}))\to \mathsf{String}.$$ The variable rule types $z$ in ${\mathrm{\Gamma }}_z;\mathrm{\Theta }$, so application has type $\mathsf{String}$. Abstraction discharges $z$ and gives the claimed function type.

Admissibility supplies the three hypotheses used by theorem 16.6. Well-typed declarations establish evidence typing. Decrease establishes termination, and non-overlap makes the selected evidence unique. The target derivation itself needs only the returned evidence’s realized signature.

The outer list request selects $\mathsf{ShowList}$. Its premise is the pair request, which selects $\mathsf{ShowPair}$. The first pair premise is the variable request $\mathsf{SHOW}[\alpha ]$, so retain $$X:\mathsf{SHOW}[\alpha ].$$ The second premise is a list request at $\mathsf{Int}$, solved by $\mathsf{ShowList}⟨\mathsf{ShowInt}⟩$. Reduction therefore returns $$(X:\mathsf{SHOW}[\alpha ],\mathsf{ShowList}⟨\mathsf{ShowPair}⟨X,\mathsf{ShowList}⟨\mathsf{ShowInt}⟩⟩⟩).$$ Grounding $\alpha$ to $\mathsf{Bool}$ and substituting $\mathsf{ShowBool}$ for $X$ gives $$\mathsf{ShowList}⟨\mathsf{ShowPair}⟨\mathsf{ShowBool},\mathsf{ShowList}⟨\mathsf{ShowInt}⟩⟩⟩,$$ which has the realized signature $$\mathsf{SHOW}[\mathsf{List}(\mathsf{Pair}(\mathsf{Bool},\mathsf{List}(\mathsf{Int})))].$$

1. Yes. This is the theorem’s ground top-level consequence.

2. No. This is a completeness claim. The published theorem is one-way soundness, and the calculus intentionally inherits incompleteness from ML module inference.

3. No. This is a coherence claim comparing successful elaborations. Type preservation of each elaboration does not establish their observational equivalence.

4. Yes. Future-world extension and a canonical solution of the residual constraints are explicit hypotheses of the soundness theorem, and the term clause concludes declarative typing after those substitutions.

The explicit argument and expected result constrain the missing module $M$ by $$M.t=\mathsf{Int}\mathsf{list}.$$ Trying either list functor removes one list constructor and generates the argument constraint $S.t=\mathsf{Int}$, solved by $\mathsf{ShowInt}$. The two complete candidates are therefore $$\mathsf{ShowList}(\mathsf{ShowInt})\text{and}\mathsf{CompactShowList}(\mathsf{ShowInt}).$$ Repeated use of either functor would be decreasing because its argument constraint is structurally smaller than its result constraint. Hence the termination check succeeds. Uniqueness fails because the two module expressions are distinct and implement different printing operations. The call is rejected as ambiguous.

Name the outer implicit integer $i_{10}$, the fresh parameter introduced while checking $add$ by $i_a$, and the inner implicit integer by $i_3$. Checking the declared implicit-function type introduces $i_a$ before checking the body, so the query in $x+?$ selects that rightmost eligible variable: $$add⇝\lambda i_a:\mathsf{Int}.\lambda x:\mathsf{Int}.x+i_a.$$ The later inner let is not in lexical scope at this definition and cannot be observed by that query.

At the use of $add$, automatic implicit elimination generates a new query at $\mathsf{Int}$. Here $i_3$ is the rightmost eligible binding, so $$add4⇝(\lambda i_a.\lambda x.x+i_a)i_{3}4{⟶}^{\ast }4+i_3.$$ Substituting the inner binding yields $4+3=7$. The outer value $10$ is shadowed at the call site.

Take The first module may define $\mathsf{empty}=[]$ and $\mathsf{insert}=\mathsf{cons}$; the second may define the empty finite set and its duplicate-removing insertion operation. Their realized signatures are and Consequently both $$\mathsf{IntLists}\mathsf{.}\mathsf{insert}3\mathsf{IntLists}\mathsf{.}\mathsf{empty}\text{and}\mathsf{IntSets}\mathsf{.}\mathsf{insert}3\mathsf{IntSets}\mathsf{.}\mathsf{empty}$$ are well typed at their different carrier types. The equality dictionary $t\to t\to \mathsf{Bool}$ contains neither an associated element type nor the $\mathsf{empty}$ and $\mathsf{insert}$ operations. Replacing the module by that single function would discard precisely the static information this class is meant to expose.

The smallest counterexample is $$\mathrm{\Theta }=\{\mathsf{EqInt}:\mathsf{EQ}[\mathsf{Int}]\}.$$ It resolves integer equality to $\mathsf{EqInt}$. If an extension is allowed to replace that head with $\mathsf{EqNever}:\mathsf{EQ}[\mathsf{Int}]$, the same request resolves to $\mathsf{EqNever}$. Stability fails already at a one-node evidence tree.

A stronger valid statement is the following. Let $\mathrm{\Theta }$ and ${\mathrm{\Theta }}^{\prime }$ be finite admissible environments, viewed as maps from result heads to declarations. Suppose that, for every head used in the derivation of $\mathrm{\Theta }⊢K[\tau ]{\Downarrow }_{\mathsf{res}}V$, the declaration stored at that head in ${\mathrm{\Theta }}^{\prime }$ is syntactically identical to the declaration stored in $\mathrm{\Theta }$. Entries at all other heads may be inserted, deleted, or replaced. Then ${\mathrm{\Theta }}^{\prime }⊢K[\tau ]{\Downarrow }_{\mathsf{res}}V$, and its deterministic resolver returns $V$.

Prove this by induction on the derivation of $V$. At a base node, the identical declaration remains the lookup result. At a functor node, the identical functor remains the lookup result, and the induction hypotheses preserve every premise evidence subtree. Reapplying R-Functor reconstructs exactly $V$. Changes at heads outside the old tree are never consulted. Admissibility of ${\mathrm{\Theta }}^{\prime }$ ensures that the deterministic resolver is defined and that no competing declaration exists at a retained head.

The two evidence paths are $$\mathsf{OrdToEq}(\mathsf{OrdInt})\text{and}\mathsf{HashToEq}(\mathsf{HashInt}),$$ and both match $\mathsf{EQ}$ with carrier $\mathsf{Int}$. The search is a diamond because distinct source modules and functors converge on the same requested module type.

An alias test may collapse the paths when both applications elaborate to a manifest alias of one named module, for example when their result signatures and module equations establish $$\mathsf{OrdToEq}(\mathsf{OrdInt})=\mathsf{EqInt}=\mathsf{HashToEq}(\mathsf{HashInt})$$ in the module language’s decidable path-equivalence relation. Merely knowing that the two $\mathsf{eq}$ functions return the same booleans on all integer inputs is not such a test. Extensional equality of arbitrary functions is not decidable in a general programming language, and the modules may contain additional components invisible to that one observation.

Let the implicit environment contain, from left to right, $$i:\mathsf{Int},b:\mathsf{Bool},y:\mathrm{\forall }X.X?\to \mathsf{Int},$$ and ultimately check a query at $\mathsf{Int}$. In both derivations, SI-Query first synthesizes the type of the same rightmost implicit variable $y$, so lexical well-scopedness does not distinguish them. SI-AllE can nevertheless choose $X=\mathsf{Int}$, after which SI-ImpE supplies $i$ and SI-Stitch reaches the checking judgment, yielding $$y[\mathsf{Int}]i:\mathsf{Int},$$ or SI-AllE can choose $X=\mathsf{Bool}$, after which SI-ImpE supplies $b$, yielding $$y[\mathsf{Bool}]b:\mathsf{Int}.$$ These are distinct elaborations of the same query.

The monomorphic uniqueness induction relies on the synthesized restricted type of a selected term determining the chain of implicit eliminations. The nondeterministic $\mathrm{\forall }$-elimination step now inserts an arbitrary type before that chain, so the induction no longer determines one premise derivation. This is failure of uniqueness even when both derivations are finite. Divergence is a separate algorithmic possibility caused by recursive implicit search; it is not needed for this counterexample.

1. Use modular implicits. Put each pretty-printer module in the lexical implicit search space of the call sites where it is intended to be unique. The search key is the constrained $\mathsf{SHOW}$ module type.

2. Use modular type classes, or equivalently explicit modules when omission is unnecessary. A module signature can carry an associated abstract output type and preserve it across an abstraction boundary.

3. Use SI implicit functions. The tolerance is an ordinary value selected by expected type and the rightmost lexical binding, exactly the required shadowing behavior.

4. Use explicit module passing. The dependency is visible at every call, and there is no candidate search whose failure, overlap, or environmental change could alter selection.

5. Use ${\mathsf{MTC}}_0$ or the full modular-type-class discipline. The pair $(\mathsf{EQ},c)$ selects one total constructor functor, and recursive requests follow the nested type structure.

For item 1, SI is a plausible alternative: one could pass an implicit value of type $t\to \mathsf{String}$. It is worse when the printer is naturally a module with associated types or auxiliary operations, because type-only value search loses that module interface and can collide with unrelated implicit functions of the same ordinary type.