Proposed type reduction rule for Scala 3

Below is a copy of a draft outlining the proposal of an additional rule for match type reduction in Scala 3. It was shared (as a Mathcha link) on Scala Contributors, as a follow-up to this discussion.

In this draft is presented an additional subtyping rule for System FM. It is meant to be a continuation of (S-Match1/2) from Fig. 2 in Type-Level Programming with Match Types, copied here:

$$\frac{\forall m< n.\Gamma \vdash \operatorname{disj}(\mathrm{T}_{s} ,\ \mathrm{S}_{m}) \ \ \ \ \ \ \ \ \ \ \ \Gamma \vdash \mathrm{T}_{s} < :\mathrm{S}_{n}}{\Gamma \vdash \mathrm{T}_{s} \ match\{\mathrm{S}_{i} \Rightarrow \mathrm{T}_{i}\} \ or\ \mathrm{T}_{d} =:=\mathrm{T}_{n}} \ \ \ \ \ \text{(S-Match1/2)}$$

(S-Match1/2) requires the premise \( \Gamma \vdash \mathrm{T}_{s} < :\mathrm{S}_{n}\) in order to apply. The new rule picks up where (S-Match1/2) leaves off, by dropping this requirement. So it is intended to be complementary with (S-Match1/2).

Before introducing it, here are two paragraphs to give some of the intuition behind it:

The new rule is about when a case can be skipped, even though it cannot be shown to be disjoint from the scrutinee. It says that it can be skipped when, for each way that the type could reduce on the \(n^{_{\Large\text{th}}}\) match, reducing the type on the remaining matches would be equivalent.

The idea is that, regardless of whether the \(n^{_{\Large\text{th}}}\) case matches, the result should be indistinguishable for the rule to apply. It achieves this by ensuring that, for all possible ways the case could match, the result would be the same as if the case had been skipped.

Here is the new rule:

$$\frac{ \begin{array}{l} \forall 𝑚< 𝑛.\Gamma \vdash \operatorname{disj}(\mathrm{T}_{s} ,\ \mathrm{S}_{m}) \ \ \ \ \ \ \ \ \ \ \ \{\Delta _{1} ,\ ...,\ \Delta _{k}\} \ \leftarrow \ \operatorname{unification}_{\Gamma }(\mathrm{T}_{s} ,\ \mathrm{S}_{n})\\ \forall j\ \leq k.\ \ \Gamma ,\ \Delta _{j} \ \vdash \ \mathrm{T}_{s} \ match\{i\ >\ n;\ \mathrm{S}_{i} \Rightarrow \mathrm{T}_{i}\} \ or\ \mathrm{T}_{d} \ =:=\ \mathrm{T}_{n} \end{array}}{\Gamma \vdash \ \ \mathrm{T}_{s} \ match\{\mathrm{S}_{i} \Rightarrow \mathrm{T}_{i}\} \ or\ \mathrm{T}_{d} \ =:=\ \mathrm{T}_{s} \ match\{i\ >\ n;\ \mathrm{S}_{i} \Rightarrow \mathrm{T}_{i}\} \ or\ \mathrm{T}_{d}}$$

Here, \(\displaystyle \mathrm{T}_{s} \ match\{i\ >\ n;\ \mathrm{S}_{i} \ \Rightarrow \ \mathrm{T}_{i}\}\) means \(\mathrm{T}_{s} \ match\{\mathrm{S}_{n+1} \Rightarrow \mathrm{T}_{n+1} ;\mathrm{S}_{n+2} \Rightarrow \mathrm{T}_{n+2} ;\ ...\}\). In other words, it is a match expression being made up of all the remaining cases after the \(n^{_{\Large\text{th}}}\).

\(\{\Delta _{1} ,\ ...,\ \Delta _{k}\} \ \leftarrow \ \operatorname{unification}_{\Gamma }(\mathrm{T}_{s} ,\ \mathrm{S}_{n})\) means that unifying \(\mathrm{T}_{s}\) and \(\mathrm{S}_{n}\) succeeds and results in a complete set of \(k\) minimal unifiers. In order to usefully formalize unification in System FM, I think the (meta-)logic has to be extended somewhat. Below is my (probably clumsy) attempt at a semi-formal presentation.

First, I define what it means for a context to be minimal for equality with the \math-container \(\operatorname{minEqCxt}\) predicate:

$$\frac{\Gamma ,\Delta \vdash \mathrm{T}_{s} =:=\ \mathrm{S}_{n} \ \ \ \ \ \ \ \forall \ \Delta '.\ \ \Delta \vdash \Delta '\ \Longrightarrow \ ( \Delta \equiv \Delta ') \ \lor \ ( \Gamma ,\ \Delta '\nvdash \mathrm{T}_{s} =:=\ \mathrm{S}_{n})}{\operatorname{minEqCxt}_{\Gamma ,\ \mathrm{T}_{s} ,\ \mathrm{S}_{n}}( \Delta )}$$

Then, I want to be able to express statements within a different class inheritance hierarchy \(\Psi'\). So I define the \(\operatorname{compatWith}\) predicate to represent compatible extensions of a given hierarchy \(\Psi\). To do so, I introduce an additional type of context, \(\Sigma\) (in addition of \(\Psi\) and \(\Xi\)), which is simply the set of all classes known to be sealed.

$$\frac{ \begin{array}{l} \Psi \subset \Psi '\ \ \ \ \ \ \ \ \operatorname{partialOrder}( \Psi ') \ \ \ \ \ \ \ \ \ \Psi '\ \operatorname{consistentWith} \ \Xi \\ \forall \ \mathrm{C}_{2} \in \Sigma .\forall \mathrm{C}_{1} .\ (\mathrm{C}_{1} ,\ \mathrm{C}_{2}) \in \Psi '\Longrightarrow (\mathrm{C}_{1} ,\ \mathrm{C}_{2}) \ \in \Psi \\ \forall \ \mathrm{C_{1} ,C}_{2} \in \boldsymbol{C} .\ (\mathrm{C}_{1} ,\ \mathrm{C}_{2}) \in \Psi '\Longrightarrow (\mathrm{C}_{1} ,\ \mathrm{C}_{2}) \ \in \Psi \end{array}}{\Psi '\ \operatorname{compatWith} \ ( \Psi ,\Xi ,pSigma )}$$

Here, \(\boldsymbol{C}\) is the set of all classes over which \(\Psi\) is defined (\(\Psi'\) may introduce additional classes). And \(\operatorname{consistentWith}\) corresponds to the consistency condition defined in the paper: “Inheritance and disjointness must be consistent in the sense that \((\mathrm{A} ,\ \mathrm{B}) \ \in \ \Xi \) implies that there is no class \(\mathrm{C}\) such that \((\mathrm{C} ,\mathrm{A}) \ \in \ \Psi \) and \((\mathrm{C} ,\ \mathrm{B}) \ \in \ \Psi \) ”.

Finally, I provide a rule for unification:

$$\frac{ \begin{array}{l} \forall \ i\ \leq k.\operatorname{minEqCxt}_{\Gamma ,\ \mathrm{T}_{s} ,\ \mathrm{S}_{n}}( \Delta _{i})\\ \forall \ \Psi '\ \operatorname{compatWith} \ ( \Psi ,\Xi ,\Sigma ) .\ \forall \ \Delta '.\ ( \Psi ';\Gamma ,\Delta '\vdash \mathrm{T}_{s} =:=\ \mathrm{S}_{n}) \ \Longrightarrow \ \exists \ i\ \leq k.\ \Gamma ,\ \Delta '\vdash \Delta _{i} \end{array}}{\{\Delta _{1} ,\ ...,\ \Delta _{k}\} \ \leftarrow \ \operatorname{unification}_{\Gamma }(\mathrm{T}_{s} ,\ \mathrm{S}_{n})}$$

Here, the inheritance context is specified explicitly when it is not equal to \(\Psi\). Notice that if the unification is known to be impossible because \(\operatorname{disj}(\mathrm{T}_{s} ,\ \mathrm{S}_{m})\), then \(k\) is \(0\). Notice also that it might be impossible to deduce any unification for \(\mathrm{T}_s\) and \(\mathrm{S}_n\), for example due to some types not being sealed (in which case the rule does not apply).

Note 1: It might be possible to make the additional rule stronger in some ways.

Note 2: It might be necessary to make the additional rule weaker in some ways to make it practical and efficiently computable.

Note 3: The additional rule need only be considered when \(\ \Gamma \ \nvdash \ \mathrm{T}_{s} \ < :\ \mathrm{S}_{n}\) and \(\Gamma \ \nvdash \ \operatorname{disj}(\mathrm{T}_{s} ,\ \mathrm{S}_{m})\) hold (adding these as premises to the rule doesn't change the typing logic).

Note 4: I probably missed a bunch of stuff, and made a bunch of mistakes.