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.