Add const parameter for assoc const of parametric impl.

engine/lib/import_thir.ml

@@ -724,18 +724,32 @@ end) : EXPR = struct
                        typ = TInt { size = S8; signedness = Unsigned };
                      })
                    l))
-      | NamedConst { def_id = id; impl; args; _ } -> (
+      | NamedConst { def_id = id; impl; args; _ } ->
           let f = GlobalVar (def_id ~value:true id) in
-          match impl with
-          | Some impl ->
-              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)
+          let args = List.map ~f:(c_generic_value e.span) args in
+          let const_args =
+            List.filter_map args ~f:(function GConst e -> Some e | _ -> None)
+          in
+          if List.is_empty const_args && Option.is_none impl then f
+          else
+            let f =
+              {
+                e = f;
+                span;
+                typ = TArrow (List.map const_args ~f:(fun e -> e.typ), typ);
+              }
+            in
+            let trait =
+              Option.map impl ~f:(c_impl_expr e.span &&& Fn.const args)
+            in
+            App
+              {
+                f;
+                trait;
+                args = const_args;
+                generic_args = [];
+                bounds_impls = [];
+              }
       | Closure { body; params; upvars; _ } ->
           let params =
             List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params

test-harness/src/snapshots/toolchain__generics into-fstar.snap

@@ -27,6 +27,18 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
+"Generics.Assoc_const_param.fst" = '''
+module Generics.Assoc_const_param
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Test (v_N: usize) = | Test : t_Test v_N
+
+let impl__A (v_N: usize) : t_Test v_N = Test <: t_Test v_N
+
+let test (_: Prims.unit) : t_Test (mk_usize 1) = impl__A (mk_usize 1)
+'''
 "Generics.Defaults_generics.fst" = '''
 module Generics.Defaults_generics
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/generics/src/lib.rs

@@ -72,3 +72,16 @@ mod impl_generics {
         }
     }
 }
+
+/// See https://github.com/cryspen/hax/issues/1289
+mod assoc_const_param {
+    struct Test<const N: usize>();
+
+    impl<const N: usize> Test<N> {
+        const A: Self = Self();
+    }
+
+    fn test() -> Test<1> {
+        Test::<1>::A
+    }
+}