hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
193 stars 20 forks source link

`try_from` passed as a closure does not give the correct module name #842

Open maximebuyse opened 2 months ago

maximebuyse commented 2 months ago
#[allow(dead_code)]

pub enum Res {
    Ok(i32),
    None
}

impl TryFrom<i32> for Res {
    type Error = i32;
    fn try_from(v: i32) -> Result<Res, i32> {
        if v > 0 {
            Ok(Res::Ok(v))
        } else {
            Ok(Res::None)
        }
    }
}

fn test() {
    let _ = vec!(1).into_iter().map(Res::try_from);
}

Open this code snippet in the playground

Here Res::try_from is translated as Core.Convert.TryFrom.try_from instead of f_try_from from the type class implementation.

github-actions[bot] commented 3 weeks ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

W95Psp commented 3 weeks ago

Here is a slightly minimized version:

#[allow(dead_code)]

fn f(f: impl FnOnce(()) -> ()) {}

/// The following `into` is (wrongly) extracted as `Core.Convert.Into.into`
fn g() {
    f(Into::into)
}
/// While here it is extracted as `Core.Convert.f_into`
fn h() {
    Into::into(())
}

Open this code snippet in the playground

It's a problem of Kind in impl exprs. From THIR, we get a GlobalName for Into::into in g: we have no impl_expr. I wonder if we should not move impl_expr and friends from the Call node to the GlobalName node, in the frontend.