Prefix variants related to types with "T"

27 files changed, 320 insertions, 321 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index c76af138..d5c9596e 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -55,7 +55,7 @@ let compute_norm_trait_types_from_preds
        that it would be enough to only visit the field [ty] of the trait type
        constraint, but for safety we visit all the fields *)
     assert (TU.trait_type_constraint_no_regions c);
-    let trait_ty = T.TraitType (c.trait_ref, c.generics, c.type_name) in
+    let trait_ty = T.TTraitType (c.trait_ref, c.generics, c.type_name) in
     let trait_ty_ref = get_ref trait_ty in
     let ty_ref = get_ref c.ty in
     let new_repr = UF.get ty_ref in
@@ -76,7 +76,7 @@ let compute_norm_trait_types_from_preds
     List.filter_map
       (fun (k, v) ->
         match k with
-        | T.TraitType (trait_ref, generics, type_name) ->
+        | T.TTraitType (trait_ref, generics, type_name) ->
             assert (generics = TypesUtils.mk_empty_generic_args);
             Some ({ C.trait_ref; type_name }, v)
         | _ -> None)
@@ -182,18 +182,18 @@ let rec ctx_normalize_ty (ctx : norm_ctx) (ty : T.ty) : T.ty =
   log#ldebug (lazy ("ctx_normalize_ty: " ^ ty_to_string ctx ty));
   match ty with
   | T.TAdt (id, generics) -> TAdt (id, ctx_normalize_generic_args ctx generics)
-  | TypeVar _ | TLiteral _ | Never -> ty
-  | Ref (r, ty, rkind) ->
+  | TVar _ | TLiteral _ | TNever -> ty
+  | TRef (r, ty, rkind) ->
       let ty = ctx_normalize_ty ctx ty in
-      T.Ref (r, ty, rkind)
-  | RawPtr (ty, rkind) ->
+      T.TRef (r, ty, rkind)
+  | TRawPtr (ty, rkind) ->
       let ty = ctx_normalize_ty ctx ty in
-      RawPtr (ty, rkind)
-  | Arrow (inputs, output) ->
+      TRawPtr (ty, rkind)
+  | TArrow (inputs, output) ->
       let inputs = List.map (ctx_normalize_ty ctx) inputs in
       let output = ctx_normalize_ty ctx output in
-      Arrow (inputs, output)
-  | TraitType (trait_ref, generics, type_name) -> (
+      TArrow (inputs, output)
+  | TTraitType (trait_ref, generics, type_name) -> (
       log#ldebug
         (lazy
           ("ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty
@@ -250,7 +250,7 @@ let rec ctx_normalize_ty (ctx : norm_ctx) (ty : T.ty) : T.ty =
                 ^ "\n- raw trait ref:\n" ^ T.show_trait_ref trait_ref));
             (* We can't project *)
             assert (trait_instance_id_is_local_clause trait_ref.trait_id);
-            T.TraitType (trait_ref, generics, type_name)
+            T.TTraitType (trait_ref, generics, type_name)
       in
       let tr : C.trait_type_ref = { C.trait_ref; type_name } in
       (* Lookup the representative, if there is *)
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 5622ef26..cf81502c 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -41,7 +41,7 @@ module Sig = struct
   let rvar_0 : T.region = T.RVar rvar_id_0
   let rg_id_0 = T.RegionGroupId.of_int 0
   let tvar_id_0 = T.TypeVarId.of_int 0
-  let tvar_0 : T.ty = T.TypeVar tvar_id_0
+  let tvar_0 : T.ty = T.TVar tvar_id_0
   let cgvar_id_0 = T.ConstGenericVarId.of_int 0
   let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0
 
@@ -150,13 +150,13 @@ module Sig = struct
   let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig =
     (* Array<T, N> *)
     let input_ty id =
-      if is_array then mk_array_ty (T.TypeVar id) cgvar_0
-      else mk_slice_ty (T.TypeVar id)
+      if is_array then mk_array_ty (T.TVar id) cgvar_0
+      else mk_slice_ty (T.TVar id)
     in
     (* usize *)
     let index_ty = usize_ty in
     (* T *)
-    let output_ty id = T.TypeVar id in
+    let output_ty id = T.TVar id in
     let cgs = if is_array then [ cg_param_0 ] else [] in
     mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut
 
@@ -165,9 +165,9 @@ module Sig = struct
 
   let array_to_slice_sig (is_mut : bool) : A.fun_sig =
     (* Array<T, N> *)
-    let input_ty id = mk_array_ty (T.TypeVar id) cgvar_0 in
+    let input_ty id = mk_array_ty (T.TVar id) cgvar_0 in
     (* Slice<T> *)
-    let output_ty id = mk_slice_ty (T.TypeVar id) in
+    let output_ty id = mk_slice_ty (T.TVar id) in
     let cgs = [ cg_param_0 ] in
     mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 24999c7d..04f6c2c3 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -124,7 +124,7 @@ let extract_adt_g_value
     (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
     (ty : ty) : extraction_ctx =
   match ty with
-  | TAdt (Tuple, generics) ->
+  | TAdt (TTuple, generics) ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
       assert (List.length generics.types = List.length field_values);
@@ -871,7 +871,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
      thus extracted to unit. We need to check that by looking up the definition *)
   let extract_as_unit =
     match (!backend, supd.struct_id) with
-    | HOL4, AdtId adt_id ->
+    | HOL4, TAdtId adt_id ->
         let d = TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls in
         d.kind = Struct []
     | _ -> false
@@ -885,7 +885,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
        - this is an array
     *)
     match supd.struct_id with
-    | AdtId _ ->
+    | TAdtId _ ->
         F.pp_open_hvbox fmt 0;
         F.pp_open_hvbox fmt ctx.indent_incr;
         (* Inner/outer brackets: there are several syntaxes for the field updates.
@@ -966,7 +966,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         if need_paren then F.pp_print_string fmt ")";
         print_bracket false orb;
         F.pp_close_box fmt ()
-    | TAssumed Array ->
+    | TAssumed TArray ->
         (* Open the boxes *)
         F.pp_open_hvbox fmt ctx.indent_incr;
         let need_paren = inside in
@@ -974,7 +974,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         (* Open the box for `Array.replicate T N [` *)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the array constructor *)
-        let cs = ctx_get_struct (TAssumed Array) ctx in
+        let cs = ctx_get_struct (TAssumed TArray) ctx in
         F.pp_print_string fmt cs;
         (* Print the parameters *)
         let _, generics = ty_as_adt e_ty in
@@ -2662,7 +2662,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt "=";
         F.pp_print_space fmt ();
-        let success = ctx_get_variant (TAssumed Result) result_return_id ctx in
+        let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
         F.pp_print_string fmt (success ^ " ())")
     | Coq ->
         F.pp_print_string fmt "Check";
@@ -2691,7 +2691,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
-        let success = ctx_get_variant (TAssumed Result) result_return_id ctx in
+        let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
         F.pp_print_string fmt ("." ^ success ^ " ())")
     | HOL4 ->
         F.pp_print_string fmt "val _ = assert_return (";
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 272e6396..d5eac6f4 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -672,11 +672,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   (* TODO: factorize the pretty-printing with what is in PrintPure *)
   let get_type_name (id : type_id) : string =
     match id with
-    | AdtId id ->
+    | TAdtId id ->
         let def = TypeDeclId.Map.find id type_decls in
         Print.name_to_string def.name
     | TAssumed aty -> show_assumed_ty aty
-    | Tuple -> raise (Failure "Unreachable")
+    | TTuple -> raise (Failure "Unreachable")
   in
   match id with
   | GlobalId gid ->
@@ -744,26 +744,26 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | VariantId (id, variant_id) ->
       let variant_name =
         match id with
-        | Tuple -> raise (Failure "Unreachable")
-        | TAssumed Result ->
+        | TTuple -> raise (Failure "Unreachable")
+        | TAssumed TResult ->
             if variant_id = result_return_id then "@result::Return"
             else if variant_id = result_fail_id then "@result::Fail"
             else raise (Failure "Unreachable")
-        | TAssumed Error ->
+        | TAssumed TError ->
             if variant_id = error_failure_id then "@error::Failure"
             else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
             else raise (Failure "Unreachable")
-        | TAssumed Fuel ->
+        | TAssumed TFuel ->
             if variant_id = fuel_zero_id then "@fuel::0"
             else if variant_id = fuel_succ_id then "@fuel::Succ"
             else raise (Failure "Unreachable")
-        | TAssumed (State | Array | Slice | Str | RawPtr _) ->
+        | TAssumed (TState | TArray | TSlice | TStr | TRawPtr _) ->
             raise
               (Failure
                  ("Unreachable: variant id ("
                  ^ VariantId.to_string variant_id
                  ^ ") for " ^ show_type_id id))
-        | AdtId id -> (
+        | TAdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Struct _ | Opaque -> raise (Failure "Unreachable")
@@ -775,12 +775,13 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | FieldId (id, field_id) ->
       let field_name =
         match id with
-        | Tuple -> raise (Failure "Unreachable")
+        | TTuple -> raise (Failure "Unreachable")
         | TAssumed
-            (State | Result | Error | Fuel | Array | Slice | Str | RawPtr _) ->
+            ( TState | TResult | TError | TFuel | TArray | TSlice | TStr
+            | TRawPtr _ ) ->
             (* We can't directly have access to the fields of those types *)
             raise (Failure "Unreachable")
-        | AdtId id -> (
+        | TAdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Enum _ | Opaque -> raise (Failure "Unreachable")
@@ -954,11 +955,11 @@ let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
   ctx_get_function (FromLlbc (FunId (FRegular id), lp, rg)) ctx
 
 let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
-  assert (id <> Tuple);
+  assert (id <> TTuple);
   ctx_get (TypeId id) ctx
 
 let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
-  ctx_get_type (AdtId id) ctx
+  ctx_get_type (TAdtId id) ctx
 
 let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
   ctx_get_type (TAssumed id) ctx
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 902b7e25..553d5863 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -226,69 +226,69 @@ let assumed_adts () : (assumed_ty * string) list =
   match !backend with
   | Lean ->
       [
-        (State, "State");
-        (Result, "Result");
-        (Error, "Error");
-        (Fuel, "Nat");
-        (Array, "Array");
-        (Slice, "Slice");
-        (Str, "Str");
-        (RawPtr Mut, "MutRawPtr");
-        (RawPtr Const, "ConstRawPtr");
+        (TState, "State");
+        (TResult, "Result");
+        (TError, "Error");
+        (TFuel, "Nat");
+        (TArray, "Array");
+        (TSlice, "Slice");
+        (TStr, "Str");
+        (TRawPtr Mut, "MutRawPtr");
+        (TRawPtr Const, "ConstRawPtr");
       ]
   | Coq | FStar | HOL4 ->
       [
-        (State, "state");
-        (Result, "result");
-        (Error, "error");
-        (Fuel, if !backend = HOL4 then "num" else "nat");
-        (Array, "array");
-        (Slice, "slice");
-        (Str, "str");
-        (RawPtr Mut, "mut_raw_ptr");
-        (RawPtr Const, "const_raw_ptr");
+        (TState, "state");
+        (TResult, "result");
+        (TError, "error");
+        (TFuel, if !backend = HOL4 then "num" else "nat");
+        (TArray, "array");
+        (TSlice, "slice");
+        (TStr, "str");
+        (TRawPtr Mut, "mut_raw_ptr");
+        (TRawPtr Const, "const_raw_ptr");
       ]
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
-  | Lean -> [ (Array, "Array.make") ]
-  | Coq -> [ (Array, "mk_array") ]
-  | FStar -> [ (Array, "mk_array") ]
-  | HOL4 -> [ (Array, "mk_array") ]
+  | Lean -> [ (TArray, "Array.make") ]
+  | Coq -> [ (TArray, "mk_array") ]
+  | FStar -> [ (TArray, "mk_array") ]
+  | HOL4 -> [ (TArray, "mk_array") ]
 
 let assumed_variants () : (assumed_ty * VariantId.id * string) list =
   match !backend with
   | FStar ->
       [
-        (Result, result_return_id, "Return");
-        (Result, result_fail_id, "Fail");
-        (Error, error_failure_id, "Failure");
-        (Error, error_out_of_fuel_id, "OutOfFuel");
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail");
+        (TError, error_failure_id, "Failure");
+        (TError, error_out_of_fuel_id, "OutOfFuel");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
   | Coq ->
       [
-        (Result, result_return_id, "Return");
-        (Result, result_fail_id, "Fail_");
-        (Error, error_failure_id, "Failure");
-        (Error, error_out_of_fuel_id, "OutOfFuel");
-        (Fuel, fuel_zero_id, "O");
-        (Fuel, fuel_succ_id, "S");
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail_");
+        (TError, error_failure_id, "Failure");
+        (TError, error_out_of_fuel_id, "OutOfFuel");
+        (TFuel, fuel_zero_id, "O");
+        (TFuel, fuel_succ_id, "S");
       ]
   | Lean ->
       [
-        (Result, result_return_id, "ret");
-        (Result, result_fail_id, "fail");
-        (Error, error_failure_id, "panic");
+        (TResult, result_return_id, "ret");
+        (TResult, result_fail_id, "fail");
+        (TError, error_failure_id, "panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
   | HOL4 ->
       [
-        (Result, result_return_id, "Return");
-        (Result, result_fail_id, "Fail");
-        (Error, error_failure_id, "Failure");
+        (TResult, result_return_id, "Return");
+        (TResult, result_fail_id, "Fail");
+        (TError, error_failure_id, "Failure");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
@@ -801,18 +801,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         match ty with
         | TAdt (type_id, generics) -> (
             match type_id with
-            | Tuple ->
+            | TTuple ->
                 (* The "pair" case is frequent enough to have its special treatment *)
                 if List.length generics.types = 2 then "p" else "t"
-            | TAssumed Result -> "r"
-            | TAssumed Error -> ConstStrings.error_basename
-            | TAssumed Fuel -> ConstStrings.fuel_basename
-            | TAssumed Array -> "a"
-            | TAssumed Slice -> "s"
-            | TAssumed Str -> "s"
-            | TAssumed State -> ConstStrings.state_basename
-            | TAssumed (RawPtr _) -> "p"
-            | AdtId adt_id ->
+            | TAssumed TResult -> "r"
+            | TAssumed TError -> ConstStrings.error_basename
+            | TAssumed TFuel -> ConstStrings.fuel_basename
+            | TAssumed TArray -> "a"
+            | TAssumed TSlice -> "s"
+            | TAssumed TStr -> "s"
+            | TAssumed TState -> ConstStrings.state_basename
+            | TAssumed (TRawPtr _) -> "p"
+            | TAdtId adt_id ->
                 let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
                 (* Derive the var name from the last ident of the type name
                  * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
@@ -821,15 +821,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
                  * be an ident *)
                 let cl = List.nth def.name (List.length def.name - 1) in
                 name_from_type_ident (Names.as_ident cl))
-        | TypeVar _ -> (
+        | TVar _ -> (
             (* TODO: use "t" also for F* *)
             match !backend with
             | FStar -> "x" (* lacking inspiration here... *)
             | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
         | TLiteral lty -> (
             match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
-        | Arrow _ -> "f"
-        | TraitType (_, _, name) -> name_from_type_ident name)
+        | TArrow _ -> "f"
+        | TTraitType (_, _, name) -> name_from_type_ident name)
   in
   let type_var_basename (_varset : StringSet.t) (basename : string) : string =
     (* Rust type variables are snake-case and start with a capital letter *)
@@ -1161,7 +1161,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
   | TAdt (type_id, generics) -> (
       let has_params = generics <> empty_generic_args in
       match type_id with
-      | Tuple ->
+      | TTuple ->
           (* This is a bit annoying, but in F*/Coq/HOL4 [()] is not the unit type:
            * we have to write [unit]... *)
           if generics.types = [] then F.pp_print_string fmt (unit_name ())
@@ -1181,7 +1181,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                 F.pp_print_space fmt ())
               (extract_rec true) generics.types;
             F.pp_print_string fmt ")")
-      | AdtId _ | TAssumed _ -> (
+      | TAdtId _ | TAssumed _ -> (
           (* HOL4 behaves differently. Where in Coq/FStar/Lean we would write:
              `tree a b`
 
@@ -1200,7 +1200,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                  argument for `Vec`). *)
               let generics =
                 match type_id with
-                | AdtId id -> (
+                | TAdtId id -> (
                     match
                       TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map
                     with
@@ -1223,7 +1223,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
               assert (const_generics = []);
               let print_tys =
                 match type_id with
-                | AdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
+                | TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
                 | TAssumed _ -> true
                 | _ -> raise (Failure "Unreachable")
               in
@@ -1243,9 +1243,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                 Collections.List.iter_link (F.pp_print_space fmt)
                   (extract_trait_ref ctx fmt no_params_tys true)
                   trait_refs)))
-  | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
+  | TVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
   | TLiteral lty -> extract_literal_type ctx fmt lty
-  | Arrow (arg_ty, ret_ty) ->
+  | TArrow (arg_ty, ret_ty) ->
       if inside then F.pp_print_string fmt "(";
       extract_rec false arg_ty;
       F.pp_print_space fmt ();
@@ -1253,7 +1253,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       extract_rec false ret_ty;
       if inside then F.pp_print_string fmt ")"
-  | TraitType (trait_ref, generics, type_name) -> (
+  | TTraitType (trait_ref, generics, type_name) -> (
       if !parameterize_trait_types then raise (Failure "Unimplemented")
       else
         let type_name =
@@ -1445,7 +1445,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     | None -> ctx.fmt.type_name def.name
     | Some info -> info.extract_name
   in
-  let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
+  let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
   (* Compute and register:
    * - the variant names, if this is an enumeration
    * - the field names, if this is a structure
@@ -1487,11 +1487,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
         let ctx =
           List.fold_left
             (fun ctx (fid, name) ->
-              ctx_add (FieldId (AdtId def.def_id, fid)) name ctx)
+              ctx_add (FieldId (TAdtId def.def_id, fid)) name ctx)
             ctx field_names
         in
         (* Add the constructor name *)
-        ctx_add (StructId (AdtId def.def_id)) cons_name ctx
+        ctx_add (StructId (TAdtId def.def_id)) cons_name ctx
     | Enum variants ->
         let variant_names =
           match info with
@@ -1527,7 +1527,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
         in
         List.fold_left
           (fun ctx (vid, vname) ->
-            ctx_add (VariantId (AdtId def.def_id, vid)) vname ctx)
+            ctx_add (VariantId (TAdtId def.def_id, vid)) vname ctx)
           ctx variant_names
     | Opaque ->
         (* Nothing to do *)
@@ -1730,7 +1730,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* If Coq: print the constructor name *)
       (* TODO: remove superfluous test not is_rec below *)
       if !backend = Coq && not is_rec then (
-        F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
+        F.pp_print_string fmt (ctx_get_struct (TAdtId def.def_id) ctx);
         F.pp_print_string fmt " ");
       (match !backend with
       | Lean -> ()
@@ -1744,7 +1744,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       | Lean -> F.pp_open_vbox fmt 0);
       (* Print the fields *)
       let print_field (field_id : FieldId.id) (f : field) : unit =
-        let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+        let field_name = ctx_get_field (TAdtId def.def_id) field_id ctx in
         (* Open a box for the field *)
         F.pp_open_box fmt ctx.indent_incr;
         F.pp_print_string fmt field_name;
@@ -1779,7 +1779,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
          i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
          we generate `inductive Foo := | mk ... *)
       let cons_name =
-        if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx
+        if !backend = Lean then "mk" else ctx_get_struct (TAdtId def.def_id) ctx
       in
       let def_name = ctx_get_local_type def.def_id ctx in
       extract_type_decl_variant ctx fmt type_decl_group def_name type_params
@@ -2223,7 +2223,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     match decl.kind with
     | Opaque -> ()
     | Struct fields ->
-        let adt_id = AdtId decl.def_id in
+        let adt_id = TAdtId decl.def_id in
         (* Generate the instruction for the record constructor *)
         let cons_name = ctx_get_struct adt_id ctx in
         extract_coq_arguments_instruction ctx fmt cons_name num_params;
@@ -2241,7 +2241,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
         (* Generate the instructions *)
         VariantId.iteri
           (fun vid (_ : variant) ->
-            let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
+            let cons_name = ctx_get_variant (TAdtId decl.def_id) vid ctx in
             extract_coq_arguments_instruction ctx fmt cons_name num_params)
           variants;
         (* Add breaks to insert new lines between definitions *)
@@ -2270,7 +2270,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
         let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
         let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
         let def_name = ctx_get_local_type decl.def_id ctx in
-        let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
+        let cons_name = ctx_get_struct (TAdtId decl.def_id) ctx in
         let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
           (* Outer box for the projector definition *)
@@ -2281,7 +2281,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           F.pp_open_hovbox fmt ctx.indent_incr;
           F.pp_print_string fmt "Definition";
           F.pp_print_space fmt ();
-          let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+          let field_name = ctx_get_field (TAdtId decl.def_id) field_id ctx in
           F.pp_print_string fmt field_name;
           (* Print the generics *)
           let as_implicits = true in
@@ -2364,7 +2364,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
           F.pp_print_string fmt "Notation";
           F.pp_print_space fmt ();
-          let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+          let field_name = ctx_get_field (TAdtId decl.def_id) field_id ctx in
           F.pp_print_string fmt ("\"" ^ record_var ^ " .(" ^ field_name ^ ")\"");
           F.pp_print_space fmt ();
           F.pp_print_string fmt ":=";
@@ -2421,7 +2421,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
    * one line *)
   F.pp_open_hvbox fmt 0;
   (* Retrieve the name *)
-  let state_name = ctx_get_assumed_type State ctx in
+  let state_name = ctx_get_assumed_type TState ctx in
   (* The syntax for Lean and Coq is almost identical. *)
   let print_axiom () =
     let axiom =
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index b1178aa7..395c0c80 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -71,7 +71,7 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig)
   let generics =
     let { T.regions; types; const_generics; trait_clauses } = sg.generics in
     let regions = List.map (fun _ -> T.RErased) regions in
-    let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in
+    let types = List.map (fun (v : T.type_var) -> T.TVar v.T.index) types in
     let const_generics =
       List.map
         (fun (v : T.const_generic_var) -> T.CGVar v.T.index)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index d4dbf80a..c54d55d4 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1889,7 +1889,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
         match bc with
         | SharedBorrow bid ->
             assert (ty_no_regions ref_ty);
-            let ty = T.Ref (T.RVar r_id, ref_ty, kind) in
+            let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
             let value = V.ABorrow (V.ASharedBorrow bid) in
             ([ { V.value; ty } ], v)
         | MutBorrow (bid, bv) ->
@@ -1897,7 +1897,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx bv.V.value));
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
-            let ty = T.Ref (T.RVar r_id, ref_ty, kind) in
+            let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
             let ignored = mk_aignored ref_ty in
             let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in
             let av = { V.value = av; ty } in
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index cf8e5994..8807f3ef 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -107,10 +107,10 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
   assert (ty_is_rty ty1 && ty_is_rty ty2);
   (* Normalize the associated types *)
   match (ty1, ty2) with
-  | T.TLiteral lit1, T.TLiteral lit2 ->
+  | TLiteral lit1, TLiteral lit2 ->
       assert (lit1 = lit2);
       default
-  | T.TAdt (id1, generics1), T.TAdt (id2, generics2) ->
+  | TAdt (id1, generics1), TAdt (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 *)
@@ -146,7 +146,7 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
       in
       (* Combine *)
       combine params_b tys_b
-  | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) ->
+  | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) ->
       (* Sanity check *)
       assert (kind1 = kind2);
       (* Explanation for the case where we check if projections intersect:
@@ -155,10 +155,10 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
       let regions_b = compare_regions r1 r2 in
       let tys_b = compare ty1 ty2 in
       combine regions_b tys_b
-  | T.TypeVar id1, T.TypeVar id2 ->
+  | TVar id1, TVar id2 ->
       assert (id1 = id2);
       default
-  | T.TraitType _, T.TraitType _ ->
+  | TTraitType _, TTraitType _ ->
       (* The types should have been normalized. If after normalization we
          get trait types, we can consider them as variables *)
       assert (ty1 = ty2);
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 48688893..b07f2629 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -272,10 +272,10 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
     (kind : V.sv_kind) (adt_id : T.type_id) (generics : T.generic_args)
     (ctx : C.eval_ctx) : V.symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
-  | T.AdtId def_id, _, _ ->
+  | T.TAdtId def_id, _, _ ->
       compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
         def_id generics ctx
-  | T.Tuple, [], _ ->
+  | T.TTuple, [], _ ->
       [ compute_expanded_symbolic_tuple_value kind generics.types ]
   | T.TAssumed T.TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value kind boxed_ty ]
@@ -306,7 +306,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       V.abstract_shared_borrows option =
     if same_symbolic_id sv original_sv then
       match proj_ty with
-      | T.Ref (r, ref_ty, T.Shared) ->
+      | T.TRef (r, ref_ty, T.Shared) ->
           (* Projector over the shared value *)
           let shared_asb = V.AsbProjReborrows (sv, ref_ty) in
           (* Check if the region is in the set of projected regions *)
@@ -548,7 +548,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         S.synthesize_symbolic_expansion_no_branching original_sv
           original_sv_place see expr
     (* Borrows *)
-    | T.Ref (region, ref_ty, rkind) ->
+    | T.TRef (region, ref_ty, rkind) ->
         expand_symbolic_value_borrow config original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
@@ -665,7 +665,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.TAdt (AdtId def_id, _) ->
+        | T.TAdt (TAdtId 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 *)
@@ -690,7 +690,7 @@ 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.TAdt ((Tuple | TAssumed TBox), _) | T.Ref (_, _, _) ->
+        | T.TAdt ((TTuple | TAssumed TBox), _) | T.TRef (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config sv None
         | T.TAdt (TAssumed (TArray | TSlice | TStr), _) ->
@@ -698,8 +698,8 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
             raise
               (Failure
                  "Attempted to greedily expand an ADT which can't be expanded ")
-        | T.TypeVar _ | T.TLiteral _ | Never | T.TraitType _ | T.Arrow _
-        | T.RawPtr _ ->
+        | T.TVar _ | T.TLiteral _ | TNever | T.TTraitType _ | T.TArrow _
+        | T.TRawPtr _ ->
             raise (Failure "Unreachable")
       in
       (* Compose and continue *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c7fcc1af..7865d7be 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -144,9 +144,9 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
       (match v.V.ty with
       | T.TAdt (T.TAssumed T.TBox, _) ->
           raise (Failure "Can't copy an assumed value other than Option")
-      | T.TAdt (T.AdtId _, _) as ty ->
+      | T.TAdt (T.TAdtId _, _) as ty ->
           assert (allow_adt_copy || ty_is_primitively_copyable ty)
-      | T.TAdt (T.Tuple, _) -> () (* Ok *)
+      | T.TAdt (T.TTuple, _) -> () (* Ok *)
       | T.TAdt
           ( T.TAssumed (TSlice | T.TArray),
             {
@@ -670,7 +670,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
           | E.TwoPhaseMut -> T.Mut
           | _ -> raise (Failure "Unreachable")
         in
-        let rv_ty = T.Ref (T.RErased, v.ty, ref_kind) in
+        let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in
         let bc =
           match bkind with
           | E.Shared | E.Shallow ->
@@ -698,7 +698,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
        fun ctx ->
         (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
         let bid = C.fresh_borrow_id () in
-        let rv_ty = T.Ref (T.RErased, v.ty, Mut) in
+        let rv_ty = T.TRef (T.RErased, v.ty, Mut) in
         let rv : V.typed_value =
           { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
         in
@@ -725,15 +725,15 @@ let eval_rvalue_aggregate (config : C.config)
     match aggregate_kind with
     | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
         match type_id with
-        | Tuple ->
+        | TTuple ->
             let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
             let v = V.VAdt { variant_id = None; field_values = values } in
             let generics = TypesUtils.mk_generic_args [] tys [] [] in
-            let ty = T.TAdt (T.Tuple, generics) in
+            let ty = T.TAdt (T.TTuple, generics) in
             let aggregated : V.typed_value = { V.value = v; ty } in
             (* Call the continuation *)
             cf aggregated ctx
-        | AdtId def_id ->
+        | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = C.ctx_lookup_type_decl ctx def_id in
             assert (
@@ -750,7 +750,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.TAdt (T.AdtId def_id, generics) in
+            let aty = T.TAdt (T.TAdtId def_id, generics) in
             let aggregated : V.typed_value = { V.value = VAdt av; ty = aty } in
             (* Call the continuation *)
             cf aggregated ctx
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 3447131c..2f7e8f3d 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -170,7 +170,7 @@ let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun =
     let child_av = mk_aignored child_rty in
 
     (* Create the shared loan *)
-    let loan_rty = T.Ref (T.RVar nrid, rty, T.Shared) in
+    let loan_rty = T.TRef (T.RVar nrid, rty, T.Shared) in
     let loan_value =
       V.ALoan (V.ASharedLoan (V.BorrowId.Set.singleton nlid, nsv, child_av))
     in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9bc25626..27020efb 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -172,20 +172,20 @@ let rec match_types (match_distinct_types : T.ty -> T.ty -> T.ty)
       in
       let generics = { T.regions; types; const_generics; trait_refs } in
       TAdt (id, generics)
-  | TypeVar vid0, TypeVar vid1 ->
+  | TVar vid0, TVar vid1 ->
       assert (vid0 = vid1);
       let vid = vid0 in
-      TypeVar vid
+      TVar vid
   | TLiteral lty0, TLiteral lty1 ->
       assert (lty0 = lty1);
       ty0
-  | Never, Never -> ty0
-  | Ref (r0, ty0, k0), Ref (r1, ty1, k1) ->
+  | TNever, TNever -> ty0
+  | TRef (r0, ty0, k0), TRef (r1, ty1, k1) ->
       let r = match_regions r0 r1 in
       let ty = match_rec ty0 ty1 in
       assert (k0 = k1);
       let k = k0 in
-      Ref (r, ty, k)
+      TRef (r, ty, k)
   | _ -> match_distinct_types ty0 ty1
 
 module MakeMatcher (M : PrimMatcher) : Matcher = struct
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 728e5226..36af1db4 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -101,7 +101,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
           T.TAdt (type_id, _) ) -> (
           (* Check consistency *)
           (match (proj_kind, type_id) with
-          | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
+          | ProjAdt (def_id, opt_variant_id), T.TAdtId def_id' ->
               assert (def_id = def_id');
               assert (opt_variant_id = adt.variant_id)
           | _ -> raise (Failure "Unreachable"));
@@ -118,7 +118,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.VAdt adt, T.TAdt (T.Tuple, _) -> (
+      | Field (ProjTuple arity, field_id), V.VAdt adt, T.TAdt (T.TTuple, _) -> (
           assert (arity = List.length adt.field_values);
           let fv = T.FieldId.nth adt.field_values field_id in
           (* Project *)
@@ -372,7 +372,7 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
   (* Initialize the expanded value *)
   let fields = List.map mk_bottom field_types in
   let av = V.VAdt { variant_id = opt_variant_id; field_values = fields } in
-  let ty = T.TAdt (T.AdtId def_id, generics) in
+  let ty = T.TAdt (TAdtId def_id, generics) in
   { V.value = av; V.ty }
 
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
@@ -381,7 +381,7 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
   let fields = List.map mk_bottom field_types in
   let v = V.VAdt { variant_id = None; field_values = fields } in
   let generics = TypesUtils.mk_generic_args [] field_types [] [] in
-  let ty = T.TAdt (T.Tuple, generics) in
+  let ty = T.TAdt (TTuple, generics) in
   { V.value = v; V.ty }
 
 (** Auxiliary helper to expand {!V.Bottom} values.
@@ -433,13 +433,13 @@ 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.TAdt (T.AdtId def_id', generics) ) ->
+        T.TAdt (TAdtId def_id', generics) ) ->
         assert (def_id = def_id');
         compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
         T.TAdt
-          ( T.Tuple,
+          ( TTuple,
             { T.regions = []; types; const_generics = []; trait_refs = [] } ) )
       ->
         assert (arity = List.length types);
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 70a77be5..e47886ec 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -43,7 +43,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
         in
         List.concat proj_fields
     | V.Bottom, _ -> raise (Failure "Unreachable")
-    | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+    | V.Borrow bc, TRef (r, ref_ty, kind) ->
         (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
         let bid, asb =
           (* Not in the set: dive *)
@@ -121,7 +121,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
           in
           V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
       | V.Bottom, _ -> raise (Failure "Unreachable")
-      | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+      | V.Borrow bc, TRef (r, ref_ty, kind) ->
           if
             (* Check if the region is in the set of projected regions (note that
              * we never project over static regions) *)
@@ -277,7 +277,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
             field_values
         in
         (V.AAdt { V.variant_id; field_values }, original_sv_ty)
-    | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
+    | SeMutRef (bid, spc), TRef (r, ref_ty, T.Mut) ->
         (* Sanity check *)
         assert (spc.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
@@ -295,7 +295,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
             if region_in_set r ancestors_regions then Some bid else None
           in
           (V.ALoan (V.AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
-    | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
+    | SeSharedRef (bids, spc), TRef (r, ref_ty, T.Shared) ->
         (* Sanity check *)
         assert (spc.V.sv_ty = ref_ty);
         (* Apply the projector to the borrowed value *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index cdcea2cc..cf9b840b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -232,7 +232,7 @@ 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.TAdt ((T.AdtId _ as type_id), generics), V.VAdt av -> (
+    | T.TAdt ((T.TAdtId _ as type_id), generics), V.VAdt av -> (
         (* There are two situations:
            - either the discriminant is already the proper one (in which case we
              don't do anything)
@@ -248,16 +248,16 @@ let set_discriminant (config : C.config) (p : E.place)
               (* Replace the value *)
               let bottom_v =
                 match type_id with
-                | T.AdtId def_id ->
+                | T.TAdtId def_id ->
                     compute_expanded_bottom_adt_value ctx def_id
                       (Some variant_id) generics
                 | _ -> raise (Failure "Unreachable")
               in
               assign_to_place config bottom_v p (cf Unit) ctx)
-    | T.TAdt ((T.AdtId _ as type_id), generics), V.Bottom ->
+    | T.TAdt ((T.TAdtId _ as type_id), generics), V.Bottom ->
         let bottom_v =
           match type_id with
-          | T.AdtId def_id ->
+          | T.TAdtId def_id ->
               compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
                 generics
           | _ -> raise (Failure "Unreachable")
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 01de6fd0..8895bd8e 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -419,7 +419,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (match (tv.V.value, tv.V.ty) with
         | V.VLiteral cv, T.TLiteral ty -> check_literal_type cv ty
         (* ADT case *)
-        | V.VAdt av, T.TAdt (T.AdtId def_id, generics) ->
+        | V.VAdt av, T.TAdt (T.TAdtId 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
@@ -445,7 +445,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.VAdt av, T.TAdt (T.Tuple, generics) ->
+        | V.VAdt av, T.TAdt (T.TTuple, generics) ->
             assert (generics.regions = []);
             assert (generics.const_generics = []);
             assert (av.V.variant_id = None);
@@ -486,7 +486,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | (T.TSlice | T.TStr), _, _, _, _ -> raise (Failure "Unexpected")
             | _ -> raise (Failure "Erroneous type"))
         | V.Bottom, _ -> (* Nothing to check *) ()
-        | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
+        | V.Borrow bc, T.TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
@@ -533,7 +533,7 @@ 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.TAdt (T.AdtId def_id, generics) ->
+        | V.AAdt av, T.TAdt (T.TAdtId 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
@@ -562,7 +562,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
               fields_with_types
         (* Tuple case *)
-        | V.AAdt av, T.TAdt (T.Tuple, generics) ->
+        | V.AAdt av, T.TAdt (T.TTuple, generics) ->
             assert (generics.regions = []);
             assert (generics.const_generics = []);
             assert (av.V.variant_id = None);
@@ -589,7 +589,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 assert (boxed_value.V.ty = boxed_ty)
             | _ -> raise (Failure "Erroneous type"))
         | V.ABottom, _ -> (* Nothing to check *) ()
-        | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
+        | V.ABorrow bc, T.TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | V.AMutBorrow (_, av), T.Mut ->
                 (* Check that the child value has the proper type *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index ee06fa07..67063af9 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
     | Assign (_, rv) -> (
         match rv with
         | Use _ | RvRef _ -> not must_end_with_exit
-        | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit
+        | Aggregate (AggregatedAdt (TTuple, _, _), []) -> not must_end_with_exit
         | _ -> false)
     | FakeRead _ | Drop _ | Nop -> not must_end_with_exit
     | Panic | Return -> true
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dd24767e..7494dc2a 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -73,10 +73,10 @@ module Values = struct
           List.map (typed_value_to_string fmt) av.field_values
         in
         match v.ty with
-        | T.TAdt (T.Tuple, _) ->
+        | T.TAdt (T.TTuple, _) ->
             (* Tuple *)
             "(" ^ String.concat ", " field_values ^ ")"
-        | T.TAdt (T.AdtId def_id, _) ->
+        | T.TAdt (T.TAdtId def_id, _) ->
             (* "Regular" ADT *)
             let adt_ident =
               match av.variant_id with
@@ -177,10 +177,10 @@ module Values = struct
           List.map (typed_avalue_to_string fmt) av.field_values
         in
         match v.ty with
-        | T.TAdt (T.Tuple, _) ->
+        | T.TAdt (T.TTuple, _) ->
             (* Tuple *)
             "(" ^ String.concat ", " field_values ^ ")"
-        | T.TAdt (T.AdtId def_id, _) ->
+        | T.TAdt (T.TAdtId def_id, _) ->
             (* "Regular" ADT *)
             let adt_ident =
               match av.variant_id with
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 7c52c423..8b737cb5 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -191,20 +191,20 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
 
 let assumed_ty_to_string (aty : assumed_ty) : string =
   match aty with
-  | State -> "State"
-  | Result -> "Result"
-  | Error -> "Error"
-  | Fuel -> "Fuel"
-  | Array -> "Array"
-  | Slice -> "Slice"
-  | Str -> "Str"
-  | RawPtr Mut -> "MutRawPtr"
-  | RawPtr Const -> "ConstRawPtr"
+  | TState -> "State"
+  | TResult -> "Result"
+  | TError -> "Error"
+  | TFuel -> "Fuel"
+  | TArray -> "Array"
+  | TSlice -> "Slice"
+  | TStr -> "Str"
+  | TRawPtr Mut -> "MutRawPtr"
+  | TRawPtr Const -> "ConstRawPtr"
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
-  | AdtId id -> fmt.type_decl_id_to_string id
-  | Tuple -> ""
+  | TAdtId id -> fmt.type_decl_id_to_string id
+  | TTuple -> ""
   | TAssumed aty -> assumed_ty_to_string aty
 
 (* TODO: duplicates  Charon.PrintTypes.const_generic_to_string *)
@@ -219,24 +219,24 @@ let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
   match ty with
   | TAdt (id, generics) -> (
       match id with
-      | Tuple ->
+      | TTuple ->
           let generics = generic_args_to_strings fmt false generics in
           "(" ^ String.concat " * " generics ^ ")"
-      | AdtId _ | TAssumed _ ->
+      | TAdtId _ | TAssumed _ ->
           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 ^ generics_s in
           if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
-  | TypeVar tv -> fmt.type_var_id_to_string tv
+  | TVar tv -> fmt.type_var_id_to_string tv
   | TLiteral lty -> literal_type_to_string lty
-  | Arrow (arg_ty, ret_ty) ->
+  | TArrow (arg_ty, ret_ty) ->
       let ty =
         ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty
       in
       if inside then "(" ^ ty ^ ")" else ty
-  | TraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = trait_ref_to_string fmt false trait_ref in
       let s =
         if generics = empty_generic_args then trait_ref ^ "::" ^ type_name
@@ -378,8 +378,8 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
 let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
     (variant_id : VariantId.id option) : string =
   match adt_id with
-  | Tuple -> "Tuple"
-  | AdtId def_id -> (
+  | TTuple -> "Tuple"
+  | TAdtId def_id -> (
       (* "Regular" ADT *)
       match variant_id with
       | Some vid -> fmt.adt_variant_to_string def_id vid
@@ -387,21 +387,21 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
   | TAssumed aty -> (
       (* Assumed type *)
       match aty with
-      | State | Array | Slice | Str | RawPtr _ ->
+      | TState | TArray | TSlice | TStr | TRawPtr _ ->
           (* Those types are opaque: we can't get there *)
           raise (Failure "Unreachable")
-      | Result ->
+      | TResult ->
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then "@Result::Return"
           else if variant_id = result_fail_id then "@Result::Fail"
           else
             raise (Failure "Unreachable: improper variant id for result type")
-      | Error ->
+      | TError ->
           let variant_id = Option.get variant_id in
           if variant_id = error_failure_id then "@Error::Failure"
           else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
           else raise (Failure "Unreachable: improper variant id for error type")
-      | Fuel ->
+      | TFuel ->
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then "@Fuel::Zero"
           else if variant_id = fuel_succ_id then "@Fuel::Succ"
@@ -410,10 +410,10 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
 let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
     (field_id : FieldId.id) : string =
   match adt_id with
-  | Tuple ->
+  | TTuple ->
       raise (Failure "Unreachable")
       (* Tuples don't use the opaque field id for the field indices, but [int] *)
-  | AdtId def_id -> (
+  | TAdtId def_id -> (
       (* "Regular" ADT *)
       let fields = fmt.adt_field_names def_id None in
       match fields with
@@ -422,10 +422,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
   | TAssumed aty -> (
       (* Assumed type *)
       match aty with
-      | State | Fuel | Array | Slice | Str ->
+      | TState | TFuel | TArray | TSlice | TStr ->
           (* Opaque types: we can't get there *)
           raise (Failure "Unreachable")
-      | Result | Error | RawPtr _ ->
+      | TResult | TError | TRawPtr _ ->
           (* Enumerations: we can't get there *)
           raise (Failure "Unreachable"))
 
@@ -437,10 +437,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
-  | TAdt (Tuple, _) ->
+  | TAdt (TTuple, _) ->
       (* Tuple *)
       "(" ^ String.concat ", " field_values ^ ")"
-  | TAdt (AdtId def_id, _) ->
+  | TAdt (TAdtId def_id, _) ->
       (* "Regular" ADT *)
       let adt_ident =
         match variant_id with
@@ -465,10 +465,10 @@ let adt_g_value_to_string (fmt : value_formatter)
   | TAdt (TAssumed aty, _) -> (
       (* Assumed type *)
       match aty with
-      | State | RawPtr _ ->
+      | TState | TRawPtr _ ->
           (* This type is opaque: we can't get there *)
           raise (Failure "Unreachable")
-      | Result ->
+      | TResult ->
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then
             match field_values with
@@ -480,13 +480,13 @@ let adt_g_value_to_string (fmt : value_formatter)
             | _ -> raise (Failure "Result::Fail takes exactly one value")
           else
             raise (Failure "Unreachable: improper variant id for result type")
-      | Error ->
+      | TError ->
           assert (field_values = []);
           let variant_id = Option.get variant_id in
           if variant_id = error_failure_id then "@Error::Failure"
           else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
           else raise (Failure "Unreachable: improper variant id for error type")
-      | Fuel ->
+      | TFuel ->
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then (
             assert (field_values = []);
@@ -496,7 +496,7 @@ let adt_g_value_to_string (fmt : value_formatter)
             | [ v ] -> "@Fuel::Succ " ^ v
             | _ -> raise (Failure "@Fuel::Succ takes exactly one value")
           else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Array | Slice | Str ->
+      | TArray | TSlice | TStr ->
           assert (variant_id = None);
           let field_values =
             List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
@@ -650,7 +650,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
       let indent2 = indent1 ^ indent_incr in
       (* The id should be a custom type decl id or an array *)
       match supd.struct_id with
-      | AdtId aid ->
+      | TAdtId aid ->
           let field_names = Option.get (fmt.adt_field_names aid None) in
           let fields =
             List.map
@@ -664,7 +664,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
           in
           let bl = if fields = [] then "" else "\n" ^ indent in
           "{" ^ s ^ String.concat "" fields ^ bl ^ "}"
-      | TAssumed Array ->
+      | TAssumed TArray ->
           let fields =
             List.map
               (fun (_, fe) ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ffbd1f09..72a6400e 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -68,14 +68,14 @@ type mutability = Mut | Const [@@deriving show, ord]
     TODO: add a prefix "T"
   *)
 type assumed_ty =
-  | State
-  | Result
-  | Error
-  | Fuel
-  | Array
-  | Slice
-  | Str
-  | RawPtr of mutability
+  | TState
+  | TResult
+  | TError
+  | TFuel
+  | TArray
+  | TSlice
+  | TStr
+  | TRawPtr of mutability
       (** The bool
           Raw pointers don't make sense in the pure world, but we don't know
           how to translate them yet and we have to handle some functions which
@@ -146,7 +146,7 @@ class virtual ['self] mapreduce_type_id_base =
       fun _ x -> (x, self#zero)
   end
 
-type type_id = AdtId of type_decl_id | Tuple | TAssumed of assumed_ty
+type type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty
 [@@deriving
   show,
     ord,
@@ -276,10 +276,10 @@ type ty =
           be able to only give back part of the ADT. We need a way to encode
           such "partial" ADTs.
        *)
-  | TypeVar of type_var_id
+  | TVar of type_var_id
   | TLiteral of literal_type
-  | Arrow of ty * ty
-  | TraitType of trait_ref * generic_args * string
+  | TArrow of ty * ty
+  | TTraitType of trait_ref * generic_args * string
       (** The string is for the name of the associated type *)
 
 and trait_ref = {
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d62a028e..8872571f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -582,7 +582,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             match app.e with
             | Qualif
                 {
-                  id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+                  id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
                   generics = _;
                 } ->
                 (* Lookup the def *)
@@ -606,7 +606,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     (!Config.backend <> Lean && !Config.backend <> Coq)
                     || not is_rec
                   then
-                    let struct_id = AdtId adt_id in
+                    let struct_id = TAdtId adt_id in
                     let init = None in
                     let updates =
                       FieldId.mapi
@@ -1085,7 +1085,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             match app.e with
             | Qualif
                 {
-                  id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+                  id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
                   generics;
                 } ->
                 (* This is a struct *)
@@ -1114,7 +1114,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                         | ( Qualif
                               {
                                 id =
-                                  Proj { adt_id = AdtId proj_adt_id; field_id };
+                                  Proj { adt_id = TAdtId proj_adt_id; field_id };
                                 generics = proj_generics;
                               },
                             Var v ) ->
@@ -1157,13 +1157,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   match (proj.e, x.e) with
                   | ( Qualif
                         {
-                          id = Proj { adt_id = AdtId proj_adt_id; field_id };
+                          id = Proj { adt_id = TAdtId proj_adt_id; field_id };
                           generics = _;
                         },
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
                       if
-                        AdtId proj_adt_id = struct_id
+                        TAdtId proj_adt_id = struct_id
                         && field_id = fid && x.ty = adt_ty
                       then Some v
                       else None
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index f8b5de6a..ea1851f0 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -12,41 +12,41 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
     (type_id : type_id) (variant_id : VariantId.id option)
     (generics : generic_args) : ty list =
   match type_id with
-  | Tuple ->
+  | TTuple ->
       (* Tuple *)
       assert (generics.const_generics = []);
       assert (generics.trait_refs = []);
       assert (variant_id = None);
       generics.types
-  | AdtId def_id ->
+  | TAdtId def_id ->
       (* "Regular" ADT *)
       let def = TypeDeclId.Map.find def_id type_decls in
       type_decl_get_instantiated_fields_types def variant_id generics
   | TAssumed aty -> (
       (* Assumed type *)
       match aty with
-      | State ->
+      | TState ->
           (* This type is opaque *)
           raise (Failure "Unreachable: opaque type")
-      | Result ->
+      | TResult ->
           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 ->
+      | TError ->
           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);
           []
-      | Fuel ->
+      | TFuel ->
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then []
           else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
           else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Array | Slice | Str | RawPtr _ ->
+      | TArray | TSlice | TStr | TRawPtr _ ->
           (* Array: when not symbolic values (for instance, because of aggregates),
              the array expressions are introduced as struct updates *)
           raise (Failure "Attempting to access the fields of an opaque type"))
@@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       assert (adt_id = supd.struct_id);
       (* The id can only be: a custom type decl or an array *)
       match adt_id with
-      | AdtId _ ->
+      | TAdtId _ ->
           let variant_id = None in
           let expected_field_tys =
             get_adt_field_types ctx.type_decls adt_id variant_id adt_generics
@@ -219,7 +219,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
               assert (expected_field_ty = fe.ty);
               check_texpression ctx fe)
             supd.updates
-      | TAssumed Array ->
+      | TAssumed TArray ->
           let expected_field_ty =
             Collections.List.to_cons_nil adt_generics.types
           in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 49c8dd70..4cc7ef91 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -59,7 +59,7 @@ module FunLoopIdSet = Collections.MakeSet (FunLoopIdOrderedType)
 
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
-  | Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+  | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
   | _ -> raise (Failure "Unreachable")
 
 let compute_literal_type (cv : literal) : literal_type =
@@ -110,7 +110,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
   let obj =
     object
       inherit [_] map_ty
-      method! visit_TypeVar _ var_id = subst.ty_subst var_id
+      method! visit_TVar _ var_id = subst.ty_subst var_id
       method! visit_CGVar _ var_id = subst.cg_subst var_id
       method! visit_Clause _ id = subst.tr_subst id
       method! visit_Self _ = subst.tr_self
@@ -249,12 +249,12 @@ let remove_meta (e : texpression) : texpression =
   in
   obj#visit_texpression () e
 
-let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1)
+let mk_arrow (ty0 : ty) (ty1 : ty) : ty = TArrow (ty0, ty1)
 
 (** Construct a type as a list of arrows: ty1 -> ... tyn  *)
 let mk_arrows (inputs : ty list) (output : ty) =
   let rec aux (tys : ty list) : ty =
-    match tys with [] -> output | ty :: tys' -> Arrow (ty, aux tys')
+    match tys with [] -> output | ty :: tys' -> TArrow (ty, aux tys')
   in
   aux inputs
 
@@ -305,7 +305,7 @@ let destruct_apps (e : texpression) : texpression * texpression list =
 (** Make an [App (app, arg)] expression *)
 let mk_app (app : texpression) (arg : texpression) : texpression =
   match app.ty with
-  | Arrow (ty0, ty1) ->
+  | TArrow (ty0, ty1) ->
       (* Sanity check *)
       assert (ty0 = arg.ty);
       let e = App (app, arg) in
@@ -340,7 +340,7 @@ let opt_destruct_function_call (e : texpression) :
 
 let opt_destruct_result (ty : ty) : ty option =
   match ty with
-  | TAdt (TAssumed Result, generics) ->
+  | TAdt (TAssumed TResult, generics) ->
       assert (generics.const_generics = []);
       assert (generics.trait_refs = []);
       Some (Collections.List.to_cons_nil generics.types)
@@ -350,14 +350,14 @@ let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty)
 
 let opt_destruct_tuple (ty : ty) : ty list option =
   match ty with
-  | TAdt (Tuple, generics) ->
+  | TAdt (TTuple, generics) ->
       assert (generics.const_generics = []);
       assert (generics.trait_refs = []);
       Some generics.types
   | _ -> None
 
 let mk_abs (x : typed_pattern) (e : texpression) : texpression =
-  let ty = Arrow (x.ty, e.ty) in
+  let ty = TArrow (x.ty, e.ty) in
   let e = Abs (x, e) in
   { e; ty }
 
@@ -370,12 +370,12 @@ let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
 
 let destruct_arrow (ty : ty) : ty * ty =
   match ty with
-  | Arrow (ty0, ty1) -> (ty0, ty1)
+  | TArrow (ty0, ty1) -> (ty0, ty1)
   | _ -> raise (Failure "Not an arrow type")
 
 let rec destruct_arrows (ty : ty) : ty list * ty =
   match ty with
-  | Arrow (ty0, ty1) ->
+  | TArrow (ty0, ty1) ->
       let tys, out_ty = destruct_arrows ty1 in
       (ty0 :: tys, out_ty)
   | _ -> ([], ty)
@@ -427,13 +427,13 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression =
 let mk_simpl_tuple_ty (tys : ty list) : ty =
   match tys with
   | [ ty ] -> ty
-  | _ -> TAdt (Tuple, mk_generic_args_from_types tys)
+  | _ -> TAdt (TTuple, mk_generic_args_from_types tys)
 
 let mk_bool_ty : ty = TLiteral TBool
-let mk_unit_ty : ty = TAdt (Tuple, empty_generic_args)
+let mk_unit_ty : ty = TAdt (TTuple, empty_generic_args)
 
 let mk_unit_rvalue : texpression =
-  let id = AdtCons { adt_id = Tuple; variant_id = None } in
+  let id = AdtCons { adt_id = TTuple; variant_id = None } in
   let qualif = { id; generics = empty_generic_args } in
   let e = Qualif qualif in
   let ty = mk_unit_ty in
@@ -474,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 = TAdt (Tuple, mk_generic_args_from_types tys) in
+      let ty = TAdt (TTuple, mk_generic_args_from_types tys) in
       let value = PatAdt { variant_id = None; field_values = vl } in
       { value; ty }
 
@@ -485,10 +485,10 @@ 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 = TAdt (Tuple, mk_generic_args_from_types tys) in
+      let ty = TAdt (TTuple, 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 id = AdtCons { adt_id = TTuple; variant_id = None } in
       let qualif = { id; generics = mk_generic_args_from_types tys } in
       (* Put everything together *)
       let cons = { e = Qualif qualif; ty } in
@@ -507,17 +507,17 @@ let ty_as_integer (t : ty) : T.integer_type =
 let ty_as_literal (t : ty) : T.literal_type =
   match t with TLiteral ty -> ty | _ -> raise (Failure "Unreachable")
 
-let mk_state_ty : ty = TAdt (TAssumed State, empty_generic_args)
+let mk_state_ty : ty = TAdt (TAssumed TState, empty_generic_args)
 
 let mk_result_ty (ty : ty) : ty =
-  TAdt (TAssumed Result, mk_generic_args_from_types [ ty ])
+  TAdt (TAssumed TResult, mk_generic_args_from_types [ ty ])
 
-let mk_error_ty : ty = TAdt (TAssumed Error, empty_generic_args)
-let mk_fuel_ty : ty = TAdt (TAssumed Fuel, empty_generic_args)
+let mk_error_ty : ty = TAdt (TAssumed TError, empty_generic_args)
+let mk_fuel_ty : ty = TAdt (TAssumed TFuel, empty_generic_args)
 
 let mk_error (error : VariantId.id) : texpression =
   let ty = mk_error_ty in
-  let id = AdtCons { adt_id = TAssumed Error; variant_id = Some error } in
+  let id = AdtCons { adt_id = TAssumed TError; variant_id = Some error } in
   let qualif = { id; generics = empty_generic_args } in
   let e = Qualif qualif in
   { e; ty }
@@ -525,16 +525,16 @@ let mk_error (error : VariantId.id) : texpression =
 let unwrap_result_ty (ty : ty) : ty =
   match ty with
   | TAdt
-      (TAssumed Result, { types = [ ty ]; const_generics = []; trait_refs = [] })
-    ->
+      ( TAssumed TResult,
+        { 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 = TAdt (TAssumed Result, mk_generic_args_from_types type_args) in
+  let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
   let id =
-    AdtCons { adt_id = TAssumed Result; variant_id = Some result_fail_id }
+    AdtCons { adt_id = TAssumed TResult; variant_id = Some result_fail_id }
   in
   let qualif = { id; generics = mk_generic_args_from_types type_args } in
   let cons_e = Qualif qualif in
@@ -549,9 +549,9 @@ 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 = TAdt (TAssumed Result, mk_generic_args_from_types type_args) in
+  let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
   let id =
-    AdtCons { adt_id = TAssumed Result; variant_id = Some result_return_id }
+    AdtCons { adt_id = TAssumed TResult; variant_id = Some result_return_id }
   in
   let qualif = { id; generics = mk_generic_args_from_types type_args } in
   let cons_e = Qualif qualif in
@@ -562,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 = TAdt (TAssumed Result, mk_generic_args_from_types [ ty ]) in
+  let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ ty ]) in
   let value =
     PatAdt { variant_id = Some result_fail_id; field_values = [ error_pat ] }
   in
@@ -574,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 = TAdt (TAssumed Result, mk_generic_args_from_types [ v.ty ]) in
+  let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ v.ty ]) in
   let value =
     PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
   in
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 490574a2..166c237a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -23,7 +23,7 @@ let st_substitute_visitor (subst : subst) =
   object
     inherit [_] A.map_statement
     method! visit_region _ r = subst.r_subst r
-    method! visit_TypeVar _ id = subst.ty_subst id
+    method! visit_TVar _ id = subst.ty_subst id
 
     method! visit_type_var_id _ _ =
       (* We should never get here because we reimplemented [visit_TypeVar] *)
@@ -67,7 +67,7 @@ let generic_args_substitute (subst : subst) (g : T.generic_args) :
 let erase_regions_subst : subst =
   {
     r_subst = (fun _ -> T.RErased);
-    ty_subst = (fun vid -> T.TypeVar vid);
+    ty_subst = (fun vid -> T.TVar vid);
     cg_subst = (fun id -> T.CGVar id);
     tr_subst = (fun id -> T.Clause id);
     tr_self = T.Self;
@@ -288,10 +288,10 @@ let ctx_adt_value_get_instantiated_field_types (ctx : C.eval_ctx)
     (adt : V.adt_value) (id : T.type_id) (generics : T.generic_args) : T.ty list
     =
   match id with
-  | T.AdtId id ->
+  | T.TAdtId id ->
       (* Retrieve the types of the fields *)
       ctx_adt_get_instantiated_field_types ctx id adt.V.variant_id generics
-  | T.Tuple ->
+  | T.TTuple ->
       assert (generics.regions = []);
       generics.types
   | T.TAssumed aty -> (
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 91edbf04..60020d9a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -397,8 +397,8 @@ let rec translate_sty (ty : T.ty) : ty =
   | T.TAdt (type_id, generics) -> (
       let generics = translate_sgeneric_args generics in
       match type_id with
-      | T.AdtId adt_id -> TAdt (AdtId adt_id, generics)
-      | T.Tuple ->
+      | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
+      | T.TTuple ->
           assert (generics.const_generics = []);
           mk_simpl_tuple_ty generics.types
       | T.TAssumed aty -> (
@@ -412,23 +412,23 @@ let rec translate_sty (ty : T.ty) : ty =
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
               )
-          | T.TArray -> TAdt (TAssumed Array, generics)
-          | T.TSlice -> TAdt (TAssumed Slice, generics)
-          | T.TStr -> TAdt (TAssumed Str, generics)))
-  | TypeVar vid -> TypeVar vid
+          | T.TArray -> TAdt (TAssumed TArray, generics)
+          | T.TSlice -> TAdt (TAssumed TSlice, generics)
+          | T.TStr -> TAdt (TAssumed TStr, generics)))
+  | TVar vid -> TVar vid
   | TLiteral ty -> TLiteral ty
-  | Never -> raise (Failure "Unreachable")
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TNever -> raise (Failure "Unreachable")
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_strait_ref trait_ref in
       let generics = translate_sgeneric_args generics in
-      TraitType (trait_ref, generics, type_name)
-  | Arrow _ -> raise (Failure "TODO")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_sgeneric_args (generics : T.generic_args) : generic_args =
   translate_generic_args translate_sty generics
@@ -506,20 +506,20 @@ let translate_type_decl (def : T.type_decl) : type_decl =
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
-  | AdtId adt_id -> AdtId adt_id
-  | T.TAssumed aty ->
+  | TAdtId adt_id -> TAdtId adt_id
+  | TAssumed aty ->
       let aty =
         match aty with
-        | T.TArray -> Array
-        | T.TSlice -> Slice
-        | T.TStr -> Str
+        | T.TArray -> TArray
+        | T.TSlice -> TSlice
+        | T.TStr -> TStr
         | T.TBox ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
             raise (Failure "Unreachable")
       in
       TAssumed aty
-  | T.Tuple -> Tuple
+  | TTuple -> TTuple
 
 (** Translate a type, seen as an input/output of a forward function
     (preserve all borrows, etc.).
@@ -536,14 +536,14 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
           let type_id = translate_type_id type_id in
           TAdt (type_id, t_generics)
-      | Tuple ->
+      | TTuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_generics.types
-      | T.TAssumed T.TBox -> (
+      | TAssumed TBox -> (
           (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (
@@ -558,20 +558,20 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
                 (Failure
                    "Unreachable: box/vec/option receives exactly one type \
                     parameter")))
-  | TypeVar vid -> TypeVar vid
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> TVar vid
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> TLiteral lty
-  | Ref (_, rty, _) -> translate rty
-  | RawPtr (ty, rkind) ->
+  | TRef (_, rty, _) -> translate rty
+  | TRawPtr (ty, rkind) ->
       let mut = match rkind with Mut -> Mut | Shared -> Const in
       let ty = translate ty in
       let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
-      TAdt (TAssumed (RawPtr mut), generics)
-  | TraitType (trait_ref, generics, type_name) ->
+      TAdt (TAssumed (TRawPtr mut), generics)
+  | TTraitType (trait_ref, generics, type_name) ->
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
-      TraitType (trait_ref, generics, type_name)
-  | Arrow _ -> raise (Failure "TODO")
+      TTraitType (trait_ref, generics, type_name)
+  | TArrow _ -> raise (Failure "TODO")
 
 and translate_fwd_generic_args (type_infos : TA.type_infos)
     (generics : T.generic_args) : generic_args =
@@ -611,7 +611,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.TAdt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _ | TAssumed (T.TArray | T.TSlice | T.TStr) ->
+      | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
           let type_id = translate_type_id type_id in
           if inside_mut then
             (* We do not want to filter anything, so we translate the generics
@@ -630,7 +630,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               let generics = translate_fwd_generic_args type_infos generics in
               Some (TAdt (type_id, generics))
             else None
-      | TAssumed T.TBox -> (
+      | TAssumed TBox -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           (* Eliminate the box *)
@@ -640,7 +640,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               raise
                 (Failure "Unreachable: boxes receive exactly one type parameter")
           )
-      | T.Tuple -> (
+      | TTuple -> (
           (* Tuples can contain borrows (which we eliminate) *)
           let tys_t = List.filter_map translate generics.types in
           match tys_t with
@@ -649,10 +649,10 @@ let rec translate_back_ty (type_infos : TA.type_infos)
               (* Note that if there is exactly one type, [mk_simpl_tuple_ty]
                * is the identity *)
               Some (mk_simpl_tuple_ty tys_t)))
-  | TypeVar vid -> wrap (TypeVar vid)
-  | Never -> raise (Failure "Unreachable")
+  | TVar vid -> wrap (TVar vid)
+  | TNever -> raise (Failure "Unreachable")
   | TLiteral lty -> wrap (TLiteral lty)
-  | Ref (r, rty, rkind) -> (
+  | TRef (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
           (* Ignore shared references, unless we are below a mutable borrow *)
@@ -663,17 +663,17 @@ let rec translate_back_ty (type_infos : TA.type_infos)
           if keep_region r then
             translate_back_ty type_infos keep_region inside_mut rty
           else None)
-  | RawPtr _ ->
+  | TRawPtr _ ->
       (* TODO: not sure what to do here *)
       None
-  | TraitType (trait_ref, generics, type_name) ->
+  | TTraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
       (* Translate the trait ref and the generics as "forward" generics -
          we do not want to filter any type *)
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       let generics = translate_fwd_generic_args type_infos generics in
-      Some (TraitType (trait_ref, generics, type_name))
-  | Arrow _ -> raise (Failure "TODO")
+      Some (TTraitType (trait_ref, generics, type_name))
+  | TArrow _ -> raise (Failure "TODO")
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -1155,7 +1155,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.TAdt (T.Tuple, _) ->
+        | TAdt (TTuple, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
@@ -1233,10 +1233,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             None
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             if field_values = [] then None
             else
@@ -1378,10 +1378,10 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.TAssumed (T.TBox | T.TArray | T.TSlice | T.TStr) ->
+        | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
             assert (field_values = []);
             (ctx, None)
-        | T.Tuple ->
+        | TTuple ->
             (* Return *)
             let variant_id = adt_v.variant_id in
             assert (variant_id = None);
@@ -2386,7 +2386,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
   let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
   let branch = translate_expression branch ctx in
   match type_id with
-  | T.AdtId adt_id ->
+  | TAdtId adt_id ->
       (* Detect if this is an enumeration or not *)
       let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
       let is_enum = TypesUtils.type_decl_is_enum tdef in
@@ -2433,14 +2433,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
             let field_proj = gen_field_proj fid var in
             mk_let monadic (mk_typed_pattern_from_var var None) field_proj e)
           id_var_pairs branch
-  | T.Tuple ->
+  | TTuple ->
       let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in
       let monadic = false in
       mk_let monadic
         (mk_simpl_tuple_pattern vars)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.TAssumed T.TBox ->
+  | TAssumed TBox ->
       (* There should be exactly one variable *)
       let var =
         match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2452,7 +2452,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.TAssumed (T.TArray | T.TSlice | T.TStr) ->
+  | TAssumed (TArray | TSlice | TStr) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
@@ -2484,7 +2484,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         let values = List.map (typed_value_to_texpression ctx ectx) values in
         let values = FieldId.mapi (fun fid v -> (fid, v)) values in
         let su : struct_update =
-          { struct_id = TAssumed Array; init = None; updates = values }
+          { struct_id = TAssumed TArray; init = None; updates = values }
         in
         { e = StructUpdate su; ty = var.ty }
     | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
@@ -2735,9 +2735,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        call to the loop forward function) *)
     let generics =
       let { types; const_generics; trait_clauses } = ctx.sg.generics in
-      let types =
-        List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
-      in
+      let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
       let const_generics =
         List.map
           (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index edd67749..ddb9d681 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -80,14 +80,14 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
                 ls
             in
             ExpandAdt exp
-        | T.Ref (_, _, _) -> (
+        | T.TRef (_, _, _) -> (
             (* Reference expansion: there should be one branch *)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
             | _ -> raise (Failure "Ill-formed borrow expansion"))
-        | T.TypeVar _
+        | T.TVar _
         | T.TLiteral TChar
-        | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ ->
+        | TNever | T.TTraitType _ | T.TArrow _ | T.TRawPtr _ ->
             raise (Failure "Ill-formed symbolic expansion")
       in
       Some (Expansion (place, sv, expansion))
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 6318c624..eddc1e42 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -121,8 +121,8 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
   let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
       (ty : ty) : partial_type_info =
     match ty with
-    | TLiteral _ | Never | TraitType _ -> ty_info
-    | TypeVar var_id -> (
+    | TLiteral _ | TNever | TTraitType _ -> ty_info
+    | TVar var_id -> (
         (* Update the information for the proper parameter, if necessary *)
         match ty_info.param_infos with
         | None -> ty_info
@@ -144,7 +144,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
             in
             let param_infos = Some param_infos in
             { ty_info with param_infos })
-    | Ref (r, rty, rkind) ->
+    | TRef (r, rty, rkind) ->
         (* Update the type info *)
         let contains_static = r_is_static r in
         let contains_borrow = true in
@@ -168,15 +168,15 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
         in
         (* Continue exploring *)
         analyze expl_info ty_info rty
-    | RawPtr (rty, _) ->
+    | TRawPtr (rty, _) ->
         (* TODO: not sure what to do here *)
         analyze expl_info ty_info rty
-    | TAdt ((Tuple | TAssumed (TBox | TSlice | TArray | TStr)), generics) ->
+    | TAdt ((TTuple | TAssumed (TBox | TSlice | TArray | TStr)), generics) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
           (fun ty_info ty -> analyze expl_info ty_info ty)
           ty_info generics.types
-    | TAdt (AdtId adt_id, generics) ->
+    | TAdt (TAdtId 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 *)
@@ -233,7 +233,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
         in
         (* Return *)
         ty_info
-    | Arrow (inputs, output) ->
+    | TArrow (inputs, output) ->
         (* Just dive into the arrow *)
         let ty_info =
           List.fold_left