[Agda] What is the type of the diagonal function?

[Jacques Carette]

The naive version of diagonal, i.e.
diag x = x , x
has the 'obvious' type. But this is rather unsatisfactory because it 
loses all dependency information. So one idea is to use

data <_> {a : Level} {A : Set a} (x : A) : Set a where
     singleton : (y : A) → y ≡ x -> < x >

and then do
diag x = x , singleton x refl
so that diag now has a very precise type [and good computational 
properties]. But this is not quite satisfactory either.

Has anyone looked into creating a "diagonal" function with a precise 
type? Eventually, I want to be able to pattern-match on this, to enforce 
that my 'input' can only be such a dependent pair. [Actually, it gets a 
little trickier still, but this is the first interesting stumbling block].

Jacques