[Agda] Influencing pattern matching order [Was: Absurd pattern; convincing Agda]

[Dominique Devriese]

Paul,

The problem is indeed in the order of pattern matching in the
outerIsEq function.
When you write

  outerIsEq : (t : Term) → Bool
  outerIsEq (var x args) = false
  outerIsEq (con c args) = false
  outerIsEq (def f args) with Data.Nat._≟_ (length args) 4
  outerIsEq (def f [])                                         | yes ()
  outerIsEq (def f (x ∷ []))                                   | yes
()                        (1)
  outerIsEq (def f (x ∷ x₁ ∷ x₂ ∷ []))                         | yes
()                         (2)
  ...
  outerIsEq (def f [])                                         | no ¬p = false
  outerIsEq (def f (x ∷ xs))                                   | no ¬p = false

Agda's internal compiled version of outerIsEq will first pattern match
on args and only after that on the result of "Data.Nat._≟_ (length
args) 4". This means that it will only look at the result of the
latter after it has been able to decide between all alternatives for
args.

In your pattern that does not typecheck,

  withoutEQ (def f (x ∷ xs)) () | no ¬p -- unsolved meta - why??

the type of the absurd pattern is "outerIsEq (def f (x ∷ xs)) | no
¬p". This does not reduce to "false = true", because Agda cannot
decide between all the patterns for args, since it only knows that
args = x ∷ xs, with xs unknown, which does not allow differentiating
between for example the patterns on lines marked (1) and (2) above.

Note: this means that your problem is not specific to the absurd pattern,
the problem is in the reduction behaviour of the type of the absurd
pattern, which would also lead to problems in similar situations without
an absurd pattern.

One solution that I have used before is the following. You can
influence the order of the pattern matches that Agda will compile your
outerIsEq function to by adding fake "with" pattern matches on known
values:

  outerIsEq (def f args) with Data.Nat._≟_ (length args) 4
  outerIsEq (def f args) | yes p with tt
  outerIsEq (def f [])                                         | yes () | tt
  outerIsEq (def f (x ∷ []))                                   | yes () | tt
  outerIsEq (def f (x ∷ x₁ ∷ []))                              | yes () | tt
  ...
  outerIsEq (def f args)                                         | no ¬p with tt
  outerIsEq (def f [])                                         | no ¬p
| tt = false
  outerIsEq (def f (x ∷ xs))                                   | no ¬p
| tt = false

This forces Agda to first pattern match on the result of "Data.Nat._≟_
(length args) 4" before it matches on args. Your absurd pattern then
compiles fine.
  withoutEQ (def f []) () | no ¬p
  withoutEQ (def f (x ∷ xs)) () | no ¬p

Note: there may be better solutions to this problem, and I'd be interested
to know about them.

Kind regards,
Dominique

2012/6/12 Paul van der Walt <paul at denknerd.org>:
> 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
>