ICE for type alias with generic of base kind
Opened this issue · 0 comments
nilehmann commented
#[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>) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^