[Agda] implicit argument equality weirdness

[Noam Zeilberger]

Consider two code snippets, which only differ by (a : A) vs {a : A},
i.e. explicit vs implicit arguments:
-------
module Test1  (A B : Set) where

  data fnAB : Set where
    lam : ((a : A) -> B) -> fnAB

  data R : fnAB -> fnAB -> Set where
    r : {f g : (a : A) -> B} -> A -> R (lam f) (lam g)

  invert : {f g : (a : A) -> B} -> R (lam f) (lam g) -> A
  invert (r a) = a
-------
module Test2  (A B : Set) where

  data fnAB : Set where
    lam : ({a : A} -> B) -> fnAB

  data R : fnAB -> fnAB -> Set where
    r : {f g : {a : A} -> B} -> A -> R (lam f) (lam g)

  invert : {f g : {a : A} -> B} -> R (lam f) (lam g) -> A
  invert (r a) = a
-------
The idea here is we define a datatype fnAB representing functions
from A to B, and some sort of relation on fnAB.  In reality this
would be some interesting relation (like, say, extensional
equality), but here I've just defined a silly relation R, which
relates any pair of fnAB's if A is inhabited.  The last part is
that we want to invert a proof that the relation holds, to get back
what we put in (which in this case is just an element of A).

The only difference between Test1 and Test2 is that the former sets
fnAB to be the explicit function space (a : A) -> B, while the latter
sets it to be the implicit function space {a : A} -> B.  But Test1
typechecks, while Test2 fails with error

  f' != f of type B
  when checking that the pattern r a has type
  R (lam (\{.a} -> f)) (lam (\{.a} -> g))

Is this a bug?

Noam