[Agda] agda error message

[Martin Escardo]

Hi guys,

I get the following message:

    n != n of type ℕ
    when checking that the expression x has type X n

I could try to show you the code, but maybe you have seen something like 
this and know what it means. A previous declaration does declare x to 
have type X n, and if I postulate the offending definition, no error is 
reported (in particular, the previously occurring x is accepted to have 
type X n).

A bit of background: before I got a message that f (g n) != n.
Then I proved that f (g n) = n, and applied the proof to the 
corresponding code, using the following to get from X(f (g n)) to the 
required X n.

coersion : {I : Set} {X : I → Set} → {i j : I} → i ≡ j → X i → X j
coersion refl x = x

But now agda is not happy with the complain n != n instead.

Any ideas? The code is too big to send in a discussion message, but I 
could try to isolate the error. I have used "coersion" successfully in 
another part of the code to achieve the same effect.

Thanks.
Martin