Merge pull request #726 from hacspec/fix-719

fix(engine/fstar): fix implicit discrepancies in traits

engine/backends/fstar/fstar_backend.ml

@@ -407,6 +407,18 @@ struct
       (* in *)
       F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange))
 
+  and fun_application ~span f args generic_args =
+    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))
+    in
+    let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
+    F.mk_app f (generic_args @ args)
+
   and pexpr_unwrapped (e : expr) =
     match e.e with
     | Literal l -> pliteral_as_expr e.span l
@@ -452,16 +464,7 @@ struct
                 chars: '" ^ s ^ "'");
         F.AST.Const (F.Const.Const_int (s, None)) |> F.term
     | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
-        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 e.span ty, F.AST.Hash))
-        in
-        let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
-        F.mk_app (pexpr f) (generic_args @ args)
+        fun_application ~span:e.span (pexpr f) args generic_args
     | If { cond; then_; else_ } ->
         F.term
         @@ F.AST.If
@@ -1156,7 +1159,7 @@ struct
     | Trait { name; generics; items } ->
         let bds =
           List.map
-            ~f:FStarBinder.(of_generic_param ~kind:Explicit e.span >> to_binder)
+            ~f:FStarBinder.(of_generic_param e.span >> to_binder)
             generics.params
         in
         let name_str = U.Concrete_ident_view.to_definition_name name in
@@ -1293,9 +1296,9 @@ struct
           @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics)
         in
         let typ =
-          F.mk_e_app
+          fun_application ~span:e.span
             (F.term @@ F.AST.Name (pglobal_ident e.span trait))
-            (List.map ~f:(pgeneric_value e.span) generic_args)
+            [] generic_args
         in
         let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in
         let fields =

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

@@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
   else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
+let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index #(t_Array v_T (sz 10)) #t_SafeIndex =
   {
     f_Output = v_T;
     f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
@@ -79,7 +79,7 @@ open FStar.Mul
 type t_Foo = | Foo : u8 -> t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
+let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
   {
     f_Output = t_Foo;
     f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8));
@@ -88,7 +88,7 @@ let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
+let impl_1: Core.Ops.Arith.t_Mul #t_Foo #t_Foo =
   {
     f_Output = t_Foo;
     f_mul_pre
@@ -131,7 +131,7 @@ let mutation_example
   (t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Index.t_Index t_MyArray usize =
+let impl: Core.Ops.Index.t_Index #t_MyArray #usize =
   {
     f_Output = u8;
     f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX);

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

@@ -48,15 +48,15 @@ open FStar.Mul
 let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
   ()
 
-class t_Foo (v_Self: Type0) = {
+class t_Foo (#v_Self: Type0) = {
   f_const_add_pre:v_N: usize -> v_Self -> bool;
   f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
   f_const_add:v_N: usize -> x0: v_Self
     -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_usize: t_Foo usize =
+let impl_Foo_for_usize: t_Foo #usize =
   {
     f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
     f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);

test-harness/src/snapshots/toolchain__include-flag into-fstar.snap

@@ -32,7 +32,7 @@ module Include_flag
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 /// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
@@ -76,7 +76,7 @@ let main_c (_: Prims.unit) : Prims.unit =
 type t_Foo = | Foo : t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
+let impl_Trait_for_Foo: t_Trait #t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =

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

@@ -54,7 +54,7 @@ type t_Bar = | Bar : t_Bar
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Convert.t_From t_Bar Prims.unit =
+let impl: Core.Convert.t_From #t_Bar #Prims.unit =
   {
     f_from_pre = (fun ((): Prims.unit) -> true);
     f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true);
@@ -65,7 +65,7 @@ val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
 /// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Convert.t_From t_Bar u8 =
+let impl_1: Core.Convert.t_From #t_Bar #u8 =
   {
     f_from_pre = (fun (x: u8) -> true);
     f_from_post = (fun (x: u8) (out: t_Bar) -> true);

test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap

@@ -32,7 +32,7 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-class t_FooTrait (v_Self: Type0) = {
+class t_FooTrait (#v_Self: Type0) = {
   f_z_pre:v_Self -> bool;
   f_z_post:v_Self -> v_Self -> bool;
   f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
@@ -173,7 +173,7 @@ type t_Bar = {
 type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
+let impl_FooTrait_for_Foo: t_FooTrait #t_Foo =
   {
     f_z_pre = (fun (self: t_Foo) -> true);
     f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);

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

@@ -108,22 +108,22 @@ type t_Foo2 =
   | Foo2_A : t_Foo2
   | Foo2_B { f_x:usize }: t_Foo2
 
-class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+class t_FooTrait (#v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
-class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
+class t_T1 (#v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
+let impl_T1_for_Foo: t_T1 #t_Foo = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
+let impl_T1_for_tuple_Foo_u8: t_T1 #(t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
+class t_T2_for_a (#v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
 
-class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
+class t_T3_e_for_a (#v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
+let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a #t_Foo = { __marker_trait = () }
 
 let v_INHERENT_CONSTANT: usize = sz 3
 
@@ -146,7 +146,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
+let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a #(t_Arity1 (t_Foo & u8)) =
   { __marker_trait = () }
 
 type t_B = | B : t_B