Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
KevSlashNull opened this issue Jun 22, 2024 · 1 comment
Labels
semantics Unexpected or unsound behaviors

Comments

@KevSlashNull
Copy link

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. ✔️ Errors as expected

printCar({
  name = "My car"
})

unknown field name

2. ✔️ Errors as expected

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

in local declaration: car: unknown field name

3. ❌ 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.

@hishamhm hishamhm added the semantics Unexpected or unsound behaviors label Sep 14, 2024
@hishamhm
Copy link
Member

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
semantics Unexpected or unsound behaviors
Projects
None yet
Development

No branches or pull requests

2 participants