Troubleshooting

This page is intended to have short snippets of common errors in Agda code, and how to fix these.

Termination checking and nested with

The function isSorted takes a list and maybe produces a witness that list is sorted.

  isSorted : (xs : List ℕ) → Option (Sorted xs)
  isSorted (x ∷ x' ∷ xs) with isLt x x'
  isSorted (x ∷ x' ∷ xs) | None = None
  isSorted (x ∷ x' ∷ xs) | Some a   with isSorted (x' ∷ xs)
  isSorted (x ∷ x' ∷ xs) | Some a        | None = None
  isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted)
  isSorted (x ∷ []) = Some singleton
  isSorted [] = Some empty

Agdas termination checker can't see that this termination check. The reason is how the with construct is desugared, it will internally create an auxiliary function and call this.

  isSorted (x ∷ x' ∷ xs) = isSorted-aux x x' xs (isLt x x')

This auxiliary function will itself create one more (since we have a nested with) this time we have:

  isSorted' x x' xs (Some a) = isSorted'' x x' xs a (isSorted (x' ∷ xs))

This call is not structurally smaller and Agdas termination checker complains. The solution is to make the recursive call earlier.

  isSorted : (xs : List ℕ) → Option (Sorted xs)
  isSorted (x ∷ x' ∷ xs) with isLt x x'  | isSorted (x' ∷ xs)
  isSorted (x ∷ x' ∷ xs) | None          | _    = None
  isSorted (x ∷ x' ∷ xs) | Some xSmaller | None = None
  isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted)
  isSorted (x ∷ []) = Some singleton
  isSorted [] = Some empty