| /-! Check for bug accidentally marking `m` as owned. -/ | |
| 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 in | |
| def isSomeWithInstanceNat (m : { m : Array (MyOption Nat) // 0 < m.size }) : Bool := | |
| (m.1.uget 0 m.2).isSomeWithInstance |