Playground reproducer : Open this code snippet in the playground

Details

In rust, both traits and trait items can have generic parameters, as in :

trait T1<A, B> {
    fn f1<C, D>(&self) -> (); // A and B do not appear
    fn f2<C, D>(&self, x: &A) -> (); // A appears
    fn f3<C, D>(&self, x: &A, y: &B) -> (); // Both appear
}

The lean backend translates trait parameters as class parameters and trait-item parameters as class-field parameters :

class T1 (Self : Type) (A : Type) (B : Type) where
  f1 (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0)
  f2 (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0)
  f3 (C : Type) (D : Type) :
    (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0)

However, in Lean, when accessing the fields of the class (as in T1.f1), the typechecker turns some of the trait-level params into implicit ones, based on whether or not they appear in the type signature of the function :

#check T1.f1 
-- T1.f1 {Self : Type} (A B : Type) [self : T1 Self A B] (C D : Type) : Self → RustM Rust_primitives.Hax.Tuple0
-- both A and B are explicit parameters

#check T1.f2 
-- T1.f2 {Self A : Type} (B : Type) [self : T1 Self A B] (C D : Type) : Self → A → RustM Rust_primitives.Hax.Tuple0
-- A is implicit, B is explicit

#check T1.f3 
-- T1.f3 {Self A B : Type} [self : T1 Self A B] (C D : Type) : Self → A → B → RustM Rust_primitives.Hax.Tuple0
-- both A and B are implicit

This results in an incorrect translation at the call site, where all trait-level params are expected to be implicit.

Workaround

trait T1<A, B> {
    fn f1<C, D>(&self, _: &Option<A>, _: &Option<B>) -> (); 
    fn f2<C, D>(&self, x: &A, _: &Option<B>) -> (); 
    fn f3<C, D>(&self, x: &A, y: &B) -> (); 
}

fn test<Ap, Bp, Cp, Dp, U: T1<Ap, Bp>>(x: U, a: &Ap, b: &Bp) -> () {
    let dummy_a = &None;
    let dummy_b = &None;
    x.f1::<Cp, Dp>(dummy_a, dummy_b);
    x.f2::<Cp, Dp>(a, dummy_b);
    x.f3::<Cp, Dp>(a, b);
}

trait T1 {
    fn f1<A, B, C, D>(&self) -> (); 
    fn f2<A, B, C, D>(&self, x: &A) -> ();
    fn f3<A, B, C, D>(&self, x: &A, y: &B) -> (); 
}

fn test<Ap, Bp, Cp, Dp, U: T1>(x: U, a: &Ap, b: &Bp) -> () {
    x.f1::<Ap, Bp, Cp, Dp>();
    x.f2::<Ap, Bp, Cp, Dp>(a);
    x.f3::<Ap, Bp, Cp, Dp>(a, b);
}

Fix

Unless the lean backend starts using impl expressions (see #1716), we need a way to provide the trait level args to the call site. Guessing which args are implicit and which are explicit seems fragile. Making all arguments explicit (using @) seems overkill, as it also makes trait bounds explicit params. Instead, the frontend could be instrumented to give both the list of trait-level generic values and the list of the corresponding parameter names at the trait definition, allowing to produce the following Lean (at the call site, no change to the class definition) :

  let _ ← (Test1.T1.f1 (A := Ap) (B := Bp) Cp Dp x);
  let _ ← (Test1.T1.f2 (A := Ap) (B := Bp) Cp Dp x a);
  let _ ← (Test1.T1.f3 (A := Ap) (B := Bp) Cp Dp x a b);

Right now, the AST at the App nodes do not contain the list A, B.