Cannot prove subtyping of (A & B) <: ((A & B) | C)

[plietar]

Playground link

The compiler is unable to prove that the following subtyping relation holds even though the usual rules for unions and intersections should allow it.

(A & B) <: ((A & B) | C)

This is because the compiler will start by splitting the left hand side intersection before the right hand side. In other words, it tries to prove (A & B) <: ((A & B) | C) by checking if either A <: ((A & B) | C) or B <: ((A & B) | C), neither of which are true.

This particular case could be solved by switching the order in which the subtyping checks happen, by instead looking if either (A & B) <: (A & B) or (A & B) <: C hold, which the former does. However this would break cases where the subtyping relation is in conjunctive form, such as ((A | B) & C) -> (A | B).

A proper solution would be to choose either CNF or DNF, and normalise types into this form before performing subtype checking. This could happen in the flatten pass for example. With CNF, the initial example would become (A & B) <: (A | C) & (B | C), which the current subtype checker is capable of proving.

Alternatively, when checking something of the form (A & B) <: (C | D), allow any of A <: (C | D), B <: (C | D), (A & B) <: C or (A & B) <: D. While this is tolerable for union and intersection with 2 elements, larger ones may cause performance issues.

[jemc]

To summarize a bit in lay terms, adopting CNF or DNF would imply making a rule that the normalized form of a type follows certain rules about what can be contained within what, in a sort of order of precedence for the logical expression of that time.

For example, in DNF, the order is OR > AND > NOT, such that an AND (type intersection) can never contain an OR (type union), and a NOT can never contain an AND or OR. CNF is the same concept, but with AND > OR > NOT as the order.

If we ever have a type expression that violates these rules, we can normalize by redistributing terms while preserving logical equivalency.

For reference, I started experimenting this past weekend with a DNF-based type representation in Mare, in case anyone wants to get a practical sense of how that normalization would work.