From 253fb96ada948361b481dd7e525ce5a0276323e7 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.dev>
Date: Wed, 26 Jun 2024 15:41:34 +0200
Subject: [PATCH] fix(proofs-lib/fstar): make type implicits on typeclasses

---
 proof-libs/fstar/core/Alloc.Vec.fst           |  4 +--
 proof-libs/fstar/core/Core.Clone.fst          |  4 +--
 proof-libs/fstar/core/Core.Cmp.fsti           | 18 +++++-----
 proof-libs/fstar/core/Core.Convert.fst        | 20 +++++------
 proof-libs/fstar/core/Core.Default.fsti       |  2 +-
 proof-libs/fstar/core/Core.Fmt.fsti           |  2 +-
 .../fstar/core/Core.Iter.Traits.Collect.fst   |  6 ++--
 .../fstar/core/Core.Iter.Traits.Iterator.fst  |  2 +-
 proof-libs/fstar/core/Core.Iter.fsti          | 22 ++++++------
 proof-libs/fstar/core/Core.Marker.fst         |  8 ++---
 proof-libs/fstar/core/Core.Num.fsti           | 16 ++++-----
 proof-libs/fstar/core/Core.Ops.Arith.fsti     | 12 +++----
 .../fstar/core/Core.Ops.Index.IndexMut.fst    |  4 +--
 proof-libs/fstar/core/Core.Ops.Index.fst      |  2 +-
 proof-libs/fstar/core/Core.Ops.Range.fsti     | 34 +++++++++----------
 proof-libs/fstar/core/Core.Ops.Try_trait.fst  |  6 ++--
 proof-libs/fstar/core/Core.Ops.fst            |  8 ++---
 proof-libs/fstar/core/Core.Slice.fsti         |  2 +-
 proof-libs/fstar/core/Rand_core.fsti          |  4 +--
 .../rust_primitives/Rust_primitives.Hax.fst   | 16 ++++-----
 .../fstar/rust_primitives/Rust_primitives.fst |  8 ++---
 21 files changed, 100 insertions(+), 100 deletions(-)

diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 01f566049..6e8f36308 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -30,8 +30,8 @@ let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index
-instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = {
-  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Vec t ()) (int_t n);
+instance update_at_tc_array t n: update_at_tc #(t_Vec t ()) #(int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index #(t_Vec t ()) #(int_t n);
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
diff --git a/proof-libs/fstar/core/Core.Clone.fst b/proof-libs/fstar/core/Core.Clone.fst
index a28310f3a..32b6aad79 100644
--- a/proof-libs/fstar/core/Core.Clone.fst
+++ b/proof-libs/fstar/core/Core.Clone.fst
@@ -1,11 +1,11 @@
 module Core.Clone
 
-class t_Clone self = {
+class t_Clone #self = {
   f_clone: x:self -> r:self {x == r}
 }
 
 (** Everything is clonable *)
-instance clone_all (t: Type): t_Clone t = {
+instance clone_all (t: Type): t_Clone #t = {
   f_clone = (fun x -> x);
 }
 
diff --git a/proof-libs/fstar/core/Core.Cmp.fsti b/proof-libs/fstar/core/Core.Cmp.fsti
index 967291795..e13a861ff 100644
--- a/proof-libs/fstar/core/Core.Cmp.fsti
+++ b/proof-libs/fstar/core/Core.Cmp.fsti
@@ -1,11 +1,11 @@
 module Core.Cmp
 open Rust_primitives
 
-class min_tc t = {
+class min_tc #t = {
   min: t -> t -> t
 }
 
-instance min_inttype (#t:inttype): min_tc (int_t t) = {
+instance min_inttype (#t:inttype): min_tc #(int_t t) = {
   min = fun a b -> if a <. b then a else b
 }
 
@@ -14,26 +14,26 @@ type t_Ordering =
   | Ordering_Equal : t_Ordering
   | Ordering_Greater : t_Ordering
 
-class t_Ord (v_Self: Type) = {
+class t_Ord (#v_Self: Type) = {
   f_cmp:v_Self -> v_Self -> t_Ordering;
   // f_max:v_Self -> v_Self -> v_Self;
   // f_min:v_Self -> v_Self -> v_Self;
   // f_clamp:v_Self -> v_Self -> v_Self -> v_Self
 }
 
-class t_PartialEq (v_Self: Type) (v_Rhs: Type) = {
+class t_PartialEq (#v_Self: Type) (#v_Rhs: Type) = {
   // __constraint_1069563329_t_PartialEq:t_PartialEq v_Self v_Rhs;
   f_eq:v_Self -> v_Rhs -> bool;
   f_ne:v_Self -> v_Rhs -> bool
 }
 
-instance all_eq (a: eqtype): t_PartialEq a a = {
+instance all_eq (a: eqtype): t_PartialEq #a #a = {
   f_eq = (fun x y -> x = y);
   f_ne = (fun x y -> x <> y);
 }
 
-class t_PartialOrd (v_Self: Type) (v_Rhs: Type) = {
-  __constraint_Rhs_t_PartialEq:t_PartialEq v_Self v_Rhs;
+class t_PartialOrd (#v_Self: Type) (#v_Rhs: Type) = {
+  __constraint_Rhs_t_PartialEq:t_PartialEq #v_Self #v_Rhs;
   // __constraint_Rhs_t_PartialOrd:t_PartialOrd v_Self v_Rhs;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
   // f_lt:v_Self -> v_Rhs -> bool;
@@ -47,7 +47,7 @@ type t_Reverse t = | Reverse of t
 let impl__then x y = x
 
 [@FStar.Tactics.Typeclasses.tcinstance]
-val ord_u64: t_Ord u64
+val ord_u64: t_Ord #u64
 
 [@FStar.Tactics.Typeclasses.tcinstance]
-val ord_reverse t {| t_Ord t |}: t_Ord (t_Reverse t)
+val ord_reverse t {| t_Ord #t |}: t_Ord #(t_Reverse t)
diff --git a/proof-libs/fstar/core/Core.Convert.fst b/proof-libs/fstar/core/Core.Convert.fst
index cfac41d66..91d71be5c 100644
--- a/proof-libs/fstar/core/Core.Convert.fst
+++ b/proof-libs/fstar/core/Core.Convert.fst
@@ -2,13 +2,13 @@
 module Core.Convert
 open Rust_primitives
 
-class try_into_tc self t = {
+class try_into_tc #self #t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
   f_try_into: self -> Core.Result.t_Result t f_Error
 }
 
-instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len) = {
+instance impl_6 (t: Type0) (len: usize): try_into_tc #(t_Slice t) #(t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t) -> 
     if Core.Slice.impl__len s = len
@@ -18,26 +18,26 @@ instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len)
 }
 
 
-instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core.Slice.impl__len s == len}) (t_Array t len) = {
+instance impl_6_refined (t: Type0) (len: usize): try_into_tc #(s: t_Slice t {Core.Slice.impl__len s == len}) #(t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t {Core.Slice.impl__len s == len}) -> 
     Core.Result.Result_Ok (s <: t_Array t len)
   )
 }
 
-class t_Into self t = {
+class t_Into #self #t = {
   f_into_pre: self -> bool;
   f_into_post: self -> t -> bool;
   f_into: self -> t;
 }
 
-class t_From self t = {
+class t_From #self #t = {
   f_from_pre: t -> bool;
   f_from_post: t -> self -> bool;
   f_from: t -> self;
 }
 
-class t_TryFrom self t = {
+class t_TryFrom #self #t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
   f_try_from_pre: t -> bool;
@@ -47,26 +47,26 @@ class t_TryFrom self t = {
 
 instance integer_into
   (t:inttype) (t':inttype { minint t >= minint t' /\ maxint t <= maxint t' })
-  : t_From (int_t t') (int_t t)
+  : t_From #(int_t t') #(int_t t)
   = {
       f_from_pre = (fun _ -> true);
       f_from_post = (fun _ _ -> true);
       f_from = (fun (x: int_t t) -> Rust_primitives.Integers.cast #t #t' x);
     }
 
-instance into_from_from a b {| t_From a b |}: t_Into b a = {
+instance into_from_from a b {| t_From #a #b |}: t_Into #b #a = {
   f_into_pre = (fun _ -> true);
   f_into_post = (fun _ _ -> true);
   f_into = (fun x -> f_from x)
 }
 
-instance from_id a: t_From a a = {
+instance from_id a: t_From #a #a = {
   f_from_pre = (fun _ -> true);
   f_from_post = (fun _ _ -> true);
   f_from = (fun x -> x)
 }
 
-class t_AsRef self t = {
+class t_AsRef #self #t = {
   f_as_ref_pre: self -> bool;
   f_as_ref_post: self -> t -> bool;
   f_as_ref: self -> t;
diff --git a/proof-libs/fstar/core/Core.Default.fsti b/proof-libs/fstar/core/Core.Default.fsti
index 406cc0774..0ef5f36d1 100644
--- a/proof-libs/fstar/core/Core.Default.fsti
+++ b/proof-libs/fstar/core/Core.Default.fsti
@@ -1,5 +1,5 @@
 module Core.Default
 
-class t_Default (t: Type0) = {
+class t_Default (#t: Type0) = {
   v_default: unit -> t;
 }
diff --git a/proof-libs/fstar/core/Core.Fmt.fsti b/proof-libs/fstar/core/Core.Fmt.fsti
index ac6a1c985..4a9cd6067 100644
--- a/proof-libs/fstar/core/Core.Fmt.fsti
+++ b/proof-libs/fstar/core/Core.Fmt.fsti
@@ -6,7 +6,7 @@ val t_Error: Type0
 type t_Result = Core.Result.t_Result unit t_Error
 
 val t_Formatter: Type0
-class t_Display t_Self = {
+class t_Display #t_Self = {
   f_fmt_pre: t_Self -> Core.Fmt.t_Formatter -> bool;
   f_fmt_post: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) -> bool;
   f_fmt: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error)
diff --git a/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst b/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
index 33b16938c..9f803e3f0 100644
--- a/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
+++ b/proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
@@ -1,14 +1,14 @@
 module Core.Iter.Traits.Collect
 
-class into_iterator self = {
+class into_iterator #self = {
   f_IntoIter: Type0;
   // f_Item: Type0;
   f_into_iter: self -> f_IntoIter;
 }
 
-let t_IntoIterator = into_iterator
+let t_IntoIterator #self = into_iterator #self
 
-unfold instance impl t {| Core.Iter.Traits.Iterator.iterator t |}: into_iterator t = {
+unfold instance impl t {| Core.Iter.Traits.Iterator.iterator #t |}: into_iterator #t = {
   f_IntoIter = t;
   f_into_iter = id;
 }
diff --git a/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst b/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
index 6a9c67564..fe4c34ff4 100644
--- a/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
+++ b/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst
@@ -28,7 +28,7 @@ unfold type t_all self item
 //   f_enumerate: t_enumerate self;
 // }
 
-class iterator (self: Type u#0): Type u#1 = {
+class iterator (#self: Type u#0): Type u#1 = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Item: Type0;
   f_next:      self -> self * option f_Item;
diff --git a/proof-libs/fstar/core/Core.Iter.fsti b/proof-libs/fstar/core/Core.Iter.fsti
index ef2095e7f..e4ae628c4 100644
--- a/proof-libs/fstar/core/Core.Iter.fsti
+++ b/proof-libs/fstar/core/Core.Iter.fsti
@@ -9,18 +9,18 @@ open Core.Iter.Traits.Iterator
 (**** Enumerate *)
 (** This lives in this file for cyclic dependencies reasons. *)
 
-val iterator_enumerate_contains it (i: iterator it)
+val iterator_enumerate_contains it (i: iterator #it)
   : t_contains (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item)
-val iterator_enumerate_fold it (i: iterator it)
+val iterator_enumerate_fold it (i: iterator #it)
   : t_fold (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item) (iterator_enumerate_contains it i)
 val iterator_enumerate_enumerate it
   : t_enumerate (Core.Iter.Adapters.Enumerate.t_Enumerate it)
-val iterator_enumerate_all it (i: iterator it)
+val iterator_enumerate_all it (i: iterator #it)
   : t_all (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item)
 val iterator_enumerate_step_by it
   : t_step_by (Core.Iter.Adapters.Enumerate.t_Enumerate it)
 
-instance iterator_enumerate it {| i: iterator it |}: iterator (Core.Iter.Adapters.Enumerate.t_Enumerate it) = 
+instance iterator_enumerate it {| i: iterator #it |}: iterator #(Core.Iter.Adapters.Enumerate.t_Enumerate it) = 
   let open Core.Iter.Adapters.Enumerate in
   {
     f_Item = (usize * i.f_Item);
@@ -43,20 +43,20 @@ instance iterator_enumerate it {| i: iterator it |}: iterator (Core.Iter.Adapter
 (**** Step_by *)
 (** This lives in this file for cyclic dependencies reasons. *)
 
-val iterator_step_by_contains it (i: iterator it)
+val iterator_step_by_contains it (i: iterator #it)
   : t_contains (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
-val iterator_step_by_fold it (i: iterator it)
+val iterator_step_by_fold it (i: iterator #it)
   : t_fold (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item (iterator_step_by_contains it i)
-val iterator_step_by_next it (i: iterator it)
+val iterator_step_by_next it (i: iterator #it)
   : t_next (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
 val iterator_step_by_enumerate it
   : t_enumerate (Core.Iter.Adapters.Step_by.t_StepBy it)
-val iterator_step_by_all it (i: iterator it)
+val iterator_step_by_all it (i: iterator #it)
   : t_all (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
 val iterator_step_by_step_by it
   : t_step_by (Core.Iter.Adapters.Step_by.t_StepBy it)
 
-unfold instance iterator_step_by it {| i: iterator it |}: iterator (Core.Iter.Adapters.Step_by.t_StepBy it) = 
+unfold instance iterator_step_by it {| i: iterator #it |}: iterator #(Core.Iter.Adapters.Step_by.t_StepBy it) = 
   let open Core.Iter.Adapters.Enumerate in
   {
     f_Item = i.f_Item;
@@ -81,7 +81,7 @@ val iterator_slice_enumerate (t: eqtype): t_enumerate (t_Slice t)
 val iterator_slice_step_by (t: eqtype): t_step_by (t_Slice t)
 val iterator_slice_all (t: eqtype): t_all (t_Slice t) t
 
-instance iterator_slice (t: eqtype): iterator (t_Slice t) = {
+instance iterator_slice (t: eqtype): iterator #(t_Slice t) = {
   f_Item = t;
   f_next = iterator_slice_next t;
   // size_hint = (fun s -> Some (Rust_primitives.Arrays.length s));
@@ -103,7 +103,7 @@ val iterator_array_enumerate (t: eqtype) len: t_enumerate (t_Array t len)
 val iterator_array_step_by (t: eqtype) len: t_step_by (t_Array t len)
 val iterator_array_all (t: eqtype) len: t_all (t_Array t len) t
 
-instance iterator_array (t: eqtype) len: iterator (t_Array t len) = {
+instance iterator_array (t: eqtype) len: iterator #(t_Array t len) = {
   f_Item = t;
   f_next = iterator_array_next t len;
   // size_hint = (fun (_s: t_Array t len) -> Some len);
diff --git a/proof-libs/fstar/core/Core.Marker.fst b/proof-libs/fstar/core/Core.Marker.fst
index dcf5440fc..9378123df 100644
--- a/proof-libs/fstar/core/Core.Marker.fst
+++ b/proof-libs/fstar/core/Core.Marker.fst
@@ -1,19 +1,19 @@
 module Core.Marker
 
-class t_Sized (h: Type) = {
+class t_Sized (#h: Type) = {
   dummy_field: unit
 }
 
 (** we consider everything to be sized *)
-instance t_Sized_all t: t_Sized t = {
+instance t_Sized_all t: t_Sized #t = {
   dummy_field = ()
 }
 
-class t_Copy (h: Type) = {
+class t_Copy (#h: Type) = {
   dummy_copy_field: unit
 }
 
 (** we consider everything to be copyable *)
-instance t_Copy_all t: t_Copy t = {
+instance t_Copy_all t: t_Copy #t = {
   dummy_copy_field = ()
 }
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 12de64b69..158c7f8d2 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -47,50 +47,50 @@ val impl__usize__leading_zeros: usize -> u32
 
 open Core.Ops.Arith
 unfold instance add_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
-  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
+  : t_AddAssign #(x: int_t t {phi1 x}) #(y: int_t t {phi2 y}) = {
     f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x +. y));
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num_lhs_refined t ($phi1: int_t t -> bool)
-  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t) = {
+  : t_AddAssign #(x: int_t t {phi1 x}) #(y: int_t t) = {
     f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x +. y));
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num_rhs_refined t ($phi1: int_t t -> bool)
-  : t_AddAssign (x: int_t t) (y: int_t t {phi1 y}) = {
+  : t_AddAssign #(x: int_t t) #(y: int_t t {phi1 y}) = {
     f_add_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num t
-  : t_AddAssign (x: int_t t) (y: int_t t) = {
+  : t_AddAssign #(x: int_t t) #(y: int_t t) = {
     f_add_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 
 unfold instance sub_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
-  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
+  : t_SubAssign #(x: int_t t {phi1 x}) #(y: int_t t {phi2 y}) = {
     f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x -. y));
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num_lhs_refined t ($phi1: int_t t -> bool)
-  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t) = {
+  : t_SubAssign #(x: int_t t {phi1 x}) #(y: int_t t) = {
     f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x -. y));
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num_rhs_refined t ($phi1: int_t t -> bool)
-  : t_SubAssign (x: int_t t) (y: int_t t {phi1 y}) = {
+  : t_SubAssign #(x: int_t t) #(y: int_t t {phi1 y}) = {
     f_sub_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num t
-  : t_SubAssign (x: int_t t) (y: int_t t) = {
+  : t_SubAssign #(x: int_t t) #(y: int_t t) = {
     f_sub_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
diff --git a/proof-libs/fstar/core/Core.Ops.Arith.fsti b/proof-libs/fstar/core/Core.Ops.Arith.fsti
index a3d75535f..20e37f0c7 100644
--- a/proof-libs/fstar/core/Core.Ops.Arith.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Arith.fsti
@@ -2,7 +2,7 @@ module Core.Ops.Arith
 open Rust_primitives
 
 
-class t_Add self rhs = {
+class t_Add #self #rhs = {
    [@@@ Tactics.Typeclasses.no_method]
    f_Output: Type;
    f_add_pre: self -> rhs -> bool;
@@ -10,7 +10,7 @@ class t_Add self rhs = {
    f_add: x:self -> y:rhs -> Pure f_Output (f_add_pre x y) (fun r -> f_add_post x y r);
 }
 
-class t_Sub self rhs = {
+class t_Sub #self #rhs = {
    [@@@ Tactics.Typeclasses.no_method]
    f_Output: Type;
    f_sub_pre: self -> rhs -> bool;
@@ -18,7 +18,7 @@ class t_Sub self rhs = {
    f_sub: x:self -> y:rhs -> Pure f_Output (f_sub_pre x y) (fun r -> f_sub_post x y r);
 }
 
-class t_Mul self rhs = {
+class t_Mul #self #rhs = {
    [@@@ Tactics.Typeclasses.no_method]
    f_Output: Type;
    f_mul_pre: self -> rhs -> bool;
@@ -26,7 +26,7 @@ class t_Mul self rhs = {
    f_mul: x:self -> y:rhs -> Pure f_Output (f_mul_pre x y) (fun r -> f_mul_post x y r);
 }
 
-class t_Div self rhs = {
+class t_Div #self #rhs = {
    [@@@ Tactics.Typeclasses.no_method]
    f_Output: Type;
    f_div_pre: self -> rhs -> bool;
@@ -34,13 +34,13 @@ class t_Div self rhs = {
    f_div: x:self -> y:rhs -> Pure f_Output (f_div_pre x y) (fun r -> f_div_post x y r);
 }
 
-class t_AddAssign self rhs = {
+class t_AddAssign #self #rhs = {
   f_add_assign_pre: self -> rhs -> bool;
   f_add_assign_post: self -> rhs -> self -> bool;
   f_add_assign: x:self -> y:rhs -> Pure self (f_add_assign_pre x y) (fun r -> f_add_assign_post x y r);
 }
 
-class t_SubAssign self rhs = {
+class t_SubAssign #self #rhs = {
   f_sub_assign_pre: self -> rhs -> bool;
   f_sub_assign_post: self -> rhs -> self -> bool;
   f_sub_assign: x:self -> y:rhs -> Pure self (f_sub_assign_pre x y) (fun r -> f_sub_assign_post x y r);
diff --git a/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst b/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
index a0b61d5ee..5f047668b 100644
--- a/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
+++ b/proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst
@@ -1,13 +1,13 @@
 module Core.Ops.Index.IndexMut
 
-class t_IndexMut t_Self t_Idx = {
+class t_IndexMut #t_Self #t_Idx = {
   f_Input: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index_mut: s:t_Self -> i:t_Idx{in_range s i} -> v:f_Input -> t_Self;
 }
 
 open Rust_primitives
-instance impl__index_mut t l n: t_IndexMut (t_Array t l) (int_t n)
+instance impl__index_mut t l n: t_IndexMut #(t_Array t l) #(int_t n)
   = { f_Input = t;
       in_range = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
       f_index_mut = (fun s i x -> Seq.upd s (v i) x);
diff --git a/proof-libs/fstar/core/Core.Ops.Index.fst b/proof-libs/fstar/core/Core.Ops.Index.fst
index 9fe2f6b82..f2c3a6653 100644
--- a/proof-libs/fstar/core/Core.Ops.Index.fst
+++ b/proof-libs/fstar/core/Core.Ops.Index.fst
@@ -1,6 +1,6 @@
 module Core.Ops.Index
 
-class t_Index t_Self t_Idx = {
+class t_Index #t_Self #t_Idx = {
   f_Output: Type0;
   f_index_pre: s:t_Self -> i:t_Idx -> Type0;
   f_index_post: s:t_Self -> i:t_Idx -> f_Output -> Type0;
diff --git a/proof-libs/fstar/core/Core.Ops.Range.fsti b/proof-libs/fstar/core/Core.Ops.Range.fsti
index fffe32635..75e95086e 100644
--- a/proof-libs/fstar/core/Core.Ops.Range.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Range.fsti
@@ -20,7 +20,7 @@ val iterator_range_enumerate t: t_enumerate (t_Range (Rust_primitives.int_t t))
 val iterator_range_step_by t: t_step_by (t_Range (Rust_primitives.int_t t))
 val iterator_range_all t: t_all (t_Range (Rust_primitives.int_t t)) (Rust_primitives.int_t t)
 
-instance iterator_range t: iterator (t_Range (Rust_primitives.int_t t)) = 
+instance iterator_range t: iterator #(t_Range (Rust_primitives.int_t t)) = 
   { f_Item = Rust_primitives.int_t t;
     f_next = (fun {f_start; f_end} -> 
        if f_start >=. f_end then ({f_start; f_end}, None)
@@ -36,7 +36,7 @@ instance iterator_range t: iterator (t_Range (Rust_primitives.int_t t)) =
 
 open Core.Ops.Index
 
-instance impl_index_range_slice t n : t_Index (t_Slice t) (t_Range (int_t n)) 
+instance impl_index_range_slice t n : t_Index #(t_Slice t) #(t_Range (int_t n)) 
   = { f_Output = t_Slice t
     ; f_index_post = (fun _ _ _ -> true)
     ; f_index_pre = (fun (s: t_Slice t) {f_start; f_end} -> 
@@ -46,14 +46,14 @@ instance impl_index_range_slice t n : t_Index (t_Slice t) (t_Range (int_t n))
           if f_start <. f_end then Seq.slice s (v f_start) (v f_end)
                               else Seq.empty)}
 
-instance impl_index_range_to_slice t n : t_Index (t_Slice t) (t_RangeTo (int_t n)) 
+instance impl_index_range_to_slice t n : t_Index #(t_Slice t) #(t_RangeTo (int_t n)) 
   = { f_Output = t_Slice t
     ; f_index_post = (fun _ _ _ -> true)
     ; f_index_pre = (fun (s: t_Slice t) ({f_end}: t_RangeTo (int_t n)) -> 
          let len = Rust_primitives.length s in v f_end <= v len)
     ; f_index = (fun s {f_end} -> if 0 < v f_end then Seq.slice s 0 (v f_end) else Seq.empty)}
 
-instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (int_t n)) 
+instance impl_index_range_from_slice t n : t_Index #(t_Slice t) #(t_RangeFrom (int_t n)) 
   = { f_Output = t_Slice t
     ; f_index_post = (fun _ _ _ -> true)
     ; f_index_pre = (fun (s: t_Slice t) ({f_start}: t_RangeFrom (int_t n)) -> 
@@ -62,34 +62,34 @@ instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (int
          let len = Rust_primitives.length s in
          if v f_start = v len then Seq.empty else Seq.slice s (v f_start) (v len))}
          
-instance impl_index_range_full_slice t : t_Index (t_Slice t) t_RangeFull
+instance impl_index_range_full_slice t : t_Index #(t_Slice t) #t_RangeFull
   = { f_Output = t_Slice t
     ; f_index_post = (fun _ _ _ -> true)
     ; f_index_pre = (fun (s: t_Slice t) _ -> True)
     ; f_index = (fun s _ -> s)}
 
-instance impl_range_index_array t len n : t_Index (t_Array t len) (t_Range (int_t n)) = 
+instance impl_range_index_array t len n : t_Index #(t_Array t len) #(t_Range (int_t n)) = 
   let i = impl_index_range_slice t n in
   { f_Output = i.f_Output
   ; f_index_post = (fun _ _ _ -> true)
   ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
   
-instance impl_range_to_index_array t len n : t_Index (t_Array t len) (t_RangeTo (int_t n)) = 
+instance impl_range_to_index_array t len n : t_Index #(t_Array t len) #(t_RangeTo (int_t n)) = 
   let i = impl_index_range_to_slice t n in
   { f_Output = i.f_Output
   ; f_index_post = (fun _ _ _ -> true)
   ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
-instance impl_range_from_index_array t len n : t_Index (t_Array t len) (t_RangeFrom (int_t n)) = 
+instance impl_range_from_index_array t len n : t_Index #(t_Array t len) #(t_RangeFrom (int_t n)) = 
   let i = impl_index_range_from_slice t n in
   { f_Output = i.f_Output
   ; f_index_post = (fun _ _ _ -> true)
   ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
-instance impl_range_full_index_array t len : t_Index (t_Array t len) t_RangeFull = 
+instance impl_range_full_index_array t len : t_Index #(t_Array t len) #t_RangeFull = 
   let i = impl_index_range_full_slice t in
   { f_Output = i.f_Output
   ; f_index_post = (fun _ _ _ -> true)
@@ -98,13 +98,13 @@ instance impl_range_full_index_array t len : t_Index (t_Array t len) t_RangeFull
 
 open Rust_primitives.Hax
 
-let update_at_tc_array_range_super t l n: t_Index (t_Array t l) (t_Range (int_t n))
+let update_at_tc_array_range_super t l n: t_Index #(t_Array t l) #(t_Range (int_t n))
   = FStar.Tactics.Typeclasses.solve
-let update_at_tc_array_range_to_super t l n: t_Index (t_Array t l) (t_RangeTo (int_t n))
+let update_at_tc_array_range_to_super t l n: t_Index #(t_Array t l) #(t_RangeTo (int_t n))
   = FStar.Tactics.Typeclasses.solve
-let update_at_tc_array_range_from_super t l n: t_Index (t_Array t l) (t_RangeFrom (int_t n))
+let update_at_tc_array_range_from_super t l n: t_Index #(t_Array t l) #(t_RangeFrom (int_t n))
   = FStar.Tactics.Typeclasses.solve
-let update_at_tc_array_range_full_super t l: t_Index (t_Array t l) t_RangeFull
+let update_at_tc_array_range_full_super t l: t_Index #(t_Array t l) #t_RangeFull
   = FStar.Tactics.Typeclasses.solve
 
 val update_at_array_range t l n
@@ -120,19 +120,19 @@ val update_at_array_range_full t l
   (s: t_Array t l) (i: t_RangeFull)
   : (update_at_tc_array_range_full_super t l).f_Output -> t_Array t l
 
-instance update_at_tc_array_range t l n: update_at_tc (t_Array t l) (t_Range (int_t n)) = {
+instance update_at_tc_array_range t l n: update_at_tc #(t_Array t l) #(t_Range (int_t n)) = {
   super_index = update_at_tc_array_range_super t l n;
   update_at = update_at_array_range t l n
 }
-instance update_at_tc_array_range_to t l n: update_at_tc (t_Array t l) (t_RangeTo (int_t n)) = {
+instance update_at_tc_array_range_to t l n: update_at_tc #(t_Array t l) #(t_RangeTo (int_t n)) = {
   super_index = update_at_tc_array_range_to_super t l n;
   update_at = update_at_array_range_to t l n
 }
-instance update_at_tc_array_range_from t l n: update_at_tc (t_Array t l) (t_RangeFrom (int_t n)) = {
+instance update_at_tc_array_range_from t l n: update_at_tc #(t_Array t l) #(t_RangeFrom (int_t n)) = {
   super_index = update_at_tc_array_range_from_super t l n;
   update_at = update_at_array_range_from t l n
 }
-instance update_at_tc_array_range_full t l: update_at_tc (t_Array t l) t_RangeFull = {
+instance update_at_tc_array_range_full t l: update_at_tc #(t_Array t l) #t_RangeFull = {
   super_index = update_at_tc_array_range_full_super t l;
   update_at = update_at_array_range_full t l
 }
diff --git a/proof-libs/fstar/core/Core.Ops.Try_trait.fst b/proof-libs/fstar/core/Core.Ops.Try_trait.fst
index 7c167e603..a240164ed 100644
--- a/proof-libs/fstar/core/Core.Ops.Try_trait.fst
+++ b/proof-libs/fstar/core/Core.Ops.Try_trait.fst
@@ -1,14 +1,14 @@
 module Core.Ops.Try_trait
 
-class t_FromResidual self r = {
+class t_FromResidual #self #r = {
    f_from_residual: r -> self;
 }
 
-class t_Try self = {
+class t_Try #self = {
    f_Output: Type0;
    f_Residual: Type0;
    [@@@FStar.Tactics.Typeclasses.tcresolve]
-   parent_FromResidual: t_FromResidual f_Residual f_Residual;
+   parent_FromResidual: t_FromResidual #f_Residual #f_Residual;
 
    f_from_output: f_Output -> self;
    f_branch: self -> Core.Ops.Control_flow.t_ControlFlow f_Residual f_Output;
diff --git a/proof-libs/fstar/core/Core.Ops.fst b/proof-libs/fstar/core/Core.Ops.fst
index 3d72f9e7b..7ecaeae8f 100644
--- a/proof-libs/fstar/core/Core.Ops.fst
+++ b/proof-libs/fstar/core/Core.Ops.fst
@@ -7,21 +7,21 @@ open Rust_primitives
 //   ( +! ): x:self -> y:rhs {in_bounds x y} -> output;
 // }
 
-class negation_tc self = {
+class negation_tc #self = {
   ( ~. ): self -> self;
 }
 
-instance negation_for_integers #t: negation_tc (int_t t) = {
+instance negation_for_integers #t: negation_tc #(int_t t) = {
   ( ~. ) = fun x -> lognot x
 }
 
-instance negation_for_bool: negation_tc bool = {
+instance negation_for_bool: negation_tc #bool = {
   ( ~. ) = not
 }
 
 open Core.Ops.Index
 
-let ( .[] ) #self #idx {| inst: t_Index self idx |}
+let ( .[] ) #self #idx {| inst: t_Index #self #idx |}
   (s:self) (i:idx{f_index_pre s i}): inst.f_Output
   = f_index s i
 
diff --git a/proof-libs/fstar/core/Core.Slice.fsti b/proof-libs/fstar/core/Core.Slice.fsti
index 4277d412f..2f7b0edf4 100644
--- a/proof-libs/fstar/core/Core.Slice.fsti
+++ b/proof-libs/fstar/core/Core.Slice.fsti
@@ -19,7 +19,7 @@ val impl__chunks_exact #a (x: t_Slice a) (cs: usize):
 
 open Core.Ops.Index
 
-instance impl__index t n: t_Index (t_Slice t) (int_t n)
+instance impl__index t n: t_Index #(t_Slice t) #(int_t n)
   = { f_Output = t;
       f_index_pre = (fun (s: t_Slice t) (i: int_t n) -> v i >= 0 && v i < v (length s));
       f_index_post = (fun _ _ _ -> true);
diff --git a/proof-libs/fstar/core/Rand_core.fsti b/proof-libs/fstar/core/Rand_core.fsti
index 60f53bb75..606458ee6 100644
--- a/proof-libs/fstar/core/Rand_core.fsti
+++ b/proof-libs/fstar/core/Rand_core.fsti
@@ -1,12 +1,12 @@
 module Rand_core
 open Rust_primitives
 
-class t_RngCore (t_Self: Type0) = {
+class t_RngCore (#t_Self: Type0) = {
   f_next_u32: t_Self -> t_Self & u32;
   f_next_u64: t_Self -> t_Self & u64;
   f_fill_bytes: t_Self -> x:t_Slice u8 -> t_Self & (y:t_Slice u8{Seq.length x == Seq.length y})
 }
 
-class t_CryptoRng (t_Self: Type0) = {
+class t_CryptoRng (#t_Self: Type0) = {
   marker_trait: unit
 }
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index 2ae166f32..af3592993 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -10,9 +10,9 @@ let repeat #a (x: a) (len: usize): t_Array a len =
   FStar.Seq.create (v len) x
 
 open Core.Ops.Index
-class update_at_tc self idx = {
+class update_at_tc #self #idx = {
   [@@@FStar.Tactics.Typeclasses.tcinstance]
-  super_index: t_Index self idx;
+  super_index: t_Index #self #idx;
   update_at: s: self -> i: idx {f_index_pre s i} -> super_index.f_Output -> self;
 }
 
@@ -21,7 +21,7 @@ open Core.Slice
 /// We have an instance for `int_t n`, but we often work with refined
 /// `int_t n`, and F* typeclass inference doesn't support subtyping
 /// well, hence the instance below.
-instance impl__index_refined t l n r: t_Index (t_Array t l) (x: int_t n {r x})
+instance impl__index_refined t l n r: t_Index #(t_Array t l) #(x: int_t n {r x})
   = { f_Output = t;
       f_index_pre = (fun (s: t_Array t l) (i: int_t n {r i}) -> v i >= 0 && v i < v l);
       f_index_post = (fun _ _ _ -> true);
@@ -30,24 +30,24 @@ instance impl__index_refined t l n r: t_Index (t_Array t l) (x: int_t n {r x})
 
 /// Similarly to `impl__index_refined`, we need to define a instance
 /// for refined `int_t n`.
-instance update_at_tc_array_refined t l n r: update_at_tc (t_Array t l) (x: int_t n {r x}) = {
+instance update_at_tc_array_refined t l n r: update_at_tc #(t_Array t l) #(x: int_t n {r x}) = {
   super_index = impl__index_refined t l n r;
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
-instance impl__index t l n: t_Index (t_Array t l) (int_t n)
+instance impl__index t l n: t_Index #(t_Array t l) #(int_t n)
   = { f_Output = t;
       f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
       f_index_post = (fun _ _ _ -> true);
       f_index = (fun s i -> Seq.index s (v i));
     }
 
-instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
-  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (int_t n);
+instance update_at_tc_array t l n: update_at_tc #(t_Array t l) #(int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index #(t_Array t l) #(int_t n);
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
-let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i})
+let (.[]<-) #self #idx {| update_at_tc #self #idx |} (s: self) (i: idx {f_index_pre s i})
   = update_at s i
 
 let array_of_list (#t:Type)
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.fst
index d80eabfde..fdcb994b1 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.fst
@@ -26,21 +26,21 @@ let (let!)
     | Core.Ops.Control_flow.ControlFlow_Continue v -> f v
     | Core.Ops.Control_flow.ControlFlow_Break b -> Core.Ops.Control_flow.ControlFlow_Break b
 
-class cast_tc a b = {
+class cast_tc #a #b = {
   cast: a -> b; 
 }
 
 /// Rust's casts operations on integers are non-panicking
 instance cast_tc_integers (t:inttype) (t':inttype)
-  : cast_tc (int_t t) (int_t t')
+  : cast_tc #(int_t t) #(int_t t')
   = { cast = (fun x -> Rust_primitives.Integers.cast_mod #t #t' x) }
 
-class unsize_tc source = {
+class unsize_tc #source = {
   output: Type;
   unsize: source -> output;
 }
 
-instance array_to_slice_unsize t n: unsize_tc (t_Array t n) = {
+instance array_to_slice_unsize t n: unsize_tc #(t_Array t n) = {
   output = (x:t_Slice t{Seq.length x == v n});
   unsize = (fun (arr: t_Array t n) -> 
             arr <: t_Slice t);