Passing functions as values result in bad naming

[maximebuyse]

Passing a function as a value in a higher order context produces bad names in extracted codes.

fn f(higher_order: impl FnOnce(()) -> ()) {}
fn main() {
    // Next line (wrongly) extracts to `f Core.Convert.Into.into`
    f(Into::into);
    // Next line (correclty) extracts to `Core.Convert.f_into ...`
    Into::into(())
}

Open this code snippet in the playground

Explanation

This is a problem in the frontend. An identifier like into::Into alone (i.e. not being called) is exported by the frontend assuming that symbol doesn't point to something callable. Thus, in the engine, we miss crucial information to deal with that identifier: we don't know that it's a function, we don't know that it's an associated function, nor from what impl block it comes from.

We need to add this information in the frontend, see issue #991.

Other examples

try_from

#[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.

from

See issue:

• https://github.com/cryspen/hax/issues/1165.

[github-actions[bot]]

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]

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.

[github-actions[bot]]

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.

[maximebuyse]

This works on main