Improve read-only difference to take advantage of read-only fields

[jclark]

At the moment, the read-only difference operation used for narrowing doesn't do anything special with readonly fields, but it could. In particular, we can encourage a pattern where a read-only string tag field (perhaps in conjunction with #555) e.g.

type Person Employee|Customer;

type Employee record {
    const role = "employee";
    decimal salary;
};

type Customer record {
    const role = "customer";
    Address address;
};

function foo(Person p) {
   if p is Employee {
      employeeFoo(p);
   }
  else {
     // safe to narrow p to Customer here
     customerFoo(p);
  }
}

Related to #828 and #1014.

[jclark]

We are trying to find a condition on T and R that allows us to safely make T -_ro R be T - R.

Suppose t be a field name. Let D be T - R. Let R_t be the type of t allowed by R and let D_t be the type of t allowed by D. Then it is a sufficient condition if

• t is readonly in T;
• t is required by R; and
• the intersection of R_t and D_t is empty

In the case above

• T is Person
• t is role
• R is Employee
• R_t is the singleton string employee
• D is exactly Customer (since Employee and Customer are disjoint)
• D_t is the singleton string customer

So the conditions all apply.

I think we can generalize this to look at all the readonly fields together.

[jclark]

We need to be careful to get the inherent type of a value with readonly fields right: the inherent type of the readonly field needs to be a singleton (analogous to read-only types_ even if the type descriptor allows more than this. Otherwise the above won't work.