decidable_pred instance not found by typeclass search

Stream: new members

[Eric Wieser]

With set_option trace.class_instance, the failing example gives

[class_instances] (0) ?x_0 a : decidable ((λ (x : perm (α ⊕ β)), x ∈ (sum_congr_hom α β).range) a) := @monoid_hom.monoid_hom.decidable_mem_range (?x_21 a) (?x_22 a) (?x_23 a) (?x_24 a) (?x_25 a) (?x_26 a) (?x_27 a)
  (?x_28 a)
failed is_def_eq

but I don't really know how to understand or get more information about that error

[Eric Wieser]

Perhaps the more telling case is:

-- fails
example (α β : Type*)
  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] : decidable_pred (λ x, x ∈ (sum_congr_hom α β).range) :=
infer_instance

-- ok
example (α β : Type*)
  [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] : decidable_pred (λ x, x ∈ (sum_congr_hom α β).range) :=
λ x, infer_instance

I thought infer_instance was able to resolve binders?