flux-rs / flux

Refinement Types for Rust
MIT License
581 stars 17 forks source link

ICE for type alias with generic of base kind #650

Open nilehmann opened 2 weeks ago

nilehmann commented 2 weeks ago
#[flux::refined_by(u: U)]
struct Ctxt<T, U> {
    #[flux::field(U[u])]
    u: U,
    t: T,
}

#[flux::refined_by(id: int)]
struct User {
    #[flux::field(i32[id])]
    id: i32,
}

#[flux::alias(type Ctxt<U as base>[u: U] = Ctxt<i32, U>[u])]
type CtxtI32<U> = Ctxt<i32, U>;

fn foo(cx: &mut CtxtI32<User>) {
    assert(cx.u.id == 0);
}

#[flux::sig(fn(bool[true]))]
fn assert(_: bool) {}
error: internal compiler error: crates/flux-refineck/src/fixpoint_encoding.rs:544:47: fixpoint crash: CrashInfo([Array [Array [Array [Number(-1), Null], String("crash: SMTLIB2 respSat = Error \"line 3 column 7908: Sort mismatch at argument #1 for function (declare-fun tuple1$36$0 ((Tuple1 k!0)) k!0) supplied sort is Int\"")]], String("Sorry, unexpected panic in liquid-fixpoint!\n")])
  --> attic/playground.rs:18:1
   |
18 | fn foo(cx: &mut CtxtI32<User>) {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^