[Lean] Implemented items that use other associated items produce invalid Lean

[JuanCoRo]

Consider the following Rust where implemented items of Foo make use of other implemented items:

pub trait Foo { 
    const F: u32;
    fn a() -> u32;
    fn b();
    fn c();
}

pub struct Bar;

impl Foo for Bar {
    const F: u32 = 1;
    fn a() -> u32 {
        Self::F
    }
    fn b() {}
    fn c() {
        Self::b()
    }
}

Which, after fixing F for #1903, produces the following Lean instance:

instance Playground.Impl : Playground.Foo Playground.Bar where
  F := 1
  a := fun (_ : Rust_primitives.Hax.Tuple0) => do
    (Playground.Foo.F Playground.Bar)
  b := fun (_ : Rust_primitives.Hax.Tuple0) => do
    (pure Rust_primitives.Hax.Tuple0.mk)
  c := fun (_ : Rust_primitives.Hax.Tuple0) => do
    (Playground.Foo.b Playground.Bar Rust_primitives.Hax.Tuple0.mk)

Here, Lean complains about using Playground.Foo.F Playground.Bar and Playground.Foo.b Playground.Bar during the instance declaration. What should be the correct generation for this instance?

[maximebuyse]

Yes, this is a problem we also have with the F* backend. The solution here is probably the same as described in #1773. We would need an engine phase to hoist the definitions outside the impls. For example, doing that manually on your example would give:

pub trait Foo { 
    const F: u32;
    fn a() -> u32;
    fn b();
    fn c();
}

pub struct Bar;

const F: u32 = 1;
fn a() -> u32 {
    F
}
fn b() {}
fn c() {
    b()
}

impl Foo for Bar {
    const F: u32 = F;
    fn a() -> u32 {
        a()
    }
    fn b() {
        b()
    }
    fn c() {
        c()
    }
}

Open this code snippet in the playground

[maximebuyse]

Another interesting related problem is when you have default methods using other items from the trait. Here, hoisting wouldn't work and I don't see a good way to solve it:

pub trait Foo { 
    fn b();
    fn c() {
        Self::b()
    }
}

Open this code snippet in the playground

[abentkamp]

Another interesting related problem is when you have default methods using other items from the trait.

I think this is not a big problem. It's possible to refer to other fields from within the default implementations, just not with the fully quantified name. See #1889

[maximebuyse]

Another interesting related problem is when you have default methods using other items from the trait.

I think this is not a big problem. It's possible to refer to other fields from within the default implementations, just not with the fully quantified name. See #1889

Oh I see, great! So you can do that in the type class definition but not when you define an instance then, that's surprising but at least we won't be stuck for the case of default methods.

I investigated a bit and it seems like it is possible to define the hoisted values as let bindings within the instance, which is nice as it removes the need for disambiguation to avoid name clashes (example).

[Edit:] This is actually not a great idea as mutual recursion is not supported for local definitions. We should just implement a phase that does the method hoisting systematically, then we will benefit from items sorting, and (when we have it) of mutual recursion blocks.