search

flux-rs / flux

Refinement Types for Rust
MIT License
648 stars 21 forks source link

Check `impl` against `trait` sigs #663

Closed ranjitjhala closed 3 months ago

ranjitjhala commented 3 months ago

Flux should reject the below, but currently doesn't, AFAICT

trait Shape {
    #[flux::sig(fn(self: _) -> i32{v: 0 <= v})]
    fn vertices(&self) -> i32;
}

// ------------------------------------------------------

struct Square {}

impl Shape for Square {
    fn vertices(&self) -> i32 {
        0 - 4   //~ ERROR: refinement type
    }
}

@nilehmann I thought we'd (?) implemented this a while ago, but clearly no...?

nilehmann commented 3 months ago

This is a duplicate of https://github.com/flux-rs/flux/issues/592, no?

ranjitjhala commented 3 months ago

ah so it is! thanks!