Bug: in some cases teal compiler cannot catch assign `interface` to `record` error.

[BLKTower]

In simple case, the compiler can catch the error correctly:

local interface I
end
local record A is I
end
local function test(a: I): I
    return a
end
local i: I
local a: A
a = test(i) -- Error: I is not a A

But if the situation is more complex, the compile results become weird:

local interface I<T>
end
local record A1
end
local record A2 is I<A1>
end
local function test<T, K is I<T>>(a: T): K
    local k: K
    return k
end
local a1: A1
local a2: A2
local ia1: I<A1>
-- test 1
a2 = ia1 -- Error: I<A1> is not a A2
a2 = test(a1) -- No error, but it should?
-- test 2
ia1 = test(a1)
a2 = ia1 -- No error, but it should?
-- test 3
local z = test(a1)
a2 = z -- Error: I<A1> is not a A2

Desired behavior: teal compiler can catch the error.

[BLKTower]

Issue below is fixed in #962

And which makes me even more confused is if I do something like this:

local interface I<T>
end
local record A1
end
local record A2 is I<A1>
end
local record B1
end
local record B2 is I<B1>
end
local function test<T, K is I<T>>(a: T): K
    local k: K
    return k
end
local a1: A1
local b1: B1
local a2: A2
local b2: B2
a2 = test(a1)
local z = test(b1) -- From the type info json, z's type is I<A1>. Why?
b2 = z -- Error: I<A1> is not a B2. Why?

This makes no sense to me. Basically once I called test() , then all the following test() call will return the same type as the first call resolved, no matter what parameter I pass to the following test() calls.

[BLKTower]

@hishamhm Hi, not sure if this issue caught your eye, but I noticed this one is not tagged as bug somehow.

[hishamhm]

hi @BLKTower -- you mean about the code snippet in the original report, right?

Upon review, I'm not sure it is really a bug, or a side-effect of our current lenient model for function signature checking. I mean, it is a soundness bug, but in some places the type system is "unsound on purpose" in order to not impose type check errors on subtyping situations in code that actually works (and which are typical of Lua code, such as callbacks).

Having said that, I can explain what is going on here:

On function calls, type checking (including inference and resolution of generics) happens like this: first, the return type is matched against the context where the function call happened (in this case, an assignment). Then parameter types are matched against the given arguments from left to right.

So here, return type K is matched against a2 which is A2. K is a type variable with constraint K is I<T>. The algorithm successfully matches one against the other: can A2 match some I<T>? Yes, matching T to A1 because A2 is I<A1>. So now, based on the return type alone, we have resolved both K and T.

Then, it matches the argument, checking a1 against T. T was inferred to be A1 and that checks out.

Note that you do get the error you're expecting if you change the function signature to

local function test<T>(a: T): I<T>

Saying K is I<T> and then using K is just an alias to saying I<T>; type constraints are wider: they mean "for all types K that match I<T>". And, specifically, the definition of "match" is lenient such that it works bivariantly (that is, in both directions), so that it can be applied the same way to function arguments and returns (and so that users don't get surprising errors on callbacks).

[BLKTower]

hi @BLKTower -- you mean about the code snippet in the original report, right?

Yes, I was referring to the original report. The issue in the reply was fixed.

Upon review, I'm not sure it is really a bug, or a side-effect of our current lenient model for function signature checking. I mean, it is a soundness bug, but in some places the type system is "unsound on purpose" in order to not impose type check errors on subtyping situations in code that actually works (and which are typical of Lua code, such as callbacks).

Having said that, I can explain what is going on here:

On function calls, type checking (including inference and resolution of generics) happens like this: first, the return type is matched against the context where the function call happened (in this case, an assignment). Then parameter types are matched against the given arguments from left to right.

So here, return type K is matched against a2 which is A2. K is a type variable with constraint K is I<T>. The algorithm successfully matches one against the other: can A2 match some I<T>? Yes, matching T to A1 because A2 is I<A1>. So now, based on the return type alone, we have resolved both K and T.

Then, it matches the argument, checking a1 against T. T was inferred to be A1 and that checks out.

Note that you do get the error you're expecting if you change the function signature to

local function test<T>(a: T): I<T> Saying K is I<T> and then using K is just an alias to saying I<T>; type constraints are wider: they mean "for all types K that match I". And, specifically, the definition of "match" is lenient such that it works bivariantly (that is, in both directions), so that it can be applied the same way to function arguments and returns (and so that users don't get surprising errors on callbacks).

Thank you so much for the detailed explanation. I think local function test<T>(a: T): I<T> is good enough for my current use case.