Problematic timeout in decidable instance

Stream: lean4

[Ioannis Konstantoulas]

I have the following structure:

#eval Lean.versionString -- "4.3.0-nightly-2023-10-05"
abbrev ValidRName (candidate : String) : Prop :=
  0 < candidate.length
  ∧ candidate.length < 100
  ∧ Char.isAlpha candidate.front
  ∧ candidate.all Char.isAlphanum

instance : Decidable (ValidRName candidate) := by
  apply instDecidableAnd

structure RName where
  name  : String
  valid : ValidRName name
deriving Repr, DecidableEq, Hashable

instance : Inhabited RName where
  default := {name := "def", valid := by decide }

If I change the default.name string to "defa", "defau", "defaul" consecutively, I observe a rapid (exponential?) increase in the decision time. Using name := "defaultName" incurs a max heartbeat timeout.

This should not be happening, I think; the ValidRName predicate is simple and the four assertions should be checking out rapidly. Any ideas?

[Sebastian Ullrich]

Fixed in lean4#2612