0.15.1: type inference regression

[lewis6991]

    local res: any = x as table
    if res is table then
      ...
    end

Gives warning:

teal/gitsigns.tl:160:12: res (of type {<any type> : <any type>} (inferred at teal/gitsigns.tl:158:58)) is always a {<any type> : <any type>}

[hishamhm]

The warning is correct though, right? The check there is redundant. In your real code, is there any extra code between the two lines which could make res not be a table?

[lewis6991]

I'm intentionally declaring the variable as any so this is what I'd expect the type checker to use and not the rval type. At least this is how every other statically typed language I've used behaves.

Obviously if the decl type is removed then the type is table and the warning would be correct.

[hishamhm]

The type checker is ultimately using the declared type, that's why you're getting a warning and not an error. But it is detecting a redundant check, that's the kind of things warnings are for.

This new behavior you're observing comes from improvements in flow-typing. For example, you'd see a similar warning in 0.14.1 for this:

    local res: any = x as table
    if res is table then
        if res is table then -- warning: res is always a table
          ...
        end
    end

Version 0.14.1 detected that the inner test is redundant; version 0.15.x detects that the outer test is well.

[lewis6991]

that's why you're getting a warning and not an error.

Dropping the type on the declaration should not cause an error here. Dead code or always true/false conditions should always be a warning. Adding the declared type then should remove that warning entirely. The declared type should act as a kind cut point in the typechecker.

This is generally how this works in languages in my experience (e.g. scala, ocaml, python with pyright). Do your experiences differ?

[hishamhm]

Adding the declared type then should remove that warning entirely. The declared type should act as a kind cut point in the typechecker.

Yes, but the sequence of events is that: a) you declare res to be any; b) you set res to be table; c) you check if res is a table. Even if "a" was a cut point, "b" happened afterwards.

Note that in principle this should produce the same effect (it currently doesn't due to the implementation, but if the flow-checker continues to get smarter, then it should)

    local res: any
    res = x as table
    if res is table then
      ...
    end

For a more appealing case describing the current semantics, note that this warning we're effectively identical to:

    local u: string | number = "hello"
    if u is string then
      ...
    end

...which leads me to think the warning of the redundant check is warranted even with the type declaration.

[lewis6991]

That's a fair way to reason about it, but I would argue that:

local res:any
res = x as table

-- !==

local res: any = x as table

Where the latter should be seen as an atomic operation, and not a compound of two smaller operations. But arguably both are valid design decisions, I've just never seen the way you've decided to do it in any other language, which means it has become a gotcha I need to be weary of.

From a type checking POV for subsequent statements I actually expect the following to be equivalent:

local res: any = x as table
local res = (x as table) as any

With the only difference being that the rval of the former is actually checked against the declared type. However because of the change in 0.15 I am now forced to rewrite my code using the latter and thus making the typing weaker, rendering declared types less useful.

local u: string | number = "hello"
   if u is string then
      ...
   end

I strongly feel there should be no warning here. If the user wants the flow checking then they should drop the declared type.

What is useful here is that u is checked as a string within the if block. That we should do more of.

[lenscas]

only skimmed the issue a bit so might have missed things, however it sounds like teal copied a feature from typescript (forgot the name, sorry about that) in which you can say to typescript "this object is of type X" which it will check to make sure that said type actually fits BUT it also remembers the exact declaration used as if normal checks have been used to nail the type down.

This to me sounds like a pretty useful feature for as long this information doesn't leak so to speak. So

local function A(): string | number
    local b : string | number = 1
   print(b+1) -- should be valid, as at this point, `b` can _only_ be used as a number
   return b  --by the same logic, we are guaranteed to return a number
end

print(A()+1) --but please, do _not_ let that knowledge leak to outside the function call.That is _bad_

[hishamhm]

If the user wants the flow checking then they should drop the declared type.

If they drop the declared type, then it will infer the initializer value's type, and the else block won't work. Teal will not do unification of the branches to infer a union; that would produce very confusing errors, inferring complex types when people make simple mistakes.

I'm still failing to understand why you want an is check on a type you are already sure of. I mean, in the original example you could just do away with the cast:

    local res: any = x
    if res is table then
      ...
    end

Is there anything else going on that the simplified example is not covering?

[hishamhm]

(@lenscas that wasn't copied from TypeScript specifically, but it's a pretty common flow typing pattern)

[lewis6991]

Ok, so Teal is more like typescript. Doesn't align with my personal intuition and experiences, but that's my problem.