Can't reference Self type when using associated refinement

[enjhnsn2]

When I try to use an associated refinement in a function spec, Flux does not seem to like it when I pass in a Self.
For example, when I verify:

#[flux_rs::refined_by(powered:bool)]
pub struct MPU<const MIN_REGION_SIZE: usize> {
    #[field(bool[powered])]
    powered: bool,
}

#[flux_rs::assoc(fn enabled(self: Self) -> bool )]
pub trait MyTrait {
    #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{r: <Self as MyTrait>::enabled(r)})]
    fn enable_app_mpu(&mut self);
}

#[flux_rs::assoc(fn enabled(self: Self) -> bool {self.powered} )]
impl<const MIN_REGION_SIZE: usize> MyTrait for MPU<MIN_REGION_SIZE> {
    #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{r: <Self as MyTrait>::enabled(r)})]
    fn enable_app_mpu(&mut self) {
        self.powered = true;
    }
}

I get the error:

error[E0999]: mismatched sorts
   --> src/main.rs:904:90
    |
904 |     #[flux_rs::sig(fn(self: &strg Self) ensures self: Self{r: <Self as MyTrait>::enabled(r)})]
    |                                                                                          ^ expected `{impl#0}::sort`, found `MPU`

It seems like Flux is expecting an instance of MyTrait rather than an MPU and does not recognize that MPU implements MyTrait. I'm pretty sure I'm just missing some syntax, but I could use a pointer lol.

On a related note, are there any plans for documentation on associated refinements? They are extremely useful, but a little hard to use due to the weird syntax.

[ranjitjhala]

@enjhnsn2 -- this is pesky indeed. I wonder if you can just "inline" the associated predicate here, so in the signature replace Self as MyTrait>::enabled(r) with r.powered ?

#[flux_rs::sig(fn(self: &strg Self) ensures self: Self{r: r.powered })]

[nilehmann]

Oh yeah, that's a good workaround. It will work in this case because we do normalize the sort of Self. What we don't normalize is the sort of <Self as MyTrait>::enabled

[enjhnsn2]

This workaround works great.