open import Agda.Builtin.Equality

id : {A : Set} → A → A
id x = x

infixr 9 _∘_
_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

test : {A : Set} {f g : A → A}
     → f ∘ f ≡ id → f ∘ f ∘ g ≡ g
test p = cong (_∘ ?) p

results in the following error:

Failed to solve the following constraints:
  ?0 (p = p) (section = id) x = g x : A (blocked on _45)
  ?0 (p = p) (section = (f ∘ f)) x = g x : A (blocked on _45)

where section is the variable in the desugared form cong (λ section → section ∘ ?).

The constraints could be solved if section weren't in scope, which it has no reason to be in my opinion since there's no way I can refer to it.

Feature request: somehow prune the section variable away from metavariables appearing inside operator sections.