Add FnDef

[N1ark]

Add FnDef as a type -- this represents a constant function, and is a ZST, unlike Arrow which is a function pointer.

Companion PR to cryspen/hax#1487.

[Nadrieril]

Why did you remove this?

[N1ark]

it would monomorphize for<'a> foo<'a>, which is not the actual use of the fn :)

[Nadrieril]

If you don't want to deal with the binder, it's fine to erase regions during mono (there's RegionBinder::erase for you)

[Nadrieril]

it would monomorphize for<'a> foo<'a>, which is not the actual use of the fn :)

why not?

fn foo<'a, T>(_: &'a T) {}
fn takes_closure(_: impl for<'a> Fn(&'a u32)) {}
fn main() {
    takes_closure(foo);
}

[N1ark]

it was monomorphising the fn twice, e.g. for this code:

fn foo<'a, T>(x: &'a T) {}

fn bar() {
    let fooint1: fn(&u8) = foo;
    fooint1(&11);
}

it was generating this:

fn test_crate::foo::<'_0_0, u8>(@1: &missing('_0_0) (u8))
{
    let @0: (); // return
    let x@1: &'_ (u8); // arg #1

    @0 := ()
    @0 := ()
    return
}

fn test_crate::foo::<'_, u8>(@1: &'_ (u8))
{
    let @0: (); // return
    let x@1: &'_ (u8); // arg #1

    @0 := ()
    @0 := ()
    return
}

[Nadrieril]

That does look good, I guess I'm surprised why this works at all. Where does it find a reference to the function item if not through FnDef? Also, if you erase() the binder I think that would get rid of the duplication you mentioned.

[N1ark]

through the parameter ! it has a ConstantExpr, which itself has a FnPtr with the right parameters!

[N1ark]

basically a fn is used either via a ConstantExpr, which contains a FnPtr, or a call, that also has one, so it works out nicely

[Nadrieril]

Ok interesting. We still need to monomorphize all types though. I'm ok with RegionBinder::new_empty(fix_args(binder.erase()) for now.

[N1ark]

done, let me know if that's what you had in mind, and if there's anything else to do for this PR :p