Stack overflow in `refine'`

[eric-wieser]

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

The following code crashes the lean server:

example : False := by
  refine' absurd (congrArg (·.1) sorry) _

Context

Zulip thread

Steps to Reproduce

1. Run the code above

Expected behavior: Lean server doesn't crash, some error is probably emitted on the tactic

Actual behavior: Lean server does crash

Versions

v4.8.0rc1

Impact

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

[eric-wieser]

The cause seems to be infinite recursion in instantiateExprMVars, which cannot call withIncRecDepth because:

• It is not in the right monad
• withIncRecDepth is defined in a later file