Fails to find instances for `Decision P` where `P` is point-free
From stdpp Require Import list.
Typeclasses eauto := debug.
(* This works *)
Lemma foo (x : nat) (l : list (nat * nat)) :
filter (λ p, x = fst p) l = l.
Proof. Abort.
(* This doesn't *)
(* ?H : "∀ x0 : nat * ?B, Decision (((λ y : nat, y = x) ∘ fst) x0)" *)
Fail Lemma foo (x : nat) (l : list (nat * nat)) :
filter ((.= x) ∘ fst) l = l.
Goal ∀ {B} (x : nat) (p : nat * B),
Decision (x = fst p).
Proof. apply _. Abort.
Goal ∀ {B} (x : nat) (p : nat * B),
Decision (((.= x) ∘ fst) p).
Proof. Fail apply _.
Based on a report by @swils (in private discussion).