[Agda] Error in pattern matching dependent family

[Pierre Hyvernat]

Hello...

I've run into a new (for me) error while working with equality:
Agda complains that

 "I'm not sure if there should be a case for the constructor ..."

Here is a minimal file illustrating my problem:

===== 8< =====
module test where

-- the same happens with the builtin equality
data _==_ {A : Set} (a : A) : A → Set where
  IDP : a == a

test : (X : Set) (x y : X) → (f : X → X) → (f x == f y) → (f y == f x)
test X x y f IDP = IDP

-- test : (X : Set) (x : X) → (f : X → X) → (f x == x) → (x == f x)
-- test X x f IDP = IDP

==============

The whole error message is
   I'm not sure if there should be a case for the constructor IDP,
   because I get stuck when trying to solve the following unification
   problems (inferred index ≟ expected index):
     f x ≟ f y
   when checking that the pattern IDP has type f x == f y

I know I can prove this by generalizing and proving symmetry of _==_, or 
by defining and using the J eliminator for _==_.
But is possible to do that directly with pattern matching? The error 
message isn't very helpful.

In my case, the output type (here "f y == f x") is quite big, and there 
are many more arguments with many dependencies. Generalizing is 
something I'd like to avoid...


If that matters, in my case, it actually happens when trying to write a 
definition like

    test f x with previous-function (f x)
    test f x | refl = ...


Pierre
-- 
Gravity is a myth, the Earth sucks.