Subtyping weirdness with optional fields

[dmkolobov]

There seems to be a regression in the subtyping of records with multiple optional fields.

In particular, while the following types correctly:

(\(x: {a: Int; b?: Int}) -> x) {a = 0}

resulting in the term:

({ a = 0 } , { b = () })

expressions like

(\(x: {a: Int; b?: Int; c?: Int}) -> x) {a = 0}

result in a sub-typing error:

1:1: expected the argument type to be a subtype of the parameter type, but got { a : Int } and (({ a : Int } & { b : (Int | ()) }) & { c : (Int | ()) })

I would expect the above to result in a term like:

(({a = 0}, { b = ()}), {c = ()})

[yzyzsun]

Hi @dmkolobov, thank you for your feedback!

The weird behavior was not expected. It's due to the ongoing change to the core representation of optional fields. I'll look into this issue and fix it soon.

[dmkolobov]

@yzyzsun Possibly related, after seeing that optional labels are now encoded as {lbl = T | ()}, I wrote the following function:

f1 (x : {a: Int} & ({b: Int} | ()))
  = x;

woB = f1 ({a = 0}, ());
withB = f1 {a = 0; b = 1};

the above typechecks as expected(according to my intuition). However, extending the right side of the union with more than two labels causes a subtyping error when trying to define an equivalent with* term:

f2 (x : {a: Int} & ({b: Int; c: Int} | ()))
  = x;

-- Ok
woBC = f2 ({a = 0}, ());

-- Subtyping Error
withBC = f2 {a = 0; b = 1; c = 2};

Thanks working on this project! We use an Haskell-like language at work with row-polymorphism based on disjoint partitioning constraints called Ermine. CP seems like it might one day be able to encode some version of our SQL-like relational programming DSL!

[yzyzsun]

Hi @dmkolobov, sorry for my late reply (I was on a trip).

First, I'd like to clarify that the current encoding of {b?: Int} is {b: Int | ()} instead of {b: Int} | (). It could work because we further add ,{b = ()} to every call sites of f1, e.g. turning f1 {a = 0} into f1 ({a = 0},{b = ()}). In short, labels are kept even when they are optional.

Concerning the bugs you mentioned, it turns out to be two separate bugs: one is due to a small typo, and the other is associated with the order of pattern matching in subtyping. They are fixed in 3ca8fc3.

Again, many thanks for your interest in CP! Btw, Ermine looks awesome but it seems no more actively developed. Are you using an in-house fork?