From 83acae9a8399a2aeaed0105e27b0ac07b410827d Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Mon, 9 Sep 2024 11:18:46 +0200
Subject: [PATCH] Update the extraction

---
 compiler/AssociatedTypes.ml  |  31 ++--
 compiler/Assumed.ml          |  23 ++-
 compiler/Extract.ml          | 125 +++++++++++----
 compiler/ExtractBase.ml      |   1 +
 compiler/ExtractTypes.ml     | 109 +++++++------
 compiler/Interpreter.ml      |  12 +-
 compiler/InterpreterUtils.ml |  21 ++-
 compiler/Pure.ml             |  29 ++--
 compiler/PureUtils.ml        |   2 +
 compiler/RegionsHierarchy.ml |   2 +-
 compiler/SymbolicToPure.ml   | 299 ++++++++++++++++++++---------------
 compiler/Translate.ml        |  12 ++
 12 files changed, 420 insertions(+), 246 deletions(-)

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index c041aa032..593ef46d9 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -82,10 +82,11 @@ let compute_norm_trait_types_from_preds (span : Meta.span option)
   in
   TraitTypeRefMap.of_list rbindings
 
-let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
-    (trait_type_constraints : trait_type_constraint list) : eval_ctx =
+let ctx_add_norm_trait_types_from_preds (span : Meta.span option)
+    (ctx : eval_ctx) (trait_type_constraints : trait_type_constraint list) :
+    eval_ctx =
   let norm_trait_types =
-    compute_norm_trait_types_from_preds (Some span) trait_type_constraints
+    compute_norm_trait_types_from_preds span trait_type_constraints
   in
   { ctx with norm_trait_types }
 
@@ -417,9 +418,9 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
   let ty = norm_ctx_normalize_ty ctx ty in
   { trait_ref; type_name; ty }
 
-let mk_norm_ctx (span : Meta.span) (ctx : eval_ctx) : norm_ctx =
+let mk_norm_ctx (span : Meta.span option) (ctx : eval_ctx) : norm_ctx =
   {
-    span = Some span;
+    span;
     norm_trait_types = ctx.norm_trait_types;
     type_decls = ctx.type_ctx.type_decls;
     fun_decls = ctx.fun_ctx.fun_decls;
@@ -430,17 +431,17 @@ let mk_norm_ctx (span : Meta.span) (ctx : eval_ctx) : norm_ctx =
     const_generic_vars = ctx.const_generic_vars;
   }
 
-let ctx_normalize_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
+let ctx_normalize_ty (span : Meta.span option) (ctx : eval_ctx) (ty : ty) : ty =
   norm_ctx_normalize_ty (mk_norm_ctx span ctx) ty
 
 (** Normalize a type and erase the regions at the same time *)
 let ctx_normalize_erase_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
-  let ty = ctx_normalize_ty span ctx ty in
+  let ty = ctx_normalize_ty (Some span) ctx ty in
   Subst.erase_regions ty
 
 let ctx_normalize_trait_type_constraint (span : Meta.span) (ctx : eval_ctx)
     (ttc : trait_type_constraint) : trait_type_constraint =
-  norm_ctx_normalize_trait_type_constraint (mk_norm_ctx span ctx) ttc
+  norm_ctx_normalize_trait_type_constraint (mk_norm_ctx (Some span) ctx) ttc
 
 (** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *)
 let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
@@ -451,7 +452,7 @@ let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
   in
   List.map
     (fun (variant_id, types) ->
-      (variant_id, List.map (ctx_normalize_ty span ctx) types))
+      (variant_id, List.map (ctx_normalize_ty (Some span) ctx) types))
     res
 
 (** Same as [type_decl_get_instantiated_field_types] but normalizes the types *)
@@ -461,7 +462,7 @@ let type_decl_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
   let types =
     Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
   in
-  List.map (ctx_normalize_ty span ctx) types
+  List.map (ctx_normalize_ty (Some span) ctx) types
 
 (** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *)
 let ctx_adt_value_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
@@ -469,7 +470,7 @@ let ctx_adt_value_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
   let types =
     Subst.ctx_adt_value_get_instantiated_field_types span ctx adt id generics
   in
-  List.map (ctx_normalize_ty span ctx) types
+  List.map (ctx_normalize_ty (Some span) ctx) types
 
 (** Same as [ctx_adt_value_get_instantiated_field_types] but normalizes the types
     and erases the regions. *)
@@ -479,7 +480,7 @@ let type_decl_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
   let types =
     Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
   in
-  let types = List.map (ctx_normalize_ty span ctx) types in
+  let types = List.map (ctx_normalize_ty (Some span) ctx) types in
   List.map Subst.erase_regions types
 
 (** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and
@@ -491,7 +492,7 @@ let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
     Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
       generics
   in
-  let types = List.map (ctx_normalize_ty span ctx) types in
+  let types = List.map (ctx_normalize_ty (Some span) ctx) types in
   List.map Subst.erase_regions types
 
 (** Same as [substitute_signature] but normalizes the types *)
@@ -507,8 +508,8 @@ let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
       sg regions_hierarchy
   in
   let { regions_hierarchy; inputs; output; trait_type_constraints } = sg in
-  let inputs = List.map (ctx_normalize_ty span ctx) inputs in
-  let output = ctx_normalize_ty span ctx output in
+  let inputs = List.map (ctx_normalize_ty (Some span) ctx) inputs in
+  let output = ctx_normalize_ty (Some span) ctx output in
   let trait_type_constraints =
     List.map
       (ctx_normalize_trait_type_constraint span ctx)
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 01885cdee..5a721fbb1 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -215,10 +215,11 @@ type assumed_fun_info = {
        *)
 }
 
-let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
+let mk_assumed_fun_info (raw : raw_assumed_fun_info) :
+    assumed_fun_id * assumed_fun_info =
   let fun_id, fun_sig, can_fail, keep_types = raw in
   let name = Charon.PrintExpressions.assumed_fun_id_to_string fun_id in
-  { fun_id; fun_sig; can_fail; name; keep_types }
+  (fun_id, { fun_id; fun_sig; can_fail; name; keep_types })
 
 (** The list of assumed functions and all their information:
     - their signature
@@ -260,11 +261,23 @@ let raw_assumed_fun_infos : raw_assumed_fun_info list =
       None );
   ]
 
-let assumed_fun_infos : assumed_fun_info list =
-  List.map mk_assumed_fun_info raw_assumed_fun_infos
+module OrderedAssumedFunId :
+  Collections.OrderedType with type t = assumed_fun_id = struct
+  type t = assumed_fun_id
+
+  let compare x y = compare_assumed_fun_id x y
+  let to_string x = show_assumed_fun_id x
+  let pp_t fmt x = Format.pp_print_string fmt (show_assumed_fun_id x)
+  let show_t x = show_assumed_fun_id x
+end
+
+module AssumedFunIdMap = Collections.MakeMap (OrderedAssumedFunId)
+
+let assumed_fun_infos : assumed_fun_info AssumedFunIdMap.t =
+  AssumedFunIdMap.of_list (List.map mk_assumed_fun_info raw_assumed_fun_infos)
 
 let get_assumed_fun_info (id : assumed_fun_id) : assumed_fun_info =
-  match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with
+  match AssumedFunIdMap.find_opt id assumed_fun_infos with
   | Some info -> info
   | None ->
       raise
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0170eb2ae..ce69f54b4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -576,7 +576,9 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
             lookup false fun_decl_id lp_id
         | FromLlbc (TraitMethod (_trait_ref, _method_name, fun_decl_id), lp_id)
           -> lookup true fun_decl_id lp_id
-        | FromLlbc (FunId (FAssumed _), _) -> None
+        | FromLlbc (FunId (FAssumed aid), _) ->
+            Some
+              (Assumed.AssumedFunIdMap.find aid ctx.builtin_sigs).explicit_info
         | Pure _ -> None
       in
       (* Filter the generics.
@@ -1213,15 +1215,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
 
     We also return names for the type parameters, const generics, etc.
 
-    TODO: do we really need the first one? We should probably always use
-    the second one.
+    TODO: do we really need the first one?
     It comes from the fact that when we print the input values for the
     decrease clause, we introduce bindings in the context (because we print
     patterns, not the variables). We should figure a cleaner way.
  *)
 let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) :
-    extraction_ctx * extraction_ctx * string list =
+    extraction_ctx * extraction_ctx * (explicit * string) list =
   (* First, add the associated types and constants if the function is a method
      in a trait declaration.
 
@@ -1250,9 +1251,11 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   (* Print the generics *)
   (* Open a box for the generics *)
   F.pp_open_hovbox fmt 0;
+  let explicit = def.signature.explicit_info in
   (let space = Some space in
    extract_generic_params def.item_meta.span ctx fmt TypeDeclId.Set.empty ~space
-     ~trait_decl def.signature.generics type_params cg_params trait_clauses);
+     ~trait_decl def.signature.generics (Some explicit) type_params cg_params
+     trait_clauses);
   (* Close the box for the generics *)
   F.pp_close_box fmt ();
   (* The input parameters - note that doing this adds bindings to the context *)
@@ -1280,6 +1283,9 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
             ctx)
           ctx body.inputs_lvs
   in
+  let type_params = List.combine explicit.explicit_types type_params in
+  let cg_params = List.combine explicit.explicit_const_generics cg_params in
+  let trait_clauses = List.map (fun x -> (Explicit, x)) trait_clauses in
   (ctx, ctx_body, List.concat [ type_params; cg_params; trait_clauses ])
 
 (** A small utility to print the types of the input parameters in the form:
@@ -1646,7 +1652,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
         (fun (name : string) ->
           F.pp_print_space fmt ();
           F.pp_print_string fmt name)
-        all_params;
+        (List.filter_map
+           (fun (e, x) -> if e = Implicit then None else Some x)
+           all_params);
       (* Print the input values: we have to be careful here to print
        * only the input values which are in common with the *forward*
        * function (the additional input values "given back" to the
@@ -1747,7 +1755,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
       (fun (name : string) ->
         F.pp_print_space fmt ();
         F.pp_print_string fmt name)
-      all_params;
+      (List.filter_map
+         (fun (e, x) -> if e = Implicit then None else Some x)
+         all_params);
     (* Print the variables *)
     List.iter
       (fun v ->
@@ -1872,8 +1882,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (name : string)
-    (generics : generic_params) (type_params : string list)
-    (cg_params : string list) (trait_clauses : string list) (ty : ty)
+    (generics : generic_params) (explicit : explicit_info)
+    (type_params : string list) (cg_params : string list)
+    (trait_clauses : string list) (ty : ty)
     (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
 
@@ -1904,7 +1915,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   (* Extract the generic parameters *)
   let space = ref true in
   extract_generic_params span ctx fmt TypeDeclId.Set.empty ~space:(Some space)
-    generics type_params cg_params trait_clauses;
+    generics (Some explicit) type_params cg_params trait_clauses;
   if not !space then F.pp_print_space fmt ();
 
   (* Open ": TYPE =" box (depth=2) *)
@@ -2053,17 +2064,19 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
           decl_ty
       else
         extract_global_decl_body_gen span ctx fmt kind decl_name global.generics
-          type_params cg_params trait_clauses decl_ty None
+          global.explicit_info type_params cg_params trait_clauses decl_ty None
   | Some body ->
       (* There is a body *)
       (* Generate: [let x_body : result u32 = Return 3] *)
       extract_global_decl_body_gen span ctx fmt SingleNonRec body_name
-        global.generics type_params cg_params trait_clauses body_ty
+        global.generics global.explicit_info type_params cg_params trait_clauses
+        body_ty
         (Some (fun fmt -> extract_texpression span ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
       (* Generate: [let x_c : u32 = eval_global x_body] *)
       extract_global_decl_body_gen span ctx fmt SingleNonRec decl_name
-        global.generics type_params cg_params trait_clauses decl_ty
+        global.generics global.explicit_info type_params cg_params trait_clauses
+        decl_ty
         (Some
            (fun fmt ->
              let all_params =
@@ -2405,6 +2418,16 @@ let generic_params_drop_prefix ~(drop_trait_clauses : bool)
   in
   { types; const_generics; trait_clauses }
 
+(** Small helper - TODO: move *)
+let explicit_info_drop_prefix (g1 : generic_params) (g2 : explicit_info) :
+    explicit_info =
+  let open Collections.List in
+  let explicit_types = drop (length g1.types) g2.explicit_types in
+  let explicit_const_generics =
+    drop (length g1.const_generics) g2.explicit_const_generics
+  in
+  { explicit_types; explicit_const_generics }
+
 (** Small helper.
 
     Extract the items for a method in a trait decl.
@@ -2422,10 +2445,11 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
     (* Extract the generics *)
     (* We need to add the generics specific to the method, by removing those
        which actually apply to the trait decl *)
-    let generics =
+    let generics, explicit_info =
       let drop_trait_clauses = false in
-      generic_params_drop_prefix ~drop_trait_clauses decl.generics
-        f.signature.generics
+      ( generic_params_drop_prefix ~drop_trait_clauses decl.generics
+          f.signature.generics,
+        explicit_info_drop_prefix decl.generics f.signature.explicit_info )
     in
     (* Note that we do not filter the LLBC generic parameters.
        This is ok because:
@@ -2446,8 +2470,8 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
     let use_arrows = generics_not_empty && not backend_uses_forall in
     let use_forall_use_sep = false in
     extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
-      ~use_forall ~use_forall_use_sep ~use_arrows generics type_params cg_params
-      trait_clauses;
+      ~use_forall ~use_forall_use_sep ~use_arrows generics (Some explicit_info)
+      type_params cg_params trait_clauses;
     if use_forall then F.pp_print_string fmt ",";
     (* Extract the inputs and output *)
     F.pp_print_space fmt ();
@@ -2508,7 +2532,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
       decl.llbc_generics generics ctx
   in
   extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
-    generics type_params cg_params trait_clauses;
+    generics (Some decl.explicit_info) type_params cg_params trait_clauses;
 
   F.pp_print_space fmt ();
   if is_empty && backend () = FStar then (
@@ -2681,33 +2705,66 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
   in
   let ty () =
     (* Filter the generics if the method is a builtin *)
-    let i_tys, _, _ = impl_generics in
-    let impl_types, i_tys, f_tys =
+    let i_tys, i_cgs, _ = impl_generics in
+    let ( impl_types,
+          impl_cgs,
+          i_tys,
+          i_cgs,
+          f_tys,
+          f_cgs,
+          f_explicit_tys,
+          f_explicit_cgs ) =
       match FunDeclId.Map.find_opt f.def_id ctx.funs_filter_type_args_map with
-      | None -> (impl.generics.types, i_tys, f.signature.generics.types)
+      | None ->
+          ( impl.generics.types,
+            impl.generics.const_generics,
+            i_tys,
+            i_cgs,
+            f.signature.generics.types,
+            f.signature.generics.const_generics,
+            f.signature.explicit_info.explicit_types,
+            f.signature.explicit_info.explicit_const_generics )
       | Some filter ->
-          let filter_list filter ls =
+          let filter_list : 'a. bool list -> 'a list -> 'a list =
+           fun filter ls ->
             let ls = List.combine filter ls in
             List.filter_map (fun (b, ty) -> if b then Some ty else None) ls
           in
           let impl_types = impl.generics.types in
-          let impl_filter =
-            Collections.List.prefix (List.length impl_types) filter
+          let impl_cgs = impl.generics.const_generics in
+          let impl_filter : 'a. 'a list -> bool list =
+           fun l -> Collections.List.prefix (List.length l) filter
           in
           let i_tys = i_tys in
-          let i_filter = Collections.List.prefix (List.length i_tys) filter in
-          ( filter_list impl_filter impl_types,
-            filter_list i_filter i_tys,
-            filter_list filter f.signature.generics.types )
+          let i_filter : 'a. 'a list -> bool list =
+           fun l -> Collections.List.prefix (List.length l) filter
+          in
+          ( filter_list (impl_filter impl_types) impl_types,
+            filter_list (impl_filter impl_cgs) impl_cgs,
+            filter_list (i_filter i_tys) i_tys,
+            filter_list (i_filter i_cgs) i_cgs,
+            filter_list filter f.signature.generics.types,
+            filter_list filter f.signature.generics.const_generics,
+            filter_list filter f.signature.explicit_info.explicit_types,
+            filter_list filter f.signature.explicit_info.explicit_const_generics
+          )
+    in
+    let f_generics =
+      { f.signature.generics with types = f_tys; const_generics = f_cgs }
+    in
+    let f_explicit =
+      {
+        explicit_types = f_explicit_tys;
+        explicit_const_generics = f_explicit_cgs;
+      }
     in
-    let f_generics = { f.signature.generics with types = f_tys } in
     (* Extract the generics - we need to quantify over the generics which
        are specific to the method, and call it will all the generics
        (trait impl + method generics) *)
     let f_generics =
       let drop_trait_clauses = true in
       generic_params_drop_prefix ~drop_trait_clauses
-        { impl.generics with types = impl_types }
+        { impl.generics with types = impl_types; const_generics = impl_cgs }
         f_generics
     in
     (* Register and print the quantified generics.
@@ -2723,7 +2780,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
     in
     let use_forall = f_generics <> empty_generic_params in
     extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
-      ~use_forall f_generics f_tys f_cgs f_tcs;
+      ~use_forall f_generics (Some f_explicit) f_tys f_cgs f_tcs;
     if use_forall then F.pp_print_string fmt ",";
     (* Extract the function call *)
     F.pp_print_space fmt ();
@@ -2732,7 +2789,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
     in
     F.pp_print_string fmt fun_name;
     let all_generics =
-      let _, i_cgs, i_tcs = impl_generics in
+      let _, _, i_tcs = impl_generics in
       List.concat [ i_tys; f_tys; i_cgs; f_cgs; i_tcs; f_tcs ]
     in
 
@@ -2809,7 +2866,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   in
   let all_generics = (type_params, cg_params, trait_clauses) in
   extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
-    impl.generics type_params cg_params trait_clauses;
+    impl.generics (Some impl.explicit_info) type_params cg_params trait_clauses;
 
   (* Print the type *)
   F.pp_print_space fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 1e65947be..a5c8fb394 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -584,6 +584,7 @@ type extraction_ctx = {
   is_provided_method : bool;
   trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
   trans_funs : pure_fun_translation A.FunDeclId.Map.t;
+  builtin_sigs : Pure.fun_sig Assumed.AssumedFunIdMap.t;
   functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
   trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
   trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index d763c69d1..c9b29d7d2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1235,29 +1235,32 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
 (**
  - [trait_decl]: if [Some], it means we are extracting the generics for a provided
    method and need to insert a trait self clause (see {!TraitSelfClauseId}).
+ - [as_implicits]: if [explicit] is [None], then we use this parameter to control
+   whether the parameters should be extract as explicit or implicit.
  *)
 let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) ?(use_forall = false)
     ?(use_forall_use_sep = true) ?(use_arrows = false)
     ?(as_implicits : bool = false) ?(space : bool ref option = None)
     ?(trait_decl : trait_decl option = None) (generics : generic_params)
-    (type_params : string list) (cg_params : string list)
-    (trait_clauses : string list) : unit =
+    (explicit : explicit_info option) (type_params : string list)
+    (cg_params : string list) (trait_clauses : string list) : unit =
   let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
   (* HOL4 doesn't support const generics *)
   cassert __FILE__ __LINE__
     (cg_params = [] || backend () <> HOL4)
     span "Constant generics are not supported yet when generating code for HOL4";
-  let left_bracket (implicit : bool) =
-    if implicit && backend () <> FStar then F.pp_print_string fmt "{"
+  let left_bracket (explicit : explicit) =
+    if explicit = Implicit && backend () <> FStar then F.pp_print_string fmt "{"
     else F.pp_print_string fmt "("
   in
-  let right_bracket (implicit : bool) =
-    if implicit && backend () <> FStar then F.pp_print_string fmt "}"
+  let right_bracket (explicit : explicit) =
+    if explicit = Implicit && backend () <> FStar then F.pp_print_string fmt "}"
     else F.pp_print_string fmt ")"
   in
-  let print_implicit_symbol (implicit : bool) =
-    if implicit && backend () = FStar then F.pp_print_string fmt "#" else ()
+  let print_implicit_symbol (explicit : explicit) =
+    if explicit = Implicit && backend () = FStar then F.pp_print_string fmt "#"
+    else ()
   in
   let insert_req_space () =
     match space with
@@ -1273,69 +1276,83 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
       insert_req_space ();
       F.pp_print_string fmt "forall");
     (* Small helper - we may need to split the parameters *)
-    let print_generics (as_implicits : bool) (type_params : string list)
-        (const_generics : const_generic_var list)
-        (trait_clauses : trait_clause list) : unit =
+    let print_generics (type_params : (explicit * string) list)
+        (const_generics : (explicit * const_generic_var) list)
+        (trait_clauses : (explicit * trait_clause) list) : unit =
       (* Note that in HOL4 we don't print the type parameters. *)
       if backend () <> HOL4 then (
         (* Print the type parameters *)
         if type_params <> [] then (
           insert_req_space ();
-          (* ( *)
-          left_bracket as_implicits;
           List.iter
-            (fun s ->
-              print_implicit_symbol as_implicits;
+            (fun (expl, s) ->
+              (* ( *)
+              left_bracket expl;
+              print_implicit_symbol expl;
               F.pp_print_string fmt s;
-              F.pp_print_space fmt ())
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt ":";
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt (type_keyword span);
+              (* ) *)
+              right_bracket expl)
             type_params;
-          F.pp_print_string fmt ":";
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt (type_keyword span);
-          (* ) *)
-          right_bracket as_implicits;
           if use_arrows then (
             F.pp_print_space fmt ();
             F.pp_print_string fmt "->"));
         (* Print the const generic parameters *)
         List.iter
-          (fun (var : const_generic_var) ->
+          (fun ((expl, var) : explicit * const_generic_var) ->
             insert_req_space ();
             (* ( *)
-            left_bracket as_implicits;
+            left_bracket expl;
             let n = ctx_get_const_generic_var span var.index ctx in
-            print_implicit_symbol as_implicits;
+            print_implicit_symbol expl;
             F.pp_print_string fmt n;
             F.pp_print_space fmt ();
             F.pp_print_string fmt ":";
             F.pp_print_space fmt ();
             extract_literal_type ctx fmt var.ty;
             (* ) *)
-            right_bracket as_implicits;
+            right_bracket expl;
             if use_arrows then (
               F.pp_print_space fmt ();
               F.pp_print_string fmt "->"))
           const_generics);
       (* Print the trait clauses *)
       List.iter
-        (fun (clause : trait_clause) ->
+        (fun ((expl, clause) : explicit * trait_clause) ->
           insert_req_space ();
           (* ( *)
-          left_bracket as_implicits;
+          left_bracket expl;
           let n = ctx_get_local_trait_clause span clause.clause_id ctx in
-          print_implicit_symbol as_implicits;
+          print_implicit_symbol expl;
           F.pp_print_string fmt n;
           F.pp_print_space fmt ();
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
           extract_trait_clause_type span ctx fmt no_params_tys clause;
           (* ) *)
-          right_bracket as_implicits;
+          right_bracket expl;
           if use_arrows then (
             F.pp_print_space fmt ();
             F.pp_print_string fmt "->"))
         trait_clauses
     in
+    (* Associate the explicit/implicit information with the parameters *)
+    let type_params, const_generics, trait_clauses =
+      match explicit with
+      | None ->
+          let expl = if as_implicits then Implicit else Explicit in
+          ( List.map (fun x -> (expl, x)) type_params,
+            List.map (fun x -> (expl, x)) generics.const_generics,
+            List.map (fun x -> (expl, x)) generics.trait_clauses )
+      | Some explicit ->
+          ( List.combine explicit.explicit_types type_params,
+            List.combine explicit.explicit_const_generics
+              generics.const_generics,
+            List.map (fun x -> (Explicit, x)) generics.trait_clauses )
+    in
     (* If we extract the generics for a provided method for a trait declaration
        (indicated by the trait decl given as input), we need to split the generics:
        - we print the generics for the trait decl
@@ -1343,9 +1360,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
        - we print the generics for the trait method
     *)
     match trait_decl with
-    | None ->
-        print_generics as_implicits type_params generics.const_generics
-          generics.trait_clauses
+    | None -> print_generics type_params const_generics trait_clauses
     | Some trait_decl ->
         (* Split the generics between the generics specific to the trait decl
            and those specific to the trait method *)
@@ -1354,29 +1369,34 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
           split_at type_params (length trait_decl.generics.types)
         in
         let dcgs, mcgs =
-          split_at generics.const_generics
-            (length trait_decl.generics.const_generics)
+          split_at const_generics (length trait_decl.generics.const_generics)
         in
         let dtrait_clauses, mtrait_clauses =
-          split_at generics.trait_clauses
-            (length trait_decl.generics.trait_clauses)
+          split_at trait_clauses (length trait_decl.generics.trait_clauses)
         in
         (* Extract the trait decl generics - note that we can always deduce
            those parameters from the trait self clause: for this reason
            they are always implicit *)
-        print_generics true dtype_params dcgs dtrait_clauses;
+        let dtype_params =
+          List.map (fun (_, x) -> (Implicit, x)) dtype_params
+        in
+        let dcgs = List.map (fun (_, x) -> (Implicit, x)) dcgs in
+        let dtrait_clauses =
+          List.map (fun (_, x) -> (Implicit, x)) dtrait_clauses
+        in
+        print_generics dtype_params dcgs dtrait_clauses;
         (* Extract the trait self clause *)
         let params =
           concat
             [
-              dtype_params;
+              map snd dtype_params;
               map
-                (fun (cg : const_generic_var) ->
+                (fun ((_, cg) : _ * const_generic_var) ->
                   ctx_get_const_generic_var trait_decl.item_meta.span cg.index
                     ctx)
                 dcgs;
               map
-                (fun c ->
+                (fun (_, c) ->
                   ctx_get_local_trait_clause trait_decl.item_meta.span
                     c.clause_id ctx)
                 dtrait_clauses;
@@ -1384,7 +1404,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
         in
         extract_trait_self_clause insert_req_space ctx fmt trait_decl params;
         (* Extract the method generics *)
-        print_generics as_implicits mtype_params mcgs mtrait_clauses)
+        print_generics mtype_params mcgs mtrait_clauses)
 
 (** Extract a type declaration.
 
@@ -1481,7 +1501,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
      supported yet when generating code for HOL4";
   (* Print the generic parameters *)
   extract_generic_params def.item_meta.span ctx_body fmt type_decl_group
-    ~use_forall def.generics type_params cg_params trait_clauses;
+    ~use_forall def.generics (Some def.explicit_info) type_params cg_params
+    trait_clauses;
   (* Print the "=" if we extract the body*)
   if extract_body then (
     F.pp_print_space fmt ();
@@ -1780,7 +1801,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Print the generics *)
           let as_implicits = true in
           extract_generic_params decl.item_meta.span ctx fmt
-            TypeDeclId.Set.empty ~as_implicits decl.generics type_params
+            TypeDeclId.Set.empty ~as_implicits decl.generics None type_params
             cg_params trait_clauses;
 
           (* Print the record parameter as "(x : ADT)" *)
@@ -1967,7 +1988,7 @@ let extract_type_decl_record_field_projectors_simp_lemmas (ctx : extraction_ctx)
           (* Print the generics *)
           let as_implicits = true in
           extract_generic_params span ctx fmt TypeDeclId.Set.empty ~as_implicits
-            decl.generics type_params cg_params trait_clauses;
+            decl.generics None type_params cg_params trait_clauses;
 
           (* Print the input parameters (the fields) *)
           let print_field (ctx : extraction_ctx) (field_id : FieldId.id)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 81a79c063..fd459d1b6 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -54,7 +54,7 @@ let normalize_inst_fun_sig (span : Meta.span) (ctx : eval_ctx)
   let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } =
     sg
   in
-  let norm = AssociatedTypes.ctx_normalize_ty span ctx in
+  let norm = AssociatedTypes.ctx_normalize_ty (Some span) ctx in
   let inputs = List.map norm inputs in
   let output = norm output in
   { sg with inputs; output }
@@ -154,7 +154,7 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
   in
   (* Compute the normalization maps *)
   let ctx =
-    AssociatedTypes.ctx_add_norm_trait_types_from_preds span ctx
+    AssociatedTypes.ctx_add_norm_trait_types_from_preds (Some span) ctx
       inst_sg.trait_type_constraints
   in
   (* Normalize the signature *)
@@ -209,8 +209,8 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx fdef.item_meta.span ctx region_groups sg.generics.types
-      sg.generics.const_generics
+    initialize_eval_ctx (Some fdef.item_meta.span) ctx region_groups
+      sg.generics.types sg.generics.const_generics
   in
   (* Instantiate the signature. This updates the context because we compute
      at the same time the normalization map for the associated types.
@@ -681,7 +681,9 @@ module Test = struct
     sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.item_meta.span;
 
     (* Create the evaluation context *)
-    let ctx = initialize_eval_ctx fdef.item_meta.span decls_ctx [] [] [] in
+    let ctx =
+      initialize_eval_ctx (Some fdef.item_meta.span) decls_ctx [] [] []
+    in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = ctx_push_uninitialized_vars fdef.item_meta.span ctx body.locals in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 982422356..d0dc88e68 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -69,27 +69,34 @@ let mk_place_from_var_id (var_id : VarId.id) : place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (span : Meta.span) (ty : ty) : symbolic_value =
+let mk_fresh_symbolic_value_opt_span (span : Meta.span option) (ty : ty) :
+    symbolic_value =
   (* Sanity check *)
-  sanity_check __FILE__ __LINE__ (ty_is_rty ty) span;
+  sanity_check_opt_span __FILE__ __LINE__ (ty_is_rty ty) span;
   let sv_id = fresh_symbolic_value_id () in
   let svalue = { sv_id; sv_ty = ty } in
   svalue
 
+let mk_fresh_symbolic_value span = mk_fresh_symbolic_value_opt_span (Some span)
+
 let mk_fresh_symbolic_value_from_no_regions_ty (span : Meta.span) (ty : ty) :
     symbolic_value =
   sanity_check __FILE__ __LINE__ (ty_no_regions ty) span;
   mk_fresh_symbolic_value span ty
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (span : Meta.span) (rty : ty) : typed_value =
-  sanity_check __FILE__ __LINE__ (ty_is_rty rty) span;
+let mk_fresh_symbolic_typed_value_opt_span (span : Meta.span option) (rty : ty)
+    : typed_value =
+  sanity_check_opt_span __FILE__ __LINE__ (ty_is_rty rty) span;
   let ty = Substitute.erase_regions rty in
   (* Generate the fresh a symbolic value *)
-  let value = mk_fresh_symbolic_value span rty in
+  let value = mk_fresh_symbolic_value_opt_span span rty in
   let value = VSymbolic value in
   { value; ty }
 
+let mk_fresh_symbolic_typed_value span =
+  mk_fresh_symbolic_typed_value_opt_span (Some span)
+
 let mk_fresh_symbolic_typed_value_from_no_regions_ty (span : Meta.span)
     (ty : ty) : typed_value =
   sanity_check __FILE__ __LINE__ (ty_no_regions ty) span;
@@ -431,7 +438,7 @@ let empty_ids_set = fst (compute_ctxs_ids [])
 (** **WARNING**: this function doesn't compute the normalized types
     (for the trait type aliases). This should be computed afterwards.
  *)
-let initialize_eval_ctx (span : Meta.span) (ctx : decls_ctx)
+let initialize_eval_ctx (span : Meta.span option) (ctx : decls_ctx)
     (region_groups : RegionGroupId.id list) (type_vars : type_var list)
     (const_generic_vars : const_generic_var list) : eval_ctx =
   reset_global_counters ();
@@ -440,7 +447,7 @@ let initialize_eval_ctx (span : Meta.span) (ctx : decls_ctx)
       (List.map
          (fun (cg : const_generic_var) ->
            let ty = TLiteral cg.ty in
-           let cv = mk_fresh_symbolic_typed_value span ty in
+           let cv = mk_fresh_symbolic_typed_value_opt_span span ty in
            (cg.index, cv))
          const_generic_vars)
   in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 3cffc8f4e..f3ae93fd1 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -514,7 +514,15 @@ and predicates = { trait_type_constraints : trait_type_constraint list }
         polymorphic = false;
       }]
 
-type type_decl = {
+(** Characterize an input parameter as explicit or implicit *)
+type explicit = Explicit | Implicit
+
+and explicit_info = {
+  explicit_types : explicit list;
+  explicit_const_generics : explicit list;
+}
+
+and type_decl = {
   def_id : type_decl_id;
   name : string;
       (** We use the name only for printing purposes (for debugging):
@@ -523,6 +531,8 @@ type type_decl = {
        *)
   item_meta : T.item_meta;
   generics : generic_params;
+  explicit_info : explicit_info;
+      (** Information about which inputs parameters are explicit/implicit *)
   llbc_generics : (Types.generic_params[@opaque]);
       (** We use the LLBC generics to generate "pretty" names, for instance
           for the variables we introduce for the trait clauses: we derive
@@ -1178,15 +1188,6 @@ type decomposed_fun_sig = {
 }
 [@@deriving show]
 
-(** Characterize an input parameter as explicit or implicit *)
-type explicit = Explicit | Implicit [@@deriving show]
-
-type explicit_info = {
-  explicit_types : explicit list;
-  explicit_const_generics : explicit list;
-}
-[@@deriving show]
-
 (** A function signature.
 
     We have the following cases:
@@ -1223,7 +1224,7 @@ type explicit_info = {
 type fun_sig = {
   generics : generic_params;
   explicit_info : explicit_info;
-      (** Information about the inputs parameters which are explicit/implicit *)
+      (** Information about which inputs parameters are explicit/implicit *)
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
           for the variables we introduce for the trait clauses: we derive
@@ -1320,6 +1321,8 @@ type global_decl = {
   llbc_generics : Types.generic_params;
       (** See the comment for [llbc_generics] in fun_decl. *)
   generics : generic_params;
+  explicit_info : explicit_info;
+      (** Information about which inputs parameters are explicit/implicit *)
   preds : predicates;
   ty : ty;
   kind : item_kind;
@@ -1332,6 +1335,8 @@ type trait_decl = {
   name : string;
   item_meta : T.item_meta;
   generics : generic_params;
+  explicit_info : explicit_info;
+      (** Information about which inputs parameters are explicit/implicit *)
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
           for the variables we introduce for the trait clauses: we derive
@@ -1356,6 +1361,8 @@ type trait_impl = {
   llbc_impl_trait : Types.trait_decl_ref;
       (** Same remark as for {!field:llbc_generics}. *)
   generics : generic_params;
+  explicit_info : explicit_info;
+      (** Information about which inputs parameters are explicit/implicit *)
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
           for the variables we introduce for the trait clauses: we derive
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 2c2a4843a..a178173d9 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -719,6 +719,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
     name = _;
     item_meta = _;
     generics = _;
+    explicit_info = _;
     llbc_generics = _;
     preds = _;
     parent_clauses;
@@ -741,6 +742,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
     impl_trait = _;
     llbc_impl_trait = _;
     generics = _;
+    explicit_info = _;
     llbc_generics = _;
     preds = _;
     parent_trait_refs;
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index f58af48ef..1c9f93095 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -332,7 +332,7 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
     List.map
       (fun (info : assumed_fun_info) ->
         (FAssumed info.fun_id, (info.name, info.fun_sig, None)))
-      assumed_fun_infos
+      (AssumedFunIdMap.values assumed_fun_infos)
   in
   FunIdMap.of_list
     (List.map
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 93cf4d9a1..105b0309c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -407,8 +407,8 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
 
 (* Some generic translation functions (we need to translate different "flavours"
    of types: forward types, backward types, etc.) *)
-let rec translate_generic_args (span : Meta.span) (translate_ty : T.ty -> ty)
-    (generics : T.generic_args) : generic_args =
+let rec translate_generic_args (span : Meta.span option)
+    (translate_ty : T.ty -> ty) (generics : T.generic_args) : generic_args =
   (* We ignore the regions: if they didn't cause trouble for the symbolic execution,
      then everything's fine *)
   let types = List.map translate_ty generics.types in
@@ -418,7 +418,7 @@ let rec translate_generic_args (span : Meta.span) (translate_ty : T.ty -> ty)
   in
   { types; const_generics; trait_refs }
 
-and translate_trait_ref (span : Meta.span) (translate_ty : T.ty -> ty)
+and translate_trait_ref (span : Meta.span option) (translate_ty : T.ty -> ty)
     (tr : T.trait_ref) : trait_ref =
   let trait_id = translate_trait_instance_id span translate_ty tr.trait_id in
   let trait_decl_ref =
@@ -426,22 +426,22 @@ and translate_trait_ref (span : Meta.span) (translate_ty : T.ty -> ty)
   in
   { trait_id; trait_decl_ref }
 
-and translate_trait_decl_ref (span : Meta.span) (translate_ty : T.ty -> ty)
-    (tr : T.trait_decl_ref) : trait_decl_ref =
+and translate_trait_decl_ref (span : Meta.span option)
+    (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) : trait_decl_ref =
   let decl_generics =
     translate_generic_args span translate_ty tr.decl_generics
   in
   { trait_decl_id = tr.trait_decl_id; decl_generics }
 
-and translate_global_decl_ref (span : Meta.span) (translate_ty : T.ty -> ty)
-    (gr : T.global_decl_ref) : global_decl_ref =
+and translate_global_decl_ref (span : Meta.span option)
+    (translate_ty : T.ty -> ty) (gr : T.global_decl_ref) : global_decl_ref =
   let global_generics =
     translate_generic_args span translate_ty gr.global_generics
   in
   { global_id = gr.global_id; global_generics }
 
-and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
-    (id : T.trait_instance_id) : trait_instance_id =
+and translate_trait_instance_id (span : Meta.span option)
+    (translate_ty : T.ty -> ty) (id : T.trait_instance_id) : trait_instance_id =
   let translate_trait_instance_id =
     translate_trait_instance_id span translate_ty
   in
@@ -452,20 +452,23 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
       TraitImpl (id, generics)
   | BuiltinOrAuto _ ->
       (* We should have eliminated those in the prepasses *)
-      craise __FILE__ __LINE__ span "Unreachable"
+      craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | Clause id -> Clause id
   | ParentClause (inst_id, decl_id, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
       ParentClause (inst_id, decl_id, clause_id)
   | FnPointer _ | Closure _ ->
-      craise __FILE__ __LINE__ span "Closures are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span "Closures are not supported yet"
   | Dyn _ ->
-      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
-  | Unsolved _ -> craise __FILE__ __LINE__ span "Couldn't solve trait bound"
-  | UnknownTrait s -> craise __FILE__ __LINE__ span ("Unknown trait found: " ^ s)
+      craise_opt_span __FILE__ __LINE__ span
+        "Dynamic trait types are not supported yet"
+  | Unsolved _ ->
+      craise_opt_span __FILE__ __LINE__ span "Couldn't solve trait bound"
+  | UnknownTrait s ->
+      craise_opt_span __FILE__ __LINE__ span ("Unknown trait found: " ^ s)
 
 (** Translate a signature type - TODO: factor out the different translation functions *)
-let rec translate_sty (span : Meta.span) (ty : T.ty) : ty =
+let rec translate_sty (span : Meta.span option) (ty : T.ty) : ty =
   let translate = translate_sty in
   match ty with
   | T.TAdt (type_id, generics) -> (
@@ -473,7 +476,9 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty =
       match type_id with
       | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
       | T.TTuple ->
-          sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
+          sanity_check_opt_span __FILE__ __LINE__
+            (generics.const_generics = [])
+            span;
           mk_simpl_tuple_ty generics.types
       | T.TAssumed aty -> (
           match aty with
@@ -482,14 +487,14 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty =
               match generics.types with
               | [ ty ] -> ty
               | _ ->
-                  craise __FILE__ __LINE__ span
+                  craise_opt_span __FILE__ __LINE__ span
                     "Box/vec/option type with incorrect number of arguments")
           | T.TArray -> TAdt (TAssumed TArray, generics)
           | T.TSlice -> TAdt (TAssumed TSlice, generics)
           | T.TStr -> TAdt (TAssumed TStr, generics)))
   | TVar vid -> TVar vid
   | TLiteral ty -> TLiteral ty
-  | TNever -> craise __FILE__ __LINE__ span "Unreachable"
+  | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TRef (_, rty, _) -> translate span rty
   | TRawPtr (ty, rkind) ->
       let mut =
@@ -504,36 +509,38 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty =
       let trait_ref = translate_strait_ref span trait_ref in
       TTraitType (trait_ref, type_name)
   | TArrow _ ->
-      craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span "Arrow types are not supported yet"
   | TDynTrait _ ->
-      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span
+        "Dynamic trait types are not supported yet"
 
-and translate_sgeneric_args (span : Meta.span) (generics : T.generic_args) :
-    generic_args =
+and translate_sgeneric_args (span : Meta.span option)
+    (generics : T.generic_args) : generic_args =
   translate_generic_args span (translate_sty span) generics
 
-and translate_strait_ref (span : Meta.span) (tr : T.trait_ref) : trait_ref =
+and translate_strait_ref (span : Meta.span option) (tr : T.trait_ref) :
+    trait_ref =
   translate_trait_ref span (translate_sty span) tr
 
-and translate_strait_instance_id (span : Meta.span) (id : T.trait_instance_id) :
-    trait_instance_id =
+and translate_strait_instance_id (span : Meta.span option)
+    (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id span (translate_sty span) id
 
-let translate_trait_clause (span : Meta.span) (clause : T.trait_clause) :
+let translate_trait_clause (span : Meta.span option) (clause : T.trait_clause) :
     trait_clause =
   let { T.clause_id; span = _; trait } = clause in
   let generics = translate_sgeneric_args span trait.decl_generics in
   { clause_id; trait_id = trait.trait_decl_id; generics }
 
-let translate_strait_type_constraint (span : Meta.span)
+let translate_strait_type_constraint (span : Meta.span option)
     (ttc : T.trait_type_constraint) : trait_type_constraint =
   let { T.trait_ref; type_name; ty } = ttc in
   let trait_ref = translate_strait_ref span trait_ref in
   let ty = translate_sty span ty in
   { trait_ref; type_name; ty }
 
-let translate_generic_params (span : Meta.span) (generics : T.generic_params) :
-    generic_params * predicates =
+let translate_generic_params (span : Meta.span option)
+    (generics : T.generic_params) : generic_params * predicates =
   let {
     T.regions = _;
     types;
@@ -552,7 +559,7 @@ let translate_generic_params (span : Meta.span) (generics : T.generic_params) :
 
 let translate_field (span : Meta.span) (f : T.field) : field =
   let field_name = f.field_name in
-  let field_ty = translate_sty span f.field_ty in
+  let field_ty = translate_sty (Some span) f.field_ty in
   let field_attr_info = f.attr_info in
   { field_name; field_ty; field_attr_info }
 
@@ -579,6 +586,55 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
         "type aliases should have been removed earlier"
   | T.Union _ | T.Opaque | T.Error _ -> Opaque
 
+(** Compute which input parameters should be implicit or explicit.
+
+    The way we do it is simple: if a parameter appears in one of the inputs,
+    then it should be implicit. For instance, the type parameter of [Vec::get]
+    should be implicit, while the type parameter of [Vec::new] should be explicit
+    (it only appears in the output).
+    Also note that here we consider the trait obligations as inputs from which
+    we can deduce an implicit parameter. For instance:
+    {[
+      let f {a : Type} (clause0 : Foo a) : ...
+             ^^^^^^^^
+          implied by clause0
+    ]}
+
+    The [input_tys] are the types of the input arguments, in case we are translating
+    a function.
+ *)
+let compute_explicit_info (generics : Pure.generic_params) (input_tys : ty list)
+    : explicit_info =
+  let implicit_tys = ref Pure.TypeVarId.Set.empty in
+  let implicit_cgs = ref Pure.ConstGenericVarId.Set.empty in
+  let visitor =
+    object
+      inherit [_] Pure.iter_type_decl
+
+      method! visit_type_var_id _ id =
+        implicit_tys := Pure.TypeVarId.Set.add id !implicit_tys
+
+      method! visit_const_generic_var_id _ id =
+        implicit_cgs := Pure.ConstGenericVarId.Set.add id !implicit_cgs
+    end
+  in
+  List.iter (visitor#visit_trait_clause ()) generics.trait_clauses;
+  List.iter (visitor#visit_ty ()) input_tys;
+  let make_explicit_ty (v : Pure.type_var) : Pure.explicit =
+    if Pure.TypeVarId.Set.mem v.index !implicit_tys then Implicit else Explicit
+  in
+  let make_explicit_cg (v : Pure.const_generic_var) : Pure.explicit =
+    if Pure.ConstGenericVarId.Set.mem v.index !implicit_cgs then Implicit
+    else Explicit
+  in
+  {
+    explicit_types = List.map make_explicit_ty generics.types;
+    explicit_const_generics = List.map make_explicit_cg generics.const_generics;
+  }
+
+let compute_fun_sig_explicit_info (sg : Pure.fun_sig) : explicit_info =
+  compute_explicit_info sg.generics sg.inputs
+
 (** Translate a type definition from LLBC
 
     Remark: this is not symbolic to pure but LLBC to pure. Still,
@@ -600,8 +656,9 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     (def.generics.regions = [])
     def.item_meta.span "ADTs containing borrows are not supported yet";
   let generics, preds =
-    translate_generic_params def.item_meta.span def.generics
+    translate_generic_params (Some def.item_meta.span) def.generics
   in
+  let explicit_info = compute_explicit_info generics [] in
   let kind = translate_type_decl_kind def.item_meta.span def.T.kind in
   let item_meta = def.item_meta in
   {
@@ -609,12 +666,13 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     name;
     item_meta;
     generics;
+    explicit_info;
     llbc_generics = def.generics;
     kind;
     preds;
   }
 
-let translate_type_id (span : Meta.span) (id : T.type_id) : type_id =
+let translate_type_id (span : Meta.span option) (id : T.type_id) : type_id =
   match id with
   | TAdtId adt_id -> TAdtId adt_id
   | TAssumed aty ->
@@ -626,7 +684,7 @@ let translate_type_id (span : Meta.span) (id : T.type_id) : type_id =
         | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
-            craise __FILE__ __LINE__ span "Unexpected box type"
+            craise_opt_span __FILE__ __LINE__ span "Unexpected box type"
       in
       TAssumed aty
   | TTuple -> TTuple
@@ -639,7 +697,7 @@ let translate_type_id (span : Meta.span) (id : T.type_id) : type_id =
 
     TODO: factor out the various translation functions.
 *)
-let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos)
+let rec translate_fwd_ty (span : Meta.span option) (type_infos : type_infos)
     (ty : T.ty) : ty =
   let translate = translate_fwd_ty span type_infos in
   match ty with
@@ -657,7 +715,7 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos)
       | TAssumed TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
-          cassert __FILE__ __LINE__
+          cassert_opt_span __FILE__ __LINE__
             (not
                (List.exists
                   (TypesUtils.ty_has_borrows type_infos)
@@ -666,11 +724,11 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos)
           match t_generics.types with
           | [ bty ] -> bty
           | _ ->
-              craise __FILE__ __LINE__ span
+              craise_opt_span __FILE__ __LINE__ span
                 "Unreachable: box/vec/option receives exactly one type \
                  parameter"))
   | TVar vid -> TVar vid
-  | TNever -> craise __FILE__ __LINE__ span "Unreachable"
+  | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TLiteral lty -> TLiteral lty
   | TRef (_, rty, _) -> translate rty
   | TRawPtr (ty, rkind) ->
@@ -686,32 +744,33 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos)
       let trait_ref = translate_fwd_trait_ref span type_infos trait_ref in
       TTraitType (trait_ref, type_name)
   | TArrow _ ->
-      craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span "Arrow types are not supported yet"
   | TDynTrait _ ->
-      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span
+        "Dynamic trait types are not supported yet"
 
-and translate_fwd_generic_args (span : Meta.span) (type_infos : type_infos)
-    (generics : T.generic_args) : generic_args =
+and translate_fwd_generic_args (span : Meta.span option)
+    (type_infos : type_infos) (generics : T.generic_args) : generic_args =
   translate_generic_args span (translate_fwd_ty span type_infos) generics
 
-and translate_fwd_trait_ref (span : Meta.span) (type_infos : type_infos)
+and translate_fwd_trait_ref (span : Meta.span option) (type_infos : type_infos)
     (tr : T.trait_ref) : trait_ref =
   translate_trait_ref span (translate_fwd_ty span type_infos) tr
 
-and translate_fwd_trait_instance_id (span : Meta.span) (type_infos : type_infos)
-    (id : T.trait_instance_id) : trait_instance_id =
+and translate_fwd_trait_instance_id (span : Meta.span option)
+    (type_infos : type_infos) (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id span (translate_fwd_ty span type_infos) id
 
 (** Simply calls [translate_fwd_ty] *)
 let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_fwd_ty ctx.span type_infos ty
+  translate_fwd_ty (Some ctx.span) type_infos ty
 
 (** Simply calls [translate_fwd_generic_args] *)
 let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     generic_args =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_fwd_generic_args ctx.span type_infos generics
+  translate_fwd_generic_args (Some ctx.span) type_infos generics
 
 (** Translate a type, when some regions may have ended.
     
@@ -719,7 +778,7 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     
     [inside_mut]: are we inside a mutable borrow?
  *)
-let rec translate_back_ty (span : Meta.span) (type_infos : type_infos)
+let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos)
     (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option
     =
   let translate = translate_back_ty span type_infos keep_region inside_mut in
@@ -753,14 +812,14 @@ let rec translate_back_ty (span : Meta.span) (type_infos : type_infos)
             else None
       | TAssumed TBox -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
-          cassert __FILE__ __LINE__
+          cassert_opt_span __FILE__ __LINE__
             (not (TypesUtils.ty_has_borrows type_infos ty))
             span "ADTs containing borrows are not supported yet";
           (* Eliminate the box *)
           match generics.types with
           | [ bty ] -> translate bty
           | _ ->
-              craise __FILE__ __LINE__ span
+              craise_opt_span __FILE__ __LINE__ span
                 "Unreachable: boxes receive exactly one type parameter")
       | TTuple -> (
           (* Tuples can contain borrows (which we eliminate) *)
@@ -772,7 +831,7 @@ let rec translate_back_ty (span : Meta.span) (type_infos : type_infos)
                * is the identity *)
               Some (mk_simpl_tuple_ty tys_t)))
   | TVar vid -> wrap (TVar vid)
-  | TNever -> craise __FILE__ __LINE__ span "Unreachable"
+  | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
   | TLiteral lty -> wrap (TLiteral lty)
   | TRef (r, rty, rkind) -> (
       match rkind with
@@ -798,15 +857,16 @@ let rec translate_back_ty (span : Meta.span) (type_infos : type_infos)
         Some (TTraitType (trait_ref, type_name))
       else None
   | TArrow _ ->
-      craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span "Arrow types are not supported yet"
   | TDynTrait _ ->
-      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
+      craise_opt_span __FILE__ __LINE__ span
+        "Dynamic trait types are not supported yet"
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
     (inside_mut : bool) (ty : T.ty) : ty option =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_back_ty ctx.span type_infos keep_region inside_mut ty
+  translate_back_ty (Some ctx.span) type_infos keep_region inside_mut ty
 
 let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
   let const_generics =
@@ -842,7 +902,9 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
   | FunId fun_id -> FunId fun_id
   | TraitMethod (trait_ref, method_name, fun_decl_id) ->
       let type_infos = ctx.type_ctx.type_infos in
-      let trait_ref = translate_fwd_trait_ref ctx.span type_infos trait_ref in
+      let trait_ref =
+        translate_fwd_trait_ref (Some ctx.span) type_infos trait_ref
+      in
       TraitMethod (trait_ref, method_name, fun_decl_id)
 
 let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
@@ -938,7 +1000,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
   if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
 
 (** Small utility. *)
-let compute_raw_fun_effect_info (span : Meta.span)
+let compute_raw_fun_effect_info (span : Meta.span option)
     (fun_infos : fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
@@ -957,7 +1019,7 @@ let compute_raw_fun_effect_info (span : Meta.span)
         is_rec = info.is_rec || Option.is_some lid;
       }
   | FunId (FAssumed aid) ->
-      sanity_check __FILE__ __LINE__ (lid = None) span;
+      sanity_check_opt_span __FILE__ __LINE__ (lid = None) span;
       {
         can_fail = Assumed.assumed_fun_can_fail aid;
         stateful_group = false;
@@ -982,8 +1044,8 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
           in
           { info with is_rec = info.is_rec || Option.is_some lid }
       | FunId (FAssumed _) ->
-          compute_raw_fun_effect_info ctx.span ctx.fun_ctx.fun_infos fun_id lid
-            gid)
+          compute_raw_fun_effect_info (Some ctx.span) ctx.fun_ctx.fun_infos
+            fun_id lid gid)
   | Some lid -> (
       (* This is necessarily for the current function *)
       match fun_id with
@@ -1008,8 +1070,9 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
     We use [bid] ("backward function id") only if we split the forward
     and the backward functions.
  *)
-let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
-    (decls_ctx : C.decls_ctx) (fun_id : A.fun_id_or_trait_method_ref)
+let translate_fun_sig_with_regions_hierarchy_to_decomposed
+    (span : Meta.span option) (decls_ctx : C.decls_ctx)
+    (fun_id : A.fun_id_or_trait_method_ref)
     (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig)
     (input_names : string option list) : decomposed_fun_sig =
   let fun_infos = decls_ctx.fun_ctx.fun_infos in
@@ -1082,8 +1145,10 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
     let keep_region r =
       match r with
       | T.RStatic -> raise Unimplemented
-      | RErased -> craise __FILE__ __LINE__ span "Unexpected erased region"
-      | RBVar _ -> craise __FILE__ __LINE__ span "Unexpected bound region"
+      | RErased ->
+          craise_opt_span __FILE__ __LINE__ span "Unexpected erased region"
+      | RBVar _ ->
+          craise_opt_span __FILE__ __LINE__ span "Unexpected bound region"
       | RFVar rid -> T.RegionId.Set.mem rid gr_regions
     in
     let inside_mut = false in
@@ -1093,7 +1158,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
     (* For now we don't supported nested borrows, so we check that there
        aren't parent regions *)
     let parents = list_ancestor_region_groups regions_hierarchy gid in
-    cassert __FILE__ __LINE__
+    cassert_opt_span __FILE__ __LINE__
       (T.RegionGroupId.Set.is_empty parents)
       span "Nested borrows are not supported yet";
     (* For now, we don't allow nested borrows, so the additional inputs to the
@@ -1252,7 +1317,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
       else false
     in
     let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in
-    sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf info) span;
+    sanity_check_opt_span __FILE__ __LINE__ (fun_sig_info_is_wf info) span;
     info
   in
 
@@ -1280,7 +1345,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
   let span =
     (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.span
   in
-  translate_fun_sig_with_regions_hierarchy_to_decomposed span decls_ctx
+  translate_fun_sig_with_regions_hierarchy_to_decomposed (Some span) decls_ctx
     (FunId (FRegular fun_id)) regions_hierarchy sg input_names
 
 let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx)
@@ -1391,49 +1456,6 @@ let compute_output_ty_from_decomposed (dsg : Pure.decomposed_fun_sig) : ty =
   in
   mk_output_ty_from_effect_info effect_info output
 
-(** Compute which input parameters should be implicit or explicit.
-
-    The way we do it is simple: if a parameter appears in one of the inputs,
-    then it should be implicit. For instance, the type parameter of [Vec::get]
-    should be implicit, while the type parameter of [Vec::new] should be explicit
-    (it only appears in the output).
-    Also note that here we consider the trait obligations as inputs from which
-    we can deduce an implicit parameter. For instance:
-    {[
-      let f {a : Type} (clause0 : Foo a) : ...
-             ^^^^^^^^
-          implied by clause0
-    ]}
- *)
-let compute_explicit_info (generics : Pure.generic_params) (input_tys : ty list)
-    : explicit_info =
-  let implicit_tys = ref Pure.TypeVarId.Set.empty in
-  let implicit_cgs = ref Pure.ConstGenericVarId.Set.empty in
-  let visitor =
-    object
-      inherit [_] Pure.iter_type_decl
-
-      method! visit_type_var_id _ id =
-        implicit_tys := Pure.TypeVarId.Set.add id !implicit_tys
-
-      method! visit_const_generic_var_id _ id =
-        implicit_cgs := Pure.ConstGenericVarId.Set.add id !implicit_cgs
-    end
-  in
-  List.iter (visitor#visit_trait_clause ()) generics.trait_clauses;
-  List.iter (visitor#visit_ty ()) input_tys;
-  let make_explicit_ty (v : Pure.type_var) : Pure.explicit =
-    if Pure.TypeVarId.Set.mem v.index !implicit_tys then Implicit else Explicit
-  in
-  let make_explicit_cg (v : Pure.const_generic_var) : Pure.explicit =
-    if Pure.ConstGenericVarId.Set.mem v.index !implicit_cgs then Implicit
-    else Explicit
-  in
-  {
-    explicit_types = List.map make_explicit_ty generics.types;
-    explicit_const_generics = List.map make_explicit_cg generics.const_generics;
-  }
-
 let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig) : fun_sig
     =
   let generics = dsg.generics in
@@ -2219,8 +2241,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           let sg = Option.get call.sg in
           let decls_ctx = ctx.decls_ctx in
           let dsg =
-            translate_fun_sig_with_regions_hierarchy_to_decomposed ctx.span
-              decls_ctx fid call.regions_hierarchy sg
+            translate_fun_sig_with_regions_hierarchy_to_decomposed
+              (Some ctx.span) decls_ctx fid call.regions_hierarchy sg
               (List.map (fun _ -> None) sg.inputs)
           in
           log#ldebug
@@ -2233,7 +2255,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                   ctx_translate_fwd_generic_args ctx all_generics
                 in
                 let tr_self =
-                  translate_fwd_trait_instance_id ctx.span
+                  translate_fwd_trait_instance_id (Some ctx.span)
                     ctx.type_ctx.type_infos tr_self
                 in
                 (tr_self, all_generics)
@@ -3108,7 +3130,9 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
     | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, const_name) ->
         let type_infos = ctx.type_ctx.type_infos in
-        let trait_ref = translate_fwd_trait_ref ctx.span type_infos trait_ref in
+        let trait_ref =
+          translate_fwd_trait_ref (Some ctx.span) type_infos trait_ref
+        in
         let qualif_id = TraitConst (trait_ref, const_name) in
         let qualif = { id = qualif_id; generics = empty_generic_args } in
         { e = Qualif qualif; ty = var.ty }
@@ -3857,6 +3881,24 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
       (* We should have checked the command line arguments before *)
       raise (Failure "Unexpected")
 
+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 =
+  (* Compute the regions hierarchy *)
+  let regions_hierarchy =
+    RegionsHierarchy.compute_regions_hierarchy_for_sig None
+      decls_ctx.type_ctx.type_decls decls_ctx.fun_ctx.fun_decls
+      decls_ctx.global_ctx.global_decls decls_ctx.trait_decls_ctx.trait_decls
+      decls_ctx.trait_impls_ctx.trait_impls fun_name sg
+  in
+  (* Compute the decomposed fun signature *)
+  let sg =
+    translate_fun_sig_with_regions_hierarchy_to_decomposed None decls_ctx
+      (FunId fun_id) regions_hierarchy sg input_names
+  in
+  (* Finish the translation *)
+  translate_fun_sig_from_decomposed sg
+
 let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* Translate *)
   let def = ctx.fun_decl in
@@ -4045,17 +4087,18 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
       item_meta.name
   in
   let generics, preds =
-    translate_generic_params trait_decl.item_meta.span llbc_generics
+    translate_generic_params (Some trait_decl.item_meta.span) llbc_generics
   in
+  let explicit_info = compute_explicit_info generics [] in
   let parent_clauses =
     List.map
-      (translate_trait_clause trait_decl.item_meta.span)
+      (translate_trait_clause (Some trait_decl.item_meta.span))
       llbc_parent_clauses
   in
   let consts =
     List.map
       (fun (name, ty) ->
-        (name, translate_fwd_ty trait_decl.item_meta.span type_infos ty))
+        (name, translate_fwd_ty (Some trait_decl.item_meta.span) type_infos ty))
       consts
   in
   {
@@ -4063,6 +4106,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     name;
     item_meta;
     generics;
+    explicit_info;
     llbc_generics;
     preds;
     parent_clauses;
@@ -4091,8 +4135,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   let span = item_meta.span in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
-    translate_trait_decl_ref span
-      (translate_fwd_ty span type_infos)
+    translate_trait_decl_ref (Some span)
+      (translate_fwd_ty (Some span) type_infos)
       llbc_impl_trait
   in
   let name =
@@ -4100,21 +4144,23 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       item_meta.name
   in
-  let generics, preds = translate_generic_params span llbc_generics in
+  let generics, preds = translate_generic_params (Some span) llbc_generics in
+  let explicit_info = compute_explicit_info generics [] in
   let parent_trait_refs =
-    List.map (translate_strait_ref span) parent_trait_refs
+    List.map (translate_strait_ref (Some span)) parent_trait_refs
   in
   let consts =
     List.map
       (fun (name, gref) ->
         ( name,
-          translate_global_decl_ref span (translate_fwd_ty span type_infos) gref
-        ))
+          translate_global_decl_ref (Some span)
+            (translate_fwd_ty (Some span) type_infos)
+            gref ))
       consts
   in
   let types =
     List.map
-      (fun (name, ty) -> (name, translate_fwd_ty span type_infos ty))
+      (fun (name, ty) -> (name, translate_fwd_ty (Some span) type_infos ty))
       types
   in
   {
@@ -4124,6 +4170,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     impl_trait;
     llbc_impl_trait;
     generics;
+    explicit_info;
     llbc_generics;
     preds;
     parent_trait_refs;
@@ -4151,9 +4198,12 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
       item_meta.name
   in
   let generics, preds =
-    translate_generic_params decl.item_meta.span llbc_generics
+    translate_generic_params (Some decl.item_meta.span) llbc_generics
+  in
+  let explicit_info = compute_explicit_info generics [] in
+  let ty =
+    translate_fwd_ty (Some decl.item_meta.span) ctx.type_ctx.type_infos ty
   in
-  let ty = translate_fwd_ty decl.item_meta.span ctx.type_ctx.type_infos ty in
   {
     span = item_meta.span;
     def_id;
@@ -4161,6 +4211,7 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
     name;
     llbc_generics;
     generics;
+    explicit_info;
     preds;
     ty;
     kind;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6465efe42..b39a2cb38 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -4,6 +4,7 @@ open Values
 open LlbcAst
 open Contexts
 open Errors
+open Assumed
 module SA = SymbolicAst
 module Micro = PureMicroPasses
 open TranslateCore
@@ -1013,6 +1014,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     translate_crate_to_pure crate
   in
 
+  (* Translate the signatures of the builtin functions *)
+  let builtin_sigs =
+    AssumedFunIdMap.map
+      (fun (info : assumed_fun_info) ->
+        SymbolicToPure.translate_fun_sig trans_ctx (FAssumed info.fun_id)
+          info.name info.fun_sig
+          (List.map (fun _ -> None) info.fun_sig.inputs))
+      assumed_fun_infos
+  in
+
   (* Initialize the names map by registering the keywords used in the
      language, as well as some primitive names ("u32", etc.).
      We insert the names of the local declarations later. *)
@@ -1080,6 +1091,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       trans_trait_impls;
       trans_types;
       trans_funs;
+      builtin_sigs;
       functions_with_decreases_clause = rec_functions;
       types_filter_type_args_map = Pure.TypeDeclId.Map.empty;
       funs_filter_type_args_map = Pure.FunDeclId.Map.empty;