Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In the condition clause of a nested if branch, if the checker is approaching maxRecLimit, it will give out certain error messages that may not be related to the recursion limit.

For example,

set_option maxRecDepth 37
def test : IO Unit := do
  pure ()
  for i in #[0] do
    for j in #[0] do
      if i != 1 && i != 2 then
        pure ()

will give out

application type mismatch
  @ite ?m.412 (i != 1 && i != 2)
argument
  i != 1 && i != 2
has type
  Bool : Type
but is expected to have type
  Prop : Type

For a lower limit (say 36), such type error exists but the checker also reports about the limit problem.
For a higher limit (say 38), the error suddenly disappears.

Context

zulip

Steps to Reproduce

Compile the code above.

Expected behavior: Give no error or report an error about maxRecLimit.

Actual behavior: Give a "strange" type-error.

Versions

Lean (version 4.3.0-nightly-2023-10-13, commit 42802f9788a8, Release)
Darwin XXXX.XXXX 23.1.0 Darwin Kernel Version 23.1.0: Tue Sep 26 22:11:17 PDT 2023; root:xnu-10002.40.89.501.1~3/RELEASE_ARM64_T8103 arm64

Additional Information

n/a

Impact

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