timeout at 'whnf' in forallTelescope

Stream: lean4

[Floris van Doorn]

I get the following error when running forallTelescope.

uncaught exception: (deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

I am a bit confused about this, I thought that forallTelescope doesn't reduce the expression at all, as opposed to forallTelescopeReducing.

I can reproduce this when I run forallTelescope on all declarations of mathlib3port (current commit - 9b3a383). Here is my code:

import Lean

open Lean Meta Core
-- you need to clone and `lake build` mathlib3port in the right directory to run this
def main (strs : List String) : IO UInt32 := do
  let env ← do
    initSearchPath (← Lean.findSysroot?) ["../mathlib3port/build/lib",
      "../mathlib3port/lean_packages/lean3port/build/lib/",
      "../mathlib3port/lean_packages/mathlib/build/lib/"]
    importModules [{module := `Mathbin}] {}
  let _ ← CoreM.toIO (MetaM.run' do
    let decls ← (← getEnv).constants.map₁.toArray.map (·.1)
    decls.forM λ nm => if !nm.isInternal then do
      let info ← getConstInfo nm
      let isprop ← forallTelescope info.type $ λ _ e => e.isProp
      IO.println s!"{nm}: {isprop}"
    else return ()
    ) {} {env := env}
  return 0

Note: when I replace forallTelescope by a structural recursion on the expression, I don't get an error.

import Lean

open Lean Meta Core

namespace Lean.Expr

def piCodomain : Expr → Expr
| forallE n t b d => piCodomain b
| e => e

end Lean.Expr


def main (strs : List String) : IO UInt32 := do
  let env ← do
    initSearchPath (← Lean.findSysroot?) ["../mathlib3port/build/lib",
      "../mathlib3port/lean_packages/lean3port/build/lib/",
      "../mathlib3port/lean_packages/mathlib/build/lib/"]
    importModules [{module := `Mathbin}] {}
  let _ ← CoreM.toIO (MetaM.run' do
    let decls ← (← getEnv).constants.map₁.toArray.map (·.1)
    decls.forM λ nm => if !nm.isInternal then do
      let info ← getConstInfo nm
      let isprop ← info.type.piCodomain.isProp
      IO.println s!"{nm}: {isprop}"
    else return ()
    ) {} {env := env}
  return 0

Is this the expected behavior (for complicated enough expressions)?

[Sebastian Ullrich]

forallTelescope may need to reduce domains to check for type classes. Which should be cheap, but it might accumulate.

[Sebastian Ullrich]

The heartbeat limit is mostly for interactive use, you can set it to some higher number (or 0) in the CoreM.toIO call

[Floris van Doorn]

Thanks! Both of those options indeed solve the problem.
I didn't know that the number of heartbeats was for the whole CoreM.toIO call instead of each whnf call individually.

[Sebastian Ullrich]

I believe it's because whnf is regarded as a helper function to be used in larger modules that define a "heartbeat scope". For example TC resolution is a scope.