Modular type classes and implicit evidence

The finite calculus uses constructor trees $\tau ::=c({\tau }_1,\dots ,{\tau }_n)$, realized atomic signatures $K[\tau ]$, and declarations $$F:K_1[{\alpha }_{j_1}],\dots ,K_m[{\alpha }_{j_m}]{\Rightarrow }_{\mathsf{mod}}K[c({\alpha }_1,\dots ,{\alpha }_n)].$$ Every premise index satisfies $j_r\in \{1,\dots ,n\}$. An environment is admissible exactly when all declarations have their displayed interfaces, every premise selects an immediate constructor argument, and no two declarations have the same result head $(K,c)$. Its complete resolution rules are

$P:K[c]\in \mathrm{\Theta }$

$\mathrm{\Theta }⊢K[c]{\Downarrow }_{\mathsf{res}}P$

$F:K_1[{\alpha }_{j_1}],\dots ,K_m[{\alpha }_{j_m}]{\Rightarrow }_{\mathsf{mod}}K[c({\alpha }_1,\dots ,{\alpha }_n)]\in \mathrm{\Theta }$$\mathrm{\Theta }⊢K_r[{\tau }_{j_r}]{\Downarrow }_{\mathsf{res}}{V}_r(1\le r\le m)$

$\mathrm{\Theta }⊢K[c({\tau }_1,\dots ,{\tau }_n)]{\Downarrow }_{\mathsf{res}}F⟨V_1,\dots ,V_m⟩$

Evidence typing is the least judgment generated by

$P:K[c]\in \mathrm{\Theta }$

$\mathrm{\Theta }⊢P:K[c]$

$F:K_1[{\alpha }_{j_1}],\dots ,K_m[{\alpha }_{j_m}]{\Rightarrow }_{\mathsf{mod}}K[c({\alpha }_1,\dots ,{\alpha }_n)]\in \mathrm{\Theta }$$\mathrm{\Theta }⊢V_r:K_r[{\tau }_{j_r}](1\le r\le m)$

$\mathrm{\Theta }⊢F⟨V_1,\dots ,V_m⟩:K[c({\tau }_1,\dots ,{\tau }_n)]$

For the selected overloaded term fragment, ordinary forms elaborate homomorphically and the two evidence-inserting rules are

$\mathrm{\Theta }⊢\mathsf{EQ}[\tau ]{\Downarrow }_{\mathsf{res}}V$$\mathrm{\Gamma };\mathrm{\Theta }⊢e_i:\tau ⇝e_i^{\prime }(i=1,2)$

$\mathrm{\Gamma };\mathrm{\Theta }⊢\mathsf{eq}[\tau ](e_1,e_2):\mathsf{Bool}⇝V.\mathsf{eq}{e}_1^{\prime }{e}_2^{\prime }$

$\mathrm{\Theta }⊢\mathsf{SHOW}[\tau ]{\Downarrow }_{\mathsf{res}}V$$\mathrm{\Gamma };\mathrm{\Theta }⊢e:\tau ⇝e^{\prime }$

$\mathrm{\Gamma };\mathrm{\Theta }⊢\mathsf{show}[\tau ](e):\mathsf{String}⇝V.\mathsf{show}{e}^{\prime }$

The inserted evidence is typed in the target by

$P:K[c]\in \mathrm{\Theta }$

$\mathrm{\Gamma };\mathrm{\Theta }⊢P:K[c]$

$\mathrm{\Theta }(F)=\overline{K}[\overline{\alpha }]{\Rightarrow }_{\mathsf{mod}}K[c(\overline{\alpha })]$$\mathrm{\Gamma };\mathrm{\Theta }⊢V_r:K_r[{\tau }_{j_r}](1\le r\le m)$

$\mathrm{\Gamma };\mathrm{\Theta }⊢F⟨V_1,\dots ,V_m⟩:K[c(\overline{\tau })]$

$\mathrm{\Gamma };\mathrm{\Theta }⊢V:K[\tau ]$$f:A(t)\text{ is a field of }K$

$\mathrm{\Gamma };\mathrm{\Theta }⊢V.f:A(\tau )$

For modular implicits, let $\mathcal{I};\mathrm{\Gamma }⊢S{\Downarrow }_{\mathsf{cand}}\{V_1,\dots ,V_n\}$ be the finite candidate set after solving the omitted module’s type-component equations. The call boundary is

$\mathcal{I};\mathrm{\Gamma }⊢S{\Downarrow }_{\mathsf{cand}}\{V\}$$\mathrm{\Gamma }⊢f:\{M:S\}\to {\tau }_1\to {\tau }_2$$\mathrm{\Gamma }⊢x:{\tau }_1$

$\mathcal{I};\mathrm{\Gamma }⊢fx⇝f\{V\}x:{\tau }_2$

The SI fragment uses restricted types $R::=X\mid T\to T$, full types $T::=R\mid T?\to T\mid \mathrm{\forall }X.T$, and one ordered context with explicit bindings $x:T$ and implicit bindings $y:T$. Figure 3 is:

$x:T\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\Rightarrow T⇝x$

$y:T\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢?\Rightarrow T⇝y$

$\mathrm{\Gamma },x:S⊢e\Leftarrow T⇝u$

$\mathrm{\Gamma }⊢\lambda x.e\Leftarrow S\to T⇝\lambda x:S^{\ast }.u$

$\mathrm{\Gamma }⊢e_1\Rightarrow S\to T⇝u$$\mathrm{\Gamma }⊢e_2\Leftarrow S⇝u^{\prime }$

$\mathrm{\Gamma }⊢e_1{e}_2\Rightarrow T⇝u{u}^{\prime }$

$y\mathsf{fresh}$$\mathrm{\Gamma },y:S⊢e\Leftarrow T⇝u$

$\mathrm{\Gamma }⊢e\Leftarrow S?\to T⇝\lambda y:S^{\ast }.u$

$\mathrm{\Gamma }⊢e\Rightarrow S?\to T⇝u$$\mathrm{\Gamma }⊢?\Leftarrow S⇝u^{\prime }$

$\mathrm{\Gamma }⊢e\Rightarrow T⇝u{u}^{\prime }$

$\mathrm{\Gamma },X⊢e\Leftarrow T⇝u$

$\mathrm{\Gamma }⊢e\Leftarrow \mathrm{\forall }X.T⇝\mathrm{\Lambda }X.u$

$\mathrm{\Gamma }⊢e\Rightarrow \mathrm{\forall }X.T⇝u$

$\mathrm{\Gamma }⊢e\Rightarrow [X:=S]T⇝u[S^{\ast }]$

$\mathrm{\Gamma }⊢e_1\Leftarrow T⇝u$$\mathrm{\Gamma },x:T⊢e_2\Rightarrow R⇝u^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{let}x:T=e_1\mathsf{in}{e}_2\Rightarrow R⇝(\lambda x:T^{\ast }.u^{\prime })u$

$\mathrm{\Gamma }⊢e_1\Leftarrow T⇝u$$y\mathsf{fresh}$$\mathrm{\Gamma },y:T⊢e_2\Rightarrow R⇝u^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{let}?:T=e_1\mathsf{in}{e}_2\Rightarrow R⇝(\lambda y:T^{\ast }.u^{\prime })u$

$\mathrm{\Gamma }⊢e\Rightarrow R⇝u$

$\mathrm{\Gamma }⊢e\Leftarrow R⇝u$

Here $(-{)}^{\ast }$ maps both arrow forms to ordinary System F arrows. The rightmost choice is an external well-scopedness condition on derivations, not a premise of SI-Query.