[Agda] Wildcards

[Guillaume Brunerie]

Hi,
I have the following code


module Test where

infix 4 _≡_

data _≡_ {A : Set} : A → A → Set where
  refl : (a : A) → a ≡ a

infix 5 _∘_

_∘_ : {A : Set} {x y z : A} (p : x ≡ y) (q : y ≡ z) → x ≡ z
refl _ ∘ q = q

assoc : {A : Set} {x y z t : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ t)
  → (p ∘ q) ∘ r ≡ p ∘ (q ∘ r)
assoc (refl _) _ _ = refl _

big-assoc : {A : Set} {x y z t u : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡
t) (s : t ≡ u)
  → (p ∘ q) ∘ (r ∘ s) ≡ p ∘ (q ∘ (r ∘ s))
big-assoc p q r s = assoc _ _ _


This does not compile because of unsolved metas at the last line, but
it works if I replace [assoc _ _ _] by [assoc p _ _].
Why can't agda guess that the arguments of [assoc] are necessarily
[p], [q] and [r ∘ s] ?
My impression is that if you try to unify the types of [assoc] and
[big-assoc], you automatically find the three arguments of [assoc], so
I do not understand why the wildcards are not sufficient.
(of course this is a simplified example, I have this problem in proofs
where the arguments of [assoc] are much more complicated, and where it
would be really nice if I could omit them)

Thanks !


Guillaume