teal-language / tl

The compiler for Teal, a typed dialect of Lua
MIT License
2.02k stars 101 forks source link

A or B result is always inferred as A when A and B are records #712

Open Aire-One opened 8 months ago

Aire-One commented 8 months ago

Hello :wave:

I think this issue is older, but with the recent nominal changes in record types, I have played a bit in my code base and stepped on that weird behavior. We can summarize the problem with the following code example :

https://teal-playground.netlify.app/?c=bG9jYWwgcmVjb3JkIEEKICAgZm9vOiBzdHJpbmcKZW5kCgpsb2NhbCByZWNvcmQgQgogICBiYXI6IHN0cmluZwplbmQKCmxvY2FsIGE6IEEKbG9jYWwgYjogQgoKbG9jYWwgcjEgPSBhIG9yIGIKcHJpbnQocjEuZm9vKQpwcmludChyMS5iYXIpCgpsb2NhbCByMiA9IGIgb3IgYQpwcmludChyMi5mb28pCnByaW50KHIyLmJhcik%3D

The issue still happens with https://github.com/teal-language/tl/pull/711 https://711--teal-playground-preview.netlify.app/?c=bG9jYWwgcmVjb3JkIEEKICAgZm9vOiBzdHJpbmcKZW5kCgpsb2NhbCByZWNvcmQgQgogICBiYXI6IHN0cmluZwplbmQKCmxvY2FsIGE6IEEKbG9jYWwgYjogQgoKbG9jYWwgcjEgPSBhIG9yIGIKcHJpbnQocjEuZm9vKQpwcmludChyMS5iYXIpCgpsb2NhbCByMiA9IGIgb3IgYQpwcmludChyMi5mb28pCnByaW50KHIyLmJhcik%3D

local record A
   foo: string
end

local record B
   bar: string
end

local a: A
local b: B

local r1 = a or b
print(r1.foo)
print(r1.bar) -- invalid key 'bar' in record 'r1' of type A

local r2 = b or a
print(r2.foo) -- invalid key 'foo' in record 'r2' of type B
print(r2.bar)

Notes :

In this example, we could say that Teal is smart and a or b is a a because the variable is supposed to be trusty since it's declared before, but :

I think r should be typed either, as a union of A and B (which is currently not allowed by Teal), or as the intersection of A and B (which is also something Teal doesn't allow). So I'm afraid I have found a worms' can :sweat_smile:

hishamhm commented 8 months ago

Hi! You do have a point. At least with the current behavior you do get an compile-time error when you try to use the value "inconsistently"...

It took me a bit to understand why this code was being accepted in the first place, but turns out that this works because the sets of fields in these records are disjoint (in plain English, because there are no incompatible fields among them). This is a rule that's in place to allow more lax parameter passing, in the absence of record subtyping: it's in practice a pretty lax form of structural checking.

I'll keep this issue open since this is one of the things I'm looking at, as I'm working on support for interfaces, which will bring proper record subtyping (yes, this is happening!)