From 0c0207121696dffea72652c092cd07209c3df356 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 11:23:21 +0200
Subject: Update charon pin

---
 charon-pin                  | 2 +-
 compiler/AssociatedTypes.ml | 4 ++--
 compiler/SymbolicToPure.ml  | 1 +
 flake.lock                  | 6 +++---
 4 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/charon-pin b/charon-pin
index 2b45bb6d..6568ef9b 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.
-c049120c15567d22520c94f570363eb4948d849f
+7cb5b367aec5768bee003d395634b30e13638b7d
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 27425a51..c0c5399f 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 _ ->
+  | Closure _ | Unsolved _ ->
       false
   | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
       trait_instance_id_is_local_clause id
@@ -443,7 +443,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
   | Closure (fid, generics) ->
       let generics = norm_ctx_normalize_generic_args ctx generics in
       (Closure (fid, generics), None)
-  | UnknownTrait _ ->
+  | Unsolved _ | UnknownTrait _ ->
       (* This is actually an error case *)
       (id, None)
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4aa24fcf..3e22d36b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -462,6 +462,7 @@ and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty)
   | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr)
   | FnPointer _ | Closure _ ->
       craise __FILE__ __LINE__ meta "Closures are not supported yet"
+  | Unsolved _ -> craise __FILE__ __LINE__ meta "Couldn't solve trait bound"
   | UnknownTrait s -> craise __FILE__ __LINE__ meta ("Unknown trait found: " ^ s)
 
 (** Translate a signature type - TODO: factor out the different translation functions *)
diff --git a/flake.lock b/flake.lock
index cad633ea..38241840 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1716398715,
-        "narHash": "sha256-z4COmDxa3DY6pVLgB85n6EVWFPkx87tr+xkJGiQvpV8=",
+        "lastModified": 1716542431,
+        "narHash": "sha256-Q+WLCH7teTpBG1ScWi5VsvpjNmUrgDSv6I6Vv8CLkaM=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "c049120c15567d22520c94f570363eb4948d849f",
+        "rev": "7cb5b367aec5768bee003d395634b30e13638b7d",
         "type": "github"
       },
       "original": {
-- 
cgit v1.2.3