typeclass inference crashes

[kim-em]

Description

This was a problem minimized and reported by @digama0 in April on Zulip, but it didn't make it here.

Steps to Reproduce

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 inst1 [f : HasFoo α] : GoodFoo α (noncanonical f).foo := sorry
instance inst2 : HasFoo Nat := sorry
instance inst3 : BetterFoo Nat HasFoo.foo := sorry
instance inst4 : GoodFoo Nat HasFoo.foo := inferInstance

Expected behavior:

One would expect that inst3`` results in successful typeclass search at inferInstanceininst4. If we comment out inst1`, which ought to be irrelevant, then this actually happens.

Actual behavior:

inferInstance fails with

typeclass instance problem is stuck, it is often due to metavariables
  GoodFoo Nat HasFoo.foo

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:

[Meta.synthInstance] 💥 GoodFoo Nat HasFoo.foo ▼
  [] new goal GoodFoo Nat HasFoo.foo ▼
  [instances] #[@BetterFoo.toGoodFoo, @inst1] 
  [] 💥 apply @inst1 to GoodFoo Nat HasFoo.foo ▼
  [tryResolve] 💥 GoodFoo Nat HasFoo.foo ≟ GoodFoo ?m.175 HasFoo.foo 

Versions

Still present at 4.11.0-rc2

Impact

This affects some typeclasses currently in Batteries about Ord instances, which we may want to adopt if available.

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

[Kha]

The relevant question is why inst1 crashed. It looks like it couldn't prove nor disprove whether it is applicable:

  [isDefEq] 💥 GoodFoo Nat HasFoo.foo =?= GoodFoo ?m.206 HasFoo.foo ▼
  [] ✅ Nat =?= ?m.206 ▶
  [] 💥 HasFoo.foo =?= HasFoo.foo ▼
  [] ✅ Nat =?= Nat 
  [] 💥 inst2 =?= noncanonical ?m.207 ▼
  [] 💥 sorryAx (HasFoo Nat) =?= { foo := fun a => HasFoo.foo a && true } ▼
  [] ✅ HasFoo Nat =?= HasFoo Nat 
  [] 💥 HasFoo.foo =?= fun a => HasFoo.foo a && true ▼
  [] 💥 fun a => HasFoo.foo a && true =?= fun a => HasFoo.foo a ▼
  [] ✅ Nat =?= Nat 
  [] 💥 HasFoo.foo a && true =?= HasFoo.foo a ▼
  [] 💥 match HasFoo.foo a with
    | false => false
    | true => true =?= HasFoo.foo a ▼
  [] 💥 match HasFoo.foo a with
    | false => false
    | true => true =?= (sorryAx (HasFoo Nat)).1 a ▼
  [] ❌ and.match_1 =?= (sorryAx (HasFoo Nat)).1 ▶
  [onFailure] 💥 match HasFoo.foo a with
    | false => false
    | true => true =?= (sorryAx (HasFoo Nat)).1 a 

[Kha]

Note that seal noncanonical fixes the issue

[Kha]

Absent further clarification on what the issue is supposed to be, I think we'll have to close this as nonactionable.