what does `[always_inline]` mean?

Stream: lean4

[Asei Inoue]

See the following code:

@[inline]
def Bool.And₁ : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

-- short circuiting!!
/-- info: false -/
#guard_msgs in
  #eval Bool.And₁ false (dbg_trace "hello"; true)

@[always_inline]
def Bool.And₂ : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

-- **not** short circuiting!!
/--
info: hello
---
info: false
-/
#guard_msgs in
  #eval Bool.And₂ false (dbg_trace "hello"; true)

When using the [inline] attribute, short-circuit evaluation is possible, but when using [always_inline], short-circuit evaluation is not possible. I do not understand the reason for this phenomenon. What does [always_inline] mean?

[Asei Inoue]

At first I thought [always_inline] would tell it to always expand inline, while [inline] would tell it to only expand inline when it expected to improve performance. However, that interpretation is inconsistent with the code example above.

[Ruben Van de Velde]

How about with@[inline, always_inline]?

[Asei Inoue]

not short-circuit

@[inline, always_inline]
def Bool.And₃ : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

/--
info: hello
---
info: false
-/
#guard_msgs in
  #eval Bool.And₃ false (dbg_trace "hello"; true)

[Henrik Böving]

For short circuiting you want to use macro_inline

[Asei Inoue]

@Henrik Böving

I know [macro_inline] exists, but why should I use [macro_inline] for short-circuit evaluation?
How do [macro_inline], [inline] and [always_inline] differ from each other?

[Henrik Böving]

macro_inline treats the function like a macro and bubbles the evaluation of arguments down to their first use sites while inline/always_inline might not do that

[Henrik Böving]

you can inspect the generated IR with set_option trace.compiler.ir.result true and observe when arguments get evaluated relative to the pattern matching there

[Markus Himmel]

Ruben Van de Velde said:

How about with@[inline, always_inline]?

I think you need to use the order @[always_inline, inline] to get the desired effect.

[Asei Inoue]

@Henrik Böving I see. Thanks.

Then why is it short-circuited even when [inline] is used?

[Henrik Böving]

I think in the inline situation the compiler merely happens to optimize it in the way that you intended it to be but that is not generally guaranteed

[Asei Inoue]

Thanks.
Are there any examples of short-circuit evaluation failure if using [inline]?