From 72db1ad2eb5835b00c45daa06257e46962000af5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 8 Feb 2024 13:21:26 +0100
Subject: Fix a small issue ollowing updates in Charon

---
 compiler/InterpreterStatements.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'compiler/InterpreterStatements.ml')

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 0cf8b88a..c17c1563 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -772,9 +772,6 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               ^ "\n- trait and method generics:\n"
               ^ generic_args_to_string ctx
                   (Option.get func.trait_and_method_generic_args)));
-          (* When instantiating, we need to group the generics for the trait ref
-             and the method *)
-          let generics = Option.get func.trait_and_method_generic_args in
           (* Lookup the trait method signature - there are several possibilities
              depending on whethere we call a top-level trait method impl or the
              method from a local clause *)
@@ -794,6 +791,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               | Some (_, id) ->
                   (* This is a required method *)
                   let method_def = ctx_lookup_fun_decl ctx id in
+                  (* We have to concatenate the generics for the impl
+                     and the generics for the method *)
+                  let generics =
+                    merge_generic_args trait_ref.generics func.generics
+                  in
                   (* Instantiate *)
                   let tr_self = TraitRef trait_ref in
                   let fid : fun_id = FRegular id in
@@ -898,6 +900,9 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               log#ldebug
                 (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
               (* Instantiate *)
+              (* When instantiating, we need to group the generics for the trait ref
+                 and the method *)
+              let generics = Option.get func.trait_and_method_generic_args in
               let regions_hierarchy =
                 LlbcAstUtils.FunIdMap.find (FRegular method_id)
                   ctx.fun_ctx.regions_hierarchies
-- 
cgit v1.2.3