deterministic timeout

Stream: lean4

[Kyle Miller]

Typechecking this function produces two error messages after a delay:

def foo (a : Float := 0.0) (b : Float := 1.0) : Float := a - b
/-
failed to synthesize
  HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
-/

If you remove the default value for either argument typechecking succeeds. I tried this on a nightly from a few days ago and the latest one.

[Kyle Miller]

I have a workaround for now:

def foo (a : Float := 0.0) (b : Float := 1.0) : Float := 0.0 + a - b

[Leonardo de Moura]

Thanks for reporting the issue. The optParam definition is affecting the type class resolution procedure.

[Leonardo de Moura]

I will try to fix it.

[Leonardo de Moura]

Pushed a fix for this
https://github.com/leanprover/lean4/commit/34dc2572f36b35fce217d8d729167256175b3b08

[Kyle Miller]

Is there an application to having the type of a be optParam Float 0.0 rather than Float in the body of the function?

[Leonardo de Moura]

Yes, it can, and I considered this option, but it would not fully solve the issue since one can write stuff such as

def foo (a : Float := 0.0) (b : Float := 1.0) (h : a - b > 0) : Float := ...

[Kyle Miller]

Could there be a general interface for letting something alter the binding domains when they're added to the local environment? For example, stripping optParam or other user annotations.

[Leonardo de Moura]

@Kyle Miller We currently do not have this kind of interface. So, one would have to redefine the elaboration functions for fun, let, etc. to modify the types before they are inserted into the local context.
However, it is not hard to add this kind of user-defined handler. It may be useful, but it would not solve the issue above. The information in the local context is used to create the lambda and forall terms that are sent to the kernel.