Cannot assign an expression of type Field to a value of type comptime Field

[ax0]

Aim

Run nargo check on the following contrived example:

fn f(i: Field, j: comptime Field)
{
    let mut x = 0;

    let _pred = (x == j);

    x = i;

}

Expected behavior

Constraint system should be successfully built.

Bug

We get the following error pointing to the line x = i;:
error: Cannot assign an expression of type Field to a value of type comptime Field

To reproduce

1. Place the above function in a Noir project.
2. Run nargo check.

Installation method

Compiled from source

Nargo version

nargo 0.4.0 (git version hash: 528a2a4, is dirty: false)

@noir-lang/noir_wasm version

No response

@noir-lang/barretenberg version

No response

@noir-lang/aztec_backend version

No response

Additional context

The error goes away if a type annotation is provided for x:

let mut x: Field = 0;

Doing this leads to unexpected values being assigned to x in more elaborate examples, but I do not have a minimal example illustrating this at present. Also note that the error goes away if the line involving the comparison (let _pred = (x == j);) is commented out.

Submission Checklist

• Once I hit submit, I will assign this issue to the Project Board with the appropriate tags.

[jfecher]

Looks like a limitation of the current type checker.

The type of x is initially inferred and we do not know yet if it needs to be comptime or not. When we see x == j because both sides of == must be the same type, we erroneously infer that x must also be a comptime Field rather than a normal field. This explains the error on the final line when the compiler sees a Field being assigned to what it thinks must be a comptime Field.

[kevaundray]

What is the proposed fix?

[kevaundray]

Once we remove comptime, we can close this issue