diff --git a/charon-pin b/charon-pin
index 7e094320c..2143bf3b9 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.
-cb50ff16b9f1066b8a97dc06da704de2da2fa41c
+527ea8e3b5dcb52edd6aef0f7bc34cc09c11dd59
diff --git a/flake.lock b/flake.lock
index a68ccaf14..a8a473334 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,15 +5,16 @@
         "crane": "crane",
         "flake-compat": "flake-compat",
         "flake-utils": "flake-utils",
+        "jail-nix": "jail-nix",
         "nixpkgs": "nixpkgs",
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1784118315,
-        "narHash": "sha256-+ujCegoDtsFk7ALTLgPcbRZkursN7Nsmo9VglSMNP9c=",
+        "lastModified": 1784853955,
+        "narHash": "sha256-r/L1qUPJ97HnJrVvIbHcEIt3c2otIcwG0dvD13WhuUo=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "cb50ff16b9f1066b8a97dc06da704de2da2fa41c",
+        "rev": "527ea8e3b5dcb52edd6aef0f7bc34cc09c11dd59",
         "type": "github"
       },
       "original": {
@@ -106,6 +107,21 @@
         "type": "github"
       }
     },
+    "jail-nix": {
+      "locked": {
+        "lastModified": 1776230864,
+        "narHash": "sha256-YsEjjdOsGEzTeD+iT7ONh071BqWAOQWpzYVei3okAXE=",
+        "owner": "~alexdavid",
+        "repo": "jail.nix",
+        "rev": "404e7da9da5ab9aa643666682b2ba1312fa5fbe8",
+        "type": "sourcehut"
+      },
+      "original": {
+        "owner": "~alexdavid",
+        "repo": "jail.nix",
+        "type": "sourcehut"
+      }
+    },
     "nixpkgs": {
       "locked": {
         "lastModified": 1762111121,
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index b613aba1b..0cf16806e 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -1712,6 +1712,7 @@ let replace_static (crate : crate) : crate =
               {
                 index = RegionId.of_int 1;
                 name = Some "'b";
+                variance = VaUnknown;
                 mutability = LtUnknown;
               };
             ];
diff --git a/src/interp/InterpUtils.ml b/src/interp/InterpUtils.ml
index 1781a5b7d..397478079 100644
--- a/src/interp/InterpUtils.ml
+++ b/src/interp/InterpUtils.ml
@@ -929,7 +929,13 @@ let instantiate_fun_sig (span : Meta.span option) (ctx : eval_ctx)
       let fresh_regions = fresh_regions in
       let fresh_region_vars : region_param list =
         List.map
-          (fun index -> { Types.index; name = None; mutability = LtUnknown })
+          (fun index ->
+            {
+              Types.index;
+              name = None;
+              variance = VaUnknown;
+              mutability = LtUnknown;
+            })
           fresh_regions
       in
       let open Substitute in
diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml
index 9c031b9b8..b084b69be 100644
--- a/src/llbc/Builtin.ml
+++ b/src/llbc/Builtin.ml
@@ -45,14 +45,20 @@ module Sig = struct
 
   (** Region 'a of id 0 *)
   let region_param_0 : region_param =
-    { index = rvar_id_0; name = Some "'a"; mutability = LtUnknown }
+    {
+      index = rvar_id_0;
+      name = Some "'a";
+      variance = VaUnknown;
+      mutability = LtUnknown;
+    }
 
   (** Region group: [{ parent={}; regions:{'a of id 0} }] *)
   let region_group_0 : region_var_group =
     { id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }
 
   (** Type parameter [T] of id 0 *)
-  let type_param_0 : type_param = { index = tvar_id_0; name = "T" }
+  let type_param_0 : type_param =
+    { index = tvar_id_0; name = "T"; variance = VaUnknown }
 
   let usize_ty : ty = TLiteral (TUInt Usize)
 
diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml
index 5ea3e9be6..d4d0c3182 100644
--- a/src/symbolic/SymbolicToPureTypes.ml
+++ b/src/symbolic/SymbolicToPureTypes.ml
@@ -215,7 +215,7 @@ let translate_strait_type_constraint (span : Meta.span option)
   { trait_ref; type_id; ty }
 
 let translate_type_param (p : T.type_param) : type_param =
-  let { index; name } : T.type_param = p in
+  let { index; name; variance = _ } : T.type_param = p in
   { index; name }
 
 let translate_generic_params (span : Meta.span option)