Function does not enforce argument record type if variable type is inferred

Description

Passing a variable to a function, which expects a specific record type, if the type of the variable does not match the argument incorrectly doesn’t error if the type of the variable is inferred from its assigned value.

Expected behavior

Function arguments should be the specified type, unless type checking is circumvented with e.g. { name = "" } as any as Car.

Example

Let’s assume this is available in each example.

global record Car
  licensePlate: string
end

global function printCar(_car: Car) end

1. :heavy_check_mark: Errors as expected

printCar({
  name = "My car"
})

unknown field name

2. :heavy_check_mark: Errors as expected

local car: Car = {
  name = ""
}
printCar(car)

in local declaration: car: unknown field name

3. :x: No error

local car = {
  name = ""
}
printCar(car)

The variable car is not a valid Car because Car does not have the field name, only licensePlate.

I can explain why that currently happens:

When you declare a literal table with { } notation, Teal tries to give it a type based on the context of declaration, from which it compares to an "expected type". In case 1, its context of declaration is an argument of type Car. In case 2, the context is declaration of a local variable of type Car.

In case 3, its context of declaration is a local variable of unknown type. So the car variable ends up with a vague anonymous record type (that is not Car). Afterwards, when type-checking the function call, Teal compares the Car type against the anonymous table type, and then two things cause the comparison to not fail: bivariant checking (that is, subtype relations are accepted in both directions), and nil non-strictness (required fields may be nil). So that anonymous record type for the literal table gets interpreted as an acceptable subtype of Car, where name is an ignored field of the subtype, and licensePlate is nil.

The semantics could be changed so that anonymous records get invariant checking upon its first use with a type, but that might be a breaking change that wouldn't work well in cases where one may need the subtyping behavior. In any case, I don't consider this to be a bug per se, but it is unsound from a theory perspective (and does cause a practical footgun in cases like this).

I will keep this open since I think we might need to revisit this behavior once we get more experience dealing with interfaces, as they get introduced in the upcoming version of Teal.

teal-language / tl