diff --git a/backend/cn/lib/cLogicalFuns.ml b/backend/cn/lib/cLogicalFuns.ml
index 6ff498065..a97eac804 100644
--- a/backend/cn/lib/cLogicalFuns.ml
+++ b/backend/cn/lib/cLogicalFuns.ml
@@ -738,7 +738,7 @@ let add_logical_funs_from_c call_funinfo funs_to_convert funs =
         let@ fbody =
           match Pmap.lookup c_fun_sym funs with
           | Some fbody -> return fbody
-          | None -> fail_n { loc; msg = Unknown_function c_fun_sym }
+          | None -> fail_n { loc; msg = Global (Unknown_function c_fun_sym) }
         in
         let@ it = c_fun_to_it loc global_context l_fun_sym c_fun_sym def fbody in
         Pp.debug
diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
index 4be62926c..8fdb6ffd1 100644
--- a/backend/cn/lib/check.ml
+++ b/backend/cn/lib/check.ml
@@ -2611,7 +2611,7 @@ let record_and_check_datatypes datatypes =
     datatypes
 
 
-(** Note: this does not check loop invariants and CN statements! *)
+(** NOTE: not clear if this checks loop invariants and CN statements! *)
 let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   Cerb_debug.begin_csv_timing ();
   (* decl, lemmata, function specification checking *)
diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml
index 76ddb603b..26b45c570 100644
--- a/backend/cn/lib/compile.ml
+++ b/backend/cn/lib/compile.ml
@@ -424,7 +424,7 @@ module EffectfulTranslation = struct
   let lookup_struct loc tag env =
     match lookup_struct_opt tag env with
     | Some def -> return def
-    | None -> fail { loc; msg = Unknown_struct tag }
+    | None -> fail { loc; msg = Global (Unknown_struct tag) }
 
 
   let lookup_member loc (_tag, def) member =
@@ -437,13 +437,13 @@ module EffectfulTranslation = struct
   let lookup_datatype loc sym env =
     match Sym.Map.find_opt sym env.datatypes with
     | Some info -> return info
-    | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype sym }
+    | None -> fail { loc; msg = Global (Unknown_datatype sym) }
 
 
   let lookup_constr loc sym env =
     match Sym.Map.find_opt sym env.datatype_constrs with
     | Some info -> return info
-    | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype_constr sym }
+    | None -> fail { loc; msg = Global (Unknown_datatype_constr sym) }
 
 
   let cannot_tell_pointee_ctype loc e =
@@ -852,7 +852,9 @@ module EffectfulTranslation = struct
              | Some fsig -> return fsig.return_bty
              | None ->
                fail
-                 { loc; msg = Unknown_logical_function { id = fsym; resource = false } }
+                 { loc;
+                   msg = Global (Unknown_logical_function { id = fsym; resource = false })
+                 }
            in
            return (apply_ fsym args (BaseTypes.Surface.inj bt) loc))
       | CNExpr_cons (c_nm, exprs) ->
@@ -1070,7 +1072,10 @@ module EffectfulTranslation = struct
         let@ pred_sig =
           match lookup_predicate pred env with
           | None ->
-            fail { loc; msg = Unknown_resource_predicate { id = pred; logical = false } }
+            fail
+              { loc;
+                msg = Global (Unknown_resource_predicate { id = pred; logical = false })
+              }
           | Some pred_sig -> return pred_sig
         in
         let output_bt = pred_sig.pred_output in
diff --git a/backend/cn/lib/global.ml b/backend/cn/lib/global.ml
index 85975a877..386f217b6 100644
--- a/backend/cn/lib/global.ml
+++ b/backend/cn/lib/global.ml
@@ -44,63 +44,89 @@ let sym_map_from_bindings xs =
   List.fold_left (fun m (nm, x) -> Sym.Map.add nm x m) Sym.Map.empty xs
 
 
-module type Reader = sig
-  type global = t
-
+type error =
+  | Unknown_function of Sym.t
+  | Unknown_struct of Sym.t
+  | Unknown_datatype of Sym.t
+  | Unknown_datatype_constr of Sym.t
+  | Unknown_resource_predicate of
+      { id : Sym.t;
+        logical : bool
+      }
+  | Unknown_logical_function of
+      { id : Sym.t;
+        resource : bool
+      }
+  | Unknown_lemma of Sym.t
+
+type global_t_alias_do_not_use = t
+
+module type ErrorReader = sig
   type 'a t
 
   val return : 'a -> 'a t
 
   val bind : 'a t -> ('a -> 'b t) -> 'b t
 
-  type state
-
-  val get : unit -> state t
+  val get_global : unit -> global_t_alias_do_not_use t
 
-  val to_global : state -> global
+  val fail : Locations.t -> error -> 'a t
 end
 
 module type Lifted = sig
   type 'a t
 
-  val get_resource_predicate_def : Sym.t -> Definition.Predicate.t option t
+  val get_resource_predicate_def : Locations.t -> Sym.t -> Definition.Predicate.t t
 
-  val get_logical_function_def : Sym.t -> Definition.Function.t option t
+  val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.t t
 
   val get_fun_decl
-    :  Sym.t ->
-    (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) option t
+    :  Locations.t ->
+    Sym.t ->
+    (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) t
 
-  val get_lemma : Sym.t -> (Cerb_location.t * AT.lemmat) option t
+  val get_lemma : Locations.t -> Sym.t -> (Cerb_location.t * AT.lemmat) t
 
-  val get_struct_decl : Sym.t -> Memory.struct_layout option t
+  val get_struct_decl : Locations.t -> Sym.t -> Memory.struct_layout t
 
-  val get_datatype : Sym.t -> BaseTypes.dt_info option t
+  val get_datatype : Locations.t -> Sym.t -> BaseTypes.dt_info t
 
-  val get_datatype_constr : Sym.t -> BaseTypes.constr_info option t
+  val get_datatype_constr : Locations.t -> Sym.t -> BaseTypes.constr_info t
 end
 
-module Lift (M : Reader) : Lifted with type 'a t := 'a M.t = struct
-  let lift f sym =
+module Lift (M : ErrorReader) : Lifted with type 'a t := 'a M.t = struct
+  let lift f loc sym msg =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let global = M.to_global state in
-    M.return (f global sym)
+    let@ global = M.get_global () in
+    match f global sym with Some x -> M.return x | None -> M.fail loc (msg global)
+
+
+  let get_logical_function_def_opt id = get_logical_function_def id
+
+  let get_logical_function_def loc id =
+    lift get_logical_function_def loc id (fun global ->
+      let res = get_resource_predicate_def global id in
+      Unknown_logical_function { id; resource = Option.is_some res })
+
 
+  let get_resource_predicate_def loc id =
+    lift get_resource_predicate_def loc id (fun global ->
+      let log = get_logical_function_def_opt global id in
+      Unknown_resource_predicate { id; logical = Option.is_some log })
 
-  let get_resource_predicate_def = lift get_resource_predicate_def
 
-  let get_logical_function_def = lift get_logical_function_def
+  let get_fun_decl loc fsym = lift get_fun_decl loc fsym (fun _ -> Unknown_function fsym)
 
-  let get_fun_decl = lift get_fun_decl
+  let get_lemma loc lsym = lift get_lemma loc lsym (fun _ -> Unknown_lemma lsym)
 
-  let get_lemma = lift get_lemma
+  let get_struct_decl loc tag = lift get_struct_decl loc tag (fun _ -> Unknown_struct tag)
 
-  let get_struct_decl = lift get_struct_decl
+  let get_datatype loc tag =
+    lift get_datatype loc tag (fun _ -> Unknown_datatype_constr tag)
 
-  let get_datatype = lift get_datatype
 
-  let get_datatype_constr = lift get_datatype_constr
+  let get_datatype_constr loc tag =
+    lift get_datatype_constr loc tag (fun _ -> Unknown_datatype_constr tag)
 end
 
 let pp_struct_layout (tag, layout) =
diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml
index bcaac62f2..e423b25a0 100644
--- a/backend/cn/lib/typeErrors.ml
+++ b/backend/cn/lib/typeErrors.ml
@@ -112,21 +112,9 @@ module RequestChain = struct
 end
 
 type message =
-  | Unknown_variable of Sym.t
-  | Unknown_function of Sym.t
-  | Unknown_struct of Sym.t
-  | Unknown_datatype of Sym.t
-  | Unknown_datatype_constr of Sym.t
-  | Unknown_resource_predicate of
-      { id : Sym.t;
-        logical : bool
-      }
-  | Unknown_logical_function of
-      { id : Sym.t;
-        resource : bool
-      }
+  | Global of Global.error
   | Unexpected_member of Id.t list * Id.t
-  | Unknown_lemma of Sym.t
+  | Unknown_variable of Sym.t
   (* some from Kayvan's compilePredicates module *)
   | First_iarg_missing
   | First_iarg_not_pointer of
@@ -272,19 +260,19 @@ let pp_message te =
   | Unknown_variable s ->
     let short = !^"Unknown variable" ^^^ squotes (Sym.pp s) in
     { short; descr = None; state = None }
-  | Unknown_function sym ->
+  | Global (Unknown_function sym) ->
     let short = !^"Unknown function" ^^^ squotes (Sym.pp sym) in
     { short; descr = None; state = None }
-  | Unknown_struct tag ->
+  | Global (Unknown_struct tag) ->
     let short = !^"Struct" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_datatype tag ->
+  | Global (Unknown_datatype tag) ->
     let short = !^"Datatype" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_datatype_constr tag ->
+  | Global (Unknown_datatype_constr tag) ->
     let short = !^"Datatype constructor" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_resource_predicate { id; logical } ->
+  | Global (Unknown_resource_predicate { id; logical }) ->
     let short = !^"Unknown resource predicate" ^^^ squotes (Sym.pp id) in
     let descr =
       if logical then
@@ -293,7 +281,7 @@ let pp_message te =
         None
     in
     { short; descr; state = None }
-  | Unknown_logical_function { id; resource } ->
+  | Global (Unknown_logical_function { id; resource }) ->
     let short = !^"Unknown logical function" ^^^ squotes (Sym.pp id) in
     let descr =
       if resource then
@@ -302,13 +290,13 @@ let pp_message te =
         None
     in
     { short; descr; state = None }
+  | Global (Unknown_lemma sym) ->
+    let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in
+    { short; descr = None; state = None }
   | Unexpected_member (expected, member) ->
     let short = !^"Unexpected member" ^^^ Id.pp member in
     let descr = !^"the struct only has members" ^^^ list Id.pp expected in
     { short; descr = Some descr; state = None }
-  | Unknown_lemma sym ->
-    let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in
-    { short; descr = None; state = None }
   | First_iarg_missing ->
     let short = !^"Missing pointer input argument" in
     let descr = !^"a predicate definition must have at least one input argument" in
diff --git a/backend/cn/lib/typeErrors.mli b/backend/cn/lib/typeErrors.mli
index a5c1b9a3e..ae3f2fc64 100644
--- a/backend/cn/lib/typeErrors.mli
+++ b/backend/cn/lib/typeErrors.mli
@@ -50,21 +50,9 @@ module RequestChain : sig
 end
 
 type message =
-  | Unknown_variable of Sym.t
-  | Unknown_function of Sym.t
-  | Unknown_struct of Sym.t
-  | Unknown_datatype of Sym.t
-  | Unknown_datatype_constr of Sym.t
-  | Unknown_resource_predicate of
-      { id : Sym.t;
-        logical : bool
-      }
-  | Unknown_logical_function of
-      { id : Sym.t;
-        resource : bool
-      }
+  | Global of Global.error
   | Unexpected_member of Id.t list * Id.t
-  | Unknown_lemma of Sym.t
+  | Unknown_variable of Sym.t
   | First_iarg_missing
   | First_iarg_not_pointer of
       { pname : Request.name;
diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml
index a0334fa9c..9019a3777 100644
--- a/backend/cn/lib/typing.ml
+++ b/backend/cn/lib/typing.ml
@@ -210,15 +210,17 @@ module ErrorReader = struct
 
   let bind = bind
 
-  type state = s
+  let get_global () =
+    let@ s = get () in
+    return s.typing_context.global
 
-  type global = Global.t
 
-  let get = get
+  let fail loc msg = fail (fun _ -> { loc; msg = Global msg })
 
-  let to_global (s : s) = s.typing_context.global
+  let get_context () =
+    let@ s = get () in
+    return s.typing_context
 
-  let to_context (s : s) = s.typing_context
 
   let lift = lift
 end
@@ -230,63 +232,12 @@ module Global = struct
 
   let is_fun_decl global id = Option.is_some @@ Global.get_fun_decl global id
 
-  let get_logical_function_def_opt id = get_logical_function_def id
-
-  let error_if_none opt loc msg =
-    let@ opt in
-    Option.fold
-      opt
-      ~some:return
-      ~none:
-        (let@ msg in
-         fail (fun _ -> { loc; msg }))
-
-
-  let get_logical_function_def loc id =
-    error_if_none
-      (get_logical_function_def id)
-      loc
-      (let@ res = get_resource_predicate_def id in
-       return (TypeErrors.Unknown_logical_function { id; resource = Option.is_some res }))
-
-
-  let get_struct_decl loc tag =
-    error_if_none (get_struct_decl tag) loc (return (TypeErrors.Unknown_struct tag))
-
-
-  let get_datatype loc tag =
-    error_if_none (get_datatype tag) loc (return (TypeErrors.Unknown_datatype tag))
-
-
-  let get_datatype_constr loc tag =
-    error_if_none
-      (get_datatype_constr tag)
-      loc
-      (return (TypeErrors.Unknown_datatype_constr tag))
-
-
   let get_struct_member_type loc tag member =
     let@ decl = get_struct_decl loc tag in
     let@ ty = get_member_type loc member decl in
     return ty
 
 
-  let get_fun_decl loc fsym =
-    error_if_none (get_fun_decl fsym) loc (return (TypeErrors.Unknown_function fsym))
-
-
-  let get_lemma loc lsym =
-    error_if_none (get_lemma lsym) loc (return (TypeErrors.Unknown_lemma lsym))
-
-
-  let get_resource_predicate_def loc id =
-    error_if_none
-      (get_resource_predicate_def id)
-      loc
-      (let@ log = get_logical_function_def_opt id in
-       return (TypeErrors.Unknown_resource_predicate { id; logical = Option.is_some log }))
-
-
   let get_fun_decls () =
     let@ global = get_global () in
     return (Sym.Map.bindings global.fun_decls)
diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml
index 14222bec2..bd6ef4246 100644
--- a/backend/cn/lib/wellTyped.ml
+++ b/backend/cn/lib/wellTyped.ml
@@ -18,33 +18,38 @@ module GlobalReader = struct
 
   let bind x f s = match x s with Ok (y, s') -> f y s' | Error err -> Error err
 
-  let get () s = Ok (s, s)
+  let get_global () s = Ok (s.Context.global, s)
 
-  let to_global ctxt = ctxt.Context.global
-
-  type global = Global.t
-
-  type state = Context.t
+  let fail loc msg _ = Error TypeErrors.{ loc; msg = Global msg }
 end
 
 module NoSolver = struct
   include GlobalReader
   include Global.Lift (GlobalReader)
 
-  type failure = TypeErrors.t
+  let fail err : 'a t = fun _ -> Error err
 
-  let liftFail typeErr = typeErr
+  let ( let@ ) = bind
+
+  let get_member_type loc member layout : Sctypes.t t =
+    let member_types = Memory.member_types layout in
+    match List.assoc_opt Id.equal member member_types with
+    | Some membertyp -> return membertyp
+    | None -> fail { loc; msg = Unexpected_member (List.map fst member_types, member) }
+
+
+  let get_struct_member_type loc tag member =
+    let@ decl = get_struct_decl loc tag in
+    let@ ty = get_member_type loc member decl in
+    return ty
 
-  let pure x s = match x s with Ok (y, _) -> Ok (y, s) | Error err -> Error err
 
-  let fail (typeErr : failure) : 'a t = fun _ -> Error (liftFail typeErr)
+  let pure x s = match x s with Ok (y, _) -> Ok (y, s) | Error err -> Error err
 
   let update f s = Ok ((), f s)
 
   let lookup f : _ t = fun s -> Ok (f s, s)
 
-  let ( let@ ) = bind
-
   let bound_a sym = lookup (Context.bound_a sym)
 
   let bound_l sym = lookup (Context.bound_l sym)
@@ -64,70 +69,6 @@ module NoSolver = struct
       fail { loc; msg = Mismatch { has = BT.pp has; expect = BT.pp expect } }
 
 
-  let error_if_none opt loc msg =
-    let@ opt in
-    Option.fold
-      opt
-      ~some:return
-      ~none:
-        (let@ msg in
-         fail { loc; msg })
-
-
-  let get_logical_function_def_opt id = get_logical_function_def id
-
-  let get_logical_function_def loc id =
-    error_if_none
-      (get_logical_function_def id)
-      loc
-      (let@ res = get_resource_predicate_def id in
-       return (TypeErrors.Unknown_logical_function { id; resource = Option.is_some res }))
-
-
-  let get_struct_decl loc tag =
-    error_if_none (get_struct_decl tag) loc (return (TypeErrors.Unknown_struct tag))
-
-
-  let get_datatype loc tag =
-    error_if_none (get_datatype tag) loc (return (TypeErrors.Unknown_datatype tag))
-
-
-  let get_datatype_constr loc tag =
-    error_if_none
-      (get_datatype_constr tag)
-      loc
-      (return (TypeErrors.Unknown_datatype_constr tag))
-
-
-  let get_member_type loc member layout : Sctypes.t t =
-    let member_types = Memory.member_types layout in
-    match List.assoc_opt Id.equal member member_types with
-    | Some membertyp -> return membertyp
-    | None -> fail { loc; msg = Unexpected_member (List.map fst member_types, member) }
-
-
-  let get_struct_member_type loc tag member =
-    let@ decl = get_struct_decl loc tag in
-    let@ ty = get_member_type loc member decl in
-    return ty
-
-
-  let get_fun_decl loc fsym =
-    error_if_none (get_fun_decl fsym) loc (return (TypeErrors.Unknown_function fsym))
-
-
-  let get_lemma loc lsym =
-    error_if_none (get_lemma lsym) loc (return (TypeErrors.Unknown_lemma lsym))
-
-
-  let get_resource_predicate_def loc id =
-    error_if_none
-      (get_resource_predicate_def id)
-      loc
-      (let@ log = get_logical_function_def_opt id in
-       return (TypeErrors.Unknown_resource_predicate { id; logical = Option.is_some log }))
-
-
   let lift = function Ok x -> return x | Error x -> fail x
 
   let run ctxt x = x ctxt
@@ -137,8 +78,6 @@ let use_ity = ref true
 
 open NoSolver
 
-let fail typeErr = fail (liftFail typeErr)
-
 open Effectful.Make (NoSolver)
 
 let illtyped_index_term (loc : Locations.t) it has ~expected ~reason =
@@ -2523,11 +2462,7 @@ module type ErrorReader = sig
 
   val bind : 'a t -> ('a -> 'b t) -> 'b t
 
-  type state
-
-  val get : unit -> state t
-
-  val to_context : state -> Context.t
+  val get_context : unit -> Context.t t
 
   val lift : 'a Or_TypeError.t -> 'a t
 end
@@ -2535,22 +2470,19 @@ end
 module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = struct
   let lift1 f x =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let context = M.to_context state in
+    let@ context = M.get_context () in
     M.lift (Result.map fst (run context (f x)))
 
 
   let lift2 f x y =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let context = M.to_context state in
+    let@ context = M.get_context () in
     M.lift (Result.map fst (f x y context))
 
 
   let lift3 f x y z =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let context = M.to_context state in
+    let@ context = M.get_context () in
     M.lift (Result.map fst (f x y z context))
 
 
@@ -2594,8 +2526,7 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru
 
   let ensure_same_argument_number loc type_ n ~expect =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let context = M.to_context state in
+    let@ context = M.get_context () in
     M.lift (Result.map fst (ensure_same_argument_number loc type_ n ~expect context))
 
 
diff --git a/backend/cn/lib/wellTyped.mli b/backend/cn/lib/wellTyped.mli
index 762140161..22296b75e 100644
--- a/backend/cn/lib/wellTyped.mli
+++ b/backend/cn/lib/wellTyped.mli
@@ -9,11 +9,7 @@ module type ErrorReader = sig
 
   val bind : 'a t -> ('a -> 'b t) -> 'b t
 
-  type state
-
-  val get : unit -> state t
-
-  val to_context : state -> Context.t
+  val get_context : unit -> Context.t t
 
   val lift : 'a Or_TypeError.t -> 'a t
 end
diff --git a/tests/cn/tree16/as_mutual_dt/tree16.c.verify b/tests/cn/tree16/as_mutual_dt/tree16.c.verify
index 20653f7a8..37b1eeaf0 100644
--- a/tests/cn/tree16/as_mutual_dt/tree16.c.verify
+++ b/tests/cn/tree16/as_mutual_dt/tree16.c.verify
@@ -8,8 +8,8 @@ tests/cn/tree16/as_mutual_dt/tree16.c:111:19: warning: 'each' expects a 'u64', b
 tests/cn/tree16/as_mutual_dt/tree16.c:121:18: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "backend/cn/lib/compile.ml", line 1571, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&i1' with type 'i32' was provided. This will become an error in the future.
+other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&i1' with type 'i32' was provided. This will become an error in the future.
 
-other location (File "backend/cn/lib/compile.ml", line 1571, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future.
+other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future.
 
 [1/1]: lookup_rec -- pass
diff --git a/tests/cn/tree16/as_partial_map/tree16.c.verify b/tests/cn/tree16/as_partial_map/tree16.c.verify
index 01ac506e8..0132fc840 100644
--- a/tests/cn/tree16/as_partial_map/tree16.c.verify
+++ b/tests/cn/tree16/as_partial_map/tree16.c.verify
@@ -14,9 +14,9 @@ tests/cn/tree16/as_partial_map/tree16.c:137:19: warning: 'each' expects a 'u64',
 tests/cn/tree16/as_partial_map/tree16.c:146:18: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "backend/cn/lib/compile.ml", line 1571, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&i2' with type 'i32' was provided. This will become an error in the future.
+other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&i2' with type 'i32' was provided. This will become an error in the future.
 
-other location (File "backend/cn/lib/compile.ml", line 1571, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future.
+other location (File "backend/cn/lib/compile.ml", line 1576, characters 38-45)  warning: 'extract' expects a 'u64', but 'read_&idx0' with type 'i32' was provided. This will become an error in the future.
 
 [1/2]: cn_get_num_nodes -- pass
 [2/2]: lookup_rec -- pass