Subtyping: Missing record fields must decode at type `reserved` for transitivity

[nomeata]

We currently have this rule:

<nat> not in <fieldtype>;*
record { <fieldtype>;* } <: record { <fieldtype'>;* } ~> f
------------------------------------------------------------------------------
record { <fieldtype>;* } <: record { <nat> : opt <datatype'>; <fieldtype'>;* }
  ~> \x.{f x with <nat> = null}

This gives record {} <: record { foo : opt bool }.

We also have record { foo : opt bool } <: record { foo : reserved } (by virtue of opt bool <: reserved).

By transitivity, we should have record {} <: record { foo : reserved }.

So it seems we need

<nat> not in <fieldtype>;*
record { <fieldtype>;* } <: record { <fieldtype'>;* } ~> f
------------------------------------------------------------------------------
record { <fieldtype>;* } <: record { <nat> : reserved; <fieldtype'>;* }
  ~> \x.{f x with <nat> = null}

as well.

(This uses null as an arbitrary representation for a reserved value. Woudn’t mind adding an explicit reserved to the textual representation and data model, that would be handy in other contexts as well.)

We could combine the two into a single rule by saying

<nat> not in <fieldtype>;*
record { <fieldtype>;* } <: record { <fieldtype'>;* } ~> f
opt empty <:  <datatype'>
------------------------------------------------------------------------------
record { <fieldtype>;* } <: record { <nat> : <datatype'>; <fieldtype'>;* }
  ~> \x.{f x with <nat> = null}

[rossberg]

Good catch. I like the combined rule.

Not sure how I feel about adding a reserved value. Reserved is meant to be the top type, so it would be somewhat odd if it was inhabited by an additional distinguished value (that has no counterpart in practice). For canonicalisation, I think null is fine, as you did in #128.

[nomeata]

Thanks! Since #128 seems to be acceptable (once refined), I’ll fix it there

[nomeata]

Fixed in #128