test(engine/f*): propagate trait-specific generics

cryspen · Jul 9, 2024 · f5881dd · f5881dd
1 parent d82d584
commit f5881dd
Show file tree

Hide file tree

Showing 10 changed files with 385 additions and 63 deletions.
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/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);
@@ -173,7 +173,12 @@ let t_NoE =
   Alloc.String.t_String
     { let _, out:(Core.Str.Iter.t_Chars & bool) =
         Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars
-          (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string)
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String
+                  #FStar.Tactics.Typeclasses.solve
+                  x
+                <:
+                string)
             <:
             Core.Str.Iter.t_Chars)
           (fun ch ->
@@ -183,8 +188,8 @@ let t_NoE =
       ~.out }
 
 let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
-  (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
-  (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
+  (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) #FStar.Tactics.Typeclasses.solve x <: u8) +!
+  (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) #FStar.Tactics.Typeclasses.solve y <: u8)
   <:
   t_BoundedU8 1uy 23uy
 

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -46,15 +46,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);
@@ -65,7 +65,11 @@ let dup
       (#v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
       (x: v_T)
-    : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)
+    : (v_T & v_T) =
+  Core.Clone.f_clone #v_T #FStar.Tactics.Typeclasses.solve x,
+  Core.Clone.f_clone #v_T #FStar.Tactics.Typeclasses.solve x
+  <:
+  (v_T & v_T)
 
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
@@ -79,8 +83,12 @@ let g
     : usize =
   (Core.Option.impl__unwrap_or #usize
       (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N)
+          #FStar.Tactics.Typeclasses.solve
           (Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N)
-              (Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N)
+              #FStar.Tactics.Typeclasses.solve
+              (Core.Convert.f_into #v_T #(t_Array usize v_N) #FStar.Tactics.Typeclasses.solve arr
+                <:
+                t_Array usize v_N)
             <:
             Core.Array.Iter.t_IntoIter usize v_N)
         <:
@@ -105,6 +113,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
             usize)
+          #FStar.Tactics.Typeclasses.solve
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN }
             <:
             Core.Ops.Range.t_Range usize)

diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/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 =

diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -52,7 +52,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);
@@ -63,7 +63,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);

diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -39,13 +39,20 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
   let acc:usize = sz 0 in
   let chunks:Core.Slice.Iter.t_ChunksExact usize =
     Core.Slice.impl__chunks_exact #usize
-      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
+      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+          #FStar.Tactics.Typeclasses.solve
+          arr
+        <:
+        t_Slice usize)
       v_CHUNK_LEN
   in
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact
             usize)
-          (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize)
+              #FStar.Tactics.Typeclasses.solve
+              chunks
             <:
             Core.Slice.Iter.t_ChunksExact usize)
         <:
@@ -57,6 +64,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
           let mean:usize = sz 0 in
           let mean:usize =
             Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+                  #FStar.Tactics.Typeclasses.solve
                   chunk
                 <:
                 Core.Slice.Iter.t_Iter usize)
@@ -71,6 +79,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
   in
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+          #FStar.Tactics.Typeclasses.solve
           (Core.Slice.Iter.impl_88__remainder #usize chunks <: t_Slice usize)
         <:
         Core.Slice.Iter.t_Iter usize)
@@ -87,7 +96,9 @@ let composed_range (n: usize) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
               (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
           (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
               #(Core.Ops.Range.t_Range usize)
               ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
                 <:
@@ -117,9 +128,13 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
             (Core.Slice.Iter.t_Chunks usize))
+          #FStar.Tactics.Typeclasses.solve
           (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
+              #FStar.Tactics.Typeclasses.solve
               (Core.Slice.impl__chunks #usize
-                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                      #FStar.Tactics.Typeclasses.solve
+                      arr
                     <:
                     t_Slice usize)
                   (sz 4)
@@ -135,7 +150,9 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
           let i, chunk:(usize & t_Slice usize) = temp_1_ in
           Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
                   (Core.Slice.Iter.t_Iter usize))
+                #FStar.Tactics.Typeclasses.solve
                 (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize)
+                    #FStar.Tactics.Typeclasses.solve
                     (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize)
                   <:
                   Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize))
@@ -155,6 +172,7 @@ let f (_: Prims.unit) : u8 =
   let acc:u8 = 0uy in
   Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8
         )
+        #FStar.Tactics.Typeclasses.solve
         ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8)
       <:
       Core.Ops.Range.t_Range u8)
@@ -171,8 +189,11 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
             usize)
+          #FStar.Tactics.Typeclasses.solve
           (Core.Slice.impl__iter #usize
-              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                  #FStar.Tactics.Typeclasses.solve
+                  arr
                 <:
                 t_Slice usize)
             <:
@@ -192,8 +213,11 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
             usize)
+          #FStar.Tactics.Typeclasses.solve
           (Core.Slice.impl__iter #usize
-              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                  #FStar.Tactics.Typeclasses.solve
+                  arr
                 <:
                 t_Slice usize)
             <:
@@ -206,7 +230,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
           let item:usize = item in
           Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
                   (Core.Ops.Range.t_Range usize))
+                #FStar.Tactics.Typeclasses.solve
                 (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+                    #FStar.Tactics.Typeclasses.solve
                     ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item }
                       <:
                       Core.Ops.Range.t_Range usize)
@@ -221,10 +247,13 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
                 let acc:usize = acc +! sz 1 in
                 Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip
                           (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize))
+                      #FStar.Tactics.Typeclasses.solve
                       (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize)
+                          #FStar.Tactics.Typeclasses.solve
                           #(Core.Ops.Range.t_Range usize)
                           (Core.Slice.impl__iter #usize
                               (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                                  #FStar.Tactics.Typeclasses.solve
                                   arr
                                 <:
                                 t_Slice usize)
@@ -254,6 +283,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec
               (usize & usize) Alloc.Alloc.t_Global)
+          #FStar.Tactics.Typeclasses.solve
           arr
         <:
         Alloc.Vec.Into_iter.t_IntoIter (usize & usize) Alloc.Alloc.t_Global)
@@ -270,6 +300,7 @@ let range1 (_: Prims.unit) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
             usize)
+          #FStar.Tactics.Typeclasses.solve
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 }
             <:
             Core.Ops.Range.t_Range usize)
@@ -288,6 +319,7 @@ let range2 (n: usize) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
             usize)
+          #FStar.Tactics.Typeclasses.solve
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize }
             <:
             Core.Ops.Range.t_Range usize)
@@ -306,7 +338,9 @@ let rev_range (n: usize) : usize =
   let acc:usize =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
             (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
           (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
               ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
                 <:
                 Core.Ops.Range.t_Range usize)

diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/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);
@@ -197,6 +197,7 @@ let foo (lhs rhs: t_S) : t_S =
   let lhs:t_S =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
             usize)
+          #FStar.Tactics.Typeclasses.solve
           ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 }
             <:
             Core.Ops.Range.t_Range usize)
@@ -245,6 +246,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
             u8)
+          #FStar.Tactics.Typeclasses.solve
           ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy }
             <:
             Core.Ops.Range.t_Range u8)

diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -104,22 +104,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
 
@@ -142,7 +142,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