[Agda] aggressive with, VFPiA

[Aaron Stump]

Dear Agda developers,

Starting in Agda version 2.4.2.5, the abstraction performed by "with" 
has (as the CHANGELOG tells us) become more aggressive.  I am sure you 
have good reasons for this change, but are you aware that you have made 
it impossible to rewrite with the same assumption twice?  Consider this 
self-contained example:

module test where

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

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

lemma : ∀ {A : Set}(f : A → A)(a : A) → f a ≡ a → f (f a) ≡ a
lemma f a p rewrite p = p

With previous versions of Agda, this would be fine.  But starting with 
2.4.2.5, this does not type check.  If we put a hole on the right-hand 
side of the sole equation for lemma, we will see this goal:

Goal: f a ≡ a
————————————————————————————————————————————————————————————
p  : a ≡ a

The "rewrite p" directive has actually been applied to rewrite the type 
of p itself, rendering it trivial and hence useless.  This is a real 
problem.  I have maybe 25 places in the Iowa Agda Library that have been 
broken by this.  I don't mind fixing them, but I think this is a major 
flaw in the new way "with" works.  One should be able to reuse 
assumptions.  For the particular example above, I actually am struggling 
to find any workaround.  How would you prove this?  Maybe inspect on 
steroids is supposed to be used?  For what I have done, usually inspect 
has been enough.  But being able to apply an assumption twice with 
rewrite seems pretty fundamental.  This is not linear logic!

There is a second issue I want to raise.  As you know (since Jesper and 
Ulf wrote me very helpful and quite detailed reviews), I am bringing 
out, with ACM Books, a textbook called "Verified Functional Programming 
in Agda" (VFPiA) this year.  The book is in the very last stages of 
proofs.  In the book, I refer readers to Agda 2.4.2.2 and IAL release 1.2:

svn co --username=guest --password=guest 
https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.2

So, certainly the book is usable.  But this release does not check with 
Agda 2.4.2.5.  Furthermore, some of what I say in the book is 
invalidated by the fact that we cannot rewrite twice with the same 
assumption.

Of course, whether the book is successful or not is not your 
responsibility, though by reviewing it for me, Ulf and Jesper have made 
some investment in its success.  But if you want to take advantage of my 
efforts here to help spread Agda to new users, it would be really a good 
idea if releases of Agda were compatible with IAL version 1.2.  I do not 
do anything very exotic.  If there are changes to compiler pragmas, that 
is fine.  And of course, I hardly expect you to limit yourself to back 
compatibility with my library. But if you could at least consider 
whether changes you make are breaking this library (and hence, to some 
extent, breaking VFPiA), I would appreciate it, and I hope it would help 
the broader Agda community.

Best wishes,
Aaron