Missing inferred borrow annotation related to arrays

[TwoFX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

In the code snippet

class MyClass (α : Type u) where

instance : MyClass Nat where

inductive MyOption (α : Type u) where
  | none
  | some (key : α)

namespace MyOption

def isSomeWithInstance [MyClass α] : MyOption α → Bool
  | none => false
  | some _ => true

def isSome : MyOption α → Bool
  | none => false
  | some _ => true

end MyOption

set_option trace.compiler.ir.result true

def isSomeWithInstanceGen [MyClass α] (m : { m : Array (MyOption α) // 0 < m.size }) : Bool :=
  (m.1.uget 0 m.2).isSomeWithInstance

def isSomeWithInstanceNat (m : { m : Array (MyOption Nat) // 0 < m.size }) : Bool :=
  (m.1.uget 0 m.2).isSomeWithInstance

def isSomeWithInstanceNatEx (m : Array (MyOption Nat)) (h : 0 < m.size) : Bool :=
  (m.uget 0 h).isSomeWithInstance

def isSomeWithInstanceGenL [MyClass α] (m : { m : List (MyOption α) // 0 < m.length }) : Bool :=
  m.1.get ⟨0, m.2⟩ |>.isSomeWithInstance

def isSomeWithInstanceNatL (m : { m : List (MyOption Nat) // 0 < m.length }) : Bool :=
  m.1.get ⟨0, m.2⟩ |>.isSomeWithInstance

def isSomeWithInstanceNatExL (m : List (MyOption Nat)) (h : 0 < m.length) : Bool :=
  m.get ⟨0, h⟩ |>.isSomeWithInstance

def isSomeGen (m : { m : Array (MyOption α) // 0 < m.size }) : Bool :=
  (m.1.uget 0 m.2).isSome

def isSomeNat (m : {m : Array (MyOption Nat) // 0 < m.size }) : Bool :=
  (m.1.uget 0 m.2).isSome

def isSomeNatEx (m : Array (MyOption Nat)) (h : 0 < m.size) : Bool :=
  (m.uget 0 h).isSome

I would expect all nine definitions to borrow the array/list, but only eight of them do so. The odd one out is isSomeWithInstanceNat (the second one). If MyClass is changed to live in Prop, then all nine borrow the array/list.

Context

This bug affects Lean.HashMap.contains (and presumably all other read operations, but I haven't checked this in detail), leading to unnecessary reference counting operations on every hashmap access. Note that the issue only becomes visible when looking at specialized IR for the operation. The IR generated for the polymorphic versions of the functions is fine.

Steps to Reproduce

1. Run the above code and check the traced IR for borrow annotations

Expected behavior: The array/list is always borrowed

Actual behavior: The array is not borrowed in isSomeWithInstanceNat.

Versions

4.9.0-nightly-2024-05-21 on live.lean-lang.org

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.