[Agda] Absurd question

[Martin Escardo]

I have a problem with absurdity in Agda, which I can solve in an 
undesirable way, which forces me to change several definitions.

I would like to both understand what the problem is, and why the 
desirable way doesn't work.

I have three types X,Y,Z, whose definition I omit here. I can define, 
using absurd patterns,

x : X
x = \a ()

y : Y
y : \()

z : Z
z : \()

These are types which have a parameter n:N that happens to be zero and 
so they trivialize in this special case, as they have occurrences of Fin 
n in their definitions.

Now I have three holes in a definition (of a fourth type), reported to 
have types X,Y,Z. I can fill the holes with x,y,z, and the definition 
type-checks.

But if I instead fill the holes with \a (), \(), and \(), expanding the 
definitions of x,y,z, then type-checking fails.

Moreover, if just one of the three holes is filled with the 
corresponding term, type checking still fails.

Additionally, if I ask the emacs interface to fill the wholes with 
ctrl-c-a, this succeeds, with expressions containing the string 
"absurd". But then the resulting expression doesn't type check.

And there is a more annoying fact. I have previous definition of 
something else that uses \() and does type check. However, when I use 
it, things fail. I instead need to use the same definition with replaced 
\() by y.

This is very mysterious to me.

I didn't manage to distil a simple instance of this to reproduce here. 
But if you are brave enough, you can search for "AGDA PROBLEM" in any of 
the two following links:

http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html
http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.lagda

Help is appreciated.

Martin