diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index 5315bfc548..f1f089fb46 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -196,7 +196,7 @@ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit := xs.size.forM fun i _ => do let x := xs[i] let p := ps[i]! - unless p.borrow do ownArg x + unless p.borrow || p.ty.isScalar do ownArg x /-- For each xs[i], if xs[i] is owned, then mark ps[i] as owned. We use this action to preserve tail calls. That is, if we have