diff --git a/charon-pin b/charon-pin
index c1cd41666..97588401c 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-ba7db7e30304485e74d9e529da808403f7d72492
+85a1ee1cdfe1d7f2672bece3d190425e1f06c881
diff --git a/flake.lock b/flake.lock
index 50479234c..a3160280f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1765477492,
-        "narHash": "sha256-mHpKN2K7nxkQ94Oe9161mHR1vcXFJhxYQ+wngujiceA=",
+        "lastModified": 1765803402,
+        "narHash": "sha256-vyKAcVlq5UURJNT4Zt1cxdS/TEWHPXcX6FsVkcJF0VI=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "ba7db7e30304485e74d9e529da808403f7d72492",
+        "rev": "85a1ee1cdfe1d7f2672bece3d190425e1f06c881",
         "type": "github"
       },
       "original": {
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index 4afae7583..93727cd05 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -189,7 +189,7 @@ let update_array_default (crate : crate) : crate =
                   in
                   let generics =
                     {
-                      sg.generics with
+                      fdecl.generics with
                       const_generics =
                         [ { index = cg_id; name = "N"; ty = TUInt Usize } ];
                     }
@@ -197,12 +197,11 @@ let update_array_default (crate : crate) : crate =
                   let sg =
                     {
                       sg with
-                      generics;
                       output =
                         TAdt { id = TBuiltin TArray; generics = array_generics };
                     }
                   in
-                  let fdecl = { fdecl with signature = sg } in
+                  let fdecl = { fdecl with signature = sg; generics } in
                   Some fdecl
               | _ -> [%internal_error] fdecl.item_meta.span)
             else (* Filter *)
diff --git a/src/Translate.ml b/src/Translate.ml
index cb8443245..071a28d61 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -355,7 +355,7 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
       (fun (info : builtin_fun_info) ->
         SymbolicToPureTypes.translate_fun_sig trans_ctx (FBuiltin info.fun_id)
           info.name info.fun_sig
-          (List.map (fun _ -> None) info.fun_sig.inputs))
+          (List.map (fun _ -> None) info.fun_sig.item_binder_value.inputs))
       builtin_fun_infos
   in
 
diff --git a/src/interp/Interp.ml b/src/interp/Interp.ml
index b4d335935..7b4a56a8f 100644
--- a/src/interp/Interp.ml
+++ b/src/interp/Interp.ml
@@ -121,11 +121,12 @@ let compute_contexts (crate : crate) : decls_ctx =
     We return a new context because we compute and add the type normalization
     map in the same step. *)
 let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
-    (sg : fun_sig) (regions_hierarchy : region_var_groups) (_kind : item_source)
-    : eval_ctx * inst_fun_sig =
+    (sg : bound_fun_sig) (regions_hierarchy : region_var_groups)
+    (_kind : item_source) : eval_ctx * inst_fun_sig =
   let tr_self = UnknownTrait "symbolic_instantiate_fun_sig" in
   let generics =
-    Substitute.generic_args_of_params_erase_regions (Some span) sg.generics
+    Substitute.generic_args_of_params_erase_regions (Some span)
+      sg.item_binder_params
   in
   let inst_sg =
     instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy
@@ -177,15 +178,16 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx)
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx (Some span) ctx region_groups sg.generics.types
-      sg.generics.const_generics marked_ids
+    initialize_eval_ctx (Some span) ctx region_groups fdef.generics.types
+      fdef.generics.const_generics marked_ids
   in
   (* Instantiate the signature. This updates the context because we compute
      at the same time the normalization map for the associated types.
   *)
   let ctx, inst_sg =
-    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
-      fdef.src
+    symbolic_instantiate_fun_sig span ctx
+      (bound_fun_sig_of_decl fdef)
+      regions_hierarchy fdef.src
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
@@ -268,8 +270,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let _, ret_inst_sg =
-    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
-      fdef.src
+    symbolic_instantiate_fun_sig span ctx
+      (bound_fun_sig_of_decl fdef)
+      regions_hierarchy fdef.src
   in
   let ret_rty = ret_inst_sg.output in
 
@@ -486,7 +489,7 @@ module Test = struct
         fdef.item_meta.name];
 
     (* Sanity check - *)
-    [%sanity_check] span (fdef.signature.generics = empty_generic_params);
+    [%sanity_check] span (fdef.generics = empty_generic_params);
     [%sanity_check] span (body.locals.arg_count = 0);
 
     (* Create the evaluation context *)
@@ -521,7 +524,7 @@ module Test = struct
       (no parameters, no arguments) - TODO: move *)
   let fun_decl_is_transparent_unit (def : fun_decl) : bool =
     Option.is_some def.body
-    && def.signature.generics = empty_generic_params
+    && def.generics = empty_generic_params
     && def.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)
diff --git a/src/interp/InterpBorrowsCore.ml b/src/interp/InterpBorrowsCore.ml
index 477a2d738..7a4909810 100644
--- a/src/interp/InterpBorrowsCore.ml
+++ b/src/interp/InterpBorrowsCore.ml
@@ -1820,16 +1820,26 @@ let rec norm_proj_tys_union (span : Meta.span) (ty1 : rty) (ty2 : rty) : rty =
       [%sanity_check] span (item1 = item2);
       TTraitType (norm_proj_trait_refs_union span tr1 tr2, item1)
   | ( TFnPtr
-        { binder_regions = binder_regions1; binder_value = inputs1, output1 },
+        {
+          binder_regions = binder_regions1;
+          binder_value =
+            { is_unsafe = false; inputs = inputs1; output = output1 };
+        },
       TFnPtr
-        { binder_regions = binder_regions2; binder_value = inputs2, output2 } )
-    ->
+        {
+          binder_regions = binder_regions2;
+          binder_value =
+            { is_unsafe = false; inputs = inputs2; output = output2 };
+        } ) ->
       (* TODO: general case *)
       [%sanity_check] span (binder_regions1 = []);
       [%sanity_check] span (binder_regions2 = []);
       let binder_value =
-        ( List.map2 (norm_proj_tys_union span) inputs1 inputs2,
-          norm_proj_tys_union span output1 output2 )
+        {
+          is_unsafe = false;
+          inputs = List.map2 (norm_proj_tys_union span) inputs1 inputs2;
+          output = norm_proj_tys_union span output1 output2;
+        }
       in
       TFnPtr { binder_regions = []; binder_value }
   | _ -> [%internal_error] span
diff --git a/src/interp/InterpStatements.ml b/src/interp/InterpStatements.ml
index 877258c7e..a9c82ee91 100644
--- a/src/interp/InterpStatements.ml
+++ b/src/interp/InterpStatements.ml
@@ -274,8 +274,8 @@ let get_builtin_function_return_type (span : Meta.span) (fid : builtin_fun_id)
   let sg = Builtin.get_builtin_fun_sig fid in
   (* Instantiate the return type  *)
   let generics = Subst.generic_args_erase_regions generics in
-  let subst = Subst.make_subst_from_generics sg.generics generics in
-  Subst.erase_regions_substitute_types subst sg.output
+  let subst = Subst.make_subst_from_generics sg.item_binder_params generics in
+  Subst.erase_regions_substitute_types subst sg.item_binder_value.output
 
 let move_return_value (config : config) (span : Meta.span)
     (pop_return_value : bool) (ctx : eval_ctx) :
@@ -659,11 +659,12 @@ let eval_non_builtin_function_call_symbolic_inst (span : Meta.span)
       in
       (* Lookup the declaration *)
       let def = ctx_lookup_fun_decl span ctx fid in
+      let signature = bound_fun_sig_of_decl def in
       [%ltrace
         "- call: " ^ call_to_string ctx call ^ "\n- call.generics:\n"
         ^ generic_args_to_string ctx func.generics
         ^ "\n- def.signature:\n"
-        ^ fun_sig_to_string ctx def.signature];
+        ^ fun_sig_to_string ctx signature];
       (* Instantiate *)
       let regions_hierarchy =
         [%silent_unwrap] span
@@ -671,7 +672,7 @@ let eval_non_builtin_function_call_symbolic_inst (span : Meta.span)
              ctx.fun_ctx.regions_hierarchies)
       in
       let inst_sg =
-        instantiate_fun_sig span ctx generics tr_self def.signature
+        instantiate_fun_sig span ctx generics tr_self signature
           regions_hierarchy
       in
       (func.kind, func.generics, def, inst_sg)
@@ -1321,9 +1322,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
       (* TODO: we need to normalize the types if we want to correctly support traits *)
       [%cassert] body.span (generics.trait_refs = [])
         "Traits are not supported yet in concrete mode";
-      let subst =
-        Subst.make_subst_from_generics def.signature.generics generics
-      in
+      let subst = Subst.make_subst_from_generics def.generics generics in
       let locals, body_st = Subst.fun_body_substitute_in_body subst body in
 
       (* Evaluate the input operands *)
@@ -1608,7 +1607,7 @@ and eval_builtin_function_call_symbolic (config : config) (span : Meta.span)
 
     (* Evaluate the function call *)
     eval_function_call_symbolic_from_inst_sig config span (FunId (FBuiltin fid))
-      sg inst_sig func.generics args dest ctx
+      sg.item_binder_value inst_sig func.generics args dest ctx
   end
   else begin
     (* Sanity check: make sure the type parameters don't contain regions -
@@ -1634,7 +1633,7 @@ and eval_builtin_function_call_symbolic (config : config) (span : Meta.span)
 
     (* Evaluate the function call *)
     eval_function_call_symbolic_from_inst_sig config span (FunId (FBuiltin fid))
-      sg inst_sig func.generics args dest ctx
+      sg.item_binder_value inst_sig func.generics args dest ctx
   end
 
 (** Evaluate a statement seen as a function body *)
diff --git a/src/interp/InterpUtils.ml b/src/interp/InterpUtils.ml
index 030057cbf..b5fbbffce 100644
--- a/src/interp/InterpUtils.ml
+++ b/src/interp/InterpUtils.ml
@@ -747,7 +747,7 @@ let initialize_eval_ctx (span : Meta.span option) (ctx : decls_ctx)
     region ids. This is mostly used in preparation of function calls (when
     evaluating in symbolic mode). *)
 let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
-    (generics : generic_args) (tr_self : trait_ref_kind) (sg : fun_sig)
+    (generics : generic_args) (tr_self : trait_ref_kind) (sg : bound_fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
   [%ldebug
     "- generics: "
@@ -769,20 +769,21 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
   in
   (* Generate fresh regions *)
   let rsubst =
-    Substitute.fresh_regions_with_substs_from_vars sg.generics.regions
+    Substitute.fresh_regions_with_substs_from_vars sg.item_binder_params.regions
       ctx.fresh_region_id
   in
   (* Generate the type substitution. *)
   [%sanity_check] span (TypesUtils.trait_instance_id_no_regions tr_self);
   let tsubst =
-    Substitute.make_type_subst_from_vars sg.generics.types generics.types
+    Substitute.make_type_subst_from_vars sg.item_binder_params.types
+      generics.types
   in
   let cgsubst =
-    Substitute.make_const_generic_subst_from_vars sg.generics.const_generics
-      generics.const_generics
+    Substitute.make_const_generic_subst_from_vars
+      sg.item_binder_params.const_generics generics.const_generics
   in
   let tr_subst =
-    Substitute.make_trait_subst_from_clauses sg.generics.trait_clauses
+    Substitute.make_trait_subst_from_clauses sg.item_binder_params.trait_clauses
       generics.trait_refs
   in
   (* Substitute the signature *)
@@ -808,7 +809,7 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
     (span : Meta.span option) (crate : crate) (fun_name : string)
     (type_vars : type_param list)
     (const_generic_vars : const_generic_param list)
-    (generic_args : generic_args) (sg : fun_sig) : inst_fun_sig =
+    (generic_args : generic_args) (sg : bound_fun_sig) : inst_fun_sig =
   (* We simply put everything into a "fake" signature, then call
      [compute_regions_hierarchy_for_sig].
 
@@ -816,7 +817,12 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
      the erased regions. When doing so, in order to make sure there are
      no collisions, we also refresh the other regions. *)
   (* Decompose the signature *)
-  let { is_unsafe; generics; inputs; output } = sg in
+  let {
+    item_binder_params = generics;
+    item_binder_value = { is_unsafe; inputs; output };
+  } =
+    sg
+  in
   (* Introduce the fresh regions *)
   let region_map = ref RegionId.Map.empty in
   let fresh_regions = ref RegionId.Set.empty in
@@ -872,7 +878,7 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
         (* Keeping the same trait refs: it shouldn't have an impact *);
       }
     in
-    Substitute.make_subst_from_generics sg.generics generic_args
+    Substitute.make_subst_from_generics sg.item_binder_params generic_args
   in
 
   (* Substitute the inputs and outputs *)
@@ -931,7 +937,12 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
       }
     in
 
-    let sg = { is_unsafe; generics; inputs; output } in
+    let sg =
+      {
+        item_binder_params = generics;
+        item_binder_value = { is_unsafe; inputs; output };
+      }
+    in
     let regions_hierarchy =
       RegionsHierarchy.compute_regions_hierarchy_for_sig span crate fun_name sg
     in
diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml
index dad632bef..117facd8b 100644
--- a/src/llbc/Builtin.ml
+++ b/src/llbc/Builtin.ml
@@ -85,11 +85,14 @@ module Sig = struct
   let mk_slice_ty (ty : ty) : ty =
     TAdt { id = TBuiltin TSlice; generics = mk_generic_args [] [ ty ] [] }
 
-  let mk_sig generics inputs output : fun_sig =
-    { is_unsafe = false; generics; inputs; output }
+  let mk_sig generics inputs output : bound_fun_sig =
+    {
+      item_binder_params = generics;
+      item_binder_value = { inputs; output; is_unsafe = false };
+    }
 
   (** [fn<T>(T) -> Box<T>] *)
-  let box_new_sig : fun_sig =
+  let box_new_sig : bound_fun_sig =
     let generics =
       mk_generic_params [] [ type_param_0 ] []
       (* <T> *)
@@ -102,7 +105,7 @@ module Sig = struct
     mk_sig generics inputs output
 
   (** [fn<T>(Box<T>) -> ()] *)
-  let box_free_sig : fun_sig =
+  let box_free_sig : bound_fun_sig =
     let generics =
       mk_generic_params [] [ type_param_0 ] []
       (* <T> *)
@@ -128,7 +131,7 @@ module Sig = struct
       a mutable borrow. *)
   let mk_array_slice_borrow_sig (cgs : const_generic_param list)
       (input_ty : ty -> ty) (index_ty : ty option) (output_ty : ty -> ty)
-      (is_mut : bool) : fun_sig =
+      (is_mut : bool) : bound_fun_sig =
     let generics =
       mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *)
     in
@@ -146,7 +149,8 @@ module Sig = struct
     in
     mk_sig generics inputs output
 
-  let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : fun_sig =
+  let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : bound_fun_sig
+      =
     (* Array<T, N> *)
     let input_ty ty =
       if is_array then mk_array_ty ty cgvar_0 else mk_slice_ty ty
@@ -161,7 +165,7 @@ module Sig = struct
   let array_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut
   let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut
 
-  let array_to_slice_sig (is_mut : bool) : fun_sig =
+  let array_to_slice_sig (is_mut : bool) : bound_fun_sig =
     (* Array<T, N> *)
     let input_ty ty = mk_array_ty ty cgvar_0 in
     (* Slice<T> *)
@@ -182,7 +186,7 @@ module Sig = struct
     mk_sig generics inputs output
 
   (** Helper: [fn<T>(&'a [T]) -> usize] *)
-  let slice_len_sig : fun_sig =
+  let slice_len_sig : bound_fun_sig =
     let generics =
       mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
     in
@@ -196,11 +200,12 @@ module Sig = struct
     mk_sig generics inputs output
 end
 
-type raw_builtin_fun_info = builtin_fun_id * fun_sig * bool * bool list option
+type raw_builtin_fun_info =
+  builtin_fun_id * bound_fun_sig * bool * bool list option
 
 type builtin_fun_info = {
   fun_id : builtin_fun_id;
-  fun_sig : fun_sig;
+  fun_sig : bound_fun_sig;
   can_fail : bool;
   name : string;
   keep_types : bool list option;
@@ -278,7 +283,7 @@ let get_builtin_fun_info (id : builtin_fun_id) : builtin_fun_info =
       raise
         (Failure ("get_builtin_fun_info: not found: " ^ show_builtin_fun_id id))
 
-let get_builtin_fun_sig (id : builtin_fun_id) : fun_sig =
+let get_builtin_fun_sig (id : builtin_fun_id) : bound_fun_sig =
   (get_builtin_fun_info id).fun_sig
 
 let get_builtin_fun_name (id : builtin_fun_id) : string =
diff --git a/src/llbc/LlbcAst.ml b/src/llbc/LlbcAst.ml
index cf76f35cd..9853fcb3f 100644
--- a/src/llbc/LlbcAst.ml
+++ b/src/llbc/LlbcAst.ml
@@ -2,6 +2,7 @@ open Types
 open Values
 include Charon.LlbcAst
 
+type bound_fun_sig = Charon.TypesUtils.bound_fun_sig
 type abs_region_group = (RegionId.id, AbsId.id) g_region_group [@@deriving show]
 type abs_region_groups = abs_region_group list [@@deriving show]
 
diff --git a/src/llbc/LlbcAstUtils.ml b/src/llbc/LlbcAstUtils.ml
index 924254bf4..a3ba97954 100644
--- a/src/llbc/LlbcAstUtils.ml
+++ b/src/llbc/LlbcAstUtils.ml
@@ -1,4 +1,5 @@
 open Types
+open TypesUtils
 open LlbcAst
 include Charon.LlbcAstUtils
 open Collections
@@ -16,9 +17,11 @@ module FunIdMap = Collections.MakeMap (FunIdOrderedType)
 module FunIdSet = Collections.MakeSet (FunIdOrderedType)
 
 let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
-    fun_sig =
+    bound_fun_sig =
   match fun_id with
-  | FRegular id -> (FunDeclId.Map.find id fun_decls).signature
+  | FRegular id ->
+      let fun_decl = FunDeclId.Map.find id fun_decls in
+      bound_fun_sig_of_decl fun_decl
   | FBuiltin aid -> Builtin.get_builtin_fun_sig aid
 
 (** Return the opaque declarations found in the crate, which are also *not
diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml
index d7f76f27d..d2c1ebd1c 100644
--- a/src/llbc/Print.ml
+++ b/src/llbc/Print.ml
@@ -5,6 +5,7 @@ open Charon.PrintTypes
 open Charon.PrintExpressions
 open Charon.PrintLlbcAst.Ast
 open Types
+open TypesUtils
 open Values
 open ValuesUtils
 open Expressions
@@ -1097,7 +1098,7 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     fun_decl_to_string env "" "  " f
 
-  let fun_sig_to_string (ctx : eval_ctx) (x : fun_sig) : string =
+  let fun_sig_to_string (ctx : eval_ctx) (x : bound_fun_sig) : string =
     let env = eval_ctx_to_fmt_env ctx in
     fun_sig_to_string env "" "  " x
 
diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml
index b85e5d619..b93a074e1 100644
--- a/src/llbc/RegionsHierarchy.ml
+++ b/src/llbc/RegionsHierarchy.ml
@@ -39,7 +39,7 @@ module Subst = Substitute
 let log = Logging.regions_hierarchy_log
 
 let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
-    (fun_name : string) (sg : fun_sig) : region_var_groups =
+    (fun_name : string) (sg : bound_fun_sig) : region_var_groups =
   [%ltrace fun_name];
   (* Create the dependency graph.
 
@@ -62,7 +62,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
     let m =
       List.map
         (fun (r : region_param) -> (RVar (Free r.index), s_set))
-        sg.generics.regions
+        sg.item_binder_params.regions
     in
     let s = (RStatic, RegionSet.empty) in
     ref (RegionMap.of_list (s :: m))
@@ -101,7 +101,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
      not the "type outlives" clauses *)
   List.iter
     (add_edges_from_region_binder add_edge_from_region_constraint)
-    sg.generics.regions_outlive;
+    sg.item_binder_params.regions_outlive;
 
   (* Explore the types in the signature to add the edges *)
   let rec explore_ty (outer : region list) (ty : ty) =
@@ -165,7 +165,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
           (binder.binder_regions = [])
           "We don't support arrow types with locally quantified regions";
         (* We can ignore the outer regions *)
-        let inputs, output = binder.binder_value in
+        let { Types.inputs; output; _ } = binder.binder_value in
         List.iter (explore_ty []) (output :: inputs)
     | TFnDef _ -> [%craise_opt_span] span "unsupported: FnDef"
     | TDynTrait _ ->
@@ -181,7 +181,8 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
 
   (* Substitute the regions in a type, then explore *)
   let explore_ty_subst ty = explore_ty [] ty in
-  List.iter explore_ty_subst (sg.output :: sg.inputs);
+  List.iter explore_ty_subst
+    (sg.item_binder_value.output :: sg.item_binder_value.inputs);
 
   (* Compute the ordered SCCs *)
   let module Scc = SCC.Make (RegionOrderedType) in
@@ -286,7 +287,7 @@ let compute_regions_hierarchies (crate : crate) : region_var_groups FunIdMap.t =
       (fun ((fid, d) : FunDeclId.id * fun_decl) ->
         ( FRegular fid,
           ( Types.name_to_string env d.item_meta.name,
-            d.signature,
+            bound_fun_sig_of_decl d,
             Some d.item_meta.span ) ))
       (FunDeclId.Map.bindings crate.fun_decls)
   in
diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml
index bfa9107a7..b4f81c3e3 100644
--- a/src/llbc/Substitute.ml
+++ b/src/llbc/Substitute.ml
@@ -2,6 +2,7 @@
     function bodies, etc. *)
 
 include Charon.Substitute
+open Charon.TypesUtils
 open Types
 open Values
 open LlbcAst
@@ -34,8 +35,9 @@ let substitute_signature (asubst : RegionGroupId.id -> AbsId.id)
     (r_id_subst : RegionId.id -> RegionId.id) (ty_sb_subst : TypeVarId.id -> ty)
     (cg_sb_subst : ConstGenericVarId.id -> const_generic)
     (tr_sb_subst : TraitClauseId.id -> trait_ref_kind)
-    (tr_sb_self : trait_ref_kind) (sg : fun_sig)
+    (tr_sb_self : trait_ref_kind) (sg : bound_fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
+  let { item_binder_params = generics; item_binder_value = sg } = sg in
   let r_sb_subst id = RVar (Free (r_id_subst id)) in
   let subst =
     subst_free_vars
@@ -63,7 +65,7 @@ let substitute_signature (asubst : RegionGroupId.id -> AbsId.id)
     List.map
       (st_substitute_visitor#visit_region_binder
          trait_type_constraint_substitute subst)
-      sg.generics.trait_type_constraints
+      generics.trait_type_constraints
   in
   {
     inputs;
diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml
index a269ad7a8..9517adc7e 100644
--- a/src/llbc/TypesAnalysis.ml
+++ b/src/llbc/TypesAnalysis.ml
@@ -371,7 +371,7 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
         (* Return *)
         { ty_info with mut_regions }
     | TFnPtr fn_sig ->
-        let inputs, output = fn_sig.binder_value in
+        let { Types.inputs; output; _ } = fn_sig.binder_value in
         (* Just dive into the arrow *)
         let ty_info =
           List.fold_left
diff --git a/src/pure/PureMicroPasses.ml b/src/pure/PureMicroPasses.ml
index f3698bb4c..bb308142a 100644
--- a/src/pure/PureMicroPasses.ml
+++ b/src/pure/PureMicroPasses.ml
@@ -7099,7 +7099,7 @@ let add_type_annotations_to_fun_decl (trans_ctx : trans_ctx)
                    be a way to translate these signatures earlier. *)
                 SymbolicToPureTypes.translate_fun_sig trans_ctx
                   (FRegular method_decl_id) method_name method_sig
-                  (List.map (fun _ -> None) method_sig.inputs)
+                  (List.map (fun _ -> None) method_sig.item_binder_value.inputs)
             | FunId (FBuiltin aid) ->
                 Builtin.BuiltinFunIdMap.find aid builtin_sigs
           in
diff --git a/src/symbolic/SymbolicToPureCore.ml b/src/symbolic/SymbolicToPureCore.ml
index 69081f7e6..5f7d242d9 100644
--- a/src/symbolic/SymbolicToPureCore.ml
+++ b/src/symbolic/SymbolicToPureCore.ml
@@ -300,7 +300,7 @@ type bs_ctx = {
 let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
   {
     crate = ctx.decls_ctx.crate;
-    generics = [ ctx.fun_decl.signature.generics ];
+    generics = [ ctx.fun_decl.generics ];
     locals = [];
   }
 
diff --git a/src/symbolic/SymbolicToPureExpressions.ml b/src/symbolic/SymbolicToPureExpressions.ml
index d33c2819f..a81a9975c 100644
--- a/src/symbolic/SymbolicToPureExpressions.ml
+++ b/src/symbolic/SymbolicToPureExpressions.ml
@@ -28,7 +28,6 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) : bs_ctx * fvar option list =
      for the backward functions. *)
   let back_var_names =
     let def_id = ctx.fun_decl.def_id in
-    let sg = ctx.fun_decl.signature in
     let regions_hierarchy =
       LlbcAstUtils.FunIdMap.find (FRegular def_id)
         ctx.fun_ctx.regions_hierarchies
@@ -38,7 +37,7 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) : bs_ctx * fvar option list =
         let rg = RegionGroupId.nth regions_hierarchy gid in
         let region_names =
           List.map
-            (fun rid -> (T.RegionId.nth sg.generics.regions rid).name)
+            (fun rid -> (T.RegionId.nth ctx.fun_decl.generics.regions rid).name)
             rg.regions
         in
         let name =
diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml
index 8af15a98e..99d32e24d 100644
--- a/src/symbolic/SymbolicToPureTypes.ml
+++ b/src/symbolic/SymbolicToPureTypes.ml
@@ -721,11 +721,12 @@ let translate_inst_fun_sig_to_decomposed_fun_type (span : Meta.span option)
 
 let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : span option)
     (decls_ctx : C.decls_ctx) (fun_id : A.fn_ptr_kind)
-    (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig)
+    (regions_hierarchy : T.region_var_groups) (sg : A.bound_fun_sig)
     (input_names : string option list) : decomposed_fun_sig =
   let inst_sg : LlbcAst.inst_fun_sig =
-    let ({ A.inputs; output; _ } : A.fun_sig) = sg in
-    [%sanity_check_opt_span] span (sg.generics.trait_type_constraints = []);
+    let ({ T.inputs; output; _ } : T.fun_sig) = sg.item_binder_value in
+    [%sanity_check_opt_span] span
+      (sg.item_binder_params.trait_type_constraints = []);
 
     let _, fresh_abs_id = V.AbsId.fresh_stateful_generator () in
     let region_gr_id_abs_id_list =
@@ -756,17 +757,17 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : span option)
   in
 
   (* Generic parameters *)
-  let generics, preds = translate_generic_params span sg.generics in
+  let generics, preds = translate_generic_params span sg.item_binder_params in
 
   let fun_ty =
     translate_inst_fun_sig_to_decomposed_fun_type span decls_ctx fun_id inst_sg
       input_names
   in
-  { generics; llbc_generics = sg.generics; preds; fun_ty }
+  { generics; llbc_generics = sg.item_binder_params; preds; fun_ty }
 
 let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
-    (fun_id : FunDeclId.id) (sg : A.fun_sig) (input_names : string option list)
-    : decomposed_fun_sig =
+    (fun_id : FunDeclId.id) (sg : A.bound_fun_sig)
+    (input_names : string option list) : decomposed_fun_sig =
   let span =
     ([%silent_unwrap_opt_span] None
        (FunDeclId.Map.find_opt fun_id decls_ctx.fun_ctx.fun_decls))
@@ -793,7 +794,8 @@ let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx)
           (LlbcAstUtils.fun_body_get_input_vars body)
   in
   let sg =
-    translate_fun_sig_to_decomposed decls_ctx fdef.def_id fdef.signature
+    translate_fun_sig_to_decomposed decls_ctx fdef.def_id
+      (bound_fun_sig_of_decl fdef)
       input_names
   in
   [%ltrace
@@ -894,8 +896,8 @@ let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig) : fun_sig
   }
 
 let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
-    (fun_name : string) (sg : A.fun_sig) (input_names : string option list) :
-    Pure.fun_sig =
+    (fun_name : string) (sg : A.bound_fun_sig)
+    (input_names : string option list) : Pure.fun_sig =
   (* Compute the regions hierarchy *)
   let regions_hierarchy =
     RegionsHierarchy.compute_regions_hierarchy_for_sig None decls_ctx.crate