Assertions don't change type of vars

[Timmmm]

This works:

function foo() -> unit = {
    var a : range(0, 1) = 0;
    let b = a;
    assert(b == 0);
    a = b + 1;
}

But this doesn't:

function foo() -> unit = {
    var a : range(0, 1) = 0;
    assert(a == 0);
    a = a + 1;
}

I assume this is because b gets the inferred type range(0, 1) and then the assert essentially creates a new variable with the inferred type int(0)... but you can't make a new variable for var since it's mutable? So the assert doesn't change its type?

Not a big deal tbh (var is quite uncommon); I'd probably only fix it if it's easy. Here's the motivating example:

val count_ones : forall 'n, 'n >= 0. (bits('n)) -> range(0, 'n)

function count_ones(x) = {
    var count : range(0, 'n) = 0;
    foreach (i from 0 to ('n - 1)) {
        if x[i] == bitone then {
            assert(count < 'n);
            count = count + 1;
        }
    };
    count
}

I think you could probably do that recursively with no assertions tbf.

[Alasdair]

Yes, flow typing doesn't affect the type of mutable variables, as you could have:

var a : range(0, 1) = 0;
assert(a == 0);
/* now we could have a : int(0) */
a = 1;
/* now the assertion wouldn't hold, so x would have to go back to it's original type */

to make it work we'd have to modify the type of a up until the assignment, but it's a bit tricky because in general the type checker does't check in evaluation order, and you could do some really ugly things like assign in a weird place like:

assert(a == 0);
f(g(arg1, arg2, a = 1));

It might be worth thinking about whether we want to do something smarter, because I have also noticed it makes loop variables quite awkward.