0.15.1: type parameter resolution regression

[lewis6991]

  local record vim
      tbl_contains: function(table, any): boolean
  end

  local record opt
    record Opt<T>
      get: function<T>(Opt<T>): T
    end

    foldopen: Opt<{string}>
  end

  local result: boolean = vim.tbl_contains(opt.foldopen:get(), 'search')  -- Error line

Results in error:

teal/gitsigns/actions.tl:509:58: argument 0: type parameter <T>: got {string}, expected {<any type> : <any type>}

Change to the following works:

  local result: boolean = vim.tbl_contains(opt.foldopen:get() as {string}, 'search')

[hishamhm]

tbl_contains: function(table, any): boolean

I think the ideal definition for this would be tbl_contains: function<K, V>({K: V}, V): boolean

...but as of 0.15.1 that doesn't typecheck either because a {string} array doesn't resolve to a {K:V} map; allowing this to work is an easy chang.

The table type is somewhat unfortunate, because it is an alias to {any:any} and that has variance problems for the key type; however, it is still a useful type for people migrating progressively from Lua to Teal, so I don't want to just get rid of it. Ideally, its type should be more like {K:V} but having it auto-register implicit type variables would make it even more magical. I already have some hacks here and there especially for table to allow for unsound behavior; maybe I should add another one.

[lewis6991]

Surely any {T} should subtype satisfy {any:any} since the key type in a list is just integer? At the very least I'd expect it to subtype satisfy table.

[lewis6991]

Also

Change to the following works:

 local result: boolean = vim.tbl_contains(opt.foldopen:get() as {string}, 'search')

This on its own should confirm this as a bug. The type is {string} so the as shouldn't change the behaviour.

[lenscas]

Surely any {T} should subtype satisfy {any:any} since the key type in a list is just integer? At the very least I'd expect it to subtype satisfy table.

if a {T} can be transformed into a {any:any} then you are suddenly allowed to put other things into the {T} than it actually allows. Or in other words, this code would be allowed:

local function breakATable(tbl:{any:any})
    tbl["lol"] = "oof"
    tbl[0]= "nice"
end

local tbl = {1,2,3}
breakATable(tbl)
for k,v in pairs(tbl) do --ipairs would also break
    print(k+1,v +1) --runtime error as a string is not a number
end

[hishamhm]

Surely any {T} should subtype satisfy {any:any} since the key type in a list is just integer?

if a {T} can be transformed into a {any:any} then you are suddenly allowed to put other things into the {T} than it actually allows.

Yep, that is the crux of the matter. @lewis6991's intuition makes sense for reading from a table, but @lenscas points the issue with writing to that table. A sound typesystem would never allow that breakATable function, but "typed dialects" like Teal and TS often end up allowing some unsound bivariant behavior to make it easier for people to transition without making the typesystem overly complicated/cumbersome for the end-user, so sometimes things like that do slip through.

I'm being more pragmatic than purist about this, so Teal has some special-cased hacks to allow for such bivariance in some places. But as the type system becomes richer and the type checker smarter, I'm hoping I can narrow down these situations where we make the typesystem intentionally lax so that they don't leak too much into places where we want the type system to be more well-behaved.

I've been making some experiments to try to further improve this, and the feedback is definitely welcome; these recent threads already gave me more food for thought!

[hishamhm]

This on its own should confirm this as a bug. The type is {string} so the as shouldn't change the behaviour.

Great point! The "cast should not change the behavior" bit is definitely a bug.

I just ran that testcase here from a development branch where I've made some huge refactors and the cast did not change the behavior, but I think this was a side effect from other changes, not something I could easily backport.

[lenscas]

Yep, that is the crux of the matter. @lewis6991's intuition makes sense for reading from a table, but @lenscas points the issue with writing to that table. A sound typesystem would never allow that breakATable function, but "typed dialects" like Teal and TS often end up allowing some unsound bivariant behavior to make it easier for people to transition without making the typesystem overly complicated/cumbersome for the end-user, so sometimes things like that do slip through.

Being able to specify that a type should be read only would fix it (a {T} can be used as a readonly<{any:any}>) as then everything that could break it isn't allowed. But that sounds like a typesystem feature that is very easy to get bugs in so probably better to wait with those kind of changes until the typesysem has settled a bit more.

[hishamhm]

@lenscas yes, that is in fact one of the experiments I've been making and yes, it is delicate to get right.