Go back to previous behaviour for val interfaces in the fsti for impl…

…s with assoc type.

engine/backends/fstar/fstar_backend.ml

@@ -1494,14 +1494,24 @@ struct
         in
         let body = F.term @@ F.AST.Record (None, fields) in
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
+        let has_type =
+          List.exists items ~f:(fun { ii_v; _ } ->
+              match ii_v with IIType _ -> true | _ -> false)
+        in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
-        if is_erased then
-          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)
-          @ erased_impl name val_type [ tcinst ] generics
-        else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl
+        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
+        let intf = F.decls ~fsti:true ~attrs:[ tcinst ] v in
+        let impl =
+          if is_erased then erased_impl name val_type [ tcinst ] generics
+          else
+            F.decls
+              ~fsti:(ctx.interface_mode && has_type)
+              ~attrs:[ tcinst ] let_impl
+        in
+        let intf = if has_type && not is_erased then [] else intf in
+        if ctx.interface_mode then intf @ impl else impl
     | Quote { quote; _ } ->
         let fstar_opts =
           Attrs.find_unique_attr e.attrs ~f:(function

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

@@ -57,19 +57,13 @@ let impl_T2_for_u8: t_T2 u8 =
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl:Core.Convert.t_From t_Bar Prims.unit
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl': Core.Convert.t_From t_Bar Prims.unit
 
 let impl = impl'
 
 /// If you need to drop the body of a method, please hoist it:
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1:Core.Convert.t_From t_Bar u8
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_1': Core.Convert.t_From t_Bar u8
@@ -81,18 +75,12 @@ val from__from': u8 -> t_Bar
 
 let from__from = from__from'
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit
 
 let impl_2 (#v_T: Type0) = impl_2' #v_T
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit