Confusing error message about bit-vector types

[davidcok]

Dafny version

3.10.0+dev

Code to produce this issue

const z := 1 as bv4 | 1 as bv2 << 2

Command to run and resulting output

dafny resolve test.dfy

What happened?

The error message is 'Error: second argument to | must be of a bitvector type (instead got bv2)'
Of course, bv2 is a bit-vector type, so what is wrong??? (It is not just not the right bit-vector type.

What type of operating system are you experiencing the problem on?

Mac

[olivier-aws]

Note that the refresh resolver (#5653) fixes this issue as it provides the clearer message:

bug.dfy(1,20): Error: type of right argument to | (bv2) must agree with the result type (bv4)
  |
1 | const z := 1 as bv4 | 1 as bv2 << 2
  |