ICE when assoc refinement is not defined in implementation
Closed this issue · 5 comments
nilehmann commented
#[flux::assoc(fn eval(x: int) -> int)]
trait MyTrait { }
impl MyTrait for i32 { }
#[flux::sig(fn(x: i32) -> i32[<T as MyTrait>::eval(x)])]
fn test01<T: MyTrait>(x: i32) -> i32 {
todo!()
}
fn test02() {
test01::<i32>(0);
}
error: internal compiler error: crates/flux-fhir-analysis/src/lib.rs:197:28: assoc reft `eval` not found in impl `DefId(0:3 ~ playground[223a]::{impl#0})`
nilehmann commented
I also discovered the following crash while trying to reproduce the issue in the op
#[flux::assoc(fn eval(x: int) -> int)]
trait MyTrait { }
impl MyTrait for i32 { }
#[flux::sig(fn(x: i32) -> i32[<T as MyTrait>::eval(x)])]
fn test00<T>(x: i32) -> i32 {
todo!()
}
error: internal compiler error: crates/flux-middle/src/rty/projections.rs:187:23: error selecting Obligation(predicate=TraitPredicate(<T as MyTrait>, polarity:Positive), depth=0): Unimplemented
ranjitjhala commented
So here we should make flux
yell since the impl
doesn't in fact define the associated refinement, yes?
ranjitjhala commented
Not sure why the second thing is failing -- the Unimplemented
seems ominous. At any rate, maybe we should also just return an Err
here instead of bug!
?
nilehmann commented
In the second, <T as MyTrait>::eval(x)
is not well-formed so we should reject the definition. It is an orthogonal issue though. I just dumped it here.
ranjitjhala commented
Aha -- I missed that we don't have the T: Trait
in the rust signature in the second one...