Default instances are not subject to the instance synthesis depth limit

Description

When working on examples for the reference manual, I noticed some interesting behavior.

Given this definition:

structure Even where
  half : Nat

these (silly, inefficient, but instructive) instances allow literals up to 254 on the latest nightly:

instance ofNatEven0 : OfNat Even 0 where
  ofNat := ⟨0⟩

instance ofNatEvenPlusTwo [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := ⟨(OfNat.ofNat n : Even).half + 1⟩

That is, these work:

#eval (0 : Even)
#eval (34 : Even)
#eval (254 : Even)

but this doesn't:

#eval (256 : Even)

But adding them as default instances changes things!

attribute [default_instance 100] ofNatEven0
attribute [default_instance 100] ofNatEvenPlusTwo

This now works, giving type Even:

#eval 500

Making that number bigger makes elaboration slower, and heartbeats run out at 892.

Steps to Reproduce

Use the code above (available here)
Note that much larger, slower instance synthesis tasks are attempted after the default_instance attribute is added.

Expected behavior:

I would expect the same size/depth limits on default instances that there are on other instances.

Actual behavior:

Much larger/deeper synthesis is performed when the instances involved are default.

Versions

The behavior is visible on all three Lean versions on live.lean-lang.org: nightly-2024-10-31, v4.13.0-rc4, and 4.11.0.

This is on live.lean-lang.org.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4