diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 0f4fd9f77..eda0b67cf 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -172,9 +172,8 @@ let t_NoE =
   x:
   Alloc.String.t_String
     { let _, out:(Core.Str.Iter.t_Chars & bool) =
-        Core.Iter.Traits.Iterator.f_any (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref x
-                <:
-                string)
+        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)
             <:
             Core.Str.Iter.t_Chars)
           (fun ch ->
@@ -184,7 +183,10 @@ 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 x <: u8) +! (Hax_lib.f_get y <: u8) <: t_BoundedU8 1uy 23uy
+  (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
+  (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
+  <:
+  t_BoundedU8 1uy 23uy
 
 let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
   x +! x <: t_Even
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index 3918f8b3a..db8f3cd46 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -67,7 +67,7 @@ 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 x, Core.Clone.f_clone x <: (v_T & v_T)
+    : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)
 
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
@@ -79,8 +79,10 @@ let g
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
       (arr: v_T)
     : usize =
-  (Core.Option.impl__unwrap_or (Core.Iter.Traits.Iterator.f_max (Core.Iter.Traits.Collect.f_into_iter
-              (Core.Convert.f_into arr <: t_Array usize v_N)
+  (Core.Option.impl__unwrap_or #usize
+      (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N)
+          (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)
             <:
             Core.Array.Iter.t_IntoIter usize v_N)
         <:
@@ -92,6 +94,7 @@ let g
 
 let call_g (_: Prims.unit) : usize =
   (g (sz 3)
+      #(t_Array usize (sz 3))
       (let list = [sz 42; sz 3; sz 49] in
         FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
         Rust_primitives.Hax.array_of_list 3 list)
@@ -102,10 +105,9 @@ let call_g (_: Prims.unit) : usize =
 let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
   let acc:usize = v_LEN +! sz 9 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = v_LEN
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ 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
index b7b010737..a4ce27894 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
-  let _:Prims.unit = main_a (Foo <: t_Foo) in
+  let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in
   let _:Prims.unit = main_c () in
   ()
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 2b54af53f..169518fc5 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
@@ -18,6 +18,7 @@ info:
       stderr: true
       stdout: true
     include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 stderr = '''
@@ -39,11 +40,14 @@ let bool_returning (x: u8) : bool = x <. 10uy
 let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let chunks:Core.Slice.Iter.t_ChunksExact usize =
-    Core.Slice.impl__chunks_exact (Core.Ops.Deref.f_deref arr <: t_Slice usize) v_CHUNK_LEN
+    Core.Slice.impl__chunks_exact #usize
+      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) 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.Clone.f_clone chunks
-
+    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
             <:
             Core.Slice.Iter.t_ChunksExact usize)
         <:
@@ -54,7 +58,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
           let chunk:t_Slice usize = chunk in
           let mean:usize = sz 0 in
           let mean:usize =
-            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter chunk
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+                  chunk
                 <:
                 Core.Slice.Iter.t_Iter usize)
               mean
@@ -67,10 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
           acc)
   in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.impl_87__remainder
-              chunks
-            <:
-            t_Slice usize)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+          (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize)
         <:
         Core.Slice.Iter.t_Iter usize)
       acc
@@ -84,7 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
 let composed_range (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_chain
+    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))
+          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
+              #(Core.Ops.Range.t_Range usize)
               ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
                 <:
                 Core.Ops.Range.t_Range usize)
@@ -111,8 +117,14 @@ let composed_range (n: usize) : usize =
 let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-              (Core.Slice.impl__chunks (Core.Ops.Deref.f_deref arr <: t_Slice usize) (sz 4)
+    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))
+          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
+              (Core.Slice.impl__chunks #usize
+                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+                    <:
+                    t_Slice usize)
+                  (sz 4)
                 <:
                 Core.Slice.Iter.t_Chunks usize)
             <:
@@ -123,8 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
       (fun acc temp_1_ ->
           let acc:usize = acc in
           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.Traits.Iterator.f_enumerate
-                    (Core.Slice.impl__iter chunk <: Core.Slice.Iter.t_Iter usize)
+          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))
+                (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize)
+                    (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize)
                   <:
                   Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize))
               <:
@@ -141,12 +155,9 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 
 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.f_start = 1uy;
-            Core.Ops.Range.f_end = 10uy
-          }
-          <:
-          Core.Ops.Range.t_Range u8)
+  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8
+        )
+        ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8)
       <:
       Core.Ops.Range.t_Range u8)
     acc
@@ -160,8 +171,10 @@ let f (_: Prims.unit) : u8 =
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter (Core.Ops.Deref.f_deref
-                  arr
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
+            usize)
+          (Core.Slice.impl__iter #usize
+              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -179,8 +192,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter (Core.Ops.Deref.f_deref
-                  arr
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
+            usize)
+          (Core.Slice.impl__iter #usize
+              (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -191,7 +206,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
       (fun acc item ->
           let acc:usize = acc in
           let item:usize = item in
-          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
+          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))
+                (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
                     ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item }
                       <:
                       Core.Ops.Range.t_Range usize)
@@ -204,8 +221,15 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
                 let acc:usize = acc in
                 let i:usize = i in
                 let acc:usize = acc +! sz 1 in
-                Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip
-                          (Core.Slice.impl__iter (Core.Ops.Deref.f_deref arr <: t_Slice usize)
+                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))
+                      (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize)
+                          #(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)
+                                  arr
+                                <:
+                                t_Slice usize)
                             <:
                             Core.Slice.Iter.t_Iter usize)
                           ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = i }
@@ -230,7 +254,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter arr
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec
+              (usize & usize) Alloc.Alloc.t_Global)
+          arr
         <:
         Alloc.Vec.Into_iter.t_IntoIter (usize & usize) Alloc.Alloc.t_Global)
       acc
@@ -244,10 +270,9 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
 let range1 (_: Prims.unit) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 15
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -263,10 +288,9 @@ let range1 (_: Prims.unit) : usize =
 let range2 (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-              Core.Ops.Range.f_start = sz 0;
-              Core.Ops.Range.f_end = n +! sz 10 <: usize
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -282,7 +306,9 @@ let range2 (n: usize) : usize =
 let rev_range (n: usize) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
+    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))
+          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
               ({ 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
index 62bf174e5..76f5002cd 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -45,11 +45,15 @@ let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
   x
 
 let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push vec 1uy in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push vec 2uy in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap vec (sz 0) (sz 1) in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
   vec
 
 let h (x: u8) : u8 =
@@ -79,9 +83,9 @@ let k
   (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
 
 let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
-                [1uy; 2uy; 3uy]
-              in
+  Alloc.Slice.impl__into_vec #u8
+    #Alloc.Alloc.t_Global
+    (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
               Rust_primitives.Hax.array_of_list 3 list)
           <:
@@ -91,9 +95,9 @@ let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
 
 let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit =
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
-                  [1uy]
-                in
+    Alloc.Slice.impl__into_vec #u8
+      #Alloc.Alloc.t_Global
+      (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                 Rust_primitives.Hax.array_of_list 1 list)
             <:
@@ -104,7 +108,7 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range v
       x
-      (Core.Slice.impl__copy_from_slice (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
+      (Core.Slice.impl__copy_from_slice #u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
   in
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v (sz 1) 3uy
@@ -117,10 +121,8 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
       ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 }
         <:
         Core.Ops.Range.t_Range usize)
-      (Core.Slice.impl__copy_from_slice (x.[ {
-                Core.Ops.Range.f_start = sz 4;
-                Core.Ops.Range.f_end = sz 5
-              }
+      (Core.Slice.impl__copy_from_slice #u8
+          (x.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 }
               <:
               Core.Ops.Range.t_Range usize ]
             <:
@@ -136,11 +138,11 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   42uy
 
 let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new () in
+  let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
-                  [1uy; 2uy; 3uy]
-                in
+    Alloc.Slice.impl__into_vec #u8
+      #Alloc.Alloc.t_Global
+      (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
                 Rust_primitives.Hax.array_of_list 3 list)
             <:
@@ -150,13 +152,16 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   in
   let tmp0, tmp1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   =
-    Alloc.Vec.impl_1__append vec1 vec2
+    Alloc.Vec.impl_1__append #u8 #Alloc.Alloc.t_Global vec1 vec2
   in
   let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp0 in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp1 in
   let _:Prims.unit = () in
   let vec1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    Alloc.Vec.impl_1__append vec1 (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    Alloc.Vec.impl_1__append #u8
+      #Alloc.Alloc.t_Global
+      vec1
+      (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   vec1
 
@@ -190,10 +195,9 @@ let impl__S__update (self: t_S) (x: u8) : t_S =
 
 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.f_start = sz 0;
-              Core.Ops.Range.f_end = sz 1
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            usize)
+          ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 }
             <:
             Core.Ops.Range.t_Range usize)
         <:
@@ -239,10 +243,9 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
   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.f_start = 1uy;
-              Core.Ops.Range.f_end = 10uy
-            }
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+            u8)
+          ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy }
             <:
             Core.Ops.Range.t_Range u8)
         <:
@@ -251,19 +254,26 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
       (fun x i ->
           let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
           let i:u8 = i in
-          { x with f_a = Alloc.Vec.impl_1__push x.f_a i <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
+          {
+            x with
+            f_a
+            =
+            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
+            <:
+            Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+          }
           <:
           t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
   in
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    { x with f_a = Core.Slice.impl__swap x.f_a (sz 0) (sz 1) }
+    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
     <:
     t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
     {
       x with
-      f_b = { x.f_b with f_field = Core.Slice.impl__swap x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
     }
     <:
     t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 576052fc1..68c009f19 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -43,8 +43,8 @@ let debug (label value: u32) : Prims.unit =
             t_Slice string)
           (Rust_primitives.unsize (let list =
                   [
-                    Core.Fmt.Rt.impl_1__new_display label <: Core.Fmt.Rt.t_Argument;
-                    Core.Fmt.Rt.impl_1__new_display value <: Core.Fmt.Rt.t_Argument
+                    Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument;
+                    Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument
                   ]
                 in
                 FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index ee3c46e86..f99f13441 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -117,10 +117,9 @@ let local_mutation (x: u32) : u32 =
     let y:u32 = x /! 2ul in
     let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in
     let y:u32 =
-      Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
-                Core.Ops.Range.f_start = 0ul;
-                Core.Ops.Range.f_end = 10ul
-              }
+      Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
+              u32)
+            ({ Core.Ops.Range.f_start = 0ul; Core.Ops.Range.f_end = 10ul }
               <:
               Core.Ops.Range.t_Range u32)
           <:
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index c54b93f95..5b8ac2c47 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -48,12 +48,11 @@ open FStar.Mul
 
 let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({
-            Core.Ops.Range.f_start = 0uy;
-            Core.Ops.Range.f_end = 5uy
-          }
-          <:
-          Core.Ops.Range.t_Range u8)
+  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+        (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+        ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
         (fun temp_0_ ->
             let _:u8 = temp_0_ in
             true)
@@ -64,23 +63,28 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range
     : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
-    Core.Iter.Traits.Iterator.f_collect it
+    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+          (Core.Ops.Range.t_Range u8) (u8 -> bool))
+      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      it
   in
   ()
 
 let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
-    Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_filter ({
-              Core.Ops.Range.f_start = 0uy;
-              Core.Ops.Range.f_end = 5uy
-            }
-            <:
-            Core.Ops.Range.t_Range u8)
+    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+          (Core.Ops.Range.t_Range u8) (u8 -> bool))
+      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+          ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8
+          )
           (fun i ->
               let i:u8 = i in
               let _, out:(Core.Slice.Iter.t_Iter u8 & bool) =
-                Core.Iter.Traits.Iterator.f_any (Core.Slice.impl__iter (Core.Ops.Deref.f_deref list
+                Core.Iter.Traits.Iterator.f_any #(Core.Slice.Iter.t_Iter u8)
+                  (Core.Slice.impl__iter #u8
+                      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list
                         <:
                         t_Slice u8)
                     <:
@@ -109,9 +113,46 @@ class t_Foo (v_Self: Type0) (v_T: Type0) = {
 
 let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X)
     : Prims.unit =
-  let _:u8 = f_to_t x in
+  let _:u8 = f_to_t #v_X #u8 x in
   ()
 '''
+"Traits.Unconstrainted_types_issue_677_.fst" = '''
+module Traits.Unconstrainted_types_issue_677_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_PolyOp (v_Self: Type0) = {
+  f_op_pre:u32 -> u32 -> bool;
+  f_op_post:u32 -> u32 -> u32 -> bool;
+  f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
+}
+
+let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp v_OP) (x: u32)
+    : u32 = f_op #v_OP x x
+
+type t_Plus = | Plus : t_Plus
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: t_PolyOp t_Plus =
+  {
+    f_op_pre = (fun (x: u32) (y: u32) -> true);
+    f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true);
+    f_op = fun (x: u32) (y: u32) -> x +! y
+  }
+
+type t_Times = | Times : t_Times
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: t_PolyOp t_Times =
+  {
+    f_op_pre = (fun (x: u32) (y: u32) -> true);
+    f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true);
+    f_op = fun (x: u32) (y: u32) -> x *! y
+  }
+
+let both (x: u32) : (u32 & u32) = twice #t_Plus x, twice #t_Times x <: (u32 & u32)
+'''
 "Traits.fst" = '''
 module Traits
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -125,7 +166,7 @@ class t_Bar (v_Self: Type0) = {
 }
 
 let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
-    : Prims.unit = f_bar x
+    : Prims.unit = f_bar #v_T x
 
 type t_Error = | Error_Fail : t_Error
 
@@ -187,7 +228,9 @@ let closure_impl_expr
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
       (it: v_I)
     : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it (fun x -> x)
+  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
+    #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit it (fun x -> x)
       <:
       Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
 
@@ -198,16 +241,18 @@ let closure_impl_expr_fngen
       (it: v_I)
       (f: v_F)
     : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it f
+  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I v_F)
+    #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit #v_F it f
       <:
       Core.Iter.Adapters.Map.t_Map v_I v_F)
 
 let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
-  let _:Prims.unit = f_assoc_f () in
-  f_method_f x
+  let _:Prims.unit = f_assoc_f #v_T () in
+  f_method_f #v_T x
 
 let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
-    : u32 = f_function_of_super_trait x
+    : u32 = f_function_of_super_trait #i1.f_AssocType x
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
@@ -220,7 +265,7 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit =
     f_assoc_f = (fun (_: Prims.unit) -> () <: Prims.unit);
     f_method_f_pre = (fun (self: Prims.unit) -> true);
     f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true);
-    f_method_f = (fun (self: Prims.unit) -> f_assoc_f ());
+    f_method_f = (fun (self: Prims.unit) -> f_assoc_f #Prims.unit ());
     f_assoc_type_pre = (fun (_: i32) -> true);
     f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true);
     f_assoc_type = fun (_: i32) -> ()
diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
index cefd74043..9f38e5e0e 100644
--- a/tests/traits/src/lib.rs
+++ b/tests/traits/src/lib.rs
@@ -108,3 +108,36 @@ mod for_clauses {
         }
     }
 }
+
+// From issue #677
+mod unconstrainted_types_issue_677 {
+    trait PolyOp {
+        fn op(x: u32, y: u32) -> u32;
+    }
+    struct Plus;
+    impl PolyOp for Plus {
+        fn op(x: u32, y: u32) -> u32 {
+            x + y
+        }
+    }
+
+    struct Times;
+    impl PolyOp for Times {
+        fn op(x: u32, y: u32) -> u32 {
+            x * y
+        }
+    }
+
+    fn twice<OP: PolyOp>(x: u32) -> u32 {
+        OP::op(x, x)
+    }
+
+    fn both(x: u32) -> (u32, u32) {
+        (twice::<Plus>(x), twice::<Times>(x))
+    }
+
+    #[test]
+    fn test() {
+        assert!(both(10) == (20, 100));
+    }
+}