[Agda] parasitic arguments in equality proofs

[Sergei Meshveliani]

Dear Agda team,

The below function test proves the equality of kind A = A + 0
by applying the function
+0p : \forall x -> x + 0p =p x

and by the symmetry law =p-sym (a certain instance of Setoid.sym):

test : (mon +m fTail) =p ((mon +m fTail) +p 0p)
test =
=p-sym {(mon +m fTail) +p 0p} {mon +m fTail}
(+0p (mon +m fTail))

The type checker insists on providing the two hidden arguments, and
generally, this feature complicates proofs greatly.
I wonder: why cannot it fill, say, the second hidden argument in

=p-sym {(mon +m fTail) +p 0p} {_} (+0p (mon +m fTail))
?

The signatures of `test' and =p-sym show that first it is proved the
equality
((mon +m fTail) +p 0p) =p (mon +m fTail) -- (I)

and then =p-sym is applied to equality (I).
Therefore the hidden argument values for =p-sym are uniquely defined.

I do not know, may be the argument values are found by a certain
unification of type expressions, which is not enough to find the above
hidden value. But can something simple be added in order to solve hidden
arguments like this?
Because the method looks evident in this example.

Can anybody explain (in simple words) what is the problem with this?

Regards,

------
Sergei