[Agda] Type error?? But I'm sure it's well-typed!

[David Leduc]

Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> "sym p" cannot be abstracted in the type of test(').

Is it a problem? If yes, then why the following example is working?

  test2 : (A : Set)(u v : A)(p q : u ≡ v) -> A
  test2 A u v p q with u | p | v | sym p
  test2 A u v p q | ._ | refl | ._ | refl = {!!}

> But there are
> dependencies, because if sym p is refl, p is also refl, and B is A.

Yes, that was in fact the point of my example: I wonder how to deal
with such dependencies. How would you proceed with my test and test'?

> Something that works is matching on p directly:

I knew this works on this small example. Unfortunately if does not
work in my development when instead of "sym p" I have a bigger proof
term with many dependencies.