Feature Request: Using compile-time constants as array lengths

[enjhnsn2]

Hello, it appears that using compile-time constants as array lengths. For example, the following code

#[flux::constant]
const BUFLEN: usize = 100;
type FixedSizeBuffer = [i32; BUFLEN];

fails with the error:

error[FLUX]: refinement of unsupported type alias
  --> src/main.rs:36:6
   |
36 |type FixedSizeBuffer = [i32; BUFLEN];
   |      ^^^^ this type alias contains unsupported features
   |
   = note: only interger literals are supported for array lengths

You can workaround this by just writing it out as

type FixedSizeBuffer = [i32; 100];

directly, but thats a little ugly.

Presumably, adding support for compile-time constant lengths is pretty straight forward, would you mind either (1) implementing it, or (2) pointing me to the appropriate part of the code so that I can implement it?

Thanks

[nilehmann]

The easiest way to support this is by opportunistically doing const eval during lifting here https://github.com/flux-rs/flux/blob/main/crates/flux-middle/src/fhir/lift.rs#L540

Handling more complicated cases like const generics is a bit more involved.