Typeclass inference crashes

Stream: lean4

[Mario Carneiro]

Minimized:

class HasFoo (α : Type u) where foo : α → Bool
class GoodFoo (α) (foo : α → Bool) : Prop
class BetterFoo (α) (foo : α → Bool) extends GoodFoo α foo

def noncanonical (f : HasFoo α) : HasFoo α where foo a := f.foo a && true
instance [f : HasFoo α] : GoodFoo α (noncanonical f).foo := sorry

instance : HasFoo Nat := sorry
instance : BetterFoo Nat HasFoo.foo := sorry
instance : GoodFoo Nat HasFoo.foo := inferInstance

Commenting out the first instance makes the last line work. Tracing instance synthesis reveals that the inference process crashes when processing the first instance, meaning that the rest of the instance search is not tried and this very easy instance search problem fails. The expected behavior is that the first instance is ignored because it doesn't match.

[Matthew Ballard]

Yeah this was the problem in #mathlib4 > Odd behaviour with inferring instances.

[Kim Morrison]

Do you want to open an issue to track this?

[Kim Morrison]

I've reported this at lean#5032.