Add type arguments for associated constants.

cryspen · Jan 14, 2025 · c46cd13 · c46cd13
1 parent fcc06df
commit c46cd13
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git 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)

diff --git 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