forked from luau-lang/rfcs
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add RFC for type error suppression (#835)
This formalizes our strategy for suppressing type errors, and fixes the weirdness of `any` being both a top and bottom type.
- Loading branch information
1 parent
53a5ca3
commit 28466cf
Showing
1 changed file
with
131 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,131 @@ | ||
# Type Error Suppression | ||
|
||
## Summary | ||
|
||
An alternative approach to type error suppression and the `any` type. | ||
|
||
## Motivation | ||
|
||
There are two reasons for this RFC: to make clearer how we're | ||
approaching error suppression, and to remove the magic "both top and | ||
bottom" behavior of the `any` type. | ||
|
||
### Error suppression | ||
|
||
Currently, we have ad hoc error suppression, where we try to avoid cascading errors, for example in | ||
```lua | ||
local x = t.p.q.r | ||
``` | ||
|
||
if `t` is a table without a `p` field, we report a type error on | ||
`t.p`, but we avoid cascading errors by assigning `t.p` an internal | ||
`error` type, and suppressing errors in property access `M.p` when `M` | ||
has type `error`. | ||
|
||
In this RFC, we clarify that error suppression occurs when the error | ||
is caused by a type `T`, and `error` is a subtype of `T`. | ||
|
||
### The `any` type | ||
|
||
The `any` type is an outlier in the type system, in that currently it | ||
is both a top type (`T` is a subtype of `any` for all types `T`) and a | ||
bottom type (`any` is a subtype of `U` for all types `U`). This is | ||
"consistent subtyping" (written `T ≾ U`) from Siek and Taha (2007), | ||
which has the issue of not being transitive (if it were, then `T ≾ U` | ||
for all types `T` and `U`, which is not a very useful definition of | ||
subtyping). | ||
|
||
The solution used by Siek and Taha is to split consistent subtyping (`S ≾ U`) | ||
into a *consistency relation* `S ~ T` and a *subtyping relation* (`T <: U`). | ||
The role of the consistency relation is to allow `any` to stand in for any type | ||
(`any ~ T` for all types `T`). | ||
|
||
We propose something different: performing *error suppression* on | ||
failures of subtyping. We treat `any` as a top type, so `T <: any`, | ||
but suppress type error messages caused by `any <: U` failing. | ||
|
||
## Design | ||
|
||
This design uses an `error` type (though adding user syntax for it is | ||
out of scope of this RFC). | ||
|
||
Call a type: | ||
|
||
* shallowly safe when any uses of `error` or `any` are inside a table or function type, and | ||
* deeply safe when it does not contain `error` or `any` anywhere. | ||
|
||
A type `T` is shallowly unsafe precisely when `error <: T`. | ||
|
||
We add a new subtyping relationship: | ||
|
||
* `any <: unknown | error` | ||
|
||
We keep the existing subtyping relationships: | ||
|
||
* `T <: any` for any type `T` | ||
|
||
We add a proviso to `unknown` being a top type: | ||
|
||
* `T <: unknown` for any *shallowly safe* type `T` | ||
|
||
Currently, we consider a subtype test to have failed when it generates | ||
no errors. We separate out the result of the check from its errors, | ||
and instead have a requirement: | ||
|
||
* If checking `T <: U` succeeds, it produces no errors. | ||
|
||
It is now possible for a subtyping test to fail, but produce no errors. | ||
For example, `number <: any` succeeds (since `any` is the top type) | ||
and `number <: string` fails with an error, but now `any <: string` fails | ||
*but produces no errors*. | ||
|
||
For end users, who only care about errors being reported, this will not be | ||
a noticable change (but see the discussion of breaking changes below). | ||
Internally though, it helps us avoid footguns, since now subtyping | ||
is transitive. | ||
|
||
The subtype testing algorithm changes: | ||
|
||
* Subtype checking returns a boolean. | ||
* Replace all of the current tests of "errors are empty" by testing the return value. | ||
* In the case of testing `any <: T`, return `true` with no errors. | ||
* In the case of testing `T <: any`, return `false` with no errors. | ||
* In the case of testing `T <: unknown`, check `T` for being a shallowly safe type. | ||
|
||
These changes are not huge, and can be implemented for both the current greedy unifier, | ||
and future constraint solvers. | ||
|
||
Theses changes have been prototyped: https://github.com/luau-lang/agda-typeck/pull/4 | ||
|
||
## Drawbacks | ||
|
||
This is theoretically a breaking change but my word you have to work hard at it. | ||
For just checking subtyping there is no difference: the new algorithm returns `true` precisely | ||
when the old algorithm generates no errors. But it can result in different unifications. | ||
|
||
For example, if `Y` is a free type variable, then currently checking `(any & Y) <: number` | ||
will not perform any unification, which makes a difference to the program: | ||
|
||
```lua | ||
function f(x : any, y) -- introduces a new free type Y for y | ||
if x == y then -- type refinement makes y have type (any & Y) | ||
return math.abs(y) -- checks (any & Y) <: number | ||
end | ||
end | ||
``` | ||
|
||
Currently we infer type `<a>(any, a) -> number` for `f`. With the new | ||
algorithm, checking `(any & Y) <: number` will succeed by unifying `Y` | ||
with `number`, so `f` will be given the more accurate type | ||
`(any, number) -> number`. | ||
|
||
So this is a breaking change, but results in a more accurate type. | ||
In practice it is unlikely that this change will do anything but help find bugs. | ||
|
||
## Alternatives | ||
|
||
We could implement Siek and Taha's algorithm, but that only helps with | ||
`any`, not with more general error supression. | ||
|
||
We could leave everything alone, and live with the weirdness of non-transitive subtyping. | ||
|