Repository: cryspen/hax (language: rust)

Issue:
Engine: F*: missing implicit type arguments for associated constants
```rust
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](https://hax-playground.cryspen.com/#fstar/e4c6c2be1c/gist=68dde1d5ba21426904f3cb5d415a8682)

The F* extraction is:
```fstar
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.


Discussion / hints:

Fix patch:
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 356b8eb07..2b265117a 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -730,14 +730,18 @@ end) : EXPR = struct
                        typ = TInt { size = S8; signedness = Unsigned };
                      })
                    l))
-      | NamedConst { def_id = id; impl; _ } -> (
+      | NamedConst { def_id = id; impl; args; _ } -> (
           let kind : Concrete_ident.Kind.t =
             match impl with Some _ -> AssociatedItem Value | _ -> Value
           in
           let f = GlobalVar (def_id kind id) in
           match impl with
           | Some impl ->
-              let trait = Some (c_impl_expr e.span impl, []) in
+              let trait =
+                Some
+                  ( c_impl_expr e.span impl,
+                    List.map ~f:(c_generic_value e.span) args )
+              in
               let f = { e = f; span; typ = TArrow ([], typ) } in
               App { f; trait; args = []; generic_args = []; bounds_impls = [] }
           | _ -> f)


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index f25ae1575..01f4b474e 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -158,7 +158,7 @@ let constants
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
       (_: Prims.unit)
     : usize =
-  (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
+  (f_ASSOCIATED_CONSTANT #v_T #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
 
 let construct_structs (a b: usize) : Prims.unit =
   let _:t_StructA = { f_a = a } <: t_StructA in