Remove g_value, g_typed_value, etc. to make values and abstract values

distinct

5 files changed, 199 insertions, 149 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 1fbe2c09..62e4d7b9 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -130,7 +130,10 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
 *)
 let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
-  assert (List.for_all (fun (var, value) -> var.var_ty = value.ty) vars);
+  assert (
+    List.for_all
+      (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
+      vars);
   let vars =
     List.map (fun (var, value) -> Var (var_to_binder var, value)) vars
   in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d6367702..ad7bdba1 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -251,11 +251,11 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
         else ()
       (** Check the borrow id and control the diving *)
 
-      method! visit_SharedBorrow env bid =
+      method! visit_SharedBorrow _env bid =
         if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid)) else ()
       (** Check the borrow id *)
 
-      method! visit_InactivatedMutBorrow env bid =
+      method! visit_InactivatedMutBorrow _env bid =
         if bid = l then raise (FoundBorrowContent (V.InactivatedMutBorrow bid))
         else ()
       (** Check the borrow id *)
@@ -372,7 +372,7 @@ let unwrap_res_to_outer_or opt default =
   match opt with Some x -> Outer x | None -> default
 
 (** Return the first loan we find in a value *)
-let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
+let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
   let obj =
     object
       inherit [_] V.iter_typed_value
@@ -387,7 +387,7 @@ let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
   with FoundLoanContent lc -> Some lc
 
 (** Check if a value contains ⊥ *)
-let rec bottom_in_value (v : V.typed_value) : bool =
+let bottom_in_value (v : V.typed_value) : bool =
   let obj =
     object
       inherit [_] V.iter_typed_value
@@ -1202,7 +1202,11 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
     Subst.type_def_get_instantiated_field_type def opt_variant_id types
   in
   (* Initialize the expanded value *)
-  let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
+  let fields =
+    List.map
+      (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value))
+      field_types
+  in
   let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
   let ty = T.Adt (T.AdtId def_id, regions, types) in
   { V.value = av; V.ty }
@@ -1211,7 +1215,9 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     V.typed_value =
   (* Generate the field values *)
-  let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
+  let fields =
+    List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types
+  in
   let v = V.Adt { variant_id = None; field_values = fields } in
   let ty = T.Adt (T.Tuple, [], field_types) in
   { V.value = v; V.ty }
@@ -1366,7 +1372,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
          We use exceptions to make it handy: whenever we update the
          context, we raise an exception wrapping the updated context.
       *)
-      let rec inspect_update v : unit =
+      let rec inspect_update (v : V.typed_value) : unit =
         match v.V.value with
         | V.Concrete _ -> ()
         | V.Bottom -> ()
@@ -1463,7 +1469,7 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
 
          We use exceptions to make it handy.
       *)
-      let rec inspect_update (end_loans : bool) v : unit =
+      let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit =
         match v.V.value with
         | V.Concrete _ -> ()
         | V.Bottom ->
@@ -1654,7 +1660,7 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       (* Move the value *)
       L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v));
       assert (not (bottom_in_value v));
-      let bottom = { V.value = Bottom; ty = v.ty } in
+      let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
       match write_place config access p bottom ctx with
       | Error _ -> failwith "Unreachable"
       | Ok ctx -> (ctx, v))
@@ -1723,7 +1729,8 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
                 | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
                     failwith "Unreachable"
               in
-              Ok { V.value = V.Concrete (Bool b); ty = T.Bool }
+              Ok
+                ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
           | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
           | E.BitOr -> (
               (* The two operands must have the same type and the result is an integer *)
@@ -1783,7 +1790,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
             if bkind = E.Shared then V.SharedBorrow bid
             else V.InactivatedMutBorrow bid
           in
-          let rv = { V.value = V.Borrow bc; ty = rv_ty } in
+          let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
           (* Compute the value with which to replace the value at place p *)
           let nv =
             match v.V.value with
@@ -1809,7 +1816,9 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
           (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
           let ctx, bid = C.fresh_borrow_id ctx in
           let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
-          let rv = { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } in
+          let rv : V.typed_value =
+            { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
+          in
           (* Compute the value with which to replace the value at place p *)
           let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
           (* Update the value in the context *)
@@ -1847,7 +1856,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
       (* Match on the aggregate kind *)
       match aggregate_kind with
       | E.AggregatedTuple ->
-          let tys = List.map (fun v -> v.V.ty) values in
+          let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
           let v = V.Adt { variant_id = None; field_values = values } in
           let ty = T.Adt (T.Tuple, [], tys) in
           Ok (ctx, { V.value = v; ty })
@@ -1859,9 +1868,13 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
             Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
               types
           in
-          assert (expected_field_types = List.map (fun v -> v.V.ty) values);
+          assert (
+            expected_field_types
+            = List.map (fun (v : V.typed_value) -> v.V.ty) values);
           (* Construct the value *)
-          let av = { V.variant_id = opt_variant_id; V.field_values = values } in
+          let av : V.adt_value =
+            { V.variant_id = opt_variant_id; V.field_values = values }
+          in
           let aty = T.Adt (T.AdtId def_id, regions, types) in
           Ok (ctx, { V.value = Adt av; ty = aty }))
 
@@ -2242,7 +2255,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
 
       (* Create and push the input variables *)
       let input_vars =
-        V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl
+        V.VarId.mapi_from1
+          (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v))
+          args_vl
       in
       let ctx = C.ctx_push_vars ctx input_vars in
 
diff --git a/src/Print.ml b/src/Print.ml
index f92102fe..359416c8 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -201,29 +201,22 @@ module Values = struct
     let regions = V.RegionId.set_to_string sp.rset_ended in
     "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"
 
-  type ('r, 'sv, 'bc, 'lc) gen_value_formatter = {
-    r_to_string : 'r -> string;
-    sv_to_string : 'sv -> string;
-    bc_to_string : 'bc -> string;
-    lc_to_string : 'lc -> string;
-  }
-  (** Auxiliary record: we use it to factorize value formatting *)
-
-  let rec g_typed_value_to_string (fmt : value_formatter)
-      (gfmt : ('r, 'sv, 'bc, 'lc) gen_value_formatter)
-      (v : ('r, 'sv, 'bc, 'lc) V.g_typed_value) : string =
-    let ty_fmt : 'r PT.type_formatter =
-      {
-        PT.r_to_string = gfmt.r_to_string;
-        PT.type_var_id_to_string = fmt.type_var_id_to_string;
-        PT.type_def_id_to_string = fmt.type_def_id_to_string;
-      }
-    in
+  let symbolic_value_proj_to_string (fmt : value_formatter)
+      (sv : V.symbolic_value) (rty : T.rty) : string =
+    symbolic_value_id_to_string sv.sv_id
+    ^ " : "
+    ^ PT.ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
+    ^ " <: "
+    ^ PT.ty_to_string (value_to_rtype_formatter fmt) rty
+
+  let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) :
+      string =
+    let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in
     match v.value with
     | Concrete cv -> constant_value_to_string cv
     | Adt av -> (
         let field_values =
-          List.map (g_typed_value_to_string fmt gfmt) av.field_values
+          List.map (typed_value_to_string fmt) av.field_values
         in
         match v.ty with
         | T.Adt (T.Tuple, _, _) ->
@@ -258,22 +251,10 @@ module Values = struct
             | _ -> failwith "Inconsistent value")
         | _ -> failwith "Inconsistent typed value")
     | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
-    | Borrow bc -> gfmt.bc_to_string bc
-    | Loan lc -> gfmt.lc_to_string lc
-    | Symbolic s -> gfmt.sv_to_string s
-
-  let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) :
-      string =
-    let gfmt =
-      {
-        r_to_string = PT.erased_region_to_string;
-        sv_to_string =
-          symbolic_proj_comp_to_string (value_to_rtype_formatter fmt);
-        bc_to_string = borrow_content_to_string fmt;
-        lc_to_string = loan_content_to_string fmt;
-      }
-    in
-    g_typed_value_to_string fmt gfmt v
+    | Borrow bc -> borrow_content_to_string fmt bc
+    | Loan lc -> loan_content_to_string fmt lc
+    | Symbolic s ->
+        symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) s
 
   and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
       string =
@@ -294,14 +275,6 @@ module Values = struct
         "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
     | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
-  let symbolic_value_proj_to_string (fmt : value_formatter)
-      (sv : V.symbolic_value) (rty : T.rty) : string =
-    symbolic_value_id_to_string sv.sv_id
-    ^ " : "
-    ^ PT.ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
-    ^ " <: "
-    ^ PT.ty_to_string (value_to_rtype_formatter fmt) rty
-
   let rec abstract_shared_borrows_to_string (fmt : value_formatter)
       (abs : V.abstract_shared_borrows) : string =
     match abs with
@@ -324,15 +297,49 @@ module Values = struct
 
   let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
       string =
-    let gfmt =
-      {
-        r_to_string = PT.region_to_string fmt.r_to_string;
-        sv_to_string = aproj_to_string fmt;
-        bc_to_string = aborrow_content_to_string fmt;
-        lc_to_string = aloan_content_to_string fmt;
-      }
-    in
-    g_typed_value_to_string fmt gfmt v
+    let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in
+    match v.value with
+    | AConcrete cv -> constant_value_to_string cv
+    | AAdt av -> (
+        let field_values =
+          List.map (typed_avalue_to_string fmt) av.field_values
+        in
+        match v.ty with
+        | T.Adt (T.Tuple, _, _) ->
+            (* Tuple *)
+            "(" ^ String.concat ", " field_values ^ ")"
+        | T.Adt (T.AdtId def_id, _, _) ->
+            (* "Regular" ADT *)
+            let adt_ident =
+              match av.variant_id with
+              | Some vid -> fmt.adt_variant_to_string def_id vid
+              | None -> fmt.type_def_id_to_string def_id
+            in
+            if List.length field_values > 0 then
+              match fmt.adt_field_names def_id av.V.variant_id with
+              | None ->
+                  let field_values = String.concat ", " field_values in
+                  adt_ident ^ " (" ^ field_values ^ ")"
+              | Some field_names ->
+                  let field_values = List.combine field_names field_values in
+                  let field_values =
+                    List.map
+                      (fun (field, value) -> field ^ " = " ^ value ^ ";")
+                      field_values
+                  in
+                  let field_values = String.concat " " field_values in
+                  adt_ident ^ " { " ^ field_values ^ " }"
+            else adt_ident
+        | T.Adt (T.Assumed aty, _, _) -> (
+            (* Assumed type *)
+            match (aty, field_values) with
+            | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
+            | _ -> failwith "Inconsistent value")
+        | _ -> failwith "Inconsistent typed value")
+    | ABottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
+    | ABorrow bc -> aborrow_content_to_string fmt bc
+    | ALoan lc -> aloan_content_to_string fmt lc
+    | ASymbolic s -> aproj_to_string fmt s
 
   and aloan_content_to_string (fmt : value_formatter) (lc : V.aloan_content) :
       string =
diff --git a/src/Values.ml b/src/Values.ml
index 633b2157..764612af 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -63,79 +63,54 @@ type symbolic_proj_comp = {
     
     "Complementary" stands for the fact that it is a projector over all the
     regions *but* the ones which are listed in the projector.
- *)
+*)
 
-(** Polymorphic iter visitor *)
-class ['self] iter_'r_ty_base =
+(** Ancestor for iter visitor for [typed_value] *)
+class ['self] iter_typed_value_base =
   object (self : 'self)
-    method visit_ty : 'env 'r. ('env -> 'r -> unit) -> 'env -> 'r ty -> unit =
-      fun _visit_'r _env _ty -> ()
-  end
+    inherit [_] VisitorsRuntime.iter
 
-(** A generic, untyped value, used in the environments.
+    method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
 
-    Parameterized by:
-    - 'ty: type
-    - 'sv: symbolic value
-    - 'bc: borrow content
-    - 'lc: loan content
+    method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
 
-    Can be specialized for "regular" values or values in abstractions.
+    method visit_symbolic_proj_comp : 'env -> symbolic_proj_comp -> unit =
+      fun _ _ -> ()
 
-    TODO: unfactorize value and avalue. Making them instanciations of `g_value`
-    creates more problems than solutions, in particular when dealing with
-    visitors (which we can't automatically generate).
-*)
-type ('r, 'sv, 'bc, 'lc) g_value =
-  | Concrete of (constant_value[@opaque])  (** Concrete (non-symbolic) value *)
-  | Adt of ('r, 'sv, 'bc, 'lc) g_adt_value
-      (** Enumerations, structures, tuples, assumed types. Note that units
-          are encoded as 0-tuples  *)
-  | Bottom  (** No value (uninitialized or moved value) *)
-  | Borrow of 'bc  (** A borrowed value *)
-  | Loan of 'lc  (** A loaned value *)
-  | Symbolic of 'sv  (** Unknown value *)
-
-and ('r, 'sv, 'bc, 'lc) g_adt_value = {
-  variant_id : VariantId.id option; [@opaque]
-  field_values : ('r, 'sv, 'bc, 'lc) g_typed_value list;
-}
+    method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
+  end
 
-(** "Generic" ADT value (not "GADT" value) *)
+(** Ancestor for map visitor for [typed_value] *)
+class ['self] map_typed_value_base =
+  object (self : 'self)
+    inherit [_] VisitorsRuntime.map
 
-and ('r, 'sv, 'bc, 'lc) g_typed_value = {
-  value : ('r, 'sv, 'bc, 'lc) g_value;
-  ty : 'r ty;
-}
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_g_typed_value";
-        variety = "iter";
-        ancestors = [ "iter_'r_ty_base" ];
-        polymorphic = true;
-        (* Heirs expect a polymorphic class *)
-        concrete = true;
-      }]
+    method visit_constant_value : 'env -> constant_value -> constant_value =
+      fun _ cv -> cv
 
-class ['self] iter_typed_value_base =
-  object (self : 'self)
-    inherit [_] iter_g_typed_value
+    method visit_erased_region : 'env -> erased_region -> erased_region =
+      fun _ r -> r
 
-    method visit_erased_region : 'env. 'env -> erased_region -> unit =
-      fun _env _ -> ()
+    method visit_symbolic_proj_comp
+        : 'env -> symbolic_proj_comp -> symbolic_proj_comp =
+      fun _ sv -> sv
 
-    method visit_symbolic_proj_comp : 'env. 'env -> symbolic_proj_comp -> unit =
-      fun _env _ -> ()
+    method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
   end
 
+(** An untyped value, used in the environments *)
 type value =
-  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value
-(** "Regular" value *)
+  | Concrete of constant_value  (** Concrete (non-symbolic) value *)
+  | Adt of adt_value  (** Enumerations and structures *)
+  | Bottom  (** No value (uninitialized or moved value) *)
+  | Borrow of borrow_content  (** A borrowed value *)
+  | Loan of loan_content  (** A loaned value *)
+  | Symbolic of symbolic_proj_comp  (** Unknown (symbolic) value *)
 
-and adt_value =
-  (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_adt_value
+and adt_value = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_value list;
+}
 
 and borrow_content =
   | SharedBorrow of (BorrowId.id[@opaque])  (** A shared value *)
@@ -157,12 +132,7 @@ and loan_content =
   | SharedLoan of (BorrowId.set_t[@opaque]) * typed_value
   | MutLoan of (BorrowId.id[@opaque])
 
-and typed_value =
-  ( erased_region,
-    symbolic_proj_comp,
-    borrow_content,
-    loan_content )
-  g_typed_value
+and typed_value = { value : value; ty : ety }
 [@@deriving
   show,
     visitors
@@ -172,6 +142,14 @@ and typed_value =
         ancestors = [ "iter_typed_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
+      },
+    visitors
+      {
+        name = "map_typed_value";
+        variety = "map";
+        ancestors = [ "map_typed_value_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
       }]
 (** "Regular" typed value (we map variables to typed values) *)
 
@@ -189,24 +167,46 @@ type aproj =
 
 type region = RegionVarId.id Types.region [@@deriving show]
 
+(** Ancestor for iter visitor for [typed_avalue] *)
 class ['self] iter_typed_avalue_base =
   object (self : 'self)
-    inherit [_] iter_g_typed_value
+    inherit [_] iter_typed_value
+
+    method visit_region : 'env -> region -> unit = fun _ _ -> ()
+
+    method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
+
+    method visit_abstract_shared_borrows
+        : 'env -> abstract_shared_borrows -> unit =
+      fun _ _ -> ()
 
-    method visit_region : 'env. 'env -> region -> unit = fun _env _r -> ()
+    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+  end
+
+(** Ancestor for MAP visitor for [typed_avalue] *)
+class ['self] map_typed_avalue_base =
+  object (self : 'self)
+    inherit [_] map_typed_value
 
-    method visit_aproj : 'env. 'env -> aproj -> unit = fun env _ -> ()
+    method visit_region : 'env -> region -> region = fun _ r -> r
 
-    method visit_typed_value : 'env. 'env -> typed_value -> unit =
-      fun _env _v -> ()
+    method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
 
     method visit_abstract_shared_borrows
-        : 'env. 'env -> abstract_shared_borrows -> unit =
-      fun _env _asb -> ()
+        : 'env -> abstract_shared_borrows -> abstract_shared_borrows =
+      fun _ asb -> asb
+
+    method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
   end
 
-type avalue = (region, aproj, aborrow_content, aloan_content) g_value
-(** Abstraction values are used inside of abstractions to properly model
+type avalue =
+  | AConcrete of constant_value
+  | AAdt of aadt_value
+  | ABottom
+  | ALoan of aloan_content
+  | ABorrow of aborrow_content
+  | ASymbolic of aproj
+      (** Abstraction values are used inside of abstractions to properly model
     borrowing relations introduced by function calls.
 
     When calling a function, we lose information about the borrow graph:
@@ -214,7 +214,10 @@ type avalue = (region, aproj, aborrow_content, aloan_content) g_value
 *)
 
 (* TODO: rename to adt_avalue? *)
-and aadt_value = (region, aproj, aborrow_content, aloan_content) g_adt_value
+and aadt_value = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_avalue list;
+}
 
 and aloan_content =
   | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
@@ -234,7 +237,9 @@ and aborrow_content =
   | AIgnoredMutBorrow of typed_avalue
   | AIgnoredSharedBorrow of abstract_shared_borrows
 
-and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
+(* TODO: we may want to merge this with typed_value - would prevent some issues
+   when accessing fields... *)
+and typed_avalue = { value : avalue; ty : rty }
 [@@deriving
   show,
     visitors
@@ -244,6 +249,14 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value
         ancestors = [ "iter_typed_avalue_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
+      },
+    visitors
+      {
+        name = "map_typed_avalue";
+        variety = "map";
+        ancestors = [ "map_typed_avalue_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
       }]
 
 type abs = {
@@ -263,6 +276,7 @@ type abs = {
     which are a special kind of value.
 *)
 
+(*
 (** Polymorphic version of the map visitor for [g_typed_value].
 
     The polymorphic visitor generated by the visitors macro caused some
@@ -575,3 +589,4 @@ class ['self] map_typed_avalue =
         : 'env -> abstract_shared_borrows -> aloan_content =
       fun _env asb -> AIgnoredSharedLoan asb
   end
+ *)
diff --git a/tests/trace_reference.txt b/tests/trace_reference.txt
index ee8828da..7023474a 100644
--- a/tests/trace_reference.txt
+++ b/tests/trace_reference.txt
@@ -6980,7 +6980,9 @@ move var@3
   (Values.Adt
      { Values.variant_id = <opaque>;
        field_values =
-       [{ Values.value = (Values.Concrete <opaque>);
+       [{ Values.value =
+          (Values.Concrete
+             (Values.Scalar { Values.value = 0; int_ty = Types.I32 }));
           ty = (Types.Integer Types.I32) }
          ]
        });
@@ -13292,7 +13294,9 @@ true
 move var@4
 
 [Debug] activate_inactivated_mut_borrow: resulting value:
-{ Values.value = (Values.Concrete <opaque>); ty = (Types.Integer Types.I32) }
+{ Values.value =
+  (Values.Concrete (Values.Scalar { Values.value = 0; int_ty = Types.I32 }));
+  ty = (Types.Integer Types.I32) }
 [Debug] end_borrows {}: context before:
 # 1 frame(s)
 
@@ -13379,7 +13383,9 @@ move var@4
 move var@6
 
 [Debug] activate_inactivated_mut_borrow: resulting value:
-{ Values.value = (Values.Concrete <opaque>); ty = (Types.Integer Types.I32) }
+{ Values.value =
+  (Values.Concrete (Values.Scalar { Values.value = 0; int_ty = Types.I32 }));
+  ty = (Types.Integer Types.I32) }
 [Debug] end_borrows {}: context before:
 # 1 frame(s)
 
@@ -16206,12 +16212,16 @@ move var@7
        [{ Values.value =
           (Values.Borrow
              (Values.MutBorrow (<opaque>,
-                { Values.value = (Values.Concrete <opaque>);
+                { Values.value =
+                  (Values.Concrete
+                     (Values.Scalar { Values.value = 0; int_ty = Types.U32 }));
                   ty = (Types.Integer Types.U32) }
                 )));
           ty =
           (Types.Ref (Types.Erased, (Types.Integer Types.U32), Types.Mut)) };
-         { Values.value = (Values.Concrete <opaque>);
+         { Values.value =
+           (Values.Concrete
+              (Values.Scalar { Values.value = 1; int_ty = Types.U32 }));
            ty = (Types.Integer Types.U32) }
          ]
        });