Type checker assumes a consuming type for something declared non-consuming

[athas]

def main (xs: *[]i32) =
  loop xs : []i32 for i < 10 do
    xs with [i] = i+1

Here we mark the loop parameter xs as non-consuming. However, the type checker infers that it must be consuming. Unfortunately, the internaliser trusts the non-consuming type annotation, leading to invalid IR and a compiler crash.

Inferring the uniquess/consumption of a loop parameter is pretty standard, but should we also do it when there is an explicit annotation, like here?