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

  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:

  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.