diff --git a/charon-pin b/charon-pin
index ceea1ef11..4ce3e7215 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.
-7fb1eaada218a3f010a3dbeb337aad30beac417f
+0faa4af666512d61017c2ca4769640733f1a9edb
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 4de5382aa..558cfacfd 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -95,7 +95,7 @@ let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
   | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _
-  | Closure _ | Unsolved _ ->
+  | Closure _ | Unsolved _ | Dyn _ ->
       false
   | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
       trait_instance_id_is_local_clause id
@@ -294,6 +294,9 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       let tr : trait_type_ref = { trait_ref; type_name } in
       (* Lookup the representative, if there is *)
       match norm_ctx_get_ty_repr ctx tr with None -> ty | Some ty -> ty)
+  | TDynTrait _ ->
+      craise_opt_span __FILE__ __LINE__ ctx.span
+        "Dynamic trait types are not supported yet"
 
 (** This returns the normalized trait instance id together with an optional
     reference to a trait **implementation** (the `trait_ref` we return has
@@ -449,6 +452,9 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
   | Unsolved _ | UnknownTrait _ ->
       (* This is actually an error case *)
       (id, None)
+  | Dyn _ ->
+      craise_opt_span __FILE__ __LINE__ ctx.span
+        "Dynamic trait types are not supported yet"
 
 and norm_ctx_normalize_generic_args (ctx : norm_ctx) (generics : generic_args) :
     generic_args =
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index c4e37646d..b14331fd9 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -665,7 +665,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
             (* We can't expand those *)
             craise __FILE__ __LINE__ span
               "Attempted to greedily expand an ADT which can't be expanded "
-        | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
+        | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _
+        | TDynTrait _ ->
             craise __FILE__ __LINE__ span "Unreachable"
       in
       (* *)
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 61fa37d95..f58af48ef 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -186,6 +186,9 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
           "We don't support arrow types with locally quantified regions";
         (* We can ignore the outer regions *)
         List.iter (explore_ty []) (output :: inputs)
+    | TDynTrait _ ->
+        craise_opt_span __FILE__ __LINE__ span
+          "Dynamic trait types are not supported yet"
   and explore_generics (outer : region list) (generics : generic_args) =
     let { regions; types; const_generics = _; trait_refs = _ } = generics in
     List.iter (fun long -> add_edges ~long ~shorts:outer) regions;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e829ed302..3d657ebf0 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -456,6 +456,8 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
   | TraitRef tr -> TraitRef (translate_trait_ref span translate_ty tr)
   | FnPointer _ | Closure _ ->
       craise __FILE__ __LINE__ span "Closures are not supported yet"
+  | Dyn _ ->
+      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
   | Unsolved _ -> craise __FILE__ __LINE__ span "Couldn't solve trait bound"
   | UnknownTrait s -> craise __FILE__ __LINE__ span ("Unknown trait found: " ^ s)
 
@@ -496,6 +498,8 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty =
       TTraitType (trait_ref, type_name)
   | TArrow _ ->
       craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+  | TDynTrait _ ->
+      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
 
 and translate_sgeneric_args (span : Meta.span) (generics : T.generic_args) :
     generic_args =
@@ -672,6 +676,8 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos)
       TTraitType (trait_ref, type_name)
   | TArrow _ ->
       craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+  | TDynTrait _ ->
+      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
 
 and translate_fwd_generic_args (span : Meta.span) (type_infos : type_infos)
     (generics : T.generic_args) : generic_args =
@@ -782,6 +788,8 @@ let rec translate_back_ty (span : Meta.span) (type_infos : type_infos)
       else None
   | TArrow _ ->
       craise __FILE__ __LINE__ span "Arrow types are not supported yet"
+  | TDynTrait _ ->
+      craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet"
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -2306,7 +2314,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let dest = mk_typed_pattern_from_var dest dest_mplace in
             (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest)
         | CastFnPtr _ ->
-            craise __FILE__ __LINE__ ctx.span "TODO: function casts")
+            craise __FILE__ __LINE__ ctx.span "TODO: function casts"
+        | CastUnsize _ ->
+            craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions")
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index b15ab38ac..d0b0b7d65 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -83,7 +83,9 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
         match ls with
         | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
         | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
-    | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
+    | TVar _
+    | TLiteral TChar
+    | TNever | TTraitType _ | TArrow _ | TRawPtr _ | TDynTrait _ ->
         craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
   in
   Expansion (place, sv, expansion)
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 86baa3921..7fb8f7ead 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -147,7 +147,7 @@ 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 _ | TNever | TTraitType _ -> ty_info
+    | TLiteral _ | TNever | TTraitType _ | TDynTrait _ -> ty_info
     | TVar var_id -> (
         (* Update the information for the proper parameter, if necessary *)
         match ty_info.param_infos with
diff --git a/flake.lock b/flake.lock
index 907aae55e..92a514b29 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1719733805,
-        "narHash": "sha256-kXtKdgbqm4PEZRmi4Rg7RRtFdlb+7HcV7N1SEeHIsBU=",
+        "lastModified": 1719820305,
+        "narHash": "sha256-KVYxodb95lcW5JOEImxAITqv/8ThWyvXF3WtR9O791k=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "7fb1eaada218a3f010a3dbeb337aad30beac417f",
+        "rev": "0faa4af666512d61017c2ca4769640733f1a9edb",
         "type": "github"
       },
       "original": {