seq() should allow constrained integer types

[ajewellamz]

Summary

Dafny will accept
seq(|s|, (n : nat) requires 0 <= n < |s| => s[n] as uint8)
or
seq(|s|, (n : int) requires 0 <= n < |s| => s[n] as uint8)
but it will not accept
seq(|s|, (n : int32) requires 0 <= n < |s| => s[n] as uint8)
which is a problem, because I'd like to avoid the use of BigInteger, for performance reasons.

Background and Motivation

I need faster generated code, and avoiding BigInteger is one of the simplest ways to do that.

Proposed Feature

Allow constrained integer types in seq() expressions.

Alternatives

No response