[Agda] Absurd pattern; convincing Agda

[Paul van der Walt]

Dear all,

I asked this question on IRC, but it was rather quiet there, so
maybe someone here could help me out.

I am using the Reflection API, and I'd like to manipulate a
value of type Term which is returned by quoteTerm. I have a
function which only works for Terms of the form (something ==
true), and this function should return the LHS if the Term has
this form. To make this function total, I also have a
predicate (validity of input checker) which only returns true
for the cases I want to take care of. See the functions here:
http://hpaste.org/69846 (excuse the formatting)

The problem is, one of the absurd patterns is accepted by Agda,
but remains yellow. This causes problems when trying to use the
module elsewhere. I can clearly see that this case can never be
reached (order of patterns matters here), but Agda doesn't
believe me.

Does anyone know how I can solve this? Maybe my approach is
really ugly?

Thanks in advance, I hope my question is clear enough.

Cheers,
Paul van der Walt
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120612/8aea6959/attachment.bin