Duplicate identifier due to quantifier

[Aurel300]

method test() {
    assert forall i: Int :: true
    var i: Int
}

This reports a duplicate identifier. It disappears if I e.g. put the two statements in separate control-flow paths. I understand that if the two lines were in the opposite order, the quantifier would be shadowing the local varaibe i, but in this order it doesn't. (Is this because we hoist variable declarations to the beginning of the block?)

[marcoeilers]

Right, this happens because the quantifier declares a variable whose name is in use in its parent scope. Our scopes basically mostly ignore where in them a variable is declared (and in the actual AST, that information is not present at all, a scope just knows which variables are declared inside it); if it's declared anywhere in that scope, its name is in use in that scope.

So I'd say this basically works as intended, even though it's not super intuitive.