Regression in 2.6.4.2 concerning `with`

[mechvel]

Regression in 2.6.4.2 concerning `with`

[andreasabel]

It not, may be I would try to simplify the example, (which is a very complex code, using many modules).

Thanks for the report.

Yes, a self-contained example would enable us to start investigating this.

[mechvel]

Here is a small self-contained test. It is type-checked by Agda-2.6.4.1 but not by 2.6.4.2.
The details are given in my initial message.
Test.agda.zip

[andreasabel]

Thanks and congrats, you found a regression in the just-released version of Agda!
A bit unfortunately, 2.6.4.2-rc1 could still handle this example, so a last-minute merge caused this.

In your example, with abstraction of any? lmOrdPair? (zip fs' fs) does not fire any more.
I am afraid changes to normalization in the following PR are the probable cause:

• #7122

CC: @jespercockx

[andreasabel]

Here is a shrinking not needing the standard library:

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Sigma

data ⊥ : Set where

data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : (A → ⊥) → Dec A

zipWith : ∀{A B C : Set} → (A → B → C) → List A → List B → List C
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
zipWith f _        _        = []

zip : ∀{A B : Set} → List A → List B → List (Σ A λ _ → B)
zip = zipWith (_,_)

Mon    = Σ Nat λ _ → Nat
Pol    = List Mon
PolPol = Σ Pol λ _ → Pol

postulate
  ANY   : ∀ {A : Set} → A
  _<lm_ : (f g : Pol) → Set
  _<lm?_ : ∀ x y → Dec (x <lm y)
  Any    : ∀{A : Set} → (A → Set) → List A → Set

LmOrdPair : PolPol → Set
LmOrdPair (f , g) =  f <lm g

lmOrdPair? : ∀ p → Dec (LmOrdPair p)
lmOrdPair? (f , g) =  f <lm? g

any? : ∀{A}{P : A → Set} → (∀ x → Dec (P x)) → ∀ xs → Dec (Any P xs)
any? P? []          = no ANY
any? P? (x ∷ xs)
    with P? x | any? P? xs
... | yes p | _     = yes ANY
... | no ¬p | yes q = yes ANY
... | no ¬p | no ¬q = no  ANY

{-# TERMINATING #-}
aux-I :  List Pol → List Pol → List Pol
aux-I fs' fs
    with any? lmOrdPair? (zip fs' fs)
... | no _  =  fs
... | yes _ =  aux-I fs' fs'

aux-I-base : ∀ fs' fs → aux-I fs' fs ≡ fs
aux-I-base fs' fs
    with any? lmOrdPair? (zip fs' fs)
... | yes anyOrd = ANY
... | no _       = refl

[andreasabel]

More shrinking, getting rid of the builtin libraries:

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

record Wrap (A : Set) : Set where
  -- pattern; no-eta-equality   -- can't turn off eta
  constructor wrap
  field wrapped : A

data Dec (A : Set) : Set where
  no : Dec A

postulate
  foo : ∀{A : Set}{P : A → Set} → (∀ x → Dec (P x)) → ∀ (x : A) → Dec (P x)
    -- can't inline P = LtWrap
    -- can't define foo = id
  Nat : Set
  P   : Nat → Set
  p?  : ∀ x → Dec (P x)

-- can't make these postulates
PWrap : Wrap Nat → Set
PWrap (wrap f) = P f

pWrap? : ∀ p → Dec (PWrap p)
pWrap? (wrap f) = p? f

bar : Wrap Nat → Wrap Nat
bar fs with foo pWrap? fs
... | no = fs

test : ∀ fs → bar fs ≡ fs
test fs with foo pWrap? fs
... | no = refl

Problem seems to be connected to eta for Wrap.

[andreasabel]

As suspected, bisect says: 3abef8d is the first bad commit (PR #7122).