diff --git a/README.md b/README.md
index 08bb3686..cf17368c 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ You can then install the dependencies with the following command:
 
 ```
 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
-  unionFind ocamlgraph menhir ocamlformat
+  ocamlgraph menhir ocamlformat
 ```
 
 Moreover, Aeneas uses the [Charon](https://github.com/AeneasVerif/charon) project and library.
diff --git a/charon-pin b/charon-pin
index 261dfbd6..57f50f86 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-04d97dd849d7a69239e28aa64859d3a4f86b4162
+1172606b471b5d9913f95cfbf944d3b943736667
diff --git a/flake.lock b/flake.lock
index 3bb9da07..debebbbb 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732711803,
-        "narHash": "sha256-wG+PavPKAM4w4E5Wvwu2EeTZb06Z/17u16b26Atz9js=",
+        "lastModified": 1732881390,
+        "narHash": "sha256-BHsHEnl6S5YXU1UMHR/wryH1CNvNaN/kxg43VwOsWFc=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "04d97dd849d7a69239e28aa64859d3a4f86b4162",
+        "rev": "1172606b471b5d9913f95cfbf944d3b943736667",
         "type": "github"
       },
       "original": {
@@ -193,11 +193,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1732674798,
-        "narHash": "sha256-oM1gjCv9R4zxDFO3as9wqQ4FI3+pDA9MKZ72L7tTIII=",
+        "lastModified": 1732847586,
+        "narHash": "sha256-SnHHSBNZ+aj8mRzYxb6yXBl9ei3K3j5agC/D8Vjw/no=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "1d569430326b0a7807ccffdb2a188b814091976c",
+        "rev": "97210ddff72fe139815f4c1ac5da74b5b0dde2d7",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index fc2a42d0..89b1a045 100644
--- a/flake.nix
+++ b/flake.nix
@@ -64,7 +64,6 @@
             yojson
             zarith
             ocamlgraph
-            unionFind
           ]);
           afterBuild = ''
             echo charon.packages.${system}.tests
diff --git a/src/dune b/src/dune
index cfb0ff59..a66dec34 100644
--- a/src/dune
+++ b/src/dune
@@ -14,7 +14,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix unionFind ocamlgraph str)
+ (libraries charon core_unix ocamlgraph str)
  (modules
   AssociatedTypes
   BorrowCheck
diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index b1724557..ed7ce976 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -23,8 +23,61 @@ let compute_contexts (m : crate) : decls_ctx =
   let global_decls = m.global_decls in
   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
+  let fmt_env : Print.fmt_env =
+    {
+      type_decls;
+      fun_decls;
+      global_decls;
+      trait_decls;
+      trait_impls;
+      regions = [];
+      generics = empty_generic_params;
+      locals = [];
+    }
+  in
+  (* Split the declaration groups between the declaration kinds (types, functions, etc.) *)
+  let type_decls_groups =
+    match split_declarations_to_group_maps m.declarations with
+    | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups
+    | Error mixed_groups ->
+        (* We detected mixed groups: print a nice error message *)
+        let any_decl_id_to_string (id : any_decl_id) : string =
+          let kind = any_decl_id_to_kind_name id in
+          let meta = LlbcAstUtils.crate_get_item_meta m id in
+          let s =
+            match meta with
+            | None -> show_any_decl_id id
+            | Some meta ->
+                kind ^ "(" ^ span_to_string meta.span ^ "): "
+                ^ Print.name_to_string fmt_env meta.name
+          in
+          "- " ^ s
+        in
+        let group_to_msg (i : int) (g : mixed_declaration_group) : string =
+          let ids = g_declaration_group_to_list g in
+          let decls = List.map any_decl_id_to_string ids in
+          let local_requires =
+            LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids)
+          in
+          let local_requires = List.map span_to_string local_requires in
+          let local_requires =
+            if local_requires <> [] then
+              "\n\n\
+               The declarations in this group are (transitively) used at the \
+               following location(s):\n"
+              ^ String.concat "\n" local_requires
+            else ""
+          in
+          "# Group "
+          ^ string_of_int (i + 1)
+          ^ ":\n" ^ String.concat "\n" decls ^ local_requires
+        in
+        let msgs = List.mapi group_to_msg mixed_groups in
+        let msgs = String.concat "\n\n" msgs in
+        craise_opt_span __FILE__ __LINE__ None
+          ("Detected groups of mixed mutually recursive definitions (such as a \
+            type mutually recursive with a function, or a function mutually \
+            recursive with a trait implementation):\n\n" ^ msgs)
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list
diff --git a/src/interp/InterpreterExpansion.ml b/src/interp/InterpreterExpansion.ml
index 3758d342..9c6355ef 100644
--- a/src/interp/InterpreterExpansion.ml
+++ b/src/interp/InterpreterExpansion.ml
@@ -649,7 +649,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
                       > 1 variants (option \
                       [greedy_expand_symbolics_with_borrows] of [config]): "
                     ^ name_to_string ctx def.item_meta.name)
-              | Alias _ | Opaque | Error _ ->
+              | Alias _ | Opaque | TError _ ->
                   craise __FILE__ __LINE__ span
                     "Attempted to greedily expand an alias or opaque type"
               | Union _ ->
diff --git a/src/interp/InterpreterLoopsCore.ml b/src/interp/InterpreterLoopsCore.ml
index a71cab4f..e1c9b46e 100644
--- a/src/interp/InterpreterLoopsCore.ml
+++ b/src/interp/InterpreterLoopsCore.ml
@@ -23,9 +23,6 @@ exception Distinct of string
 
 type ctx_or_update = (eval_ctx, updt_env_kind) result
 
-(** Union Find *)
-module UF = UnionFind.Make (UnionFind.StoreMap)
-
 (** A small utility.
 
     Remark: we use projection markers, meaning we compute maps from/to
diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml
index 5e317418..effadd42 100644
--- a/src/llbc/TypesAnalysis.ml
+++ b/src/llbc/TypesAnalysis.ml
@@ -385,7 +385,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             "type aliases should have been removed earlier"
       | Union _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unions are not supported"
-      | Opaque | Error _ ->
+      | Opaque | TError _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
     (* Substitute the regions in the fields *)
diff --git a/src/pure/PureMicroPasses.ml b/src/pure/PureMicroPasses.ml
index 49157705..25ce368d 100644
--- a/src/pure/PureMicroPasses.ml
+++ b/src/pure/PureMicroPasses.ml
@@ -1385,7 +1385,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Alias _ | Opaque | Error _ ->
+                  | Enum _ | Alias _ | Opaque | TError _ ->
                       craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
                   | Union _ ->
                       craise __FILE__ __LINE__ def.item_meta.span
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index 81bac9aa..01172a1c 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -595,7 +595,7 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   | Alias _ ->
       craise __FILE__ __LINE__ span
         "type aliases should have been removed earlier"
-  | T.Union _ | T.Opaque | T.Error _ -> Opaque
+  | T.Union _ | T.Opaque | T.TError _ -> Opaque
 
 (** Compute which input parameters should be implicit or explicit.