From 4a20533d9ba8487b159f69c42bddf3e8b455f3c7 Mon Sep 17 00:00:00 2001
From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Date: Thu, 6 Jan 2022 12:48:09 -0600
Subject: [PATCH] RFC: Fix an unsoundness issue around stripping optional
properties (#276)
* Fix an unsoundness issue around stripping optional properties
Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com>
---
docs/unsealed-table-literals.md | 76 +++++++++++++++++++
...le-subtyping-strips-optional-properties.md | 66 ++++++++++++++++
2 files changed, 142 insertions(+)
create mode 100644 docs/unsealed-table-literals.md
create mode 100644 docs/unsealed-table-subtyping-strips-optional-properties.md
diff --git a/docs/unsealed-table-literals.md b/docs/unsealed-table-literals.md
new file mode 100644
index 0000000..320bf7c
--- /dev/null
+++ b/docs/unsealed-table-literals.md
@@ -0,0 +1,76 @@
+# Unsealed table literals
+
+## Summary
+
+Currently the only way to create an unsealed table is as an empty table literal `{}`.
+This RFC proposes making all table literals unsealed.
+
+## Motivation
+
+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 the only way to create an unsealed table is using an empty table literal, so
+```lua
+ local t = {}
+ t.p = 5
+ t.q = "hi"
+```
+typechecks, but
+```lua
+ local t = { p = 5 }
+ t.q = "hi"
+```
+does not.
+
+This causes problems in examples, in particular developers
+may initialize properties but not methods:
+```lua
+ local t = { p = 5 }
+ function t.f() return t.p end
+```
+
+## Design
+
+The proposed change is straightforward: make all table literals unsealed.
+
+## Drawbacks
+
+Making all table literals unsealed is a conservative change, it only removes type errors.
+
+It does encourage developers to add new properties to tables during initialization, which
+may be considered poor style.
+
+It does mean that some spelling mistakes will not be caught, for example
+```lua
+local t = {x = 1, y = 2}
+if foo then
+ t.z = 3 -- is z a typo or intentional 2-vs-3 choice?
+end
+```
+
+In particular, we no longer warn about adding properties to array-like tables.
+```lua
+local a = {1,2,3}
+a.p = 5
+```
+
+## Alternatives
+
+We could introduce a new table state for unsealed-but-precise
+tables. The trade-off is that that would be more precise, at the cost
+of adding user-visible complexity to the type system.
+
+We could continue to treat array-like tables as sealed.
\ No newline at end of file
diff --git a/docs/unsealed-table-subtyping-strips-optional-properties.md b/docs/unsealed-table-subtyping-strips-optional-properties.md
new file mode 100644
index 0000000..deecfdb
--- /dev/null
+++ b/docs/unsealed-table-subtyping-strips-optional-properties.md
@@ -0,0 +1,66 @@
+# Only strip optional properties from unsealed tables during subtyping
+
+## Summary
+
+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.
+
+## Motivation
+
+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:
+```lua
+ 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:
+```lua
+ local t : { p: number, q: string? } = { p = 5, q = "hi" }
+ local u : { p: number } = { p = 5, q = false }
+ t = u
+```
+
+## Design
+
+The fix for this source of unsoundness is twofold:
+
+1. make all table literals unsealed, and
+2. only allow stripping optional properties from when the
+ supertype is sealed and the subtype is unsealed.
+
+This RFC is for (2). There is a [separate RFC](unsealed-table-literals.md) for (1).
+
+## Drawbacks
+
+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:
+```lua
+ 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.
+
+## Alternatives
+
+We could just live with unsoundness.
+