[Agda] Absurd pattern; convincing Agda

Andreas Abel andreas.abel at ifi.lmu.de
Tue Jun 12 16:54:56 CEST 2012

Hi Paul,

this is how to convince Agda.  Just split one level deeper:

   withoutEQ (def f (x ∷ [])) () | no ¬p
   withoutEQ (def f (x ∷ x₁ ∷ xs)) () | no ¬p

Now the unsolved meta is gone.

The problem was that the equations given for a match do not always hold 
literally.  In you case, this equation does not reduce:

   outerIsEq (def f (x ∷ xs)) | no ¬p = false

This is because internally, Agda decided it wants to split on xs before 
reducing.  I'd consider this unwanted behavior on the side of Agda. See:


In a simple case, consider the equations

   and : Bool -> Bool -> Bool
   and false x = false
   and y false = false
   and _ _     = true

One of

   and false x
   and y false

will not reduce to false, since Agda converts this definition into a 
case tree, so it will either match on the first (likely) or the second 
argument.  So you will likely get the equations

   and false x    = false
   and true false = false
   and true true  = true

and the type

   and y false == false

will not be empty.

Why in your specific case you do not get the equations you specified, I 
cannot tell.

Hope that helps.


On 12.06.2012 14:36, Paul van der Walt wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list