Engine: F*: missing implicit type arguments for associated constants

[W95Psp]

trait Trait {
    const C: u8;
    fn function();
}

fn f<T: Trait>(x: T) -> u8 {
    T::function();
    T::C
}

Open this code snippet in the playground

The F* extraction is:

let f (#v_T: Type0) (#i1: t_Trait v_T) (x: v_T): u8 =
  f_function #v_T #FStar.Tactics.Typeclasses.solve ();
  f_C                      #FStar.Tactics.Typeclasses.solve

Here, the call to f_C is wrong: we are missing the v_T implicit argument.

[W95Psp]

I worked on that locally.