Infer the type of a lambda parameter from a UDT copy-and-update expression

[bettinaheim]

Describe the bug

The type inference fails for the following code

let f = (n, i) -> [0, size = n] w/ i <- 1; // produces an error

The compiler generates an error on the i in the lambda body that states: "Expecting an expression of type Int or Range. Got an expression of type 'b". This error in particular persists even after adding the line

let f = (n, i) -> [0, size = n] w/ i <- 1; // produces an error
let arr = f(5, 0);

Also copy-and-update expressions for user defined types seems to not be working in the body of a lambda, and produce cryptic errors. For a type newtype Foo = (A : Int, B : Int); the compiler produces the following error:

Expected behavior

The compiler should be able to infer that i needs to be of Int with or without the second line.

[bamarsha]

The first issue with the array update is caused by the type inference applying the Indexed constraint too early - after the type of the array is known but before the type of the index i is known. I think this can be fixed unobtrusively by making the compiler smarter about when it applies the constraint.

The second issue with the UDT update is a symptom of a more fundamental issue. Without knowing the type of foo, the compiler does not know whether A is an expression referring to a variable A, or a symbol literal referring to a UDT item name A. The decision cannot easily be deferred until the type of foo is known, because that would make expression verification and type inference mutually recursive, which I would really recommend against doing.

The least obtrusive solution that I can think of for the UDT issue is to change copy-and-update to rely only on lexical information to determine whether it's an array update or a UDT update, rather than on type information. The rule could be:

For a copy-and-update expression x w/ y <- z:

1. If y is an identifier expression referring to an identifier i, then if i is a local variable in scope, treat i as the index or range for an array update expression. If i is not in scope, then treat i as a named item for a UDT update expression.
2. If y is not an identifier expression, treat y as the index or range for an array update expression.

But what I would strongly recommend from a language design standpoint, is to make UDT updates and array updates syntactically distinct. For example, when you update a record in F# using { x with f = v }, there's no question that f is a field name, not an expression. IMO, this is a much cleaner design, as well as being easier to compile and provide code completion for.

[bamarsha]

#1377 covers the first issue with the array index. I renamed this issue to focus on the UDT type inference problem. Since this situation was out of scope for the current implementation of type inference due to the language design, this is asking for additional functionality, so I think this is more like an enhancement than a bug.

[bamarsha]

Discussed during a language design meeting today, and we decided to go with the heuristic above:

For a copy-and-update expression x w/ y <- z:

1. If y is an identifier expression referring to an identifier i, then if i is a local variable in scope, treat i as the index or range for an array update expression. If i is not in scope, then treat i as a named item for a UDT update expression.
2. If y is not an identifier expression, treat y as the index or range for an array update expression.

In the future we might revisit the syntax, but for now we want to avoid breakage, and this heuristic is expected to have high compatibility with existing code.

[bamarsha]

There's a potential (future) issue if you imagine Q# supporting global constants. Imagine you have

// speculating on syntax for constants
const X : Int = 3;

function Foo(xs : Bool[]) : Bool[] {
    return xs w/ X <- 3; // error
}

Since X is not a local variable, the expression would compile as a UDT copy-and-update, which is not intended. You could extend the rule to check for local variables or global constants. But that allows for spooky action at a distance:

newtype Vec2 = (X : Int, Y : Int);

function Foo(v : Vec2) -> Vec2 {
    return v w/ X <- 3; // works
}

At a later time, someone (even a library!) adds a constant X to an opened namespace. Then the expression compiles as an array copy-and-update, which is not intended.

For the moment this is not a problem because Q# does not support global constants, only callables. Will Q# never support global constants? Or will the syntax be different? Or will we require let x = X; in the first example?