Type-class search fails for `∀ [foo], bar`

class foo (n : ℕ) : Prop :=
(has_true : true)

class bar (n : ℕ) : Prop :=
(has_true : true)

@[reducible] def quux := ∀ n [foo n], bar n

lemma have_quux : quux := by intros n h; constructor; constructor

example [quux] : quux := by apply_instance
example [∀ n [foo n], bar n] : quux := by apply_instance
example [∀ n [foo n], bar n] : ∀ n [foo n], bar n := by apply_instance
example [∀ n [foo n], bar n] (n) [foo n] : bar n := by apply_instance
example [quux] (n) [foo n] : bar n := by apply_instance

I'm not sure if we should/can fix this in general because it conflicts with the frozen instances policy. Although in this case here it could be solved via unification.

Start by running the supplied Lean reproducer and examining the type-class search behavior for the quantified instance forms. The issue raises a possible unification-based fix but also a conflict with the frozen instances policy, so first establish the intended policy and scope with maintainers. Done means an agreed behavior is implemented and the examples have appropriate regression coverage.