experiment

test it

fix tests

src/Init/GetElem.lean

@@ -404,7 +404,7 @@ instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
     simp only [getElem?, decidableGetElem?]
     split <;> rfl
   getElem!_def xs i := by
-    simp only [getElem!, getElem?, decidableGetElem?, get!Internal, getD, getElem]
+    simp only [getElem!, getElem?, decidableGetElem?, get!Internal, getElem]
     split <;> rfl
 
 @[simp] theorem getInternal_eq_getElem (a : Array α) (i : Nat) (h) :
@@ -412,8 +412,8 @@ instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
 
 @[simp] theorem get!Internal_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) :
     a.get!Internal i = a[i]! := by
-  simp only [get!Internal, getD, getInternal_eq_getElem, getElem!_def]
-  split <;> simp_all [getElem?_pos, getElem?_neg]
+  simp only [get!Internal, getInternal_eq_getElem, getElem!_def]
+  split <;> simp_all [getElem?_pos, getElem?_neg, panic, panicCore]
 
 end Array
 

src/Init/Prelude.lean

@@ -3255,23 +3255,6 @@ Examples:
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
   dite (LT.lt i a.size) (fun h => a.getInternal i h) (fun _ => v₀)
 
-/--
-Version of `Array.get!Internal` that does not increment the reference count of its result.
-
-This is only intended for direct use by the compiler.
--/
-@[extern "lean_array_get_borrowed"]
-unsafe opaque Array.get!InternalBorrowed {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α
-
-/--
-Use the indexing notation `a[i]!` instead.
-
-Access an element from an array, or panic if the index is out of bounds.
--/
-@[extern "lean_array_get"]
-def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-  Array.getD a i default
-
 /--
 Adds an element to the end of an array. The resulting array's size is one greater than the input
 array. If there are no other references to the array, then it is modified in-place.
@@ -3648,8 +3631,8 @@ will prevent the actual monad from being "copied" to the code being specialized.
 When we reimplement the specializer, we may consider copying `inst` if it also
 occurs outside binders or if it is an instance.
 -/
-@[never_extract, extern "lean_panic_fn"]
-def panicCore {α : Sort u} [Inhabited α] (msg : String) : α := default
+@[never_extract, extern "lean_panic_fn_borrowed"]
+def panicCore {α : Sort u} [@&Inhabited α] (msg : String) : α := default
 
 /--
 `(panic "msg" : α)` has a built-in implementation which prints `msg` to
@@ -3666,6 +3649,24 @@ elimination and other optimizations that assume that the expression is pure.
 def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
   panicCore msg
 
+/--
+Version of `Array.get!Internal` that does not increment the reference count of its result.
+
+This is only intended for direct use by the compiler.
+-/
+@[extern "lean_array_get_borrowed"]
+unsafe opaque Array.get!InternalBorrowed {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α
+
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
+--@[extern "lean_array_get"]
+@[inline]
+def Array.get!Internal {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+  dite (LT.lt i a.size) (fun h => a.getInternal i h) (fun _ => (panic "bad bad"))
+
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -342,6 +342,11 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .unbox var _ => mkApp (.const `unbox []) (.fvar var)
   | .isShared fvarId _ => mkApp (.const `isShared []) (.fvar fvarId)
 
+def LetValue.isPersistent (val : LetValue .impure) : Bool :=
+  match val with
+  | .fap _ xs => xs.isEmpty -- all global constants are persistent
+  | _ => false
+
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
   binderName : Name

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -235,11 +235,6 @@ def withParams (ps : Array (Param .impure)) (x : RcM α) : RcM α := do
       { ctx with idx := ctx.idx + 1, varMap }
   withReader update x
 
-def LetValue.isPersistent (val : LetValue .impure) : Bool :=
-  match val with
-  | .fap _ xs => xs.isEmpty -- all global constants are persistent
-  | _ => false
-
 @[inline]
 def withLetDecl (decl : LetDecl .impure) (x : RcM α) : RcM α := do
   let update := fun ctx =>

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -389,6 +389,10 @@ where
     | .fap ``Array.uget args =>
       if let .fvar parent := args[1]! then
         if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
+    | .fap f #[] =>
+      -- We do not need to own `z` as `f` is persistent and thus stays alive at least until the end
+      -- of execution.
+      return ()
     | .fap f args =>
       let ps ← getParamInfo (.decl f)
       ownFVar z (.functionCallResult z)

src/include/lean/lean.h

@@ -319,6 +319,7 @@ LEAN_EXPORT void lean_set_panic_messages(bool flag);
 
 LEAN_EXPORT void lean_panic(char const * msg, bool force_stderr);
 LEAN_EXPORT lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
+LEAN_EXPORT lean_object * lean_panic_fn_borrowed(b_lean_obj_arg default_val, lean_object * msg);
 
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
@@ -847,11 +848,10 @@ static inline lean_obj_res lean_array_fget_borrowed(b_lean_obj_arg a, b_lean_obj
 
 LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
 
-static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
-            lean_dec(def_val);
             return lean_array_uget(a, idx);
         }
     }
@@ -859,14 +859,14 @@ static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
+    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }
 
-static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get_borrowed(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
-            lean_dec(def_val);
             return lean_array_get_core(a, idx);
         }
     }
@@ -874,6 +874,7 @@ static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
+    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }
 

src/runtime/object.cpp

@@ -196,6 +196,11 @@ extern "C" LEAN_EXPORT object * lean_panic_fn(object * default_val, object * msg
     return default_val;
 }
 
+extern "C" LEAN_EXPORT object * lean_panic_fn_borrowed(b_obj_arg default_val, object * msg) {
+    lean_inc(default_val);
+    return lean_panic_fn(default_val, msg);
+}
+
 extern "C" LEAN_EXPORT object * lean_sorry(uint8) {
     lean_internal_panic("executed 'sorry'");
     lean_unreachable();

src/runtime/object.h

@@ -194,7 +194,7 @@ inline object * mk_empty_array() { return lean_mk_empty_array(); }
 inline object * mk_empty_array(b_obj_arg capacity) { return lean_mk_empty_array_with_capacity(capacity); }
 inline object * array_uget(b_obj_arg a, usize i) { return lean_array_uget(a, i); }
 inline obj_res array_fget(b_obj_arg a, b_obj_arg i) { return lean_array_fget(a, i); }
-inline object * array_get(obj_arg def_val, b_obj_arg a, b_obj_arg i) { return lean_array_get(def_val, a, i); }
+inline object * array_get(b_obj_arg def_val, b_obj_arg a, b_obj_arg i) { return lean_array_get(def_val, a, i); }
 inline obj_res copy_array(obj_arg a, bool expand = false) { return lean_copy_expand_array(a, expand); }
 inline object * array_uset(obj_arg a, usize i, obj_arg v) { return lean_array_uset(a, i, v); }
 inline object * array_fset(obj_arg a, b_obj_arg i, obj_arg v) { return lean_array_fset(a, i, v); }