Regression in 2.6.4.2 concerning with
#7148
Comments
Thanks for the report. Yes, a self-contained example would enable us to start investigating this. |
|
Here is a small self-contained test. It is type-checked by Agda-2.6.4.1 but not by 2.6.4.2. |
|
Thanks and congrats, you found a regression in the just-released version of Agda! In your example, CC: @jespercockx |
|
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 |
|
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 = reflProblem seems to be connected to eta for |
with
…ion. Regression introduced in agda#7122.
Uh oh!
There was an error while loading. Please reload this page.
This is on agda-2.6.4.2 built by
$ cabal install -foptimise-heavily -j1,
used with stdlib-2.0,
ghc-9.0.2, under Linux Debian 12, x86_64 machine.
The below module fragment is type-checked by agda-2.6.4.1 but not by agda-2.6.4.2 :
The command is
$ agda $agdaLibOpt $agdaFlags GBasis/OverEuclidean/I.agda +RTS -M7G
where $agdaFlags = --auto-inline --guardedness.
The report is
Which Agda is more correct in this case: 2.6.4.1 or 2.6.4.2 ?
Is this fragment sufficient to guess of the source?
It not, may be I would try to simplify the example, (which is a very complex code, using many modules).
The text was updated successfully, but these errors were encountered: