fix(engine/fstar): generics on functions are now always implicit

engine/backends/fstar/fstar_backend.ml

@@ -344,16 +344,7 @@ struct
 
   and c_trait_goal span trait_goal =
     let trait = F.term @@ F.AST.Name (pconcrete_ident trait_goal.trait) in
-    List.map
-      ~f:(fun g ->
-        let term = pgeneric_value span g in
-        ( term,
-          match g with
-          | GType _ -> F.AST.Hash
-          | GConst _ -> F.AST.Nothing
-          | GLifetime _ -> . ))
-      trait_goal.args
-    |> F.mk_app trait
+    List.map ~f:(pgeneric_value span) trait_goal.args |> F.mk_e_app trait
 
   and pgeneric_value span (g : generic_value) =
     match g with
@@ -416,14 +407,16 @@ struct
       (* in *)
       F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange))
 
-  and fun_application ~span f args generic_args =
+  and make_application ~span ~generic_qualifier f args generic_args =
+    let is_arrow =
+      (* TODO: why? add documentation *)
+      [%matches? GType (TArrow _)]
+    in
     let generic_args =
       generic_args
-      |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
-      |> List.map ~f:(function
-           | GConst const -> (pexpr const, F.AST.Nothing)
-           | GLifetime _ -> .
-           | GType ty -> (pty span ty, F.AST.Hash))
+      |> List.filter ~f:(is_arrow >> not)
+      |> List.map ~f:(pgeneric_value span)
+      |> List.map ~f:(fun g -> (g, generic_qualifier))
     in
     let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
     F.mk_app f (generic_args @ args)
@@ -473,7 +466,8 @@ struct
                 chars: '" ^ s ^ "'");
         F.AST.Const (F.Const.Const_int (s, None)) |> F.term
     | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
-        fun_application ~span:e.span (pexpr f) args generic_args
+        make_application ~span:e.span ~generic_qualifier:F.AST.Hash (pexpr f)
+          args generic_args
     | If { cond; then_; else_ } ->
         F.term
         @@ F.AST.If
@@ -644,7 +638,7 @@ struct
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
       | GPType { default = _ } -> { kind; typ = F.type0_term; ident }
-      | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
+      | GPConst { typ } -> { kind; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =
       match c with
@@ -685,6 +679,10 @@ struct
     let to_term (x : t) : F.AST.term =
       F.term @@ F.AST.Var (FStar_Ident.lid_of_ns_and_id [] (to_ident x))
 
+    let to_qualified_term (x : t) : F.AST.term * F.AST.imp =
+      ( to_term x,
+        match x.kind with Explicit -> F.AST.Nothing | _ -> F.AST.Hash )
+
     let to_binder (x : t) : F.AST.binder =
       F.AST.
         {
@@ -1168,7 +1166,7 @@ struct
     | Trait { name; generics; items } ->
         let bds =
           List.map
-            ~f:FStarBinder.(of_generic_param e.span >> to_binder)
+            ~f:FStarBinder.(of_generic_param ~kind:Explicit e.span >> to_binder)
             generics.params
         in
         let name_str = U.Concrete_ident_view.to_definition_name name in
@@ -1211,14 +1209,16 @@ struct
                     let inputs = generics @ inputs in
                     let output = pty e.span output in
                     let ty_pre_post =
-                      let inputs = List.map ~f:FStarBinder.to_term inputs in
+                      let inputs =
+                        List.map ~f:FStarBinder.to_qualified_term inputs
+                      in
                       let add_pre n = n ^ "_pre" in
                       let pre_name_str =
                         U.Concrete_ident_view.to_definition_name
                           (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident)
                       in
                       let pre =
-                        F.mk_e_app (F.term_of_lid [ pre_name_str ]) inputs
+                        F.mk_app (F.term_of_lid [ pre_name_str ]) inputs
                       in
                       let result = F.term_of_lid [ "result" ] in
                       let add_post n = n ^ "_post" in
@@ -1227,9 +1227,9 @@ struct
                           (Concrete_ident.Create.map_last ~f:add_post i.ti_ident)
                       in
                       let post =
-                        F.mk_e_app
+                        F.mk_app
                           (F.term_of_lid [ post_name_str ])
-                          (inputs @ [ result ])
+                          (inputs @ [ (result, F.AST.Nothing) ])
                       in
                       let post =
                         F.mk_e_abs
@@ -1295,7 +1295,7 @@ struct
           @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics)
         in
         let typ =
-          fun_application ~span:e.span
+          make_application ~generic_qualifier:F.AST.Nothing ~span:e.span
             (F.term @@ F.AST.Name (pglobal_ident e.span trait))
             [] generic_args
         in