Unfortunate type inference failure

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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 following piece of code:

def foo : Option Nat := sorry

def test (expire : Option Nat) : IO Unit := do
  let (expiresAt, notify) ←
    if let some dur := expire then
      let notify := foo |>.map (· > dur) |>.getD true
      pure (some dur, notify)
    else
      pure (none, false)

we get:

type mismatch, result value has type
  Option (?m.449 x✝) × Bool : Type
but is expected to have type
  Option Nat × Prop : Type

as Lean has determined notify to be Prop because it did not insert a coercion in the |>.map (· > dur) function but instead coerced true from getD to be a Prop.
It would be great if our type inference engine could handle a situation like this properly.

Context

This was minimized from a piece of code while writing mini-redis

Expected behavior: Should typecheck as is

Actual behavior: Doesn't typecheck :(

Versions

Lean 4.21.0-nightly-2025-05-21
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the minimal reproducer in the issue and confirm the mismatch on the specified Lean nightly release, without Mathlib or Batteries. Investigate Lean's type inference and coercion handling around Option.map and getD; done means the snippet typechecks as written without producing the Option Nat × Prop mismatch.