You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 37deftest : IO Unit := do
pure ()
for i in #[0] do
for j in #[0] doif i != 1 && i != 2then
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.
Prerequisites
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,
will give out
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
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.
The text was updated successfully, but these errors were encountered: