flux-rs / flux

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

ICE when assoc refinement is not defined in implementation #649

Open nilehmann opened 2 weeks ago

nilehmann commented 2 weeks ago
#[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 2 weeks ago

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 1 day ago

So here we should make flux yell since the impl doesn't in fact define the associated refinement, yes?