Zulip Chat Archive

Stream: lean4

Topic: Misleading error message when approaching recursive limit

Schrodinger ZHU Yifan (Oct 26 2023 at 19:51):

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 ()

Reports

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

Schrodinger ZHU Yifan (Oct 26 2023 at 23:56):

I updated the example to a more minimal case. Sorry for providing a long one before. Should I open an issue for it?

Scott Morrison (Oct 27 2023 at 00:02):

Yes please. But please include also what you expect to see!

Shreyas Srinivas (Oct 27 2023 at 00:15):

Scott Morrison said:

Yes please. But please include also what you expect to see!

I think @Schrodinger ZHU Yifan means that there are no type errors thrown when maxRecDepth is set to 38 or higher instead. So maybe the expected error message is running out of maxHeartBeats error message that some typeclass instance problems throw.

Schrodinger ZHU Yifan (Oct 27 2023 at 00:16):

Yes, there should be no error. If maxRecDepth affects the type checking result, it should report errors related to limit.

Schrodinger ZHU Yifan (Oct 27 2023 at 00:17):

image.png

limit-related error does exist if you set it to 36. However, for certain cases (say 37), it only reports strange type errors.

Schrodinger ZHU Yifan (Oct 27 2023 at 00:18):

image.png

Shreyas Srinivas (Oct 27 2023 at 00:18):

You still get the type error for 36 though

Schrodinger ZHU Yifan (Oct 27 2023 at 00:19):

Shreyas Srinivas said:

You still get the type error for 36 though

indeed.

Shreyas Srinivas (Oct 27 2023 at 00:19):

For 38 there are suddenly no type errors

Shreyas Srinivas (Oct 27 2023 at 00:19):

Best guess: the elaborator just spit out the term as is when it ran out of heartbeats and if then else gets treated as the ite for Prop. Some edge case behaviour.

Shreyas Srinivas (Oct 27 2023 at 00:21):

I think we can find out what the elaborator was doing in that last step by turning on the trace. I'll quickly look up the docs for the correct option

Shreyas Srinivas (Oct 27 2023 at 00:26):

Better guess: This coe was the last step and somehow the term was sent on for typechecking w/o this step.

LeanProject.lean:8:9

[Elab.coe] adding coercion for i != 1 && j != 2 : Bool =?= Prop

Schrodinger ZHU Yifan (Oct 27 2023 at 00:29):

Issue: https://github.com/leanprover/lean4/issues/2775

Shreyas Srinivas (Oct 27 2023 at 00:32):

I don't feel confident declaring it a bug before an expert chimes in, even though it looks like one.

Eric Wieser (Oct 27 2023 at 00:33):

Wow, nice job finding a bug that appears at exactly 37!

Schrodinger ZHU Yifan (Oct 27 2023 at 00:37):

While such "error" can be "by design", the error message can be improved at least.

Shreyas Srinivas (Oct 27 2023 at 00:38):

Agreed. I think this is some weird edge case. I just can't find a way for trace.elab.step.result to print the heartbeat count

Shreyas Srinivas (Oct 27 2023 at 00:39):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC