deterministic timeout with structures

Stream: lean4

[Uranus Testing]

On local computer I have “version 4.0.0-nightly-2022-06-29, commit 98b8e300e1ab” installed, where it takes around 30 seconds to typecheck these lines. On CI (where always used latest build) it falls down with an error (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached. And after update on local machine Lean produces timeout too.
I don’t have some particular MWE, but similar issues also happen here and here.
In first and seconds examples timeout happens while trying to typecheck some structures. Third examples indirectly uses other big structures (ring, field, dedekind) too, so it’s probably somehow related.
I have noticed earlier that structures in Lean 4 are typically slower in typechecking than it was in Lean 3, because I had a similar problem fixed by replacing typeclasses with nested sigma’s.

[Leonardo de Moura]

Could you please create #mwe(s) for these issues? It would help us a lot.

[Uranus Testing]

So I finally created MWE.
I also noticed that problem disappears (but in this case typechecking takes around 30 seconds too; this is probably longer than it was in Lean 3, but I am not sure) if we replace zeroeqv with axiom zeroeqv {A : Type u} (H : hset A) : 0-Type (or somehow avoid using it). Anyway, there were no such problems in Lean 3.

[Leonardo de Moura]

Thanks for creating the #mwe.
The performance issue is due to the new "eta for structures" feature. https://github.com/leanprover/lean4/issues/777
On my machine, the def dual declaration takes 11 secs to elaborate. When I disable the "eta for structures", it takes around 0.2 secs.
I will keep investigating.

[Leonardo de Moura]

It also explains the discrepancy with respect to Lean 3. Lean 3 does not implement definitional eta for structures.

[Leonardo de Moura]

Pushed a fix for this performance issue. Now, def dual in the #mwe above takes 0.1 sec to be elaborated on my machine.