Agda: With applications in generated code

[GoogleCodeExporter]

I have encountered the error message

 Not implemented: type checking of with application

when using rewrite. It seems as if the rewrite machinery generates code with explicit with applications.

Original issue reported on code.google.com by nils.anders.danielsson on 27 Dec 2009 at 4:27

[GoogleCodeExporter]

module Bug where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

data Unit : Set where
  unit : Unit

f : Unit → Unit
f u with u
... | unit = unit

postulate
  eq : ∀ u → f u ≡ unit

foo : Unit → Set₁
foo u rewrite eq u = Set

-- Bug.agda:20,1-25
-- Not implemented: type checking of with application
-- when checking that the expression f u | u has type _35 u

Original comment by nils.anders.danielsson on 2 Jan 2010 at 11:44

• Changed state: Accepted
• Added labels: Priority-High

[GoogleCodeExporter]

Original comment by [email protected] on 4 Jun 2010 at 1:46

• Changed state: Fixed

[fredefox]

Was this bug closed inadvertently?

I just encountered a piece of syntax for with-application presented to me in the Agda minibuffer that I never really thought about before. As an example:

f n | even n

As I understand it, it's the value of f n given the result of even n. f in this case is defined using with-abstractions. However, when I copy this definition into my file (doing an equality proof using EqReasoning) I get the error Not implemented: type checking of with application.

Here is a (somewhat) minimal example:

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Relation.Binary.PropositionalEquality public
open ≡-Reasoning public

not : Bool → Bool
not true = false
not false = true

even : Nat → Bool
even zero = true
even (suc x) = not (even x)

halve : Nat → Nat
halve zero = zero
halve (suc zero) = zero
halve (suc (suc n)) = suc (halve n)

f : Nat → Nat
f n with even n
... | false = 3 * n + 1
... | true  = halve n

postulate ω : {A : Set} → A

collatz : ∀ n → f n ≡ 1
collatz n = begin
  f n                ≡⟨ refl ⟩
  f n | even n       ≡⟨ ω ⟩
  1                  ∎

I'm running Agda version 2.6.0-f8af12d

This is relevant to me in my specific situation because I want to prove f | φ from f | ψ knowing ψ → φ so a nice way to formulate this as a work-around would also be very welcome.

[andreasabel]

No, this bug was fixed by not going through abstract syntax when checking rewrite. The problem was that Agda produced code for itself it wanted to type-check, but failed due to with-applications.

Now, Agda only fails on with-applications that the user tries to write. That is another issue, see #2839. Please discuss the feature request there.