Status: Implemented
Currently subtyping allows optional properties to be stripped from table types during subtyping. This RFC proposes only allowing that when the subtype is unsealed and the supertype is sealed.
Table types can be sealed or unsealed. These are different in that:
Unsealed table types are precise: if a table has unsealed type { p: number, q: string }
then it is guaranteed to have only properties p
and q
.
Sealed tables support width subtyping: if a table has sealed type { p: number }
then it is guaranteed to have at least property p
, so we allow { p: number, q: string }
to be treated as a subtype of { p: number }
Unsealed tables can have properties added to them: if t
has unsealed type
{ p: number }
then after the assignment t.q = "hi"
, t
’s type is updated to be
{ p: number, q: string }
.
Unsealed tables are subtypes of sealed tables.
Currently we allow subtyping to strip away optional fields as long as the supertype is sealed. This is necessary for examples, for instance:
local t : { p: number, q: string? } = { p = 5, q = "hi" }
t = { p = 7 }
typechecks because { p : number }
is a subtype of
{ p : number, q : string? }
. Unfortunately this is not sound,
since sealed tables support width subtyping:
local t : { p: number, q: string? } = { p = 5, q = "hi" }
local u : { p: number } = { p = 5, q = false }
t = u
The fix for this source of unsoundness is twofold:
This RFC is for (2). There is a separate RFC for (1).
This introduces new type errors (it has to, since it is fixing a source of unsoundness). This means that there are now false positives such as:
local t : { p: number, q: string? } = { p = 5, q = "hi" }
local u : { p: number } = { p = 5, q = "lo" }
t = u
These false positives are so similar to sources of unsoundness that it is difficult to see how to allow them soundly.
We could just live with unsoundness.