Unexpectedly lax on setting integer key in {string: any}

[wqferr]

The following code works fine on master, but only if both overloads are declared

local record f
   lambda: function(string, {string: any}): function
   lambda: function({string: any}): function --> should be using this overload
end

local deg2rad = f.lambda {"x*pi/180", pi=math.pi} --> passing an intersection type as a {string:any}
print(deg2rad(180))
print(deg2rad(0))
print(deg2rad(60))

[lenscas]

https://teal-playground.netlify.app/?c=bG9jYWwgcmVjb3JkIGYKICAgbGFtYmRhOiBmdW5jdGlvbigpCiAgIGxhbWJkYTogZnVuY3Rpb24oe3N0cmluZzogaW50ZWdlcn0pOiBmdW5jdGlvbiAtLT4gc2hvdWxkIGJlIHVzaW5nIHRoaXMgb3ZlcmxvYWQKZW5kCgpsb2NhbCBkZWcycmFkID0gZi5sYW1iZGEoezIsIHBpPTJ9KSAtLT4gcGFzc2luZyBhbiBpbnRlcnNlY3Rpb24gdHlwZSBhcyBhIHtzdHJpbmc6YW55fQpwcmludChkZWcycmFkKDE4MCkpCnByaW50KGRlZzJyYWQoMCkpCnByaW50KGRlZzJyYWQoNjApKQoKLS10aGlzIGFsc28gd29ya3MKbG9jYWwgZGVnMnJhZDIgPSBmLmxhbWJkYSh7Im5pY2UiLHA9MX0p

managed to simplify it even more. Looks like any overload makes the typechecker overly lax. The type checker does still care about some of the types in the table though. So, it almost is like it has structural typing....

[hishamhm]

local record f
   g: function(integer)
   g: function({string: any})
end

f.g({true, hello="world"})

It seems to get confused with tables that mix array and map parts (which doesn't fully surprise me), but only in polymorphic functions in records (which is the weirder part)...

[hishamhm]

Ok, so here's what's happening:

• on non-polymorphic functions, we use bidirectional inference (that is, we use the knowledge that the table literal is inside a function argument, sending typing info "outside-in" rather than the regular "inside-out") to expect it to be a map, and then when the literal is checked, it is checked invariantly against the map type, and then we get the failure once we see non-map entries.
• on polymorphic functions, we can't narrow the arguments to a single expected type beforehand (since a valid type signature for the function can only be determined after all arguments have been processed), so when the literal is checked, is it checked generally, and it ends up being inferred as an arrayrecord (e.g. record {boolean} hello: string end in my shortest example above). When trying the possibilities in the polymorphic function type, what happens is that the arrayrecord is checked bivariantly against the map type, and then it passes.

We do bivariant (weaker) checks in function arguments in general (poly or non-poly) because we don't have a way to annotate that function arguments are covariant or contravariant, and Lua coders, having naver had those limitations, regularly use them in both ways. TypeScript does the same.

However, for table literals in places where we know the expected type (such as a non-polymorphic function), we can do a stronger invariant check because it doesn't really make sense for a programmer to write down a literal table value of one type on a function that expects another — if you're writing elements to be immediately discarded on a table, that's most certainly a bug. A main reason why we do this kind of bidirectional typing with expected types is to allow type variables of generic functions to flow into the function arguments.

Here's a demonstration of how checking changes between table literals and table variables for various types:

local record AR
   {boolean}
   hello: string
end

local function wants_arrayrecord(x: AR)
end

local function wants_map(m: {string: string})
end

local function wants_array(a: {boolean})
end

local arrayrecord: AR = {true, true, hello = "world"}
local map: {string: string} = {hello = "world"}
local array: {boolean} = {true, true}

--------------------------------------------------------------------------------
wants_arrayrecord(arrayrecord)                     -- accepts, trivial
wants_arrayrecord({true, true, hello = "world"})   -- accepts, trivial

--wants_arrayrecord(map)                           -- rejects, can't guarantee all map keys match record
wants_arrayrecord({hello = "world"})               -- accepts! bidirectional typing allows us to check map keys

wants_arrayrecord(array)                           -- accepts, bivariant check: array <: arrayrecord
wants_arrayrecord({true, true})                    -- accepts, bivariant check: array <: arrayrecord
--------------------------------------------------------------------------------
wants_map(arrayrecord)                             -- accepts! can check that all record values match map values
--wants_map({true, true, hello = "world"})         -- rejects, invariant check: arrayrecord =/= map

wants_map(map)                                     -- accepts, trivial
wants_map({hello = "world"})                       -- accepts, trivial

--wants_map(array)                                 -- rejects even in bivariant check: array </: map, map </: array
--wants_map({true, true})                          -- rejects, invariant check: array =/= map
--------------------------------------------------------------------------------
wants_array(arrayrecord)                           -- accepts! bivariant check: arrayrecord :> array
--wants_array({true, true, hello = "world"})       -- rejects, invariant check: arrayrecord =/= array

--wants_array(map)                                 -- rejects even in bivariant check: array </: map, map </: array
--wants_array({hello = "world"})                   -- rejects, invariant check: map =/= array

wants_array(array)                                 -- accepts, trivial
wants_array({true, true})                          -- accepts, trivial

So what now?

I don't think I'm going to make any immediate changes to this behavior for now, even if the inconsistent lax behaviour you described for poly functions is indeed unsettling. (One possibility to address this would be to "backtrack" the bidirectional inference of table literals when checking possibilities for polymorphic functions; I'm afraid it would be rather hacky with the current implementation though.) But it is really good to know that we have this issue, and I'll keep it in mind as I continue thinking about generalizing intersection types.