Interface only val impl with parameters.

engine/backends/fstar/fstar_backend.ml

@@ -1478,8 +1478,8 @@ struct
         let impl_val = ctx.interface_mode && not has_type in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
         if impl_val then
-          let generics_types = List.map ~f:FStarBinder.to_typ generics in
-          let val_type = F.mk_e_arrow generics_types typ in
+          let generics_binders = List.map ~f:FStarBinder.to_binder generics in
+          let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
           let v = F.AST.Val (name, val_type) in
           (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
           @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -20,8 +20,35 @@ info:
     include_flag: "+:** -interface_only::Foo"
     backend_options: ~
 ---
-exit = 0
-stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+exit = 101
+stderr = """
+Compiling interface-only v0.1.0 (WORKSPACE_ROOT/cli/interface-only)
+warning: type `param` should have an upper camel case name
+  --> cli/interface-only/src/lib.rs:55:12
+   |
+55 | pub struct param<const SIZE: usize> {
+   |            ^^^^^ help: convert the identifier to upper camel case: `Param`
+   |
+   = note: `#[warn(non_camel_case_types)]` on by default
+
+error[E0117]: only traits defined in the current crate can be implemented for types defined outside of the crate
+  --> cli/interface-only/src/lib.rs:49:1
+   |
+49 | impl <T> From<()> for Vec<T> {
+   | ^^^^^^^^^--------^^^^^------
+   |          |            |
+   |          |            `std::vec::Vec` is not defined in the current crate
+   |          this is not defined in the current crate because this is a foreign trait
+   |
+   = note: impl doesn't have any local type before any uncovered type parameters
+   = note: for more information see https://doc.rust-lang.org/reference/items/implementations.html#orphan-rules
+   = note: define and implement a trait or new type instead
+
+For more information about this error, try `rustc --explain E0117`.
+
+warning: `interface-only` (lib) generated 2 warnings (1 duplicate)
+error: could not compile `interface-only` (lib) due to 1 previous error; 2 warnings emitted
+\u001B[1m\u001B[33mwarning\u001B[0m: \u001B[1mhax: running `cargo build` was not successful, continuing anyway.\u001B[0m"""
 
 [stdout]
 diagnostics = []
@@ -35,6 +62,8 @@ open FStar.Mul
 
 type t_Bar = | Bar : t_Bar
 
+type t_param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
@@ -47,6 +76,12 @@ val impl_1:Core.Convert.t_From t_Bar u8
 
 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_2 (#v_T: Type0) : Core.Convert.t_From (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global) Prims.unit
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_param v_SIZE) Prims.unit
+
 /// This item contains unsafe blocks and raw references, two features
 /// not supported by hax. Thanks to the `-i` flag and the `+:`
 /// modifier, `f` is still extractable as an interface.

tests/cli/interface-only/src/lib.rs

@@ -45,3 +45,19 @@ impl From<u8> for Bar {
         from(x)
     }
 }
+
+impl<T> From<()> for Vec<T> {
+    fn from((): ()) -> Self {
+        Vec::new()
+    }
+}
+
+pub struct param<const SIZE: usize> {
+    pub(crate) value: [u8; SIZE],
+}
+
+impl<const SIZE: usize> From<()> for param<SIZE> {
+    fn from((): ()) -> Self {
+        param { value: [0; SIZE] }
+    }
+}