Regression in 2.6.2: primEraseEquality fails to compute (lack of normalization)

[Trebor-Huang]

I'm implementing NbE for STLC. I found out that if I wrap some of my substitution lemmas with primEraseEquality, it blocks the computation of concrete terms when I hit C-c C-n.

How should I start debugging the source of the problem? I have no idea how to produce a MWE. I don't know how to read terms like this:

⟦
 (^ ^ var (𝕤 𝕫) ∙ (var (𝕤 𝕫) ∙ var 𝕫)) ∙
 (^ ^ ^ var (𝕤 𝕤 𝕫) ∙ var 𝕫 ∙ var (𝕤 𝕫))
 ⟧
 (λ v → reflect (var v))
 | ^ ^ var (𝕤 𝕫) ∙ (var (𝕤 𝕫) ∙ var 𝕫)
 | symm (Agda.Builtin.Equality.Erase.primEraseEquality refl)

Does this mean that primEraseEquality blocks even on refl? I'm not sure I understand how it works, but in the docs it says

The function takes a proof of an equality between two values x and y and stays stuck on it until x and y actually become definitionally equal. Whenever that is the case, primEraseEquality e reduces to refl.

But since the normalization result is Agda.Builtin.Equality.Erase.primEraseEquality refl (I enabled --prop --safe flags), shouldn't x and y already be definitionally equal?

My Agda version is v2.6.2.1-af5bfc0, running on OS X.

[andreasabel]

Such terms come from a stuck with-auxiliary function.

[Trebor-Huang]

So it is stuck when rewriting with symm (primEraseEquality refl), right?

[Trebor-Huang]

I tried to print that term with --show-implicit on. It produces a huge term

primEraseEquality {LEVEL} {TYPE}
    {TERM1} {TERM2} refl

Then I copy-pasted these two terms, and let Agda typecheck

_ : TERM1 ≡ TERM2
_ = refl

And it checks as expected. Then why couldn't primEraseEquality compute? I think after printing all the implicit variables, they are definitely definitionally equal.

[gallais]

Are the values equal up to eta or on the nose? Or are they equal up to whnf or just nf?
Because according to the comments in the code primEraseEquality only does whnf
at the moment (no eta, no nf):

agda/src/full/Agda/TypeChecking/Primitive.hs

Lines 555 to 566 in 7028350

	-- Andreas, 2013-07-22.
	-- Note that we cannot call the conversion checker here,
	-- because 'reduce' might be called in a context where
	-- some bound variables do not have a type (just __DUMMY_TYPE__),
	-- and the conversion checker for eliminations does not
	-- like this.
	-- We can only do untyped equality, e.g., by normalisation.
	-- Jesper, 2020-04-04: We reduce rather than normalise for
	-- efficiency reasons. In general this is weaker but it is
	-- equivalent at base types. A stronger version of
	-- primEraseEquality (using type-directed conversion) may be
	-- implemented using --rewriting.

[Trebor-Huang]

They are plain data values. The complete term is too long to paste here I guess. But I also noticed that when I shift some symm or rewrite around some of the blocking primEraseEquality disappears (and others appear :( ). I'll keep trying to minimize it.

[jespercockx]

@Trebor-Huang could you try if you still have the same problem if you use this erasure function instead of primEraseEquality:

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  eraseEquality : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≡ y
  eraseEquality-comp : ∀ {ℓ} {A : Set ℓ} {x : A} {eq : x ≡ x} → eraseEquality eq ≡ refl

{-# REWRITE eraseEquality-comp #-}

This one does use type-directed conversion, while I believe primEraseEquality is only guaranteed to compute on closed first-order terms.

[Trebor-Huang]

Yes, I was going to do that. The problem does go away with the REWRITE version. But I'm still wondering why primEraseEquality did not reduce. I can narrow it down to

^ ^ var (𝕤 𝕫) ∙ (var (𝕤 𝕫) ∙ var 𝕫)

which is a plain lambda term using the well-scoped de Bruijn syntax.

[jespercockx]

Perhaps the reason is that primEraseEquality uses reduce rather than normalise, so it will not normalise constructor arguments.

[UlfNorell]

That seems like a bug, no? Here's a small test case

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Erase

data Wrap : Set where
  wrap : Nat → Wrap

test : wrap (1 + 1) ≡ wrap 2
test = primEraseEquality refl

thm : test ≡ refl
thm = refl   -- Fails: primEraseEquality refl != refl

[andreasabel]

agda-bisect says:
f728537 is the first bad commit (ping @jespercockx)

Date: Sun Apr 5 09:08:54 2020 +0200

[ perf ] Reduce instead of normalise in primEraseEquality

Reasoning: the current implementation is anyway incomplete b/c of eta-equality, so we might as well make it a bit weaker if this avoids a call to normalise. If this breaks anything, a workaround is to use rewrite rules instead.

[andreasabel]

It seems to me that we should revert f728537 because it confuses the users.

However, @jespercockx seems to suggest that the REWRITE version works better. If we go for the REWRITE version, we should place it somewhere canonical and deprecate the old primEraseEquality.
A caveat is of course that then the user needs --rewriting in their project, and this might have repercussions.

[jespercockx]

The way I see it each of them has their own use cases:

• primEraseEquality is used for implementing decidable equality on primitive, non-composite types such as Float and String.
• eraseEquality defined with rewrite rules is used when you actually want an equality that computes to refl whenever it becomes reflexive.

So IMO the only thing that should really change is the documentation which should point users towards the version they need.

[UlfNorell]

non-composite types such as Float and String

Also works for Nat since suc is strict.

[Trebor-Huang]

Is it possible to internally use REWRITE mechanisms to define eraseEquality, but make it exempt from the --rewriting flag? Is that safe? I think since eraseEquality is defined via a postulate it is a conservative extension.

[jespercockx]

The easiest way to do that is just to change the implementation of primEraseEquality to use pureEqualTerm from Agda.TypeChecking.Conversion.Pure, which is the function internally used by --rewriting as well. However, that might make it less efficient than the current implementation for base types Float, String, Nat, ... so I'm not sure if we want to do that.

[Trebor-Huang]

The easiest way to do that is just to change the implementation of primEraseEquality to use pureEqualTerm from Agda.TypeChecking.Conversion.Pure, which is the function internally used by --rewriting as well. However, that might make it less efficient than the current implementation for base types Float, String, Nat, ... so I'm not sure if we want to do that.

Why not keep both versions? This means

• Add a built-in eraseEquality (we can bikeshed a better name later), that act exactly like the version using rewrite pragmas, but without requiring the --rewrite flag;
• Keep the primEraseEquality in place where we need efficiency on the base types;
• Switch to eraseEquality where appropriate in the standard library. (Is there even any place where we should switch?)

[andreasabel]

The discussion has died down. So I went ahead and proposed the easiest fix by reverting the commit that introduced the regression: #5811.