fix(engine/fstar): fixes #719

hacspec · Jun 20, 2024 · 6c77640 · 6c77640
1 parent d10f891
commit 6c77640
Show file tree

Hide file tree

Showing 10 changed files with 121 additions and 127 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -458,7 +458,7 @@ struct
           |> List.map ~f:(function
                | GConst const -> (pexpr const, F.AST.Nothing)
                | GLifetime _ -> .
-               | GType ty -> (pty e.span ty, F.AST.Hash))
+               | GType ty -> (pty e.span ty, F.AST.Nothing))
         in
         let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
         F.mk_app (pexpr f) (generic_args @ args)
@@ -626,7 +626,7 @@ struct
     type kind = Implicit | Tcresolve | Explicit
     type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term }
 
-    let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t
+    let of_generic_param ?(kind : kind = Explicit) span (p : generic_param) : t
         =
       let ident = plocal_ident p.ident in
       match p.kind with
@@ -641,8 +641,8 @@ struct
           let typ = c_trait_goal span goal in
           { kind = Tcresolve; ident = F.id name; typ }
 
-    let of_generics ?(kind : kind = Implicit) span generics : t list =
-      List.map ~f:(of_generic_param ~kind span) generics.params
+    let of_generics ?(kind : kind = Explicit) span generics : t list =
+      List.map ~f:(of_generic_param ~kind:Explicit span) generics.params
       @ List.mapi ~f:(of_generic_constraint span) generics.constraints
 
     let of_typ span (nth : int) typ : t =
@@ -1166,7 +1166,7 @@ struct
             ~f:(fun i ->
               let name = U.Concrete_ident_view.to_definition_name i.ti_ident in
               let generics =
-                FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics
+                FStarBinder.of_generics ~kind:Explicit i.ti_span i.ti_generics
               in
               let bds = generics |> List.map ~f:FStarBinder.to_binder in
               let fields =

diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -37,7 +37,7 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : Type0
 
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : Type0
 '''
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);
@@ -172,8 +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.Iter.t_Chars
-          (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String 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 ->
@@ -183,8 +183,7 @@ 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) x <: u8) +! (Hax_lib.f_get (t_BoundedU8 10uy 11uy) 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
@@ -45,7 +45,7 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+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) = {
@@ -63,26 +63,23 @@ let impl_Foo_for_usize: t_Foo usize =
     f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
   }
 
-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)
+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)
 
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
 let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
 
 let g
       (v_N: usize)
-      (#v_T: Type0)
+      (v_T: Type0)
       (#[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 #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.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)
         <:
@@ -94,7 +91,7 @@ let g
 
 let call_g (_: Prims.unit) : usize =
   (g (sz 3)
-      #(t_Array usize (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)
@@ -105,7 +102,7 @@ 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.t_Range
+    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 }
             <:
@@ -122,7 +119,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
 
 let repeat
       (v_LEN: usize)
-      (#v_T: Type0)
+      (v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
       (x: v_T)
     : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN

diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
@@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = ()
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
 /// Direct dependencies
-let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
+let main_a (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
   let _:Prims.unit = main_a_b () in
@@ -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 #t_Foo (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
@@ -40,14 +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 #usize
-      (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice 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)
       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
+    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.Clone.f_clone (Core.Slice.Iter.t_ChunksExact usize) chunks
             <:
             Core.Slice.Iter.t_ChunksExact usize)
         <:
@@ -58,7 +58,7 @@ 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 #(t_Slice usize)
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize)
                   chunk
                 <:
                 Core.Slice.Iter.t_Iter usize)
@@ -72,8 +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 #(t_Slice usize)
-          (Core.Slice.Iter.impl_87__remainder #usize 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
@@ -87,10 +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.Adapters.Chain.t_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.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)
@@ -117,11 +117,11 @@ 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.Adapters.Enumerate.t_Enumerate
+    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
+          (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)
@@ -135,10 +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.Adapters.Enumerate.t_Enumerate
+          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.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))
               <:
@@ -155,8 +155,7 @@ 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.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)
@@ -171,10 +170,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.Iter.t_Iter
+    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
+          (Core.Slice.impl__iter usize
+              (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -192,10 +191,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.Iter.t_Iter
+    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
+          (Core.Slice.impl__iter usize
+              (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
                 <:
                 t_Slice usize)
             <:
@@ -206,9 +205,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.Adapters.Rev.t_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.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)
@@ -221,12 +220,12 @@ 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.Adapters.Zip.t_Zip
+                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)
+                      (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)
@@ -254,7 +253,7 @@ 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 #(Alloc.Vec.t_Vec
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Alloc.Vec.t_Vec
               (usize & usize) Alloc.Alloc.t_Global)
           arr
         <:
@@ -270,7 +269,7 @@ 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.t_Range
+    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 }
             <:
@@ -288,7 +287,7 @@ 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.t_Range
+    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 }
             <:
@@ -306,9 +305,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.Adapters.Rev.t_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.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)