diff --git a/charon-ml/src/Expressions.ml b/charon-ml/src/Expressions.ml
index afacd6f2..df87e947 100644
--- a/charon-ml/src/Expressions.ml
+++ b/charon-ml/src/Expressions.ml
@@ -149,6 +149,7 @@ class ['self] map_constant_expr_base =
 type cast_kind =
   | CastScalar of literal_type * literal_type
   | CastFnPtr of ty * ty
+  | CastUnsize of ty * ty
 
 (* Remark: no `ArrayToSlice` variant: it gets eliminated in a micro-pass. *)
 and unop =
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
index c94a2ed2..9c211d91 100644
--- a/charon-ml/src/GAstOfJson.ml
+++ b/charon-ml/src/GAstOfJson.ml
@@ -764,6 +764,10 @@ let cast_kind_of_json (js : json) : (cast_kind, string) result =
         let* src_ty = ty_of_json src_ty in
         let* tgt_ty = ty_of_json tgt_ty in
         Ok (CastFnPtr (src_ty, tgt_ty))
+    | `Assoc [ ("Unsize", `List [ src_ty; tgt_ty ]) ] ->
+        let* src_ty = ty_of_json src_ty in
+        let* tgt_ty = ty_of_json tgt_ty in
+        Ok (CastUnsize (src_ty, tgt_ty))
     | _ -> Error "")
 
 let unop_of_json (js : json) : (unop, string) result =
diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml
index b424dd6b..e825ebe4 100644
--- a/charon-ml/src/PrintExpressions.ml
+++ b/charon-ml/src/PrintExpressions.ml
@@ -59,6 +59,8 @@ let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string =
       ^ ">"
   | CastFnPtr (src, tgt) ->
       "cast<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
+  | CastUnsize (src, tgt) ->
+      "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
 
 let unop_to_string (env : ('a, 'b) fmt_env) (unop : unop) : string =
   match unop with
diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs
index 5c9997c1..e09eebbc 100644
--- a/charon/src/ast/expressions.rs
+++ b/charon/src/ast/expressions.rs
@@ -156,6 +156,12 @@ pub enum CastKind {
     /// Remark: for now we don't support conversions with Char.
     Scalar(LiteralTy, LiteralTy),
     FnPtr(Ty, Ty),
+    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
+    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
+    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
+    ///
+    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
+    Unsize(Ty, Ty),
 }
 
 /// Binary operations.
diff --git a/charon/src/lib.rs b/charon/src/lib.rs
index 4234a6a1..0e5f9157 100644
--- a/charon/src/lib.rs
+++ b/charon/src/lib.rs
@@ -11,10 +11,12 @@
 //! we reconstructed the control-flow to have `if ... then ... else ...`,
 //! loops, etc. instead of `GOTO`s).
 
+#![expect(incomplete_features)]
 #![feature(rustc_private)]
-#![feature(box_patterns)]
 // For rustdoc: prevents overflows
 #![recursion_limit = "256"]
+#![feature(box_patterns)]
+#![feature(deref_patterns)]
 #![feature(if_let_guard)]
 #![feature(impl_trait_in_assoc_type)]
 #![feature(iter_array_chunks)]
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index f538717a..eb5656d2 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -97,9 +97,16 @@ impl<C: AstFormatter> FmtWithCtx<C> for gast::Body {
 impl<C: AstFormatter> FmtWithCtx<C> for CastKind {
     fn fmt_with_ctx(&self, ctx: &C) -> String {
         match self {
-            CastKind::Scalar(src, tgt) => format!("cast<{src},{tgt}>"),
+            CastKind::Scalar(src, tgt) => format!("cast<{src}, {tgt}>"),
             CastKind::FnPtr(src, tgt) => {
-                format!("cast<{},{}>", src.fmt_with_ctx(ctx), tgt.fmt_with_ctx(ctx))
+                format!("cast<{}, {}>", src.fmt_with_ctx(ctx), tgt.fmt_with_ctx(ctx))
+            }
+            CastKind::Unsize(src, tgt) => {
+                format!(
+                    "unsize_cast<{}, {}>",
+                    src.fmt_with_ctx(ctx),
+                    tgt.fmt_with_ctx(ctx)
+                )
             }
         }
     }
diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/translate/translate_functions_to_ullbc.rs
index 1fcf70ef..4c4a25cd 100644
--- a/charon/src/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/translate/translate_functions_to_ullbc.rs
@@ -598,7 +598,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let tgt_ty = self.translate_ty(span, erase_regions, tgt_ty)?;
 
                 // Translate the operand
-                let (op, src_ty) = self.translate_operand_with_type(span, operand)?;
+                let (operand, src_ty) = self.translate_operand_with_type(span, operand)?;
 
                 match (cast_kind, &src_ty, &tgt_ty) {
                     (hax::CastKind::IntToInt, _, _) => {
@@ -608,48 +608,43 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::Scalar(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     (
                         hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize),
-                        Ty::Ref(_, t1, kind1),
-                        Ty::Ref(_, t2, kind2),
+                        Ty::Ref(
+                            _,
+                            deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Array), generics)),
+                            kind1,
+                        ),
+                        Ty::Ref(
+                            _,
+                            deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Slice), generics1)),
+                            kind2,
+                        ),
                     ) => {
                         // In MIR terminology, we go from &[T; l] to &[T] which means we
                         // effectively "unsize" the type, as `l` no longer appears in the
                         // destination type. At runtime, the converse happens: the length
                         // materializes into the fat pointer.
-                        match (&**t1, &**t2) {
-                            (
-                                Ty::Adt(TypeId::Assumed(AssumedTy::Array), generics),
-                                Ty::Adt(TypeId::Assumed(AssumedTy::Slice), generics1),
-                            ) => {
-                                assert!(
-                                    generics.types.len() == 1 && generics.const_generics.len() == 1
-                                );
-                                assert!(generics.types[0] == generics1.types[0]);
-                                assert!(kind1 == kind2);
-                                Ok(Rvalue::UnaryOp(
-                                    UnOp::ArrayToSlice(
-                                        *kind1,
-                                        generics.types[0].clone(),
-                                        generics.const_generics[0].clone(),
-                                    ),
-                                    op,
-                                ))
-                            }
-                            _ => {
-                                error_or_panic!(
-                                    self,
-                                    span,
-                                    format!(
-                                        "Unsupported cast:\n\n- rvalue: {:?}\n\n- src={:?}\n\n- dst={:?}",
-                                        rvalue, src_ty, tgt_ty
-                                    )
-                                )
-                            }
-                        }
+                        assert!(generics.types.len() == 1 && generics.const_generics.len() == 1);
+                        assert!(generics.types[0] == generics1.types[0]);
+                        assert!(kind1 == kind2);
+                        Ok(Rvalue::UnaryOp(
+                            UnOp::ArrayToSlice(
+                                *kind1,
+                                generics.types[0].clone(),
+                                generics.const_generics[0].clone(),
+                            ),
+                            operand,
+                        ))
+                    }
+                    (hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize), _, _) => {
+                        Ok(Rvalue::UnaryOp(
+                            UnOp::Cast(CastKind::Unsize(src_ty.clone(), tgt_ty.clone())),
+                            operand,
+                        ))
                     }
                     (
                         hax::CastKind::PointerCoercion(hax::PointerCoercion::ClosureFnPointer(
@@ -663,7 +658,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let tgt_ty = tgt_ty.clone();
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     (
@@ -675,7 +670,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let tgt_ty = tgt_ty.clone();
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     _ => {
diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out
index 7de6e8bf..31cc8171 100644
--- a/charon/tests/ui/closures.out
+++ b/charon/tests/ui/closures.out
@@ -141,7 +141,7 @@ fn test_crate::test_closure_u32(@1: u32) -> u32
     let @5: u32; // anonymous local
 
     @3 := {test_crate::test_closure_u32::closure} {}
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(move (@3))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (f@2)
@@ -174,7 +174,7 @@ fn test_crate::test_closure_ref_u32<'a>(@1: &'a (u32)) -> &'a (u32)
     let @6: &'_ (u32); // anonymous local
 
     @3 := {test_crate::test_closure_ref_u32::closure} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32),fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32)>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32), fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32)>(move (@3))
     drop @3
     @fake_read(f@2)
     @5 := copy (f@2)
@@ -209,7 +209,7 @@ fn test_crate::test_closure_ref_param<'_0, T>(@1: &'_0 (T)) -> &'_0 (T)
     let @6: &'_ (T); // anonymous local
 
     @3 := {test_crate::test_closure_ref_param::closure<T>} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T),fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T)>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T), fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T)>(move (@3))
     drop @3
     @fake_read(f@2)
     @5 := copy (f@2)
@@ -246,7 +246,7 @@ fn test_crate::test_map_option2(@1: core::option::Option<u32>) -> core::option::
     let @5: fn(u32) -> u32; // anonymous local
 
     @3 := {test_crate::test_map_option2::closure} {}
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(move (@3))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (x@1)
@@ -337,7 +337,7 @@ fn test_crate::test_id_clone(@1: u32) -> u32
     let @3: fn(u32) -> u32; // anonymous local
     let @4: u32; // anonymous local
 
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(const (test_crate::id_clone<u32>[core::clone::impls::{impl core::clone::Clone for u32#8}]))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(const (test_crate::id_clone<u32>[core::clone::impls::{impl core::clone::Clone for u32#8}]))
     @fake_read(f@2)
     @3 := copy (f@2)
     @4 := copy (x@1)
@@ -358,7 +358,7 @@ where
     let @3: fn(T) -> T; // anonymous local
     let @4: T; // anonymous local
 
-    f@2 := cast<fn(T) -> T,fn(T) -> T>(const (test_crate::id_clone<T>[@TraitClause0]))
+    f@2 := cast<fn(T) -> T, fn(T) -> T>(const (test_crate::id_clone<T>[@TraitClause0]))
     @fake_read(f@2)
     @3 := copy (f@2)
     @4 := move (x@1)
@@ -431,7 +431,7 @@ fn test_crate::test_regions<'a>(@1: &'a (u32)) -> u32
     let @6: &'_ (&'_ (u32)); // anonymous local
 
     @3 := {test_crate::test_regions::closure} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32,fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32, fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (f@2)
diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out
index 855400fe..65d72cfe 100644
--- a/charon/tests/ui/issue-114-opaque-bodies.out
+++ b/charon/tests/ui/issue-114-opaque-bodies.out
@@ -101,7 +101,7 @@ fn core::convert::num::{impl core::convert::From<i32> for i64#83}::from(@1: i32)
     let @0: i64; // return
     let small@1: i32; // arg #1
 
-    @0 := cast<i32,i64>(copy (small@1))
+    @0 := cast<i32, i64>(copy (small@1))
     return
 }
 
diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out
index 524045cd..a1ccf1f3 100644
--- a/charon/tests/ui/no_nested_borrows.out
+++ b/charon/tests/ui/no_nested_borrows.out
@@ -118,7 +118,7 @@ fn test_crate::cast_u32_to_i32(@1: u32) -> i32
     let @2: u32; // anonymous local
 
     @2 := copy (x@1)
-    @0 := cast<u32,i32>(move (@2))
+    @0 := cast<u32, i32>(move (@2))
     drop @2
     return
 }
@@ -130,7 +130,7 @@ fn test_crate::cast_bool_to_i32(@1: bool) -> i32
     let @2: bool; // anonymous local
 
     @2 := copy (x@1)
-    @0 := cast<bool,i32>(move (@2))
+    @0 := cast<bool, i32>(move (@2))
     drop @2
     return
 }
diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out
new file mode 100644
index 00000000..cb45ab7b
--- /dev/null
+++ b/charon/tests/ui/result-unwrap.out
@@ -0,0 +1,169 @@
+# Final LLBC before serialization:
+
+enum core::result::Result<T, E> =
+|  Ok(T)
+|  Err(E)
+
+
+enum core::fmt::rt::Alignment =
+|  Left()
+|  Right()
+|  Center()
+|  Unknown()
+
+
+enum core::option::Option<T> =
+|  None()
+|  Some(T)
+
+
+struct core::fmt::Formatter<'a>
+  where
+      'a : 'a,
+ =
+{
+  flags: u32,
+  fill: char,
+  align: core::fmt::rt::Alignment,
+  width: core::option::Option<usize>,
+  precision: core::option::Option<usize>,
+  buf: &'a mut (dyn (exists(TODO)))
+}
+
+struct core::fmt::Error = {}
+
+trait core::fmt::Debug<Self>
+{
+    fn fmt : core::fmt::Debug::fmt
+}
+
+fn core::result::unwrap_failed<'_0, '_1>(@1: &'_0 (Str), @2: &'_1 (dyn (exists(TODO)))) -> !
+
+fn core::result::{core::result::Result<T, E>}::unwrap<T, E>(@1: core::result::Result<T, E>) -> T
+where
+    [@TraitClause0]: core::fmt::Debug<E>,
+{
+    let t@0: T; // return
+    let self@1: core::result::Result<T, E>; // arg #1
+    let e@2: E; // local
+    let @3: !; // anonymous local
+    let @4: &'_ (dyn (exists(TODO))); // anonymous local
+    let @5: &'_ (E); // anonymous local
+
+    match self@1 {
+        0 => {
+            nop
+        },
+        1 => {
+            e@2 := move ((self@1 as variant @1).0)
+            @5 := &e@2
+            @4 := unsize_cast<&'_ (E), &'_ (dyn (exists(TODO)))>(move (@5))
+            drop @5
+            @3 := core::result::unwrap_failed(const ("called `Result::unwrap()` on an `Err` value"), move (@4))
+        }
+    }
+    t@0 := move ((self@1 as variant @0).0)
+    return
+}
+
+trait core::fmt::LowerHex<Self>
+{
+    fn fmt : core::fmt::LowerHex::fmt
+}
+
+fn core::fmt::num::{impl core::fmt::LowerHex for u32#60}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+impl core::fmt::num::{impl core::fmt::LowerHex for u32#60} : core::fmt::LowerHex<u32>
+{
+    fn fmt = core::fmt::num::{impl core::fmt::LowerHex for u32#60}::fmt
+}
+
+fn core::fmt::LowerHex::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+trait core::fmt::Display<Self>
+{
+    fn fmt : core::fmt::Display::fmt
+}
+
+fn core::fmt::num::imp::{impl core::fmt::Display for u32#5}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+impl core::fmt::num::imp::{impl core::fmt::Display for u32#5} : core::fmt::Display<u32>
+{
+    fn fmt = core::fmt::num::imp::{impl core::fmt::Display for u32#5}::fmt
+}
+
+fn core::fmt::Display::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+trait core::fmt::UpperHex<Self>
+{
+    fn fmt : core::fmt::UpperHex::fmt
+}
+
+fn core::fmt::num::{impl core::fmt::UpperHex for u32#61}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+impl core::fmt::num::{impl core::fmt::UpperHex for u32#61} : core::fmt::UpperHex<u32>
+{
+    fn fmt = core::fmt::num::{impl core::fmt::UpperHex for u32#61}::fmt
+}
+
+fn core::fmt::UpperHex::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+fn core::fmt::num::{impl core::fmt::Debug for u32#86}::fmt<'_0, '_1, '_2>(@1: &'_0 (u32), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+{
+    let @0: core::result::Result<(), core::fmt::Error>; // return
+    let self@1: &'_ (u32); // arg #1
+    let f@2: &'_ mut (core::fmt::Formatter<'_>); // arg #2
+    let @3: u32; // anonymous local
+    let @4: u32; // anonymous local
+    let @5: u32; // anonymous local
+    let @6: u32; // anonymous local
+
+    @4 := copy ((*(f@2)).flags)
+    @3 := move (@4) & const (16 : u32)
+    drop @4
+    switch move (@3) {
+        0 : u32 => {
+            drop @3
+            @6 := copy ((*(f@2)).flags)
+            @5 := move (@6) & const (32 : u32)
+            drop @6
+            switch move (@5) {
+                0 : u32 => {
+                    drop @5
+                    @0 := core::fmt::num::imp::{impl core::fmt::Display for u32#5}::fmt(move (self@1), move (f@2))
+                },
+                _ => {
+                    drop @5
+                    @0 := core::fmt::num::{impl core::fmt::UpperHex for u32#61}::fmt(move (self@1), move (f@2))
+                }
+            }
+        },
+        _ => {
+            drop @3
+            @0 := core::fmt::num::{impl core::fmt::LowerHex for u32#60}::fmt(move (self@1), move (f@2))
+        }
+    }
+    return
+}
+
+impl core::fmt::num::{impl core::fmt::Debug for u32#86} : core::fmt::Debug<u32>
+{
+    fn fmt = core::fmt::num::{impl core::fmt::Debug for u32#86}::fmt
+}
+
+fn test_crate::unwrap(@1: core::result::Result<u32, u32>) -> u32
+{
+    let @0: u32; // return
+    let res@1: core::result::Result<u32, u32>; // arg #1
+    let @2: core::result::Result<u32, u32>; // anonymous local
+
+    @2 := copy (res@1)
+    @0 := core::result::{core::result::Result<T, E>}::unwrap<u32, u32>[core::fmt::num::{impl core::fmt::Debug for u32#86}](move (@2))
+    drop @2
+    return
+}
+
+fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+
+
diff --git a/charon/tests/ui/unsupported/result-unwrap.rs b/charon/tests/ui/result-unwrap.rs
similarity index 54%
rename from charon/tests/ui/unsupported/result-unwrap.rs
rename to charon/tests/ui/result-unwrap.rs
index 75f39da5..e6c515bb 100644
--- a/charon/tests/ui/unsupported/result-unwrap.rs
+++ b/charon/tests/ui/result-unwrap.rs
@@ -1,8 +1,5 @@
-//@ known-failure
-//@ no-check-output
 //@ charon-args=--extract-opaque-bodies
 
-// Errors because dyn types are not supported.
 fn unwrap(res: Result<u32, u32>) -> u32 {
     res.unwrap()
 }
diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out
new file mode 100644
index 00000000..5a648896
--- /dev/null
+++ b/charon/tests/ui/unsize.out
@@ -0,0 +1,126 @@
+# Final LLBC before serialization:
+
+opaque type alloc::rc::Rc<T, A>
+
+struct alloc::alloc::Global = {}
+
+opaque type alloc::string::String
+
+fn alloc::rc::{alloc::rc::Rc<T, alloc::alloc::Global>#8}::new<T>(@1: T) -> alloc::rc::Rc<T, alloc::alloc::Global>
+
+fn alloc::string::{alloc::string::String}::new() -> alloc::string::String
+
+trait core::clone::Clone<Self>
+{
+    fn clone : core::clone::Clone::clone
+    fn clone_from
+}
+
+fn alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone<'_0>(@1: &'_0 (alloc::string::String)) -> alloc::string::String
+
+fn alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone_from<'_0, '_1>(@1: &'_0 mut (alloc::string::String), @2: &'_1 (alloc::string::String))
+
+impl alloc::string::{impl core::clone::Clone for alloc::string::String#6} : core::clone::Clone<alloc::string::String>
+{
+    fn clone = alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone
+    fn clone_from = alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone_from
+}
+
+fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+
+fn test_crate::foo()
+{
+    let @0: (); // return
+    let array@1: Array<i32, 2 : usize>; // local
+    let @2: &'_ (Slice<i32>); // anonymous local
+    let @3: &'_ (Array<i32, 2 : usize>); // anonymous local
+    let @4: &'_ (Array<i32, 2 : usize>); // anonymous local
+    let @5: alloc::boxed::Box<Slice<i32>>; // anonymous local
+    let @6: alloc::boxed::Box<Array<i32, 2 : usize>>; // anonymous local
+    let @7: Array<i32, 2 : usize>; // anonymous local
+    let @8: alloc::rc::Rc<Slice<i32>, alloc::alloc::Global>; // anonymous local
+    let @9: alloc::rc::Rc<Array<i32, 2 : usize>, alloc::alloc::Global>; // anonymous local
+    let @10: Array<i32, 2 : usize>; // anonymous local
+    let string@11: alloc::string::String; // local
+    let @12: &'_ (dyn (exists(TODO))); // anonymous local
+    let @13: &'_ (alloc::string::String); // anonymous local
+    let @14: &'_ (alloc::string::String); // anonymous local
+    let @15: alloc::boxed::Box<dyn (exists(TODO))>; // anonymous local
+    let @16: alloc::boxed::Box<alloc::string::String>; // anonymous local
+    let @17: alloc::string::String; // anonymous local
+    let @18: &'_ (alloc::string::String); // anonymous local
+    let @19: alloc::rc::Rc<dyn (exists(TODO)), alloc::alloc::Global>; // anonymous local
+    let @20: alloc::rc::Rc<alloc::string::String, alloc::alloc::Global>; // anonymous local
+    let @21: alloc::string::String; // anonymous local
+    let @22: &'_ (alloc::string::String); // anonymous local
+    let @23: (); // anonymous local
+
+    array@1 := [const (0 : i32), const (0 : i32); 2 : usize]
+    @fake_read(array@1)
+    @4 := &array@1
+    @3 := &*(@4)
+    @2 := @ArrayToSliceShared<'_, i32, 2 : usize>(move (@3))
+    drop @3
+    @fake_read(@2)
+    drop @4
+    drop @2
+    @7 := copy (array@1)
+    @6 := @BoxNew<Array<i32, 2 : usize>>(move (@7))
+    @5 := unsize_cast<alloc::boxed::Box<Array<i32, 2 : usize>>, alloc::boxed::Box<Slice<i32>>>(move (@6))
+    drop @6
+    drop @7
+    drop @6
+    @fake_read(@5)
+    drop @5
+    drop @5
+    @10 := copy (array@1)
+    @9 := alloc::rc::{alloc::rc::Rc<T, alloc::alloc::Global>#8}::new<Array<i32, 2 : usize>>(move (@10))
+    @8 := unsize_cast<alloc::rc::Rc<Array<i32, 2 : usize>, alloc::alloc::Global>, alloc::rc::Rc<Slice<i32>, alloc::alloc::Global>>(move (@9))
+    drop @9
+    drop @10
+    drop @9
+    @fake_read(@8)
+    drop @8
+    drop @8
+    string@11 := alloc::string::{alloc::string::String}::new()
+    @fake_read(string@11)
+    @14 := &string@11
+    @13 := &*(@14)
+    @12 := unsize_cast<&'_ (alloc::string::String), &'_ (dyn (exists(TODO)))>(move (@13))
+    drop @13
+    @fake_read(@12)
+    drop @14
+    drop @12
+    @18 := &string@11
+    @17 := alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone(move (@18))
+    drop @18
+    @16 := @BoxNew<alloc::string::String>(move (@17))
+    @15 := unsize_cast<alloc::boxed::Box<alloc::string::String>, alloc::boxed::Box<dyn (exists(TODO))>>(move (@16))
+    drop @16
+    drop @17
+    drop @16
+    @fake_read(@15)
+    drop @15
+    drop @15
+    @22 := &string@11
+    @21 := alloc::string::{impl core::clone::Clone for alloc::string::String#6}::clone(move (@22))
+    drop @22
+    @20 := alloc::rc::{alloc::rc::Rc<T, alloc::alloc::Global>#8}::new<alloc::string::String>(move (@21))
+    @19 := unsize_cast<alloc::rc::Rc<alloc::string::String, alloc::alloc::Global>, alloc::rc::Rc<dyn (exists(TODO)), alloc::alloc::Global>>(move (@20))
+    drop @20
+    drop @21
+    drop @20
+    @fake_read(@19)
+    drop @19
+    drop @19
+    @23 := ()
+    @0 := move (@23)
+    drop string@11
+    drop string@11
+    drop array@1
+    @0 := ()
+    return
+}
+
+
+
diff --git a/charon/tests/ui/unsize.rs b/charon/tests/ui/unsize.rs
new file mode 100644
index 00000000..984b8a3e
--- /dev/null
+++ b/charon/tests/ui/unsize.rs
@@ -0,0 +1,14 @@
+use std::fmt::Display;
+use std::rc::Rc;
+
+fn foo() {
+    let array: [_; 2] = [0, 0];
+    let _: &[_] = &array;
+    let _: Box<[_]> = Box::new(array);
+    let _: Rc<[_]> = Rc::new(array);
+
+    let string = String::new();
+    let _: &dyn Display = &string;
+    let _: Box<dyn Display> = Box::new(string.clone());
+    let _: Rc<dyn Display> = Rc::new(string.clone());
+}