Reflect const-generics in refinements

[ranjitjhala]

(via: https://github.com/flux-rs/flux/pull/481#discussion_r1297422785)

So this is the hard part. I've been thinking for a while about generic consts appearing in refinements. I think supporting that would be very cool.

This is related to global consts (e.g., const N: i32 = 3) which we do support inside refinements with ExprKind:: ConstDefId. I was thinking that we can maybe represent generic consts with the same variant. Then, we only need to be careful when encoding into fixpoint to differentiate between global consts, for which we assume a value, and generic consts which we leave opaque (we could also have a different variant in ExprKind). This change should be relatively simple and it would allow us to remove the tracked_span_bug here.

The next step would be to support const generics in our surface syntax. For that, the tricky part is name resolution. It shouldn't be that complicated though, we just need to track those names when desugaring and decide what to do with shadowing.

All this can go into a different PR.

Originally posted by @nilehmann in https://github.com/flux-rs/flux/pull/481#discussion_r1297422785