[Agda] Pattern matching weirdness?

[Pierre Hyvernat]

Hello...

I started using Agda again after a while away from it, and I just 
encountered a strange thing. After defining dependent sums with a data:

   data ∑ (X : Set) (Y : X → Set) : Set where
     <_,_> : (x : X) → Y x → ∑ X Y
   π1 : {X : Set} -> {Y : X -> Set} -> (∑ X Y) -> X
   π1 < x , _ > = x
   π2 : {X : Set} -> {Y : X -> Set} -> (p : ∑ X Y) -> Y (π1 p)
   π2 < _ , y > = y

I had a definition by pattern matching
   F < a , b > = ... something involving a and b ...


After a little while, I had a problem which was solved by replacing my 
definition with
   F ab = ... something involving (π1 ab) and (π2 ab) ...

Is that a feature, or a bug?
Are there some subtle issues with surjectivity of constructors?


Pierre
-- 
For every complex problem, there is a solution that is
simple, neat, and wrong.
    -- H. L. Mencken