Start adding support for traits

31 files changed, 1258 insertions, 776 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
new file mode 100644
index 00000000..4e5625cb
--- /dev/null
+++ b/compiler/AssociatedTypes.ml
@@ -0,0 +1,91 @@
+(** This file implements utilities to handle trait associated types, in
+    particular with normalization helpers.
+
+    When normalizing a type, we simplify the references to the trait associated
+    types, and choose a representative when there are equalities between types
+    enforced by local clauses (i.e., clauses of the shape [where Trait1::T = Trait2::U]).
+ *)
+
+module T = Types
+module TU = TypesUtils
+module V = Values
+module E = Expressions
+module A = LlbcAst
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+
+(** The local logger *)
+let log = L.associated_types_log
+
+(** Normalize a type by simplyfying the references to trait associated types
+    and choosing a representative when there are equalities between types
+    enforced by local clauses (i.e., `where Trait1::T = Trait2::U`. *)
+let ctx_normalize_type (_ctx : C.eval_ctx) (_ty : 'r T.ty) : 'r T.ty =
+  raise (Failure "Unimplemented")
+
+(** Same as [type_decl_get_instantiated_variants_fields_rtypes] but normalizes the types *)
+let type_decl_get_inst_norm_variants_fields_rtypes (ctx : C.eval_ctx)
+    (def : T.type_decl) (generics : T.rgeneric_args) :
+    (T.VariantId.id option * T.rty list) list =
+  let res =
+    Subst.type_decl_get_instantiated_variants_fields_rtypes def generics
+  in
+  List.map
+    (fun (variant_id, types) ->
+      (variant_id, List.map (ctx_normalize_type ctx) types))
+    res
+
+(** Same as [type_decl_get_instantiated_field_rtypes] but normalizes the types *)
+let type_decl_get_inst_norm_field_rtypes (ctx : C.eval_ctx) (def : T.type_decl)
+    (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) :
+    T.rty list =
+  let types =
+    Subst.type_decl_get_instantiated_field_rtypes def opt_variant_id generics
+  in
+  List.map (ctx_normalize_type ctx) types
+
+(** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *)
+let ctx_adt_value_get_inst_norm_field_rtypes (ctx : C.eval_ctx)
+    (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) :
+    T.rty list =
+  let types =
+    Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id generics
+  in
+  List.map (ctx_normalize_type ctx) types
+
+(** Same as [ctx_adt_value_get_instantiated_field_etypes] but normalizes the types *)
+let type_decl_get_inst_norm_field_etypes (ctx : C.eval_ctx) (def : T.type_decl)
+    (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) :
+    T.ety list =
+  let types =
+    Subst.type_decl_get_instantiated_field_etypes def opt_variant_id generics
+  in
+  List.map (ctx_normalize_type ctx) types
+
+(** Same as [ctx_adt_get_instantiated_field_etypes] but normalizes the types *)
+let ctx_adt_get_inst_norm_field_etypes (ctx : C.eval_ctx)
+    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
+    (generics : T.egeneric_args) : T.ety list =
+  let types =
+    Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
+      generics
+  in
+  List.map (ctx_normalize_type ctx) types
+
+(** Same as [substitute_signature] but normalizes the types *)
+let ctx_subst_norm_signature (ctx : C.eval_ctx)
+    (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
+    (r_subst : T.RegionVarId.id -> T.RegionId.id)
+    (ty_subst : T.TypeVarId.id -> T.rty)
+    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
+    (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id)
+    (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+  let sg =
+    Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self
+      sg
+  in
+  let { A.regions_hierarchy; inputs; output } = sg in
+  let inputs = List.map (ctx_normalize_type ctx) inputs in
+  let output = ctx_normalize_type ctx output in
+  { regions_hierarchy; inputs; output }
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 25462504..e156c335 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -63,75 +63,81 @@ module Sig = struct
 
   let empty_const_generic_params : T.const_generic_var list = []
 
+  let mk_generic_args regions types const_generics : T.sgeneric_args =
+    { regions; types; const_generics; trait_refs = [] }
+
+  let mk_generic_params regions types const_generics : T.generic_params =
+    { regions; types; const_generics; trait_clauses = [] }
+
   let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) :
       T.sty =
     let ref_kind = if is_mut then T.Mut else T.Shared in
     mk_ref_ty r ty ref_kind
 
   let mk_array_ty (ty : T.sty) (cg : T.const_generic) : T.sty =
-    Adt (Assumed Array, [], [ ty ], [ cg ])
+    Adt (Assumed Array, mk_generic_args [] [ ty ] [ cg ])
+
+  let mk_slice_ty (ty : T.sty) : T.sty =
+    Adt (Assumed Slice, mk_generic_args [] [ ty ] [])
 
-  let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, [], [ ty ], [])
-  let range_ty : T.sty = Adt (Assumed Range, [], [ usize_ty ], [])
+  let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] [])
+
+  let mk_sig generics regions_hierarchy inputs output : A.fun_sig =
+    let preds : T.predicates =
+      { regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
+    in
+    {
+      generics;
+      preds;
+      parent_params_info = None;
+      regions_hierarchy;
+      inputs;
+      output;
+    }
 
   (** [fn<T>(&'a mut T, T) -> T] *)
   let mem_replace_sig : A.fun_sig =
     (* The signature fields *)
-    let region_params = [ region_param_0 ] (* <'a> *) in
+    let regions = [ region_param_0 ] (* <'a> *) in
     let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
+    let types = [ type_param_0 ] (* <T> *) in
+    let generics = mk_generic_params regions types [] in
     let inputs =
       [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ]
     in
     let output = tvar_0 (* T *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(T) -> Box<T>] *)
   let box_new_sig : A.fun_sig =
-    {
-      region_params = [];
-      regions_hierarchy = [];
-      type_params = [ type_param_0 ] (* <T> *);
-      const_generic_params = empty_const_generic_params;
-      inputs = [ tvar_0 (* T *) ];
-      output = mk_box_ty tvar_0 (* Box<T> *);
-    }
+    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
+    let regions_hierarchy = [] in
+    let inputs = [ tvar_0 (* T *) ] in
+    let output = mk_box_ty tvar_0 (* Box<T> *) in
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(Box<T>) -> ()] *)
   let box_free_sig : A.fun_sig =
-    {
-      region_params = [];
-      regions_hierarchy = [];
-      type_params = [ type_param_0 ] (* <T> *);
-      const_generic_params = empty_const_generic_params;
-      inputs = [ mk_box_ty tvar_0 (* Box<T> *) ];
-      output = mk_unit_ty (* () *);
-    }
+    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
+    let regions_hierarchy = [] in
+    let inputs = [ mk_box_ty tvar_0 (* Box<T> *) ] in
+    let output = mk_unit_ty (* () *) in
+    mk_sig generics regions_hierarchy inputs output
 
   (** Helper for [Box::deref_shared] and [Box::deref_mut].
       Returns:
       [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T]
   *)
   let box_deref_gen_sig (is_mut : bool) : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params = [ type_param_0 ] (* <T> *);
-      const_generic_params = empty_const_generic_params;
-      inputs =
-        [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ];
-      output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *);
-    }
+    let inputs =
+      [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]
+    in
+    let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<'a, T>(&'a Box<T>) -> &'a T] *)
   let box_deref_shared_sig = box_deref_gen_sig false
@@ -141,26 +147,18 @@ module Sig = struct
 
   (** [fn<T>() -> Vec<T>] *)
   let vec_new_sig : A.fun_sig =
-    let region_params = [] in
+    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
     let regions_hierarchy = [] in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs = [] in
     let output = mk_vec_ty tvar_0 (* Vec<T> *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(&'a mut Vec<T>, T)] *)
   let vec_push_sig : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [
         mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
@@ -168,21 +166,14 @@ module Sig = struct
       ]
     in
     let output = mk_unit_ty (* () *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(&'a mut Vec<T>, usize, T)] *)
   let vec_insert_sig : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [
         mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
@@ -191,42 +182,28 @@ module Sig = struct
       ]
     in
     let output = mk_unit_ty (* () *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(&'a Vec<T>) -> usize] *)
   let vec_len_sig : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ]
     in
     let output = mk_usize_ty (* usize *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** Helper:
       [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T]
    *)
   let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [
         mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
@@ -234,14 +211,7 @@ module Sig = struct
       ]
     in
     let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *)
   let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false
@@ -266,10 +236,10 @@ module Sig = struct
   let mk_array_slice_borrow_sig (cgs : T.const_generic_var list)
       (input_ty : T.TypeVarId.id -> T.sty) (index_ty : T.sty option)
       (output_ty : T.TypeVarId.id -> T.sty) (is_mut : bool) : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [
         mk_ref_ty rvar_0
@@ -285,14 +255,7 @@ module Sig = struct
         (output_ty type_param_0.index)
         is_mut (* &'a (mut) output_ty<T> *)
     in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = cgs;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 
   let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig =
     (* Array<T, N> *)
@@ -342,22 +305,15 @@ module Sig = struct
       [fn<T>(&'a [T]) -> usize]
    *)
   let slice_len_sig : A.fun_sig =
-    (* The signature fields *)
-    let region_params = [ region_param_0 ] in
+    let generics =
+      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
+    in
     let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let type_params = [ type_param_0 ] (* <T> *) in
     let inputs =
       [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ]
     in
     let output = mk_usize_ty (* usize *) in
-    {
-      region_params;
-      regions_hierarchy;
-      type_params;
-      const_generic_params = empty_const_generic_params;
-      inputs;
-      output;
-    }
+    mk_sig generics regions_hierarchy inputs output
 end
 
 type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 14b5d559..2d396924 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -255,11 +255,28 @@ type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
 type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
 
+type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t }
+[@@deriving show]
+
+type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t }
+[@@deriving show]
+
+type decls_ctx = {
+  type_ctx : type_context;
+  fun_ctx : fun_context;
+  global_ctx : global_context;
+  trait_decls_ctx : trait_decls_context;
+  trait_impls_ctx : trait_impls_context;
+}
+[@@deriving show]
+
 (** Evaluation context *)
 type eval_ctx = {
   type_context : type_context;
   fun_context : fun_context;
   global_context : global_context;
+  trait_decls_context : trait_decls_context;
+  trait_impls_context : trait_impls_context;
   region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
@@ -267,6 +284,7 @@ type eval_ctx = {
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
+  trait_clauses : etrait_ref list;
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -308,6 +326,12 @@ let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
     global_decl =
   GlobalDeclId.Map.find gid ctx.global_context.global_decls
 
+let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl =
+  TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls
+
+let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
+  TraitImplId.Map.find id ctx.trait_impls_context.trait_impls
+
 (** Retrieve a variable's value in the current frame *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
   snd (env_lookup_var env vid)
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index b72fa078..f4406653 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -70,14 +70,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
           method! visit_rvalue _env rv =
             match rv with
-            | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> ()
+            | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> ()
             | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
                 can_fail := EU.binop_can_fail bop || !can_fail
 
           method! visit_Call env call =
             (match call.func with
-            | Regular id ->
+            | FunId (Regular id) ->
                 if FunDeclId.Set.mem id fun_ids then (
                   can_diverge := true;
                   is_rec := true)
@@ -86,9 +86,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
                   self#may_fail info.can_fail;
                   stateful := !stateful || info.stateful;
                   can_diverge := !can_diverge || info.can_diverge
-            | Assumed id ->
+            | FunId (Assumed id) ->
                 (* None of the assumed functions can diverge nor are considered stateful *)
-                can_fail := !can_fail || Assumed.assumed_can_fail id);
+                can_fail := !can_fail || Assumed.assumed_can_fail id
+            | TraitMethod _ ->
+                (* We consider trait functions can fail, diverge, and are not stateful *)
+                can_fail := true;
+                can_diverge := true);
             super#visit_Call env call
 
           method! visit_Panic env =
@@ -141,7 +145,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
   let rec analyze_decl_groups (decls : declaration_group list) : unit =
     match decls with
     | [] -> ()
-    | Type _ :: decls' -> analyze_decl_groups decls'
+    | (Type _ | TraitDecl _ | TraitImpl _) :: decls' ->
+        analyze_decl_groups decls'
     | Fun decl :: decls' ->
         analyze_fun_decl_group decl;
         analyze_decl_groups decls'
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 37eeb333..eb66013d 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -12,27 +12,30 @@ module SA = SymbolicAst
 (** The local logger *)
 let log = L.interpreter_log
 
-let compute_type_fun_global_contexts (m : A.crate) :
-    C.type_context * C.fun_context * C.global_context =
-  let type_decls_list, _, _ = split_declarations m.declarations in
+let compute_contexts (m : A.crate) : C.decls_ctx =
+  let type_decls_list, _, _, _, _ = split_declarations m.declarations in
   let type_decls = m.types in
   let fun_decls = m.functions in
   let global_decls = m.globals in
-  let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
+  let trait_decls = m.trait_decls in
+  let trait_impls = m.trait_impls in
+  let type_decls_groups, _, _, _, _ =
     split_declarations_to_group_maps m.declarations
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list
   in
-  let type_context = { C.type_decls_groups; type_decls; type_infos } in
-  let fun_context = { C.fun_decls } in
-  let global_context = { C.global_decls } in
-  (type_context, fun_context, global_context)
-
-let initialize_eval_context (type_context : C.type_context)
-    (fun_context : C.fun_context) (global_context : C.global_context)
+  let type_ctx = { C.type_decls_groups; type_decls; type_infos } in
+  let fun_ctx = { C.fun_decls } in
+  let global_ctx = { C.global_decls } in
+  let trait_decls_ctx = { C.trait_decls } in
+  let trait_impls_ctx = { C.trait_impls } in
+  { C.type_ctx; fun_ctx; global_ctx; trait_decls_ctx; trait_impls_ctx }
+
+let initialize_eval_context (ctx : C.decls_ctx)
     (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list)
-    (const_generic_vars : T.const_generic_var list) : C.eval_ctx =
+    (const_generic_vars : T.const_generic_var list)
+    (trait_clauses : T.etrait_ref list) : C.eval_ctx =
   C.reset_global_counters ();
   let const_generic_vars_map =
     T.ConstGenericVarId.Map.of_list
@@ -44,33 +47,35 @@ let initialize_eval_context (type_context : C.type_context)
          const_generic_vars)
   in
   {
-    C.type_context;
-    C.fun_context;
-    C.global_context;
+    C.type_context = ctx.type_ctx;
+    C.fun_context = ctx.fun_ctx;
+    C.global_context = ctx.global_ctx;
+    C.trait_decls_context = ctx.trait_decls_ctx;
+    C.trait_impls_context = ctx.trait_impls_ctx;
     C.region_groups;
     C.type_vars;
     C.const_generic_vars;
     C.const_generic_vars_map;
+    C.trait_clauses;
     C.env = [ C.Frame ];
     C.ended_regions = T.RegionId.Set.empty;
   }
 
 (** Initialize an evaluation context to execute a function.
 
-      Introduces local variables initialized in the following manner:
-      - input arguments are initialized as symbolic values
-      - the remaining locals are initialized as [⊥]
-      Abstractions are introduced for the regions present in the function
-      signature.
-      
-      We return:
-      - the initialized evaluation context
-      - the list of symbolic values introduced for the input values
-      - the instantiated function signature
+    Introduces local variables initialized in the following manner:
+    - input arguments are initialized as symbolic values
+    - the remaining locals are initialized as [⊥]
+    Abstractions are introduced for the regions present in the function
+    signature.
+
+    We return:
+    - the initialized evaluation context
+    - the list of symbolic values introduced for the input values
+    - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun (type_context : C.type_context)
-    (fun_context : C.fun_context) (global_context : C.global_context)
-    (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
+let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl)
+    : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
    * with the input values (which behave as if they had been returned
@@ -88,8 +93,8 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
     List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
   in
   let ctx =
-    initialize_eval_context type_context fun_context global_context
-      region_groups sg.type_params sg.const_generic_params
+    initialize_eval_context ctx region_groups sg.generics.types
+      sg.generics.const_generics sg.generics.trait_clauses
   in
   (* Instantiate the signature *)
   let type_params =
@@ -508,17 +513,12 @@ module Test = struct
       (lazy ("test_unit_function: " ^ Print.fun_name_to_string fdef.A.name));
 
     (* Sanity check - *)
-    assert (List.length fdef.A.signature.region_params = 0);
-    assert (List.length fdef.A.signature.type_params = 0);
+    assert (fdef.A.signature.generics = TypesUtils.mk_empty_generic_params);
     assert (body.A.arg_count = 0);
 
     (* Create the evaluation context *)
-    let type_context, fun_context, global_context =
-      compute_type_fun_global_contexts crate
-    in
-    let ctx =
-      initialize_eval_context type_context fun_context global_context [] [] []
-    in
+    let decls_ctx = compute_contexts crate in
+    let ctx = initialize_eval_context decls_ctx [] [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
@@ -546,9 +546,7 @@ module Test = struct
       (no parameters, no arguments) - TODO: move *)
   let fun_decl_is_transparent_unit (def : A.fun_decl) : bool =
     Option.is_some def.body
-    && def.A.signature.region_params = []
-    && def.A.signature.type_params = []
-    && def.A.signature.const_generic_params = []
+    && def.A.signature.generics = TypesUtils.mk_empty_generic_params
     && def.A.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)
@@ -562,20 +560,4 @@ module Test = struct
       test_unit_function crate def.A.def_id
     in
     A.FunDeclId.Map.iter test_unit_fun unit_funs
-
-  (** Execute the symbolic interpreter on a function. *)
-  let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
-      (fun_context : C.fun_context) (global_context : C.global_context)
-      (fdef : A.fun_decl) : unit =
-    (* Debug *)
-    log#ldebug
-      (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
-
-    (* Evaluate *)
-    let _ =
-      evaluate_function_symbolic synthesize type_context fun_context
-        global_context fdef
-    in
-
-    ()
 end
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index bf083aa4..e7da045c 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -100,15 +100,18 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
     (compare_regions : T.RegionId.id T.region -> T.RegionId.id T.region -> bool)
     (ty1 : T.rty) (ty2 : T.rty) : bool =
   let compare = compare_rtys default combine compare_regions in
+  (* Normalize the associated types *)
   match (ty1, ty2) with
   | T.Literal lit1, T.Literal lit2 ->
       assert (lit1 = lit2);
       default
-  | T.Adt (id1, regions1, tys1, cgs1), T.Adt (id2, regions2, tys2, cgs2) ->
+  | T.Adt (id1, generics1), T.Adt (id2, generics2) ->
       assert (id1 = id2);
       (* There are no regions in the const generics, so we ignore them,
          but we still check they are the same, for sanity *)
-      assert (cgs1 = cgs2);
+      assert (generics1.const_generics = generics2.const_generics);
+
+      (* We also ignore the trait refs *)
 
       (* The check for the ADTs is very crude: we simply compare the arguments
        * two by two.
@@ -123,14 +126,14 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
        * this check would still be a reasonable conservative approximation. *)
 
       (* Check the region parameters *)
-      let regions = List.combine regions1 regions2 in
+      let regions = List.combine generics1.regions generics2.regions in
       let params_b =
         List.fold_left
           (fun b (r1, r2) -> combine b (compare_regions r1 r2))
           default regions
       in
       (* Check the type parameters *)
-      let tys = List.combine tys1 tys2 in
+      let tys = List.combine generics1.types generics2.types in
       let tys_b =
         List.fold_left
           (fun b (ty1, ty2) -> combine b (compare ty1 ty2))
@@ -150,6 +153,11 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
   | T.TypeVar id1, T.TypeVar id2 ->
       assert (id1 = id2);
       default
+  | T.TraitType _, T.TraitType _ ->
+      (* The types should have been normalized. If after normalization we
+         get trait types, we can consider them as variables *)
+      assert (ty1 = ty2);
+      default
   | _ ->
       log#lerror
         (lazy
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 81e73e3e..ea692386 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -9,6 +9,7 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open TypesUtils
 module Inv = Invariants
@@ -204,7 +205,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
   apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
     expansion ctx
 
-(** Compute the expansion of a non-assumed (i.e.: not [Option], [Box], etc.)
+(** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
     adt value.
 
     The function might return a list of values if the symbolic value to expand
@@ -214,18 +215,15 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (def_id : T.TypeDeclId.id)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) (ctx : C.eval_ctx) : V.symbolic_expansion list
-    =
+    (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (generics : T.rgeneric_args)
+    (ctx : C.eval_ctx) : V.symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = C.ctx_lookup_type_decl ctx def_id in
-  assert (List.length regions = List.length def.T.region_params);
+  assert (List.length generics.regions = List.length def.T.generics.regions);
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
-    Subst.type_decl_get_instantiated_variants_fields_rtypes def regions types
-      cgs
+    Assoc.type_decl_get_inst_norm_variants_fields_rtypes ctx def generics
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
@@ -280,15 +278,14 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (adt_id : T.type_id)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) (ctx : C.eval_ctx) : V.symbolic_expansion list
-    =
-  match (adt_id, regions, types) with
+    (kind : V.sv_kind) (adt_id : T.type_id) (generics : T.rgeneric_args)
+    (ctx : C.eval_ctx) : V.symbolic_expansion list =
+  match (adt_id, generics.regions, generics.types) with
   | T.AdtId def_id, _, _ ->
       compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
-        def_id regions types cgs ctx
-  | T.Tuple, [], _ -> [ compute_expanded_symbolic_tuple_value kind types ]
+        def_id generics ctx
+  | T.Tuple, [], _ ->
+      [ compute_expanded_symbolic_tuple_value kind generics.types ]
   | T.Assumed T.Option, [], [ ty ] ->
       compute_expanded_symbolic_option_value expand_enumerations kind ty
   | T.Assumed T.Box, [], [ boxed_ty ] ->
@@ -543,12 +540,12 @@ let expand_symbolic_value_no_branching (config : C.config)
    fun cf ctx ->
     match rty with
     (* ADTs *)
-    | T.Adt (adt_id, regions, types, cgs) ->
+    | T.Adt (adt_id, generics) ->
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
           compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
-            regions types cgs ctx
+            generics ctx
         in
         (* There should be exacly one branch *)
         let see = Collections.List.to_cons_nil seel in
@@ -600,12 +597,12 @@ let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
   (* Execute *)
   match rty with
   (* ADTs *)
-  | T.Adt (adt_id, regions, types, cgs) ->
+  | T.Adt (adt_id, generics) ->
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
         compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
-          regions types cgs ctx
+          generics ctx
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
@@ -679,7 +676,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
           ^ symbolic_value_to_string ctx sv));
       let cc : cm_fun =
         match sv.V.sv_ty with
-        | T.Adt (AdtId def_id, _, _, _) ->
+        | T.Adt (AdtId def_id, _) ->
             (* {!expand_symbolic_value_no_branching} checks if there are branchings,
              * but we prefer to also check it here - this leads to cleaner messages
              * and debugging *)
@@ -704,16 +701,16 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
                      [config]): "
                    ^ Print.name_to_string def.name))
             else expand_symbolic_value_no_branching config sv None
-        | T.Adt ((Tuple | Assumed Box), _, _, _) | T.Ref (_, _, _) ->
+        | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config sv None
-        | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _, _, _)
-          ->
+        | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) ->
             (* We can't expand those *)
             raise
               (Failure
                  "Attempted to greedily expand an ADT which can't be expanded ")
-        | T.TypeVar _ | T.Literal _ | Never -> raise (Failure "Unreachable")
+        | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ ->
+            raise (Failure "Unreachable")
       in
       (* Compose and continue *)
       comp cc expand cf ctx
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 2f6a7b49..51f6ff05 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -7,6 +7,7 @@ module E = Expressions
 open Utils
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open TypesUtils
 open ValuesUtils
@@ -141,11 +142,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
   | V.Adt av ->
       (* Sanity check *)
       (match v.V.ty with
-      | T.Adt (T.Assumed (T.Box | Vec), _, _, _) ->
+      | T.Adt (T.Assumed (T.Box | Vec), _) ->
           raise (Failure "Can't copy an assumed value other than Option")
-      | T.Adt (T.AdtId _, _, _, _) -> assert allow_adt_copy
-      | T.Adt ((T.Assumed Option | T.Tuple), _, _, _) -> () (* Ok *)
-      | T.Adt (T.Assumed (Slice | T.Array), [], [ ty ], []) ->
+      | T.Adt (T.AdtId _, _) -> assert allow_adt_copy
+      | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *)
+      | T.Adt
+          ( T.Assumed (Slice | T.Array),
+            {
+              regions = [];
+              types = [ ty ];
+              const_generics = [];
+              trait_refs = [];
+            } ) ->
           assert (ty_is_primitively_copyable ty)
       | _ -> raise (Failure "Unreachable"));
       let ctx, fields =
@@ -263,6 +271,9 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
       match cv.value with
       | E.CLiteral lit ->
           cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
+      | E.TraitConst (_trait_ref, _generics, _const_name) ->
+          (* TODO *)
+          raise (Failure "Unimplemented")
       | E.CVar vid -> (
           let ctx0 = ctx in
           (* Lookup the const generic value *)
@@ -681,7 +692,8 @@ let eval_rvalue_aggregate (config : C.config)
     | E.AggregatedTuple ->
         let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
         let v = V.Adt { variant_id = None; field_values = values } in
-        let ty = T.Adt (T.Tuple, [], tys, []) in
+        let generics = TypesUtils.mk_generic_args [] tys [] [] in
+        let ty = T.Adt (T.Tuple, generics) in
         let aggregated : V.typed_value = { V.value = v; ty } in
         (* Call the continuation *)
         cf aggregated ctx
@@ -692,20 +704,22 @@ let eval_rvalue_aggregate (config : C.config)
           assert (List.length values = 1)
         else raise (Failure "Unreachable");
         (* Construt the value *)
-        let aty = T.Adt (T.Assumed T.Option, [], [ ty ], []) in
+        let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in
+        let aty = T.Adt (T.Assumed T.Option, generics) in
         let av : V.adt_value =
           { V.variant_id = Some variant_id; V.field_values = values }
         in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
-    | E.AggregatedAdt (def_id, opt_variant_id, regions, types, cgs) ->
+    | E.AggregatedAdt (def_id, opt_variant_id, generics) ->
         (* Sanity checks *)
         let type_decl = C.ctx_lookup_type_decl ctx def_id in
-        assert (List.length type_decl.region_params = List.length regions);
+        assert (
+          List.length type_decl.generics.regions = List.length generics.regions);
         let expected_field_types =
-          Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
-            types cgs
+          Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
+            generics
         in
         assert (
           expected_field_types
@@ -714,7 +728,7 @@ let eval_rvalue_aggregate (config : C.config)
         let av : V.adt_value =
           { V.variant_id = opt_variant_id; V.field_values = values }
         in
-        let aty = T.Adt (T.AdtId def_id, regions, types, cgs) in
+        let aty = T.Adt (T.AdtId def_id, generics) in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
@@ -734,7 +748,8 @@ let eval_rvalue_aggregate (config : C.config)
         let av : V.adt_value =
           { V.variant_id = None; V.field_values = values }
         in
-        let aty = T.Adt (T.Assumed T.Range, [], [ ety ], []) in
+        let generics = TypesUtils.mk_generic_args_from_types [ ety ] in
+        let aty = T.Adt (T.Assumed T.Range, generics) in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
@@ -744,7 +759,8 @@ let eval_rvalue_aggregate (config : C.config)
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
         assert (len = Z.of_int (List.length values));
-        let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in
+        let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
+        let ty = T.Adt (T.Assumed T.Array, generics) in
         (* In order to generate a better AST, we introduce a symbolic
            value equal to the array. The reason is that otherwise, the
            array we introduce here might be duplicated in the generated
@@ -777,7 +793,7 @@ let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
   (* Delegate to the proper auxiliary function *)
   match rvalue with
   | E.Use op -> comp_wrap (eval_operand config op) ctx
-  | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
+  | E.RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
   | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
   | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
   | E.Aggregate (aggregate_kind, ops) ->
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 10205c27..a34a7d06 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -554,10 +554,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       C.type_context;
       fun_context;
       global_context;
+      trait_decls_context;
+      trait_impls_context;
       region_groups;
       type_vars;
       const_generic_vars;
       const_generic_vars_map;
+      trait_clauses;
       env = _;
       ended_regions = ended_regions0;
     } =
@@ -567,10 +570,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       C.type_context = _;
       fun_context = _;
       global_context = _;
+      trait_decls_context = _;
+      trait_impls_context = _;
       region_groups = _;
       type_vars = _;
       const_generic_vars = _;
       const_generic_vars_map = _;
+      trait_clauses = _;
       env = _;
       ended_regions = ended_regions1;
     } =
@@ -582,10 +588,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
         C.type_context;
         fun_context;
         global_context;
+        trait_decls_context;
+        trait_impls_context;
         region_groups;
         type_vars;
         const_generic_vars;
         const_generic_vars_map;
+        trait_clauses;
         env;
         ended_regions;
       }
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9248e513..8cab546e 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -149,20 +149,25 @@ let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty)
     (match_regions : 'r -> 'r -> 'r) (ty0 : 'r T.ty) (ty1 : 'r T.ty) : 'r T.ty =
   let match_rec = match_types match_distinct_types match_regions in
   match (ty0, ty1) with
-  | Adt (id0, regions0, tys0, cgs0), Adt (id1, regions1, tys1, cgs1) ->
+  | Adt (id0, generics0), Adt (id1, generics1) ->
       assert (id0 = id1);
-      assert (cgs0 = cgs1);
+      assert (generics0.const_generics = generics1.const_generics);
+      assert (generics0.trait_refs = generics1.trait_refs);
       let id = id0 in
-      let cgs = cgs1 in
+      let const_generics = generics1.const_generics in
+      let trait_refs = generics1.trait_refs in
       let regions =
         List.map
           (fun (id0, id1) -> match_regions id0 id1)
-          (List.combine regions0 regions1)
+          (List.combine generics0.regions generics1.regions)
       in
-      let tys =
-        List.map (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1)
+      let types =
+        List.map
+          (fun (ty0, ty1) -> match_rec ty0 ty1)
+          (List.combine generics0.types generics1.types)
       in
-      Adt (id, regions, tys, cgs)
+      let generics = { T.regions; types; const_generics; trait_refs } in
+      Adt (id, generics)
   | TypeVar vid0, TypeVar vid1 ->
       assert (vid0 = vid1);
       let vid = vid0 in
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 04dc8892..465d0028 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -3,6 +3,7 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open Cps
 open ValuesUtils
@@ -97,7 +98,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       match (pe, v.V.value, v.V.ty) with
       | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id),
           V.Adt adt,
-          T.Adt (type_id, _, _, _) ) -> (
+          T.Adt (type_id, _) ) -> (
           (* Check consistency *)
           (match (proj_kind, type_id) with
           | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
@@ -119,8 +120,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
               let updated = { v with value = nadt } in
               Ok (ctx, { res with updated }))
       (* Tuples *)
-      | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _, _)
-        -> (
+      | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _) -> (
           assert (arity = List.length adt.field_values);
           let fv = T.FieldId.nth adt.field_values field_id in
           (* Project *)
@@ -145,9 +145,9 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       (* Box dereferencement *)
       | ( DerefBox,
           Adt { variant_id = None; field_values = [ bv ] },
-          T.Adt (T.Assumed T.Box, _, _, _) ) -> (
-          (* We allow moving inside of boxes. In practice, this kind of
-           * manipulations should happen only inside unsage code, so
+          T.Adt (T.Assumed T.Box, _) ) -> (
+          (* We allow moving outside of boxes. In practice, this kind of
+           * manipulations should happen only inside unsafe code, so
            * it shouldn't happen due to user code, and we leverage it
            * when implementing box dereferencement for the concrete
            * interpreter *)
@@ -357,24 +357,23 @@ let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok ctx -> ctx
 
-let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
+let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (regions : T.erased_region list) (types : T.ety list)
-    (cgs : T.const_generic list) : V.typed_value =
+    (generics : T.egeneric_args) : V.typed_value =
   (* Lookup the definition and check if it is an enumeration - it
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
-  let def = T.TypeDeclId.Map.find def_id tyctx in
-  assert (List.length regions = List.length def.T.region_params);
+  let def = C.ctx_lookup_type_decl ctx def_id in
+  assert (List.length generics.regions = List.length def.T.generics.regions);
   (* Compute the field types *)
   let field_types =
-    Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
+    Assoc.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id generics
   in
   (* Initialize the expanded value *)
   let fields = List.map mk_bottom field_types in
   let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
-  let ty = T.Adt (T.AdtId def_id, regions, types, cgs) in
+  let ty = T.Adt (T.AdtId def_id, generics) in
   { V.value = av; V.ty }
 
 let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
@@ -387,7 +386,8 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
     else raise (Failure "Unreachable")
   in
   let av = V.Adt { variant_id = Some variant_id; field_values } in
-  let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ], []) in
+  let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in
+  let ty = T.Adt (T.Assumed T.Option, generics) in
   { V.value = av; ty }
 
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
@@ -395,7 +395,8 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
   (* Generate the field values *)
   let fields = List.map mk_bottom field_types in
   let v = V.Adt { variant_id = None; field_values = fields } in
-  let ty = T.Adt (T.Tuple, [], field_types, []) in
+  let generics = TypesUtils.mk_generic_args [] field_types [] [] in
+  let ty = T.Adt (T.Tuple, generics) in
   { V.value = v; V.ty }
 
 (** Auxiliary helper to expand {!V.Bottom} values.
@@ -447,19 +448,29 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
     match (pe, ty) with
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
-        T.Adt (T.AdtId def_id', regions, types, cgs) ) ->
+        T.Adt (T.AdtId def_id', generics) ) ->
         assert (def_id = def_id');
-        compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id
-          opt_variant_id regions types cgs
+        compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
     (* Option *)
     | ( Field (ProjOption variant_id, _),
-        T.Adt (T.Assumed T.Option, [], [ ty ], []) ) ->
+        T.Adt
+          ( T.Assumed T.Option,
+            {
+              T.regions = [];
+              types = [ ty ];
+              const_generics = [];
+              trait_refs = [];
+            } ) ) ->
         compute_expanded_bottom_option_value variant_id ty
     (* Tuples *)
-    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) ->
-        assert (arity = List.length tys);
+    | ( Field (ProjTuple arity, _),
+        T.Adt
+          ( T.Tuple,
+            { T.regions = []; types; const_generics = []; trait_refs = [] } ) )
+      ->
+        assert (arity = List.length types);
         (* Generate the field values *)
-        compute_expanded_bottom_tuple_value tys
+        compute_expanded_bottom_tuple_value types
     | _ ->
         raise
           (Failure
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 4a9f3b41..041b0a97 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -3,6 +3,7 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open Cps
 open InterpreterExpansion
@@ -56,12 +57,10 @@ val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
 
 (** Compute an expanded ADT ⊥ value *)
 val compute_expanded_bottom_adt_value :
-  T.type_decl T.TypeDeclId.Map.t ->
+  C.eval_ctx ->
   T.TypeDeclId.id ->
   T.VariantId.id option ->
-  T.erased_region list ->
-  T.ety list ->
-  T.const_generic list ->
+  T.egeneric_args ->
   V.typed_value
 
 (** Compute an expanded [Option] ⊥ value *)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index faed066b..9e0c2b75 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -3,6 +3,7 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open TypesUtils
 open InterpreterUtils
@@ -24,12 +25,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
   else
     match (v.V.value, ty) with
     | V.Literal _, T.Literal _ -> []
-    | V.Adt adt, T.Adt (id, region_params, tys, cgs) ->
+    | V.Adt adt, T.Adt (id, generics) ->
         (* Retrieve the types of the fields *)
         let field_types =
-          Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-            region_params tys cgs
+          Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
         in
+
         (* Project over the field values *)
         let fields_types = List.combine adt.V.field_values field_types in
         let proj_fields =
@@ -103,11 +104,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
     let value : V.avalue =
       match (v.V.value, ty) with
       | V.Literal _, T.Literal _ -> V.AIgnored
-      | V.Adt adt, T.Adt (id, region_params, tys, cgs) ->
+      | V.Adt adt, T.Adt (id, generics) ->
           (* Retrieve the types of the fields *)
           let field_types =
-            Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-              region_params tys cgs
+            Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
           in
           (* Project over the field values *)
           let fields_types = List.combine adt.V.field_values field_types in
@@ -268,8 +268,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
   let (value, ty) : V.avalue * T.rty =
     match (see, original_sv_ty) with
     | SeLiteral _, T.Literal _ -> (V.AIgnored, original_sv_ty)
-    | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys, _cgs)
-      ->
+    | SeAdt (variant_id, field_values), T.Adt (_id, _generics) ->
         (* Project over the field values *)
         let field_values =
           List.map
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 6d520059..d38f8b95 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -17,6 +17,7 @@ open InterpreterProjectors
 open InterpreterExpansion
 open InterpreterPaths
 open InterpreterExpressions
+module PCtx = Print.EvalCtxLlbcAst
 
 (** The local logger *)
 let log = L.statements_log
@@ -232,9 +233,8 @@ let set_discriminant (config : C.config) (p : E.place)
   let update_value cf (v : V.typed_value) : m_fun =
    fun ctx ->
     match (v.V.ty, v.V.value) with
-    | ( T.Adt
-          (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs),
-        V.Adt av ) -> (
+    | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av
+      -> (
         (* There are two situations:
            - either the discriminant is already the proper one (in which case we
              don't do anything)
@@ -251,28 +251,26 @@ let set_discriminant (config : C.config) (p : E.place)
               let bottom_v =
                 match type_id with
                 | T.AdtId def_id ->
-                    compute_expanded_bottom_adt_value
-                      ctx.type_context.type_decls def_id (Some variant_id)
-                      regions types cgs
+                    compute_expanded_bottom_adt_value ctx def_id
+                      (Some variant_id) generics
                 | T.Assumed T.Option ->
-                    assert (regions = []);
+                    assert (generics.regions = []);
                     compute_expanded_bottom_option_value variant_id
-                      (Collections.List.to_cons_nil types)
+                      (Collections.List.to_cons_nil generics.types)
                 | _ -> raise (Failure "Unreachable")
               in
               assign_to_place config bottom_v p (cf Unit) ctx)
-    | ( T.Adt
-          (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs),
-        V.Bottom ) ->
+    | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom
+      ->
         let bottom_v =
           match type_id with
           | T.AdtId def_id ->
-              compute_expanded_bottom_adt_value ctx.type_context.type_decls
-                def_id (Some variant_id) regions types cgs
+              compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
+                generics
           | T.Assumed T.Option ->
-              assert (regions = []);
+              assert (generics.regions = []);
               compute_expanded_bottom_option_value variant_id
-                (Collections.List.to_cons_nil types)
+                (Collections.List.to_cons_nil generics.types)
           | _ -> raise (Failure "Unreachable")
         in
         assign_to_place config bottom_v p (cf Unit) ctx
@@ -301,24 +299,34 @@ let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx =
 let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
 
 (** Small helper: compute the type of the return value for a specific
-    instantiation of a non-local function.
+    instantiation of an assumed function.
  *)
-let get_non_local_function_return_type (fid : A.assumed_fun_id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (const_generic_params : T.const_generic list) : T.ety =
+let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
+    (generics : T.egeneric_args) : T.ety =
+  assert (generics.trait_refs = []);
   (* [Box::free] has a special treatment *)
-  match (fid, region_params, type_params, const_generic_params) with
-  | A.BoxFree, [], [ _ ], [] -> mk_unit_ty
+  match fid with
+  | A.BoxFree ->
+      assert (generics.regions = []);
+      assert (List.length generics.types = 1);
+      assert (generics.const_generics = []);
+      mk_unit_ty
   | _ ->
       (* Retrieve the function's signature *)
       let sg = Assumed.get_assumed_sig fid in
       (* Instantiate the return type  *)
-      let tsubst = Subst.make_type_subst_from_vars sg.type_params type_params in
-      let cgsubst =
-        Subst.make_const_generic_subst_from_vars sg.const_generic_params
-          const_generic_params
+      (* There shouldn't be any reference to Self *)
+      let tr_self : T.erased_region T.trait_instance_id =
+        T.UnknownTrait __FUNCTION__
+      in
+      let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+        Subst.make_esubst_from_generics sg.generics generics tr_self
       in
-      Subst.erase_regions_substitute_types tsubst cgsubst sg.output
+      let ty =
+        Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+          sg.output
+      in
+      Assoc.ctx_normalize_type ctx ty
 
 let move_return_value (config : C.config) (pop_return_value : bool)
     (cf : V.typed_value option -> m_fun) : m_fun =
@@ -418,19 +426,19 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   in
   comp cf_pop cf_assign
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_replace_concrete (_config : C.config)
-    (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_args : T.const_generic list) : cm_fun =
+(** Auxiliary function - see {!eval_assumed_function_call} *)
+let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) :
+    cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_new_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_args : T.const_generic list) : cm_fun =
+(** Auxiliary function - see {!eval_assumed_function_call} *)
+let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
+    cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
-  match (region_params, type_params, cg_args, ctx.env) with
+  match
+    (generics.regions, generics.types, generics.const_generics, ctx.env)
+  with
   | ( [],
       [ boxed_ty ],
       [],
@@ -448,7 +456,8 @@ let eval_box_new_concrete (config : C.config)
       (* Create the new box *)
       let cf_create cf (moved_input_value : V.typed_value) : m_fun =
         (* Create the box value *)
-        let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ], []) in
+        let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in
+        let box_ty = T.Adt (T.Assumed T.Box, generics) in
         let box_v =
           V.Adt { variant_id = None; field_values = [ moved_input_value ] }
         in
@@ -467,13 +476,14 @@ let eval_box_new_concrete (config : C.config)
   | _ -> raise (Failure "Inconsistent state")
 
 (** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
-    and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *)
+    and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *)
 let eval_box_deref_mut_or_shared_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_args : T.const_generic list) (is_mut : bool) : cm_fun =
+    (generics : T.egeneric_args) (is_mut : bool) : cm_fun =
  fun cf ctx ->
   (* Check the arguments *)
-  match (region_params, type_params, cg_args, ctx.env) with
+  match
+    (generics.regions, generics.types, generics.const_generics, ctx.env)
+  with
   | ( [],
       [ boxed_ty ],
       [],
@@ -495,7 +505,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
         { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
       in
       let borrow_kind = if is_mut then E.Mut else E.Shared in
-      let rv = E.Ref (p, borrow_kind) in
+      let rv = E.RvRef (p, borrow_kind) in
       let cf_borrow = eval_rvalue_not_global config rv in
 
       (* Move the borrow to its destination *)
@@ -514,23 +524,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
       comp cf_borrow cf_move cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_deref_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_args : T.const_generic list) : cm_fun =
+(** Auxiliary function - see {!eval_assumed_function_call} *)
+let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) :
+    cm_fun =
   let is_mut = false in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
-    is_mut
+  eval_box_deref_mut_or_shared_concrete config generics is_mut
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_deref_mut_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_args : T.const_generic list) : cm_fun =
+(** Auxiliary function - see {!eval_assumed_function_call} *)
+let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args)
+    : cm_fun =
   let is_mut = true in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
-    is_mut
+  eval_box_deref_mut_or_shared_concrete config generics is_mut
 
-(** Auxiliary function - see {!eval_non_local_function_call}.
+(** Auxiliary function - see {!eval_assumed_function_call}.
 
     [Box::free] is not handled the same way as the other assumed functions:
     - in the regular case, whenever we need to evaluate an assumed function,
@@ -549,11 +555,10 @@ let eval_box_deref_mut_concrete (config : C.config)
     It thus updates the box value (by calling {!drop_value}) and updates
     the destination (by setting it to [()]).
 *)
-let eval_box_free (config : C.config) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_args : T.const_generic list)
+let eval_box_free (config : C.config) (generics : T.egeneric_args)
     (args : E.operand list) (dest : E.place) : cm_fun =
  fun cf ctx ->
-  match (region_params, type_params, cg_args, args) with
+  match (generics.regions, generics.types, generics.const_generics, args) with
   | [], [ boxed_ty ], [], [ E.Move input_box_place ] ->
       (* Required type checking *)
       let input_box = InterpreterPaths.read_place Write input_box_place ctx in
@@ -570,20 +575,18 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       cc cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
+(** Auxiliary function - see {!eval_assumed_function_call} *)
 let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
-    (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_args : T.const_generic list) : cm_fun =
+    (_generics : T.egeneric_args) : cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
 (** Evaluate a non-local function call in concrete mode *)
-let eval_non_local_function_call_concrete (config : C.config)
-    (fid : A.assumed_fun_id) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_args : T.const_generic list)
+let eval_assumed_function_call_concrete (config : C.config)
+    (fid : A.assumed_fun_id) (generics : T.egeneric_args)
     (args : E.operand list) (dest : E.place) : cm_fun =
   (* Sanity check: we don't fully handle the const generic vars environment
      in concrete mode yet *)
-  assert (cg_args = []);
+  assert (generics.const_generics = []);
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
@@ -592,7 +595,7 @@ let eval_non_local_function_call_concrete (config : C.config)
   match fid with
   | A.BoxFree ->
       (* Degenerate case: box_free *)
-      eval_box_free config region_params type_params cg_args args dest
+      eval_box_free config generics args dest
   | _ ->
       (* "Normal" case: not box_free *)
       (* Evaluate the operands *)
@@ -607,16 +610,14 @@ let eval_non_local_function_call_concrete (config : C.config)
        * but it made it less clear where the computed values came from,
        * so we reversed the modifications. *)
       let cf_eval_call cf (args_vl : V.typed_value list) : m_fun =
+       fun ctx ->
         (* Push the stack frame: we initialize the frame with the return variable,
            and one variable per input argument *)
         let cc = push_frame in
 
         (* Create and push the return variable *)
         let ret_vid = E.VarId.zero in
-        let ret_ty =
-          get_non_local_function_return_type fid region_params type_params
-            cg_args
-        in
+        let ret_ty = get_assumed_function_return_type ctx fid generics in
         let ret_var = mk_var ret_vid (Some "@return") ret_ty in
         let cc = comp cc (push_uninitialized_var ret_var) in
 
@@ -633,20 +634,14 @@ let eval_non_local_function_call_concrete (config : C.config)
          * access to a body. *)
         let cf_eval_body : cm_fun =
           match fid with
-          | A.Replace ->
-              eval_replace_concrete config region_params type_params cg_args
-          | BoxNew ->
-              eval_box_new_concrete config region_params type_params cg_args
-          | BoxDeref ->
-              eval_box_deref_concrete config region_params type_params cg_args
-          | BoxDerefMut ->
-              eval_box_deref_mut_concrete config region_params type_params
-                cg_args
+          | A.Replace -> eval_replace_concrete config generics
+          | BoxNew -> eval_box_new_concrete config generics
+          | BoxDeref -> eval_box_deref_concrete config generics
+          | BoxDerefMut -> eval_box_deref_mut_concrete config generics
           | BoxFree ->
               (* Should have been treated above *) raise (Failure "Unreachable")
           | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
-              eval_vec_function_concrete config fid region_params type_params
-                cg_args
+              eval_vec_function_concrete config fid generics
           | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
           | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
           | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
@@ -660,13 +655,13 @@ let eval_non_local_function_call_concrete (config : C.config)
         let cc = comp cc (pop_frame_assign config dest) in
 
         (* Continue *)
-        cc cf
+        cc cf ctx
       in
       (* Compose and apply *)
       comp cf_eval_ops cf_eval_call
 
-let instantiate_fun_sig (type_params : T.ety list)
-    (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
+let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args)
+    (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
@@ -685,7 +680,7 @@ let instantiate_fun_sig (type_params : T.ety list)
     T.RegionGroupId.Map.find rg_id asubst_map
   in
   (* Generate fresh regions and their substitutions *)
-  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in
+  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in
   (* Generate the type substitution
    * Note that we need the substitution to map the type variables to
    * {!rty} types (not {!ety}). In order to do that, we convert the
@@ -694,13 +689,28 @@ let instantiate_fun_sig (type_params : T.ety list)
    * This is a current limitation of the analysis: there is still some
    * work to do to properly handle full type parametrization.
    * *)
-  let rtype_params = List.map ety_no_regions_to_rty type_params in
-  let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in
+  let rtype_params = List.map ety_no_regions_to_rty generics.types in
+  let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in
   let cgsubst =
-    Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args
+    Subst.make_const_generic_subst_from_vars sg.generics.const_generics
+      generics.const_generics
+  in
+  (* TODO: something annoying with the trait ref subst: we need to use region
+     types, but the arguments use erased regions. For now we use the fact
+     that no regions should appear inside. In the future: we should merge
+     ety and rty. *)
+  let trait_refs =
+    List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref
+      generics.trait_refs
+  in
+  let tr_subst =
+    Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs
   in
   (* Substitute the signature *)
-  let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in
+  let inst_sig =
+    Assoc.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst
+      tr_self sg
+  in
   (* Return *)
   inst_sig
 
@@ -839,7 +849,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
                   match rvalue with
                   | E.Global _ -> raise (Failure "Unreachable")
                   | E.Use _
-                  | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow))
+                  | E.RvRef (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow))
                   | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _
                   | E.Aggregate _ ->
                       let rp = rvalue_get_place rvalue in
@@ -896,7 +906,9 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      (eval_local_function_call_concrete config global.body_id [] [] [] [] dest)
+      let generics = TypesUtils.mk_empty_generic_args in
+      (eval_transparent_function_call_concrete config global.body_id generics []
+         dest)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -1040,26 +1052,26 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
 and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
-  (* There are two cases:
+  (* There are several cases:
      - this is a local function, in which case we execute its body
-     - this is a non-local function, in which case there is a special treatment
+     - this is an assumed function, in which case there is a special treatment
+     - this is a trait method
   *)
   match call.func with
-  | A.Regular fid ->
-      eval_local_function_call config fid call.region_args call.type_args
-        call.const_generic_args call.args call.dest
-  | A.Assumed fid ->
-      eval_non_local_function_call config fid call.region_args call.type_args
-        call.const_generic_args call.args call.dest
+  | A.FunId (A.Regular fid) ->
+      eval_transparent_function_call config fid call.generics call.args
+        call.dest
+  | A.FunId (A.Assumed fid) ->
+      eval_assumed_function_call config fid call.generics call.args call.dest
+  | A.TraitMethod _ -> raise (Failure "Unimplemented")
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
-    (_region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+and eval_transparent_function_call_concrete (config : C.config)
+    (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list)
+    (dest : E.place) : st_cm_fun =
   (* Sanity check: we don't fully handle the const generic vars environment
      in concrete mode yet *)
-  assert (cg_args = []);
+  assert (generics.const_generics = []);
   fun cf ctx ->
     (* Retrieve the (correctly instantiated) body *)
     let def = C.ctx_lookup_fun_decl ctx fid in
@@ -1073,16 +1085,14 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
                ^ Print.name_to_string def.name))
       | Some body -> body
     in
-    let tsubst =
-      Subst.make_type_subst_from_vars def.A.signature.type_params type_args
-    in
-    let cgsubst =
-      Subst.make_const_generic_subst_from_vars
-        def.A.signature.const_generic_params cg_args
-    in
-    let locals, body_st =
-      Subst.fun_body_substitute_in_body tsubst cgsubst body
+    (* TODO: we need to normalize the types if we want to correctly support traits *)
+    assert (ctx.trait_clauses = [] && generics.trait_refs = []);
+    (* There shouldn't be any reference to Self *)
+    let tr_self = T.UnknownTrait __FUNCTION__ in
+    let subst =
+      Subst.make_esubst_from_generics def.A.signature.generics generics tr_self
     in
+    let locals, body_st = Subst.fun_body_substitute_in_body subst body in
 
     (* Evaluate the input operands *)
     assert (List.length args = body.A.arg_count);
@@ -1139,22 +1149,23 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
     cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
-    (region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+and eval_transparent_function_call_symbolic (config : C.config)
+    (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list)
+    (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Retrieve the (correctly instantiated) signature *)
   let def = C.ctx_lookup_fun_decl ctx fid in
   let sg = def.A.signature in
   (* Instantiate the signature and introduce fresh abstraction and region ids
    * while doing so *)
-  let inst_sg = instantiate_fun_sig type_args cg_args sg in
+  (* There shouldn't be any reference to Self *)
+  let tr_self = T.UnknownTrait __FUNCTION__ in
+  let inst_sg = instantiate_fun_sig ctx generics tr_self sg in
   (* Sanity check *)
   assert (List.length args = List.length def.A.signature.inputs);
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
-    region_args type_args cg_args args dest cf ctx
+    generics args dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1162,10 +1173,8 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
     calls in symbolic mode: only their signatures matter.
  *)
 and eval_function_call_symbolic_from_inst_sig (config : C.config)
-    (fid : A.fun_id) (inst_sg : A.inst_fun_sig)
-    (_region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+    (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (generics : T.egeneric_args)
+    (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
@@ -1232,8 +1241,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     let expr = cf ctx in
 
     (* Synthesize the symbolic AST *)
-    S.synthesize_regular_function_call fid call_id ctx abs_ids type_args cg_args
-      args args_places ret_spc dest_place expr
+    S.synthesize_regular_function_call fid call_id ctx abs_ids generics args
+      args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
 
@@ -1294,9 +1303,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   cc (cf Unit) ctx
 
 (** Evaluate a non-local function call in symbolic mode *)
-and eval_non_local_function_call_symbolic (config : C.config)
-    (fid : A.assumed_fun_id) (region_args : T.erased_region list)
-    (type_args : T.ety list) (cg_args : T.const_generic list)
+and eval_assumed_function_call_symbolic (config : C.config)
+    (fid : A.assumed_fun_id) (generics : T.egeneric_args)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Sanity check: make sure the type parameters don't contain regions -
@@ -1304,7 +1312,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   assert (
     List.for_all
       (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
-      type_args);
+      generics.types);
 
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
@@ -1315,7 +1323,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   | A.BoxFree ->
       (* Degenerate case: box_free - note that this is not really a function
        * call: no need to call a "synthesize_..." function *)
-      eval_box_free config region_args type_args cg_args args dest (cf Unit) ctx
+      eval_box_free config generics args dest (cf Unit) ctx
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1327,55 +1335,50 @@ and eval_non_local_function_call_symbolic (config : C.config)
             (* should have been treated above *)
             raise (Failure "Unreachable")
         | _ ->
-            instantiate_fun_sig type_args cg_args (Assumed.get_assumed_sig fid)
+            (* There shouldn't be any reference to Self *)
+            let tr_self = T.UnknownTrait __FUNCTION__ in
+            instantiate_fun_sig ctx generics tr_self
+              (Assumed.get_assumed_sig fid)
       in
 
       (* Evaluate the function call *)
       eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
-        region_args type_args cg_args args dest cf ctx
+        generics args dest cf ctx
 
 (** Evaluate a non-local (i.e, assumed) function call such as [Box::deref]
     (auxiliary helper for [eval_statement]) *)
-and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
-    (region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id)
+    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
     (lazy
-      (let type_args =
-         "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]"
-       in
+      (let generics = PCtx.egeneric_args_to_string ctx generics in
        let args =
          "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]"
        in
        let dest = place_to_string ctx dest in
-       "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
-       ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: "
-       ^ dest));
+       "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
+       ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest));
 
   match config.mode with
   | C.ConcreteMode ->
-      eval_non_local_function_call_concrete config fid region_args type_args
-        cg_args args dest (cf Unit) ctx
+      eval_assumed_function_call_concrete config fid generics args dest
+        (cf Unit) ctx
   | C.SymbolicMode ->
-      eval_non_local_function_call_symbolic config fid region_args type_args
-        cg_args args dest cf ctx
+      eval_assumed_function_call_symbolic config fid generics args dest cf ctx
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
-    (region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id)
+    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
   match config.mode with
   | ConcreteMode ->
-      eval_local_function_call_concrete config fid region_args type_args cg_args
-        args dest
+      eval_transparent_function_call_concrete config fid generics args dest
   | SymbolicMode ->
-      eval_local_function_call_symbolic config fid region_args type_args cg_args
-        args dest
+      eval_transparent_function_call_symbolic config fid generics args dest
 
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 814bc964..0a086fb2 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -32,7 +32,11 @@ val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun
     Note: there are no region parameters, because they should be erased.
  *)
 val instantiate_fun_sig :
-  T.ety list -> T.const_generic list -> LA.fun_sig -> LA.inst_fun_sig
+  C.eval_ctx ->
+  T.egeneric_args ->
+  T.rtrait_instance_id ->
+  LA.fun_sig ->
+  LA.inst_fun_sig
 
 (** Helper.
 
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 637f1b1e..1513465c 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -273,7 +273,7 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | Ref (p, _) -> Some p
+  | RvRef (p, _) -> Some p
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index f29c7f88..9ac5ce13 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -7,6 +7,7 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module A = LlbcAst
 module L = Logging
 open Cps
@@ -406,13 +407,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (match (tv.V.value, tv.V.ty) with
         | V.Literal cv, T.Literal ty -> check_literal_type cv ty
         (* ADT case *)
-        | V.Adt av, T.Adt (T.AdtId def_id, regions, tys, cgs) ->
+        | V.Adt av, T.Adt (T.AdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
             let def = C.ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
-            assert (List.length regions = List.length def.region_params);
-            assert (List.length tys = List.length def.type_params);
+            assert (
+              List.length generics.regions = List.length def.generics.regions);
+            assert (List.length generics.types = List.length def.generics.types);
             (* Check that the variant id is consistent *)
             (match (av.V.variant_id, def.T.kind) with
             | Some variant_id, T.Enum variants ->
@@ -421,8 +423,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | _ -> raise (Failure "Erroneous typing"));
             (* Check that the field types are correct *)
             let field_types =
-              Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id
-                tys cgs
+              Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id
+                generics
             in
             let fields_with_types =
               List.combine av.V.field_values field_types
@@ -431,20 +433,28 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.Adt av, T.Adt (T.Tuple, regions, tys, cgs) ->
-            assert (regions = []);
-            assert (cgs = []);
+        | V.Adt av, T.Adt (T.Tuple, generics) ->
+            assert (generics.regions = []);
+            assert (generics.const_generics = []);
             assert (av.V.variant_id = None);
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
-            let fields_with_types = List.combine av.V.field_values tys in
+            let fields_with_types =
+              List.combine av.V.field_values generics.types
+            in
             List.iter
               (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
               fields_with_types
         (* Assumed type case *)
-        | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> (
+        | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> (
             assert (av.V.variant_id = None || aty_id = T.Option);
-            match (aty_id, av.V.field_values, regions, tys, cgs) with
+            match
+              ( aty_id,
+                av.V.field_values,
+                generics.regions,
+                generics.types,
+                generics.const_generics )
+            with
             (* Box *)
             | T.Box, [ inner_value ], [], [ inner_ty ], []
             | T.Option, [ inner_value ], [], [ inner_ty ], [] ->
@@ -520,14 +530,17 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (* Check the current pair (value, type) *)
         (match (atv.V.value, atv.V.ty) with
         (* ADT case *)
-        | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys, cgs) ->
+        | V.AAdt av, T.Adt (T.AdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
             let def = C.ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
-            assert (List.length regions = List.length def.region_params);
-            assert (List.length tys = List.length def.type_params);
-            assert (List.length cgs = List.length def.const_generic_params);
+            assert (
+              List.length generics.regions = List.length def.generics.regions);
+            assert (List.length generics.types = List.length def.generics.types);
+            assert (
+              List.length generics.const_generics
+              = List.length def.generics.const_generics);
             (* Check that the variant id is consistent *)
             (match (av.V.variant_id, def.T.kind) with
             | Some variant_id, T.Enum variants ->
@@ -536,8 +549,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | _ -> raise (Failure "Erroneous typing"));
             (* Check that the field types are correct *)
             let field_types =
-              Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id
-                regions tys cgs
+              Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id
+                generics
             in
             let fields_with_types =
               List.combine av.V.field_values field_types
@@ -546,20 +559,28 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.AAdt av, T.Adt (T.Tuple, regions, tys, cgs) ->
-            assert (regions = []);
-            assert (cgs = []);
+        | V.AAdt av, T.Adt (T.Tuple, generics) ->
+            assert (generics.regions = []);
+            assert (generics.const_generics = []);
             assert (av.V.variant_id = None);
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
-            let fields_with_types = List.combine av.V.field_values tys in
+            let fields_with_types =
+              List.combine av.V.field_values generics.types
+            in
             List.iter
               (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
               fields_with_types
         (* Assumed type case *)
-        | V.AAdt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> (
+        | V.AAdt av, T.Adt (T.Assumed aty_id, generics) -> (
             assert (av.V.variant_id = None);
-            match (aty_id, av.V.field_values, regions, tys, cgs) with
+            match
+              ( aty_id,
+                av.V.field_values,
+                generics.regions,
+                generics.types,
+                generics.const_generics )
+            with
             (* Box *)
             | T.Box, [ boxed_value ], [], [ boxed_ty ], [] ->
                 assert (boxed_value.V.ty = boxed_ty)
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 9dc1f5e3..d0f5b0c5 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -57,6 +57,9 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
 (** Logger for Invariants *)
 let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
 
+(** Logger for AssociatedTypes *)
+let associated_types_log = L.get_logger "MainLogger.AssociatedTypes"
+
 (** Logger for SCC *)
 let scc_log = L.get_logger "MainLogger.Graph.SCC"
 
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index b348ba1d..1058fab0 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -107,7 +107,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
         false
     | Assign (_, rv) -> (
         match rv with
-        | Use _ | Ref _ -> not must_end_with_exit
+        | Use _ | RvRef _ -> not must_end_with_exit
         | Aggregate (AggregatedTuple, []) -> not must_end_with_exit
         | _ -> false)
     | FakeRead _ | Drop _ | Nop -> not must_end_with_exit
@@ -376,7 +376,7 @@ let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
 
         method! visit_Assign env p rv =
           match (p.projection, rv) with
-          | [], E.Ref (_, E.Shallow) ->
+          | [], E.RvRef (_, E.Shallow) ->
               (* Filter *)
               filtered := E.VarId.Set.add p.var_id !filtered;
               Nop
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 9aa73d7c..aebfd09c 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -21,6 +21,9 @@ module Values = struct
     type_decl_id_to_string : T.TypeDeclId.id -> string;
     const_generic_var_id_to_string : T.ConstGenericVarId.id -> string;
     global_decl_id_to_string : T.GlobalDeclId.id -> string;
+    trait_decl_id_to_string : T.TraitDeclId.id -> string;
+    trait_impl_id_to_string : T.TraitImplId.id -> string;
+    trait_clause_id_to_string : T.TraitClauseId.id -> string;
     adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
     var_id_to_string : E.VarId.id -> string;
     adt_field_names :
@@ -34,6 +37,9 @@ module Values = struct
       PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
       PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
       PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
+      PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+      PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+      PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
     }
 
   let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter =
@@ -43,6 +49,9 @@ module Values = struct
       PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
       PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
       PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
+      PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+      PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+      PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
     }
 
   let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
@@ -52,6 +61,9 @@ module Values = struct
       PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
       PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
       PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
+      PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+      PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+      PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
     }
 
   let var_id_to_string (id : E.VarId.id) : string =
@@ -86,10 +98,10 @@ module Values = struct
           List.map (typed_value_to_string fmt) av.field_values
         in
         match v.ty with
-        | T.Adt (T.Tuple, _, _, _) ->
+        | T.Adt (T.Tuple, _) ->
             (* Tuple *)
             "(" ^ String.concat ", " field_values ^ ")"
-        | T.Adt (T.AdtId def_id, _, _, _) ->
+        | T.Adt (T.AdtId def_id, _) ->
             (* "Regular" ADT *)
             let adt_ident =
               match av.variant_id with
@@ -111,7 +123,7 @@ module Values = struct
                   let field_values = String.concat " " field_values in
                   adt_ident ^ " { " ^ field_values ^ " }"
             else adt_ident
-        | T.Adt (T.Assumed aty, _, _, _) -> (
+        | T.Adt (T.Assumed aty, _) -> (
             (* Assumed type *)
             match (aty, field_values) with
             | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
@@ -201,10 +213,10 @@ module Values = struct
           List.map (typed_avalue_to_string fmt) av.field_values
         in
         match v.ty with
-        | T.Adt (T.Tuple, _, _, _) ->
+        | T.Adt (T.Tuple, _) ->
             (* Tuple *)
             "(" ^ String.concat ", " field_values ^ ")"
-        | T.Adt (T.AdtId def_id, _, _, _) ->
+        | T.Adt (T.AdtId def_id, _) ->
             (* "Regular" ADT *)
             let adt_ident =
               match av.variant_id with
@@ -226,7 +238,7 @@ module Values = struct
                   let field_values = String.concat " " field_values in
                   adt_ident ^ " { " ^ field_values ^ " }"
             else adt_ident
-        | T.Adt (T.Assumed aty, _, _, _) -> (
+        | T.Adt (T.Assumed aty, _) -> (
             (* Assumed type *)
             match (aty, field_values) with
             | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
@@ -452,6 +464,9 @@ module Contexts = struct
       PV.adt_variant_to_string = fmt.adt_variant_to_string;
       PV.var_id_to_string = fmt.var_id_to_string;
       PV.adt_field_names = fmt.adt_field_names;
+      PV.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+      PV.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+      PV.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
     }
 
   let ast_to_value_formatter (fmt : PA.ast_formatter) : PV.value_formatter =
@@ -486,6 +501,15 @@ module Contexts = struct
       let def = C.ctx_lookup_global_decl ctx def_id in
       name_to_string def.name
     in
+    let trait_decl_id_to_string def_id =
+      let def = C.ctx_lookup_trait_decl ctx def_id in
+      name_to_string def.name
+    in
+    let trait_impl_id_to_string def_id =
+      let def = C.ctx_lookup_trait_impl ctx def_id in
+      name_to_string def.name
+    in
+    let trait_clause_id_to_string id = PT.trait_clause_id_to_pretty_string id in
     let adt_variant_to_string =
       PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
     in
@@ -506,6 +530,9 @@ module Contexts = struct
       adt_variant_to_string;
       var_id_to_string;
       adt_field_names;
+      trait_decl_id_to_string;
+      trait_impl_id_to_string;
+      trait_clause_id_to_string;
     }
 
   let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : PA.ast_formatter =
@@ -521,6 +548,15 @@ module Contexts = struct
       let def = C.ctx_lookup_global_decl ctx def_id in
       global_name_to_string def.name
     in
+    let trait_decl_id_to_string def_id =
+      let def = C.ctx_lookup_trait_decl ctx def_id in
+      name_to_string def.name
+    in
+    let trait_impl_id_to_string def_id =
+      let def = C.ctx_lookup_trait_impl ctx def_id in
+      name_to_string def.name
+    in
+    let trait_clause_id_to_string id = PT.trait_clause_id_to_pretty_string id in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
       r_to_string = ctx_fmt.PV.r_to_string;
@@ -533,6 +569,9 @@ module Contexts = struct
       adt_field_to_string;
       fun_decl_id_to_string;
       global_decl_id_to_string;
+      trait_decl_id_to_string;
+      trait_impl_id_to_string;
+      trait_clause_id_to_string;
     }
 
   (** Split an [env] at every occurrence of [Frame], eliminating those elements.
@@ -608,6 +647,12 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.ctx_to_rtype_formatter fmt in
     PT.rty_to_string fmt t
 
+  let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string
+      =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_etype_formatter fmt in
+    PT.egeneric_args_to_string fmt x
+
   let borrow_content_to_string (ctx : C.eval_ctx) (bc : V.borrow_content) :
       string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index dfb2c9fd..724f1e0a 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -8,6 +8,9 @@ type type_formatter = {
   type_decl_id_to_string : TypeDeclId.id -> string;
   const_generic_var_id_to_string : ConstGenericVarId.id -> string;
   global_decl_id_to_string : GlobalDeclId.id -> string;
+  trait_decl_id_to_string : TraitDeclId.id -> string;
+  trait_impl_id_to_string : TraitImplId.id -> string;
+  trait_clause_id_to_string : TraitClauseId.id -> string;
 }
 
 type value_formatter = {
@@ -18,6 +21,9 @@ type value_formatter = {
   adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string;
   var_id_to_string : VarId.id -> string;
   adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
+  trait_decl_id_to_string : TraitDeclId.id -> string;
+  trait_impl_id_to_string : TraitImplId.id -> string;
+  trait_clause_id_to_string : TraitClauseId.id -> string;
 }
 
 let value_to_type_formatter (fmt : value_formatter) : type_formatter =
@@ -26,6 +32,9 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter =
     type_decl_id_to_string = fmt.type_decl_id_to_string;
     const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
     global_decl_id_to_string = fmt.global_decl_id_to_string;
+    trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+    trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+    trait_clause_id_to_string = fmt.trait_clause_id_to_string;
   }
 
 (* TODO: we need to store which variables we have encountered so far, and
@@ -42,6 +51,9 @@ type ast_formatter = {
   adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
   fun_decl_id_to_string : FunDeclId.id -> string;
   global_decl_id_to_string : GlobalDeclId.id -> string;
+  trait_decl_id_to_string : TraitDeclId.id -> string;
+  trait_impl_id_to_string : TraitImplId.id -> string;
+  trait_clause_id_to_string : TraitClauseId.id -> string;
 }
 
 let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -53,6 +65,9 @@ let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
     adt_variant_to_string = fmt.adt_variant_to_string;
     var_id_to_string = fmt.var_id_to_string;
     adt_field_names = fmt.adt_field_names;
+    trait_decl_id_to_string = fmt.trait_decl_id_to_string;
+    trait_impl_id_to_string = fmt.trait_impl_id_to_string;
+    trait_clause_id_to_string = fmt.trait_clause_id_to_string;
   }
 
 let ast_to_type_formatter (fmt : ast_formatter) : type_formatter =
@@ -70,31 +85,51 @@ let literal_type_to_string = Print.PrimitiveValues.literal_type_to_string
 let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string
 let literal_to_string = Print.PrimitiveValues.literal_to_string
 
+(* Remark: not using generic_params on purpose, because we may use parameters
+   which either come from LLBC or from pure, and the [generic_params] type
+   for those ASTs is not the same. Note that it works because we actually don't
+   need to know the trait clauses to print the AST: we can thus ignore them.
+*)
 let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     (global_decls : A.global_decl GlobalDeclId.Map.t)
-    (type_params : type_var list)
+    (trait_decls : A.trait_decl TraitDeclId.Map.t)
+    (trait_impls : A.trait_impl TraitImplId.Map.t) (type_params : type_var list)
     (const_generic_params : const_generic_var list) : type_formatter =
   let type_var_id_to_string vid =
-    let var = T.TypeVarId.nth type_params vid in
+    let var = TypeVarId.nth type_params vid in
     type_var_to_string var
   in
   let const_generic_var_id_to_string vid =
-    let var = T.ConstGenericVarId.nth const_generic_params vid in
+    let var = ConstGenericVarId.nth const_generic_params vid in
     const_generic_var_to_string var
   in
   let type_decl_id_to_string def_id =
-    let def = T.TypeDeclId.Map.find def_id type_decls in
+    let def = TypeDeclId.Map.find def_id type_decls in
     name_to_string def.name
   in
   let global_decl_id_to_string def_id =
-    let def = T.GlobalDeclId.Map.find def_id global_decls in
+    let def = GlobalDeclId.Map.find def_id global_decls in
+    name_to_string def.name
+  in
+  let trait_decl_id_to_string def_id =
+    let def = TraitDeclId.Map.find def_id trait_decls in
     name_to_string def.name
   in
+  let trait_impl_id_to_string def_id =
+    let def = TraitImplId.Map.find def_id trait_impls in
+    name_to_string def.name
+  in
+  let trait_clause_id_to_string id =
+    Print.PT.trait_clause_id_to_pretty_string id
+  in
   {
     type_var_id_to_string;
     type_decl_id_to_string;
     const_generic_var_id_to_string;
     global_decl_id_to_string;
+    trait_decl_id_to_string;
+    trait_impl_id_to_string;
+    trait_clause_id_to_string;
   }
 
 (* TODO: there is a bit of duplication with Print.fun_decl_to_ast_formatter.
@@ -106,7 +141,8 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
 let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     (fun_decls : A.fun_decl FunDeclId.Map.t)
     (global_decls : A.global_decl GlobalDeclId.Map.t)
-    (type_params : type_var list)
+    (trait_decls : A.trait_decl TraitDeclId.Map.t)
+    (trait_impls : A.trait_impl TraitImplId.Map.t) (type_params : type_var list)
     (const_generic_params : const_generic_var list) : ast_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
@@ -141,6 +177,17 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     let def = GlobalDeclId.Map.find def_id global_decls in
     global_name_to_string def.name
   in
+  let trait_decl_id_to_string def_id =
+    let def = TraitDeclId.Map.find def_id trait_decls in
+    name_to_string def.name
+  in
+  let trait_impl_id_to_string def_id =
+    let def = TraitImplId.Map.find def_id trait_impls in
+    name_to_string def.name
+  in
+  let trait_clause_id_to_string id =
+    Print.PT.trait_clause_id_to_pretty_string id
+  in
   {
     type_var_id_to_string;
     const_generic_var_id_to_string;
@@ -151,6 +198,9 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     adt_field_to_string;
     fun_decl_id_to_string;
     global_decl_id_to_string;
+    trait_decl_id_to_string;
+    trait_impl_id_to_string;
+    trait_clause_id_to_string;
   }
 
 let assumed_ty_to_string (aty : assumed_ty) : string =
@@ -182,20 +232,18 @@ let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) :
 
 let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
   match ty with
-  | Adt (id, tys, cgs) -> (
-      let tys = List.map (ty_to_string fmt false) tys in
-      let cgs = List.map (const_generic_to_string fmt) cgs in
-      let params = List.append tys cgs in
+  | Adt (id, generics) -> (
       match id with
       | Tuple ->
-          assert (cgs = []);
-          "(" ^ String.concat " * " tys ^ ")"
+          let generics = generic_args_to_strings fmt false generics in
+          "(" ^ String.concat " * " generics ^ ")"
       | AdtId _ | Assumed _ ->
-          let params_s =
-            if params = [] then "" else " " ^ String.concat " " params
+          let generics = generic_args_to_strings fmt true generics in
+          let generics_s =
+            if generics = [] then "" else " " ^ String.concat " " generics
           in
-          let ty_s = type_id_to_string fmt id ^ params_s in
-          if params <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
+          let ty_s = type_id_to_string fmt id ^ generics_s in
+          if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
   | TypeVar tv -> fmt.type_var_id_to_string tv
   | Literal lty -> literal_type_to_string lty
   | Arrow (arg_ty, ret_ty) ->
@@ -204,6 +252,62 @@ let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
       in
       if inside then "(" ^ ty ^ ")" else ty
 
+and generic_args_to_strings (fmt : type_formatter) (inside : bool)
+    (generics : generic_args) : string list =
+  let tys = List.map (ty_to_string fmt inside) generics.types in
+  let cgs = List.map (const_generic_to_string fmt) generics.const_generics in
+  let trait_refs =
+    List.map (trait_ref_to_string fmt inside) generics.trait_refs
+  in
+  List.concat [ tys; cgs; trait_refs ]
+
+and generic_args_to_string (fmt : type_formatter) (generics : generic_args) :
+    string =
+  String.concat " " (generic_args_to_strings fmt true generics)
+
+and trait_ref_to_string (fmt : type_formatter) (inside : bool) (tr : trait_ref)
+    : string =
+  let trait_id = trait_instance_id_to_string fmt false tr.trait_id in
+  let generics = generic_args_to_string fmt tr.generics in
+  let s = trait_id ^ generics in
+  if tr.generics = empty_generic_args || not inside then s else "(" ^ s ^ ")"
+
+and trait_instance_id_to_string (fmt : type_formatter) (inside : bool)
+    (id : trait_instance_id) : string =
+  match id with
+  | Self -> "Self"
+  | TraitImpl id -> fmt.trait_impl_id_to_string id
+  | Clause id -> fmt.trait_clause_id_to_string id
+  | ParentClause (inst_id, clause_id) ->
+      let inst_id = trait_instance_id_to_string fmt false inst_id in
+      let clause_id = fmt.trait_clause_id_to_string clause_id in
+      "parent(" ^ inst_id ^ ")::" ^ clause_id
+  | ItemClause (inst_id, item_name, clause_id) ->
+      let inst_id = trait_instance_id_to_string fmt false inst_id in
+      let clause_id = fmt.trait_clause_id_to_string clause_id in
+      "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
+  | TraitRef tr -> trait_ref_to_string fmt inside tr
+  | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
+
+let trait_clause_to_string (fmt : type_formatter) (clause : trait_clause) :
+    string =
+  let clause_id = fmt.trait_clause_id_to_string clause.clause_id in
+  let trait_id = fmt.trait_decl_id_to_string clause.trait_id in
+  let generics = generic_args_to_strings fmt true clause.generics in
+  let generics =
+    if generics = [] then "" else " " ^ String.concat " " generics
+  in
+  "[" ^ clause_id ^ "]: " ^ trait_id ^ generics
+
+let generic_params_to_strings (fmt : type_formatter) (generics : generic_params)
+    : string list =
+  let tys = List.map type_var_to_string generics.types in
+  let cgs = List.map const_generic_var_to_string generics.const_generics in
+  let trait_clauses =
+    List.map (trait_clause_to_string fmt) generics.trait_clauses
+  in
+  List.concat [ tys; cgs; trait_clauses ]
+
 let field_to_string fmt inside (f : field) : string =
   match f.field_name with
   | None -> ty_to_string fmt inside f.field_ty
@@ -217,11 +321,10 @@ let variant_to_string fmt (v : variant) : string =
   ^ ")"
 
 let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
-  let types = def.type_params in
   let name = name_to_string def.name in
   let params =
-    if types = [] then ""
-    else " " ^ String.concat " " (List.map type_var_to_string types)
+    if def.generics = empty_generic_params then ""
+    else " " ^ String.concat " " (generic_params_to_strings fmt def.generics)
   in
   match def.kind with
   | Struct fields ->
@@ -353,10 +456,10 @@ let adt_g_value_to_string (fmt : value_formatter)
     (field_values : 'v list) (ty : ty) : string =
   let field_values = List.map value_to_string field_values in
   match ty with
-  | Adt (Tuple, _, _) ->
+  | Adt (Tuple, _) ->
       (* Tuple *)
       "(" ^ String.concat ", " field_values ^ ")"
-  | Adt (AdtId def_id, _, _) ->
+  | Adt (AdtId def_id, _) ->
       (* "Regular" ADT *)
       let adt_ident =
         match variant_id with
@@ -378,7 +481,7 @@ let adt_g_value_to_string (fmt : value_formatter)
             let field_values = String.concat " " field_values in
             adt_ident ^ " { " ^ field_values ^ " }"
       else adt_ident
-  | Adt (Assumed aty, _, _) -> (
+  | Adt (Assumed aty, _) -> (
       (* Assumed type *)
       match aty with
       | State ->
@@ -631,7 +734,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
   (* There are two possibilities: either the [app] is an instantiated,
    * top-level qualifier (function, ADT constructore...), or it is a "regular"
    * expression *)
-  let app, tys =
+  let app, generics =
     match app.e with
     | Qualif qualif ->
         (* Qualifier case *)
@@ -656,9 +759,9 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
         in
         (* Convert the type instantiation *)
         let ty_fmt = ast_to_type_formatter fmt in
-        let tys = List.map (ty_to_string ty_fmt true) qualif.type_args in
+        let generics = generic_args_to_strings ty_fmt true qualif.generics in
         (* *)
-        (qualif_s, tys)
+        (qualif_s, generics)
     | _ ->
         (* "Regular" expression case *)
         let inside = args <> [] || (args = [] && inside) in
@@ -673,7 +776,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
     texpression_to_string fmt inside indent1 indent_incr
   in
   let args = List.map arg_to_string args in
-  let all_args = List.append tys args in
+  let all_args = List.append generics args in
   (* Put together *)
   let e =
     if all_args = [] then app else app ^ " " ^ String.concat " " all_args
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 55513cc2..147c14b9 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -13,6 +13,9 @@ module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
 module FunDeclId = A.FunDeclId
 module GlobalDeclId = A.GlobalDeclId
+module TraitDeclId = T.TraitDeclId
+module TraitImplId = T.TraitImplId
+module TraitClauseId = T.TraitClauseId
 
 (** We redefine identifiers for loop: in {!Values}, the identifiers are global
     (they monotonically increase across functions) while in {!module:Pure} we want
@@ -38,6 +41,10 @@ type integer_type = T.integer_type [@@deriving show, ord]
 type const_generic_var = T.const_generic_var [@@deriving show, ord]
 type const_generic = T.const_generic [@@deriving show, ord]
 type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
+type trait_decl_id = T.trait_decl_id [@@deriving show, ord]
+type trait_impl_id = T.trait_impl_id [@@deriving show, ord]
+type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
+type trait_item_name = T.trait_item_name [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -177,6 +184,14 @@ class ['self] iter_ty_base =
     inherit! [_] T.iter_const_generic
     inherit! [_] PV.iter_literal_type
     method visit_type_var_id : 'env -> type_var_id -> unit = fun _ _ -> ()
+    method visit_trait_decl_id : 'env -> trait_decl_id -> unit = fun _ _ -> ()
+    method visit_trait_impl_id : 'env -> trait_impl_id -> unit = fun _ _ -> ()
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> unit =
+      fun _ _ -> ()
+
+    method visit_trait_item_name : 'env -> trait_item_name -> unit =
+      fun _ _ -> ()
   end
 
 (** Ancestor for map visitor for [ty] *)
@@ -186,6 +201,18 @@ class ['self] map_ty_base =
     inherit! [_] T.map_const_generic
     inherit! [_] PV.map_literal_type
     method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id =
+      fun _ x -> x
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id =
+      fun _ x -> x
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id =
+      fun _ x -> x
+
+    method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name =
+      fun _ x -> x
   end
 
 (** Ancestor for reduce visitor for [ty] *)
@@ -195,6 +222,18 @@ class virtual ['self] reduce_ty_base =
     inherit! [_] T.reduce_const_generic
     inherit! [_] PV.reduce_literal_type
     method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_item_name : 'env -> trait_item_name -> 'a =
+      fun _ _ -> self#zero
   end
 
 (** Ancestor for mapreduce visitor for [ty] *)
@@ -206,10 +245,24 @@ class virtual ['self] mapreduce_ty_base =
 
     method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a =
       fun _ x -> (x, self#zero)
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_clause_id
+        : 'env -> trait_clause_id -> trait_clause_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_item_name
+        : 'env -> trait_item_name -> trait_item_name * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 type ty =
-  | Adt of type_id * ty list * const_generic list
+  | Adt of type_id * generic_args
       (** {!Adt} encodes ADTs and tuples and assumed types.
 
           TODO: what about the ended regions? (ADTs may be parameterized
@@ -220,6 +273,23 @@ type ty =
   | TypeVar of type_var_id
   | Literal of literal_type
   | Arrow of ty * ty
+
+and trait_ref = { trait_id : trait_instance_id; generics : generic_args }
+
+and generic_args = {
+  types : ty list;
+  const_generics : const_generic list;
+  trait_refs : trait_ref list;
+}
+
+and trait_instance_id =
+  | Self
+  | TraitImpl of trait_impl_id
+  | Clause of trait_clause_id
+  | ParentClause of trait_instance_id * trait_clause_id
+  | ItemClause of trait_instance_id * trait_item_name * trait_clause_id
+  | TraitRef of trait_ref
+  | UnknownTrait of string
 [@@deriving
   show,
     visitors
@@ -265,11 +335,24 @@ type type_decl_kind = Struct of field list | Enum of variant list | Opaque
 
 type type_var = T.type_var [@@deriving show]
 
+type trait_clause = {
+  clause_id : trait_clause_id;
+  trait_id : trait_decl_id;
+  generics : generic_args;
+}
+[@@deriving show]
+
+type generic_params = {
+  types : type_var list;
+  const_generics : const_generic_var list;
+  trait_clauses : trait_clause list;
+}
+[@@deriving show]
+
 type type_decl = {
   def_id : TypeDeclId.id;
   name : name;
-  type_params : type_var list;
-  const_generic_params : const_generic_var list;
+  generics : generic_params;
   kind : type_decl_kind;
 }
 [@@deriving show]
@@ -463,18 +546,13 @@ type qualif_id =
   | Proj of projection  (** Field projector *)
 [@@deriving show]
 
-(** An instantiated qualified.
+(** An instantiated qualifier.
 
     Note that for now we have a clear separation between types and expressions,
-    which explains why we have the [type_params] field: a function or ADT
+    which explains why we have the [generics] field: a function or ADT
     constructor is always fully instantiated.
  *)
-type qualif = {
-  id : qualif_id;
-  type_args : ty list;
-  const_generic_args : const_generic list;
-}
-[@@deriving show]
+type qualif = { id : qualif_id; generics : generic_args } [@@deriving show]
 
 type field_id = FieldId.id [@@deriving show, ord]
 type var_id = VarId.id [@@deriving show, ord]
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index d145ce93..77b12811 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -9,17 +9,19 @@ open PureUtils
     of fields is fixed: it shouldn't be used for arrays, slices, etc.
  *)
 let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
-    (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list)
-    (cgs : const_generic list) : ty list =
+    (type_id : type_id) (variant_id : VariantId.id option)
+    (generics : generic_args) : ty list =
   match type_id with
   | Tuple ->
       (* Tuple *)
+      assert (generics.const_generics = []);
+      assert (generics.trait_refs = []);
       assert (variant_id = None);
-      tys
+      generics.types
   | AdtId def_id ->
       (* "Regular" ADT *)
       let def = TypeDeclId.Map.find def_id type_decls in
-      type_decl_get_instantiated_fields_types def variant_id tys cgs
+      type_decl_get_instantiated_fields_types def variant_id generics
   | Assumed aty -> (
       (* Assumed type *)
       match aty with
@@ -27,14 +29,14 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           (* This type is opaque *)
           raise (Failure "Unreachable: opaque type")
       | Result ->
-          let ty = Collections.List.to_cons_nil tys in
+          let ty = Collections.List.to_cons_nil generics.types in
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then [ ty ]
           else if variant_id = result_fail_id then [ mk_error_ty ]
           else
             raise (Failure "Unreachable: improper variant id for result type")
       | Error ->
-          assert (tys = []);
+          assert (generics = empty_generic_args);
           let variant_id = Option.get variant_id in
           assert (
             variant_id = error_failure_id || variant_id = error_out_of_fuel_id);
@@ -45,14 +47,14 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
           else raise (Failure "Unreachable: improper variant id for fuel type")
       | Option ->
-          let ty = Collections.List.to_cons_nil tys in
+          let ty = Collections.List.to_cons_nil generics.types in
           let variant_id = Option.get variant_id in
           if variant_id = option_some_id then [ ty ]
           else if variant_id = option_none_id then []
           else
             raise (Failure "Unreachable: improper variant id for option type")
       | Range ->
-          let ty = Collections.List.to_cons_nil tys in
+          let ty = Collections.List.to_cons_nil generics.types in
           assert (variant_id = None);
           [ ty; ty ]
       | Vec | Array | Slice | Str ->
@@ -88,12 +90,13 @@ let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx =
       { ctx with env }
   | PatAdt av ->
       (* Compute the field types *)
-      let type_id, tys, cgs = ty_as_adt v.ty in
+      let type_id, generics = ty_as_adt v.ty in
       let field_tys =
-        get_adt_field_types ctx.type_decls type_id av.variant_id tys cgs
+        get_adt_field_types ctx.type_decls type_id av.variant_id generics
       in
       let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
         if ty <> v.ty then (
+          (* TODO: we need to normalize the types *)
           log#serror
             ("check_typed_pattern: not the same types:" ^ "\n- ty: "
            ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
@@ -142,31 +145,29 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
           (* Note we can only project fields of structures (not enumerations) *)
           (* Deconstruct the projector type *)
           let adt_ty, field_ty = destruct_arrow e.ty in
-          let adt_id, adt_type_args, adt_cg_args = ty_as_adt adt_ty in
+          let adt_id, adt_generics = ty_as_adt adt_ty in
           (* Check the ADT type *)
           assert (adt_id = proj_adt_id);
-          assert (adt_type_args = qualif.type_args);
-          assert (adt_cg_args = qualif.const_generic_args);
+          assert (adt_generics = qualif.generics);
           (* Retrieve and check the expected field type *)
           let variant_id = None in
           let expected_field_tys =
             get_adt_field_types ctx.type_decls proj_adt_id variant_id
-              qualif.type_args qualif.const_generic_args
+              qualif.generics
           in
           let expected_field_ty = FieldId.nth expected_field_tys field_id in
           assert (expected_field_ty = field_ty)
       | AdtCons id -> (
           let expected_field_tys =
             get_adt_field_types ctx.type_decls id.adt_id id.variant_id
-              qualif.type_args qualif.const_generic_args
+              qualif.generics
           in
           let field_tys, adt_ty = destruct_arrows e.ty in
           assert (expected_field_tys = field_tys);
           match adt_ty with
-          | Adt (type_id, tys, cgs) ->
+          | Adt (type_id, generics) ->
               assert (type_id = id.adt_id);
-              assert (tys = qualif.type_args);
-              assert (cgs = qualif.const_generic_args)
+              assert (generics = qualif.generics)
           | _ -> raise (Failure "Unreachable")))
   | Let (monadic, pat, re, e_next) ->
       let expected_pat_ty = if monadic then destruct_result re.ty else re.ty in
@@ -212,15 +213,14 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
          | Some ty -> assert (ty = e.ty));
       (* Check the fields *)
       (* Retrieve and check the expected field type *)
-      let adt_id, adt_type_args, adt_cg_args = ty_as_adt e.ty in
+      let adt_id, adt_generics = ty_as_adt e.ty in
       assert (adt_id = supd.struct_id);
       (* The id can only be: a custom type decl or an array *)
       match adt_id with
       | AdtId _ ->
           let variant_id = None in
           let expected_field_tys =
-            get_adt_field_types ctx.type_decls adt_id variant_id adt_type_args
-              adt_cg_args
+            get_adt_field_types ctx.type_decls adt_id variant_id adt_generics
           in
           List.iter
             (fun (fid, fe) ->
@@ -229,7 +229,9 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
               check_texpression ctx fe)
             supd.updates
       | Assumed Array ->
-          let expected_field_ty = Collections.List.to_cons_nil adt_type_args in
+          let expected_field_ty =
+            Collections.List.to_cons_nil adt_generics.types
+          in
           List.iter
             (fun (_, fe) ->
               assert (expected_field_ty = fe.ty);
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index f099ef9c..1357793b 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -89,14 +89,31 @@ let mk_mplace (var_id : E.VarId.id) (name : string option)
     (projection : mprojection) : mplace =
   { var_id; name; projection }
 
+let empty_generic_params : generic_params =
+  { types = []; const_generics = []; trait_clauses = [] }
+
+let empty_generic_args : generic_args =
+  { types = []; const_generics = []; trait_refs = [] }
+
+let mk_generic_args_from_types (types : ty list) : generic_args =
+  { types; const_generics = []; trait_refs = [] }
+
+type subst = {
+  ty_subst : TypeVarId.id -> ty;
+  cg_subst : ConstGenericVarId.id -> const_generic;
+  tr_subst : TraitClauseId.id -> trait_instance_id;
+  tr_self : trait_instance_id;
+}
+
 (** Type substitution *)
-let ty_substitute (tsubst : TypeVarId.id -> ty)
-    (cgsubst : ConstGenericVarId.id -> const_generic) (ty : ty) : ty =
+let ty_substitute (subst : subst) (ty : ty) : ty =
   let obj =
     object
       inherit [_] map_ty
-      method! visit_TypeVar _ var_id = tsubst var_id
-      method! visit_ConstGenericVar _ var_id = cgsubst var_id
+      method! visit_TypeVar _ var_id = subst.ty_subst var_id
+      method! visit_ConstGenericVar _ var_id = subst.cg_subst var_id
+      method! visit_Clause _ id = subst.tr_subst id
+      method! visit_Self _ = subst.tr_self
     end
   in
   obj#visit_ty () ty
@@ -115,6 +132,18 @@ let make_const_generic_subst (vars : const_generic_var list)
     (cgs : const_generic list) : ConstGenericVarId.id -> const_generic =
   Substitute.make_const_generic_subst_from_vars vars cgs
 
+let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) :
+    TraitClauseId.id -> trait_instance_id =
+  let clauses = List.map (fun x -> x.clause_id) clauses in
+  let refs = List.map (fun x -> TraitRef x) refs in
+  let ls = List.combine clauses refs in
+  let mp =
+    List.fold_left
+      (fun mp (k, v) -> TraitClauseId.Map.add k v mp)
+      TraitClauseId.Map.empty ls
+  in
+  fun id -> TraitClauseId.Map.find id mp
+
 (** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
@@ -135,20 +164,27 @@ let type_decl_get_fields (def : type_decl)
              - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
           ^ opt_variant_id))
 
+let make_subst_from_generics (params : generic_params) (args : generic_args)
+    (tr_self : trait_instance_id) : subst =
+  let ty_subst = make_type_subst params.types args.types in
+  let cg_subst =
+    make_const_generic_subst params.const_generics args.const_generics
+  in
+  let tr_subst = make_trait_subst params.trait_clauses args.trait_refs in
+  { ty_subst; cg_subst; tr_subst; tr_self }
+
 (** Instantiate the type variables for the chosen variant in an ADT definition,
     and return the list of the types of its fields *)
 let type_decl_get_instantiated_fields_types (def : type_decl)
-    (opt_variant_id : VariantId.id option) (types : ty list)
-    (cgs : const_generic list) : ty list =
-  let ty_subst = make_type_subst def.type_params types in
-  let cg_subst = make_const_generic_subst def.const_generic_params cgs in
+    (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list =
+  (* There shouldn't be any reference to Self *)
+  let tr_self = UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.generics generics tr_self in
   let fields = type_decl_get_fields def opt_variant_id in
-  List.map (fun f -> ty_substitute ty_subst cg_subst f.field_ty) fields
+  List.map (fun f -> ty_substitute subst f.field_ty) fields
 
-let fun_sig_substitute (tsubst : TypeVarId.id -> ty)
-    (cgsubst : ConstGenericVarId.id -> const_generic) (sg : fun_sig) :
-    inst_fun_sig =
-  let subst = ty_substitute tsubst cgsubst in
+let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
+  let subst = ty_substitute subst in
   let inputs = List.map subst sg.inputs in
   let output = subst sg.output in
   let doutputs = List.map subst sg.doutputs in
@@ -194,9 +230,9 @@ let is_global (e : texpression) : bool =
 let is_const (e : texpression) : bool =
   match e.e with Const _ -> true | _ -> false
 
-let ty_as_adt (ty : ty) : type_id * ty list * const_generic list =
+let ty_as_adt (ty : ty) : type_id * generic_args =
   match ty with
-  | Adt (id, tys, cgs) -> (id, tys, cgs)
+  | Adt (id, generics) -> (id, generics)
   | _ -> raise (Failure "Unreachable")
 
 (** Remove the external occurrences of {!Meta} *)
@@ -294,28 +330,30 @@ let destruct_qualif_app (e : texpression) : qualif * texpression list =
 
 (** Destruct an expression into a function call, if possible *)
 let opt_destruct_function_call (e : texpression) :
-    (fun_or_op_id * ty list * texpression list) option =
+    (fun_or_op_id * generic_args * texpression list) option =
   match opt_destruct_qualif_app e with
   | None -> None
   | Some (qualif, args) -> (
       match qualif.id with
-      | FunOrOp fun_id -> Some (fun_id, qualif.type_args, args)
+      | FunOrOp fun_id -> Some (fun_id, qualif.generics, args)
       | _ -> None)
 
 let opt_destruct_result (ty : ty) : ty option =
   match ty with
-  | Adt (Assumed Result, tys, cgs) ->
-      assert (cgs = []);
-      Some (Collections.List.to_cons_nil tys)
+  | Adt (Assumed Result, generics) ->
+      assert (generics.const_generics = []);
+      assert (generics.trait_refs = []);
+      Some (Collections.List.to_cons_nil generics.types)
   | _ -> None
 
 let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty)
 
 let opt_destruct_tuple (ty : ty) : ty list option =
   match ty with
-  | Adt (Tuple, tys, cgs) ->
-      assert (cgs = []);
-      Some tys
+  | Adt (Tuple, generics) ->
+      assert (generics.const_generics = []);
+      assert (generics.trait_refs = []);
+      Some generics.types
   | _ -> None
 
 let mk_abs (x : typed_pattern) (e : texpression) : texpression =
@@ -387,14 +425,16 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression =
     - if there is > one type: wrap them in a tuple
  *)
 let mk_simpl_tuple_ty (tys : ty list) : ty =
-  match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys, [])
+  match tys with
+  | [ ty ] -> ty
+  | _ -> Adt (Tuple, mk_generic_args_from_types tys)
 
 let mk_bool_ty : ty = Literal Bool
-let mk_unit_ty : ty = Adt (Tuple, [], [])
+let mk_unit_ty : ty = Adt (Tuple, empty_generic_args)
 
 let mk_unit_rvalue : texpression =
   let id = AdtCons { adt_id = Tuple; variant_id = None } in
-  let qualif = { id; type_args = []; const_generic_args = [] } in
+  let qualif = { id; generics = empty_generic_args } in
   let e = Qualif qualif in
   let ty = mk_unit_ty in
   { e; ty }
@@ -434,7 +474,7 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
   | [ v ] -> v
   | _ ->
       let tys = List.map (fun (v : typed_pattern) -> v.ty) vl in
-      let ty = Adt (Tuple, tys, []) in
+      let ty = Adt (Tuple, mk_generic_args_from_types tys) in
       let value = PatAdt { variant_id = None; field_values = vl } in
       { value; ty }
 
@@ -445,11 +485,11 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
   | _ ->
       (* Compute the types of the fields, and the type of the tuple constructor *)
       let tys = List.map (fun (v : texpression) -> v.ty) vl in
-      let ty = Adt (Tuple, tys, []) in
+      let ty = Adt (Tuple, mk_generic_args_from_types tys) in
       let ty = mk_arrows tys ty in
       (* Construct the tuple constructor qualifier *)
       let id = AdtCons { adt_id = Tuple; variant_id = None } in
-      let qualif = { id; type_args = tys; const_generic_args = [] } in
+      let qualif = { id; generics = mk_generic_args_from_types tys } in
       (* Put everything together *)
       let cons = { e = Qualif qualif; ty } in
       mk_apps cons vl
@@ -467,32 +507,36 @@ let ty_as_integer (t : ty) : T.integer_type =
 let ty_as_literal (t : ty) : T.literal_type =
   match t with Literal ty -> ty | _ -> raise (Failure "Unreachable")
 
-let mk_state_ty : ty = Adt (Assumed State, [], [])
-let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ], [])
-let mk_error_ty : ty = Adt (Assumed Error, [], [])
-let mk_fuel_ty : ty = Adt (Assumed Fuel, [], [])
+let mk_state_ty : ty = Adt (Assumed State, empty_generic_args)
+
+let mk_result_ty (ty : ty) : ty =
+  Adt (Assumed Result, mk_generic_args_from_types [ ty ])
+
+let mk_error_ty : ty = Adt (Assumed Error, empty_generic_args)
+let mk_fuel_ty : ty = Adt (Assumed Fuel, empty_generic_args)
 
 let mk_error (error : VariantId.id) : texpression =
   let ty = mk_error_ty in
   let id = AdtCons { adt_id = Assumed Error; variant_id = Some error } in
-  let qualif = { id; type_args = []; const_generic_args = [] } in
+  let qualif = { id; generics = empty_generic_args } in
   let e = Qualif qualif in
   { e; ty }
 
 let unwrap_result_ty (ty : ty) : ty =
   match ty with
-  | Adt (Assumed Result, [ ty ], cgs) ->
-      assert (cgs = []);
+  | Adt
+      (Assumed Result, { types = [ ty ]; const_generics = []; trait_refs = [] })
+    ->
       ty
   | _ -> raise (Failure "not a result type")
 
 let mk_result_fail_texpression (error : texpression) (ty : ty) : texpression =
   let type_args = [ ty ] in
-  let ty = Adt (Assumed Result, type_args, []) in
+  let ty = Adt (Assumed Result, mk_generic_args_from_types type_args) in
   let id =
     AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id }
   in
-  let qualif = { id; type_args; const_generic_args = [] } in
+  let qualif = { id; generics = mk_generic_args_from_types type_args } in
   let cons_e = Qualif qualif in
   let cons_ty = mk_arrow error.ty ty in
   let cons = { e = cons_e; ty = cons_ty } in
@@ -505,11 +549,11 @@ let mk_result_fail_texpression_with_error_id (error : VariantId.id) (ty : ty) :
 
 let mk_result_return_texpression (v : texpression) : texpression =
   let type_args = [ v.ty ] in
-  let ty = Adt (Assumed Result, type_args, []) in
+  let ty = Adt (Assumed Result, mk_generic_args_from_types type_args) in
   let id =
     AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id }
   in
-  let qualif = { id; type_args; const_generic_args = [] } in
+  let qualif = { id; generics = mk_generic_args_from_types type_args } in
   let cons_e = Qualif qualif in
   let cons_ty = mk_arrow v.ty ty in
   let cons = { e = cons_e; ty = cons_ty } in
@@ -518,7 +562,7 @@ let mk_result_return_texpression (v : texpression) : texpression =
 (** Create a [Fail err] pattern which captures the error *)
 let mk_result_fail_pattern (error_pat : pattern) (ty : ty) : typed_pattern =
   let error_pat : typed_pattern = { value = error_pat; ty = mk_error_ty } in
-  let ty = Adt (Assumed Result, [ ty ], []) in
+  let ty = Adt (Assumed Result, mk_generic_args_from_types [ ty ]) in
   let value =
     PatAdt { variant_id = Some result_fail_id; field_values = [ error_pat ] }
   in
@@ -530,7 +574,7 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern =
   mk_result_fail_pattern error_pat ty
 
 let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
-  let ty = Adt (Assumed Result, [ v.ty ], []) in
+  let ty = Adt (Assumed Result, mk_generic_args_from_types [ v.ty ]) in
   let value =
     PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
   in
@@ -565,11 +609,11 @@ let rec typed_pattern_to_texpression (pat : typed_pattern) : texpression option
           let fields_values = List.map (fun e -> Option.get e) fields in
 
           (* Retrieve the type id and the type args from the pat type (simpler this way *)
-          let adt_id, type_args, const_generic_args = ty_as_adt pat.ty in
+          let adt_id, generics = ty_as_adt pat.ty in
 
           (* Create the constructor *)
           let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
-          let qualif = { id = qualif_id; type_args; const_generic_args } in
+          let qualif = { id = qualif_id; generics } in
           let cons_e = Qualif qualif in
           let field_tys =
             List.map (fun (v : texpression) -> v.ty) fields_values
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 38850243..64e7716a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -9,51 +9,53 @@ module E = Expressions
 module A = LlbcAst
 module C = Contexts
 
-(** Substitute types variables and regions in a type. *)
-let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : 'r1 T.ty) :
-    'r2 T.ty =
-  let open T in
-  let visitor =
-    object
-      inherit [_] map_ty
-      method visit_'r _ r = rsubst r
-      method! visit_TypeVar _ id = tsubst id
-
-      method! visit_type_var_id _ _ =
-        (* We should never get here because we reimplemented [visit_TypeVar] *)
-        raise (Failure "Unexpected")
+type ('r1, 'r2) subst = {
+  r_subst : 'r1 -> 'r2;
+  ty_subst : T.TypeVarId.id -> 'r2 T.ty;
+  cg_subst : T.ConstGenericVarId.id -> T.const_generic;
+      (** Substitution from *local* trait clause to trait instance *)
+  tr_subst : T.TraitClauseId.id -> 'r2 T.trait_instance_id;
+      (** Substitution for the [Self] trait instance *)
+  tr_self : 'r2 T.trait_instance_id;
+}
+
+let ty_substitute_visitor (subst : ('r1, 'r2) subst) =
+  object
+    inherit [_] T.map_ty
+    method visit_'r _ r = subst.r_subst r
+    method! visit_TypeVar _ id = subst.ty_subst id
 
-      method! visit_ConstGenericVar _ id = cgsubst id
+    method! visit_type_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_TypeVar] *)
+      raise (Failure "Unexpected")
 
-      method! visit_const_generic_var_id _ _ =
-        (* We should never get here because we reimplemented [visit_Var] *)
-        raise (Failure "Unexpected")
-    end
-  in
+    method! visit_ConstGenericVar _ id = subst.cg_subst id
 
-  visitor#visit_ty () ty
+    method! visit_const_generic_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_Var] *)
+      raise (Failure "Unexpected")
 
-let rty_substitute (rsubst : T.RegionId.id -> T.RegionId.id)
-    (tsubst : T.TypeVarId.id -> T.rty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.rty) : T.rty =
-  let rsubst r =
-    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
-  in
-  ty_substitute rsubst tsubst cgsubst ty
+    method! visit_Clause _ id = subst.tr_subst id
+    method! visit_Self _ = subst.tr_self
+  end
 
-let ety_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.ety) : T.ety =
-  let rsubst r = r in
-  ty_substitute rsubst tsubst cgsubst ty
+(** Substitute types variables and regions in a type. *)
+let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty =
+  let visitor = ty_substitute_visitor subst in
+  visitor#visit_ty () ty
 
 (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
 let erase_regions (ty : T.rty) : T.ety =
-  ty_substitute
-    (fun _ -> T.Erased)
-    (fun vid -> T.TypeVar vid)
-    (fun id -> T.ConstGenericVar id)
-    ty
+  let subst =
+    {
+      r_subst = (fun _ -> T.Erased);
+      ty_subst = (fun vid -> T.TypeVar vid);
+      cg_subst = (fun id -> T.ConstGenericVar id);
+      tr_subst = (fun id -> T.Clause id);
+      tr_self = T.Self;
+    }
+  in
+  ty_substitute subst ty
 
 (** Generate fresh regions for region variables.
 
@@ -78,18 +80,20 @@ let fresh_regions_with_substs (region_vars : T.region_var list) :
   (* Generate the substitution from region var id to region *)
   let rid_subst id = T.RegionVarId.Map.find id rid_map in
   (* Generate the substitution from region to region *)
-  let rsubst r =
+  let r_subst r =
     match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
   in
   (* Return *)
-  (fresh_region_ids, rid_subst, rsubst)
+  (fresh_region_ids, rid_subst, r_subst)
 
-(** Erase the regions in a type and substitute the type variables *)
-let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic)
-    (ty : 'r T.region T.ty) : T.ety =
-  let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
-  ty_substitute rsubst tsubst cgsubst ty
+(** Erase the regions in a type and perform a substitution *)
+let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ety)
+    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
+    (tr_subst : T.TraitClauseId.id -> T.etrait_instance_id)
+    (tr_self : T.etrait_instance_id) (ty : 'r T.ty) : T.ety =
+  let r_subst (_ : 'r) : T.erased_region = T.Erased in
+  let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in
+  ty_substitute subst ty
 
 (** Create a region substitution from a list of region variable ids and a list of
     regions (with which to substitute the region variable ids *)
@@ -146,16 +150,62 @@ let make_const_generic_subst_from_vars (vars : T.const_generic_var list)
     (List.map (fun (x : T.const_generic_var) -> x.T.index) vars)
     cgs
 
-(** Instantiate the type variables in an ADT definition, and return, for
-    every variant, the list of the types of its fields *)
-let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : (T.VariantId.id option * T.rty list) list =
-  let r_subst = make_region_subst_from_vars def.T.region_params regions in
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
+(** Create a trait substitution from a list of trait clause ids and a list of
+    trait refs *)
+let make_trait_subst (clause_ids : T.TraitClauseId.id list)
+    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+  let ls = List.combine clause_ids trs in
+  let mp =
+    List.fold_left
+      (fun mp (k, v) -> T.TraitClauseId.Map.add k (T.TraitRef v) mp)
+      T.TraitClauseId.Map.empty ls
+  in
+  fun id -> T.TraitClauseId.Map.find id mp
+
+let make_trait_subst_from_clauses (clauses : T.trait_clause list)
+    (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id =
+  make_trait_subst
+    (List.map (fun (x : T.trait_clause) -> x.T.clause_id) clauses)
+    trs
+
+let make_subst_from_generics (params : T.generic_params)
+    (args : 'r T.generic_args) (tr_self : 'r T.trait_instance_id) :
+    (T.region_var_id T.region, 'r) subst =
+  let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in
+  let ty_subst = make_type_subst_from_vars params.T.types args.T.types in
+  let cg_subst =
+    make_const_generic_subst_from_vars params.T.const_generics
+      args.T.const_generics
+  in
+  let tr_subst =
+    make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs
+  in
+  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+
+let make_esubst_from_generics (params : T.generic_params)
+    (generics : T.egeneric_args) (tr_self : T.etrait_instance_id) =
+  let r_subst _ = T.Erased in
+  let ty_subst = make_type_subst_from_vars params.types generics.T.types in
   let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
+    make_const_generic_subst_from_vars params.const_generics
+      generics.T.const_generics
   in
+  let tr_subst =
+    make_trait_subst_from_clauses params.trait_clauses generics.T.trait_refs
+  in
+  { r_subst; ty_subst; cg_subst; tr_subst; tr_self }
+
+(** Instantiate the type variables in an ADT definition, and return, for
+    every variant, the list of the types of its fields.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
+let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
+    (generics : T.rgeneric_args) : (T.VariantId.id option * T.rty list) list =
+  (* There shouldn't be any reference to Self *)
+  let tr_self = T.UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.T.generics generics tr_self in
   let (variants_fields : (T.VariantId.id option * T.field list) list) =
     match def.T.kind with
     | T.Enum variants ->
@@ -171,191 +221,218 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
   in
   List.map
     (fun (id, fields) ->
-      ( id,
-        List.map
-          (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
-          fields ))
+      (id, List.map (fun f -> ty_substitute subst f.T.field_ty) fields))
     variants_fields
 
 (** Instantiate the type variables in an ADT definition, and return the list
-    of types of the fields for the chosen variant *)
+    of types of the fields for the chosen variant.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : T.rty list =
-  let r_subst = make_region_subst_from_vars def.T.region_params regions in
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
-  let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
-  in
+    (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) :
+    T.rty list =
+  (* For now, check that there are no clauses - otherwise we might need
+     to normalize the types *)
+  assert (def.generics.trait_clauses = []);
+  (* There shouldn't be any reference to Self *)
+  let tr_self = T.UnknownTrait __FUNCTION__ in
+  let subst = make_subst_from_generics def.T.generics generics tr_self in
   let fields = TU.type_decl_get_fields def opt_variant_id in
-  List.map
-    (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
-    fields
+  List.map (fun f -> ty_substitute subst f.T.field_ty) fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
-    context *)
+    context.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (cgs : T.const_generic list) : T.rty list =
+    (generics : T.rgeneric_args) : T.rty list =
   let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_rtypes def opt_variant_id regions types cgs
+  type_decl_get_instantiated_field_rtypes def opt_variant_id generics
 
 (** Return the types of the properly instantiated ADT value (note that
-    here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *)
+    here, ADT is understood in its broad meaning: ADT, assumed value or tuple).
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+ *)
 let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
-    (adt : V.adt_value) (id : T.type_id)
-    (region_params : T.RegionId.id T.region list) (type_params : T.rty list)
-    (cg_params : T.const_generic list) : T.rty list =
+    (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) :
+    T.rty list =
   match id with
   | T.AdtId id ->
       (* Retrieve the types of the fields *)
-      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id
-        region_params type_params cg_params
+      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id generics
   | T.Tuple ->
-      assert (List.length region_params = 0);
-      type_params
+      assert (generics.regions = []);
+      generics.types
   | T.Assumed aty -> (
       match aty with
       | T.Box | T.Vec ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          generics.types
       | T.Option ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          if adt.V.variant_id = Some T.option_some_id then type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          if adt.V.variant_id = Some T.option_some_id then generics.types
           else if adt.V.variant_id = Some T.option_none_id then []
           else raise (Failure "Unreachable")
       | T.Range ->
-          assert (List.length region_params = 0);
-          assert (List.length type_params = 1);
-          assert (List.length cg_params = 0);
-          type_params
+          assert (generics.regions = []);
+          assert (List.length generics.types = 1);
+          assert (generics.const_generics = []);
+          generics.types
       | T.Array | T.Slice | T.Str ->
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
 
 (** Instantiate the type variables in an ADT definition, and return the list
-    of types of the fields for the chosen variant *)
+    of types of the fields for the chosen variant.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+*)
 let type_decl_get_instantiated_field_etypes (def : T.type_decl)
-    (opt_variant_id : T.VariantId.id option) (types : T.ety list)
-    (cgs : T.const_generic list) : T.ety list =
-  let ty_subst = make_type_subst_from_vars def.T.type_params types in
-  let cg_subst =
-    make_const_generic_subst_from_vars def.T.const_generic_params cgs
+    (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) :
+    T.ety list =
+  (* For now, check that there are no clauses - otherwise we might need
+     to normalize the types *)
+  assert (def.generics.trait_clauses = []);
+  (* There shouldn't be any reference to Self *)
+  let tr_self : T.erased_region T.trait_instance_id =
+    T.UnknownTrait __FUNCTION__
+  in
+  let { r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+    make_esubst_from_generics def.T.generics generics tr_self
   in
   let fields = TU.type_decl_get_fields def opt_variant_id in
   List.map
-    (fun f -> erase_regions_substitute_types ty_subst cg_subst f.T.field_ty)
+    (fun (f : T.field) ->
+      erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+        f.T.field_ty)
     fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
-    context *)
+    context.
+
+    **IMPORTANT**: this function doesn't normalize the types, you may want to
+    use the [AssociatedTypes] equivalent instead.
+ *)
 let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (types : T.ety list) (cgs : T.const_generic list) : T.ety list =
+    (generics : T.egeneric_args) : T.ety list =
   let def = C.ctx_lookup_type_decl ctx def_id in
-  type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
+  type_decl_get_instantiated_field_etypes def opt_variant_id generics
 
-let statement_substitute_visitor (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) =
+let statement_substitute_visitor
+    (subst : (T.erased_region, T.erased_region) subst) =
+  (* Keep in synch with [ty_substitute_visitor] *)
   object
     inherit [_] A.map_statement
-    method! visit_ety _ ty = ety_substitute tsubst cgsubst ty
-    method! visit_ConstGenericVar _ id = cgsubst id
+    method! visit_'r _ r = subst.r_subst r
+    method! visit_TypeVar _ id = subst.ty_subst id
+
+    method! visit_type_var_id _ _ =
+      (* We should never get here because we reimplemented [visit_TypeVar] *)
+      raise (Failure "Unexpected")
+
+    method! visit_ConstGenericVar _ id = subst.cg_subst id
 
     method! visit_const_generic_var_id _ _ =
       (* We should never get here because we reimplemented [visit_Var] *)
       raise (Failure "Unexpected")
+
+    method! visit_Clause _ id = subst.tr_subst id
+    method! visit_Self _ = subst.tr_self
   end
 
 (** Apply a type substitution to a place *)
-let place_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (p : E.place) :
-    E.place =
+let place_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (p : E.place) : E.place =
   (* There is in fact nothing to do *)
-  (statement_substitute_visitor tsubst cgsubst)#visit_place () p
+  (statement_substitute_visitor subst)#visit_place () p
 
 (** Apply a type substitution to an operand *)
-let operand_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (op : E.operand) :
-    E.operand =
-  (statement_substitute_visitor tsubst cgsubst)#visit_operand () op
+let operand_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (op : E.operand) : E.operand =
+  (statement_substitute_visitor subst)#visit_operand () op
 
 (** Apply a type substitution to an rvalue *)
-let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (rv : E.rvalue) :
-    E.rvalue =
-  (statement_substitute_visitor tsubst cgsubst)#visit_rvalue () rv
+let rvalue_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (rv : E.rvalue) : E.rvalue =
+  (statement_substitute_visitor subst)#visit_rvalue () rv
 
 (** Apply a type substitution to an assertion *)
-let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (a : A.assertion) :
-    A.assertion =
-  (statement_substitute_visitor tsubst cgsubst)#visit_assertion () a
+let assertion_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (a : A.assertion) : A.assertion =
+  (statement_substitute_visitor subst)#visit_assertion () a
 
 (** Apply a type substitution to a call *)
-let call_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (call : A.call) :
-    A.call =
-  (statement_substitute_visitor tsubst cgsubst)#visit_call () call
+let call_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (call : A.call) : A.call =
+  (statement_substitute_visitor subst)#visit_call () call
 
 (** Apply a type substitution to a statement *)
-let statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (st : A.statement) :
-    A.statement =
-  (statement_substitute_visitor tsubst cgsubst)#visit_statement () st
+let statement_substitute (subst : (T.erased_region, T.erased_region) subst)
+    (st : A.statement) : A.statement =
+  (statement_substitute_visitor subst)#visit_statement () st
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
-let fun_body_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (body : A.fun_body) :
+let fun_body_substitute_in_body
+    (subst : (T.erased_region, T.erased_region) subst) (body : A.fun_body) :
     A.var list * A.statement =
-  let rsubst r = r in
   let locals =
     List.map
-      (fun (v : A.var) ->
-        { v with A.var_ty = ty_substitute rsubst tsubst cgsubst v.A.var_ty })
+      (fun (v : A.var) -> { v with A.var_ty = ty_substitute subst v.A.var_ty })
       body.A.locals
   in
-  let body = statement_substitute tsubst cgsubst body.body in
+  let body = statement_substitute subst body.body in
   (locals, body)
 
-(** Substitute a function signature *)
+(** Substitute a function signature.
+
+    **IMPORTANT:** this function doesn't normalize the types.
+ *)
 let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
-    (rsubst : T.RegionVarId.id -> T.RegionId.id)
-    (tsubst : T.TypeVarId.id -> T.rty)
-    (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (sg : A.fun_sig) :
-    A.inst_fun_sig =
-  let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
-    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+    (r_subst : T.RegionVarId.id -> T.RegionId.id)
+    (ty_subst : T.TypeVarId.id -> T.rty)
+    (cg_subst : T.ConstGenericVarId.id -> T.const_generic)
+    (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id)
+    (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig =
+  let r_subst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
+    match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
   in
-  let inputs = List.map (ty_substitute rsubst' tsubst cgsubst) sg.A.inputs in
-  let output = ty_substitute rsubst' tsubst cgsubst sg.A.output in
+  let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
+  let inputs = List.map (ty_substitute subst) sg.A.inputs in
+  let output = ty_substitute subst sg.A.output in
   let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
     let id = asubst rg.id in
-    let regions = List.map rsubst rg.regions in
+    let regions = List.map r_subst rg.regions in
     let parents = List.map asubst rg.parents in
     { id; regions; parents }
   in
   let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
   { A.regions_hierarchy; inputs; output }
 
-(** Substitute type variable identifiers in a type *)
-let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
+(** Substitute variable identifiers in a type *)
+let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
     : 'r T.ty =
   let open T in
   let visitor =
     object
       inherit [_] map_ty
       method visit_'r _ r = r
-      method! visit_type_var_id _ id = tsubst id
-      method! visit_const_generic_var_id _ id = cgsubst id
+      method! visit_type_var_id _ id = ty_subst id
+      method! visit_const_generic_var_id _ id = cg_subst id
     end
   in
 
@@ -371,10 +448,10 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
    [visit_'r] if we define a class which visits objects of types [ety] and [rty]
    while inheriting a class which visit [ty]...
 *)
-let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
+let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) =
@@ -383,10 +460,10 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       inherit [_] T.map_ty
 
       method visit_'r _ r =
-        match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+        match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid)
 
-      method! visit_type_var_id _ id = tsubst id
-      method! visit_const_generic_var_id _ id = cgsubst id
+      method! visit_type_var_id _ id = ty_subst id
+      method! visit_const_generic_var_id _ id = cg_subst id
     end
   in
 
@@ -395,7 +472,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       inherit [_] C.map_env
       method! visit_borrow_id _ bid = bsubst bid
       method! visit_loan_id _ bid = bsubst bid
-      method! visit_ety _ ty = ty_substitute_ids tsubst cgsubst ty
+      method! visit_ety _ ty = ty_substitute_ids ty_subst cg_subst ty
       method! visit_rty env ty = subst_rty#visit_ty env ty
       method! visit_symbolic_value_id _ id = ssubst id
 
@@ -405,7 +482,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       (** We *do* visit meta-values *)
       method! visit_mvalue env v = self#visit_typed_value env v
 
-      method! visit_region_id _ id = rsubst id
+      method! visit_region_id _ id = r_subst id
       method! visit_region_var_id _ id = rvsubst id
       method! visit_abstraction_id _ id = asubst id
     end
@@ -425,20 +502,20 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
     method visit_env (env : C.env) : C.env = visitor#visit_env () env
   end
 
-let typed_value_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_value_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) :
     V.typed_value =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_typed_value v
 
-let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (v : V.typed_value) : V.typed_value =
-  typed_value_subst_ids rsubst
+  typed_value_subst_ids r_subst
     (fun x -> x)
     (fun x -> x)
     (fun x -> x)
@@ -446,41 +523,41 @@ let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
     (fun x -> x)
     v
 
-let typed_avalue_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_avalue_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) :
     V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_typed_avalue v
 
-let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let abs_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_abs x
 
-let env_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
+let env_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id)
     (rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
-    (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
-    (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
+    (ty_subst : T.TypeVarId.id -> T.TypeVarId.id)
+    (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
     (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
     (bsubst : V.BorrowId.id -> V.BorrowId.id)
     (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
-  (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+  (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst)
     #visit_env x
 
-let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id)
     (x : V.typed_avalue) : V.typed_avalue =
   let asubst _ = raise (Failure "Unreachable") in
-  (subst_ids_visitor rsubst
+  (subst_ids_visitor r_subst
      (fun x -> x)
      (fun x -> x)
      (fun x -> x)
@@ -490,9 +567,9 @@ let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
     #visit_typed_avalue
     x
 
-let env_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) (x : C.env) : C.env
-    =
-  (subst_ids_visitor rsubst
+let env_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : C.env) :
+    C.env =
+  (subst_ids_visitor r_subst
      (fun x -> x)
      (fun x -> x)
      (fun x -> x)
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 17cdcabc..0f107897 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -43,10 +43,7 @@ type call = {
           borrows (we need to perform lookups).
        *)
   abstractions : V.AbstractionId.id list;
-  (* TODO: rename to "...args" *)
-  type_params : T.ety list;
-  (* TODO: rename to "...args" *)
-  const_generic_params : T.const_generic list;
+  generics : T.egeneric_args;
   args : V.typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dda1f22..6c2c049b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -52,6 +52,9 @@ type fun_context = {
 type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
 [@@deriving show]
 
+type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
+type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
+
 (** Whenever we translate a function call or an ended abstraction, we
     store the related information (this is useful when translating ended
     children abstractions).
@@ -120,6 +123,8 @@ type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
   global_context : global_context;
+  trait_decls_ctx : trait_decls_context;
+  trait_impls_ctx : trait_impls_context;
   fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   sg : fun_sig;
@@ -205,7 +210,7 @@ type bs_ctx = {
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
   Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
     ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
-    ctx.fun_decl
+    ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
 
 let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
   let rvar_to_string = Print.Types.region_var_id_to_string in
@@ -223,16 +228,19 @@ let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
     adt_variant_to_string = ast_fmt.adt_variant_to_string;
     var_id_to_string;
     adt_field_names = ast_fmt.adt_field_names;
+    trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
+    trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
+    trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
   }
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
-  let type_params = ctx.fun_decl.signature.type_params in
-  let cg_params = ctx.fun_decl.signature.const_generic_params in
+  let generics = ctx.fun_decl.signature.generics in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
-    cg_params
+  PrintPure.mk_ast_formatter type_decls fun_decls global_decls
+    ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
+    generics.const_generics
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
@@ -254,12 +262,11 @@ let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
   Print.PT.rty_to_string fmt ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
-  let type_params = def.type_params in
-  let cg_params = def.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
-    PrintPure.mk_type_formatter type_decls global_decls type_params cg_params
+    PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
+      ctx.trait_impls_ctx def.generics.types def.generics.const_generics
   in
   PrintPure.type_decl_to_string fmt def
 
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 857fea97..cac56487 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
             assert (otherwise_see = None);
             (* Return *)
             ExpandInt (int_ty, branches, otherwise)
-        | T.Adt (_, _, _, _) ->
+        | T.Adt (_, _) ->
             (* Branching: it is necessarily an enumeration expansion *)
             let get_variant (see : V.symbolic_expansion option) :
                 T.VariantId.id option * V.symbolic_value list =
@@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
             | _ -> raise (Failure "Ill-formed borrow expansion"))
-        | T.TypeVar _ | T.Literal Char | Never ->
+        | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ ->
             raise (Failure "Ill-formed symbolic expansion")
       in
       Some (Expansion (place, sv, expansion))
@@ -97,10 +97,10 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
   synthesize_symbolic_expansion sv place [ Some see ] el
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
-    (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
-    (const_generic_params : T.const_generic list) (args : V.typed_value list)
-    (args_places : mplace option list) (dest : V.symbolic_value)
-    (dest_place : mplace option) (e : expression option) : expression option =
+    (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args)
+    (args : V.typed_value list) (args_places : mplace option list)
+    (dest : V.symbolic_value) (dest_place : mplace option)
+    (e : expression option) : expression option =
   Option.map
     (fun e ->
       let call =
@@ -108,8 +108,7 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
           call_id;
           ctx;
           abstractions;
-          type_params;
-          const_generic_params;
+          generics;
           args;
           dest;
           args_places;
@@ -125,26 +124,27 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
 
 let synthesize_regular_function_call (fun_id : A.fun_id)
     (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx)
-    (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
-    (const_generic_params : T.const_generic list) (args : V.typed_value list)
-    (args_places : mplace option list) (dest : V.symbolic_value)
-    (dest_place : mplace option) (e : expression option) : expression option =
+    (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args)
+    (args : V.typed_value list) (args_places : mplace option list)
+    (dest : V.symbolic_value) (dest_place : mplace option)
+    (e : expression option) : expression option =
   synthesize_function_call
     (Fun (fun_id, call_id))
-    ctx abstractions type_params const_generic_params args args_places dest
-    dest_place e
+    ctx abstractions generics args args_places dest dest_place e
 
 let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop)
     (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
-  synthesize_function_call (Unop unop) ctx [] [] [] [ arg ] [ arg_place ] dest
-    dest_place e
+  let generics = TypesUtils.mk_empty_generic_args in
+  synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ]
+    dest dest_place e
 
 let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop)
     (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value)
     (arg1_place : mplace option) (dest : V.symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
-  synthesize_function_call (Binop binop) ctx [] [] [] [ arg0; arg1 ]
+  let generics = TypesUtils.mk_empty_generic_args in
+  synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ]
     [ arg0_place; arg1_place ] dest dest_place e
 
 let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 70ef5e3d..ca661108 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -280,9 +280,7 @@ let translate_crate_to_pure (crate : A.crate) :
   log#ldebug (lazy "translate_crate_to_pure");
 
   (* Compute the type and function contexts *)
-  let type_context, fun_context, global_context =
-    compute_type_fun_global_contexts crate
-  in
+  let type_context, fun_context, global_context = compute_contexts crate in
   let fun_infos =
     FA.analyze_module crate fun_context.C.fun_decls
       global_context.C.global_decls !Config.use_state
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 925f6d39..95c7206a 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -14,11 +14,10 @@ type expl_info = subtype_info [@@deriving show]
 
 type type_borrows_info = {
   contains_static : bool;
-      (** Does the type (transitively) contains a static borrow? *)
-  contains_borrow : bool;
-      (** Does the type (transitively) contains a borrow? *)
+      (** Does the type (transitively) contain a static borrow? *)
+  contains_borrow : bool;  (** Does the type (transitively) contain a borrow? *)
   contains_nested_borrows : bool;
-      (** Does the type (transitively) contains nested borrows? *)
+      (** Does the type (transitively) contain nested borrows? *)
   contains_borrow_under_mut : bool;
 }
 [@@deriving show]
@@ -61,7 +60,7 @@ let initialize_g_type_info (param_infos : 'p) : 'p g_type_info =
 
 let initialize_type_decl_info (def : type_decl) : type_decl_info =
   let param_info = { under_borrow = false; under_mut_borrow = false } in
-  let param_infos = List.map (fun _ -> param_info) def.type_params in
+  let param_infos = List.map (fun _ -> param_info) def.generics.types in
   initialize_g_type_info param_infos
 
 let type_decl_info_to_partial_type_info (info : type_decl_info) :
@@ -122,7 +121,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
   let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
       (ty : 'r ty) : partial_type_info =
     match ty with
-    | Literal _ | Never -> ty_info
+    | Literal _ | Never | TraitType _ -> ty_info
     | TypeVar var_id -> (
         (* Update the information for the proper parameter, if necessary *)
         match ty_info.param_infos with
@@ -171,20 +170,18 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         analyze expl_info ty_info rty
     | Adt
         ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)),
-          _,
-          tys,
-          _ ) ->
+          generics ) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
           (fun ty_info ty -> analyze expl_info ty_info ty)
-          ty_info tys
-    | Adt (AdtId adt_id, regions, tys, _cgs) ->
+          ty_info generics.types
+    | Adt (AdtId adt_id, generics) ->
         (* Lookup the information for this type definition *)
         let adt_info = TypeDeclId.Map.find adt_id infos in
         (* Update the type info with the information from the adt *)
         let ty_info = update_ty_info ty_info adt_info.borrows_info in
         (* Check if 'static appears in the region parameters *)
-        let found_static = List.exists r_is_static regions in
+        let found_static = List.exists r_is_static generics.regions in
         let borrows_info = ty_info.borrows_info in
         let borrows_info =
           {
@@ -196,7 +193,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         let ty_info = { ty_info with borrows_info } in
         (* For every instantiated type parameter: update the exploration info
          * then explore the type *)
-        let params_tys = List.combine adt_info.param_infos tys in
+        let params_tys = List.combine adt_info.param_infos generics.types in
         let ty_info =
           List.fold_left
             (fun ty_info (param_info, ty) ->
diff --git a/compiler/dune b/compiler/dune
index 6785cad4..db099c3c 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -12,6 +12,7 @@
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
  (libraries charon core_unix unionFind ocamlgraph)
  (modules
+  AssociatedTypes
   Assumed
   Collections
   Config