Prophet

So, I'm currently implementing polymorphic variants for Polaris. These are roughly the sum-type equivalent of row polymorphic records, i.e.

[ `A(5), `B("a") ]

has type

List(< A(Int), B(String) | r0 >)

Here r0 is a unification variable, which means that, depending on the choice of r0 this could be a type that contains the given constructors for A and B, one that additionally contains a constructor C(Bool), or any other variant type, as long as it contains constructors for A and B.

Most of this is relatively straight forward, but I'm really not sure how to deal with pattern matching. The issue here is that there are two ways to pattern match on a polymorphic variant

Case 1

let f(x) = match x {
    `A(y) -> y + 1
    `B(y) -> y + 2
}

In this case, the inferred type for x should obviously be < A(Int), B(Int) >, i.e. a type that only contains A and B and no other constructors.

Crucially, the type < A(Int), B(Int) | r0 > would be wrong here, since the match does not handle any other constructors.

Case 2

let f(x) = match x {
    `A(y) -> y + 1
    `B(y) -> y + 2
    _ -> 0
}

This time, there is a case for any other possible constructor, so < A(Int), B(Int) > is too limiting. After all, calling f(C(5)) would be perfectly fine at runtime!

So really, this should infer the type of x to be < A(Int), B(Int) | r0 >. I'm just... not sure how to do this.

The way I handle inference for other patterns right now is (roughly) to infer the types of each pattern and then unify all of them. Usually this leads to the desired results, but in this case this is a bit problematic.

If I were to infer the type of an individual constructor pattern A(x) to be a closed variant < A(a0) >, then neither of the above cases would compile, since the typechecker would need to unify < A(Int) > ~ < B(Int) >, which is obviously impossible.

If I were to infer these as open variants instead (< A(a0) | r0 >), then Case 2 would work flawlessly, but Case 1 would infer to < A(Int), B(Int) | r0 >, which is too generic!

What I really need to do is to somehow infer individual patterns to < A(a0) | #r0 > or something, where #r0 is some kind of special unification variable that defaults to <> (the empty variant), unless it is unified with a regular unification variable. This way, Case 1 would default to #r0 := <>, which would infer < A(Int), B(Int) > for x (good!) and Case 2 would unify the previous type with a fresh unification variable a0 for the wildcard pattern, preventing the defaulting of #r0 and inferring the type `< A(Int), B(Int) | r0 >.

This doesn't sound too difficult, but if you paid close attention, you will notice that this still doesn't quite work. In Case 2, the wildcard case does not unify #r0 ~ a0, but < A(a0) | #r0 > ~ a0.

So to make this work, #r0 would need to decay to a regular type variable whenever it is somehow part of a type that is unified with another regular unification variable. This sounds... complicated.

I'm not sure that this is the right approach.