I have encountered a performance regression: Agda 2.6.5-d99c822 type-checks a proof of reflexivity quickly, whereas Agda 2.7.0 does not. Here is the goal type, normalised and including hidden arguments, printed by Agda 2.7.0:
Reflexive-relation._≡_
(Equivalence-relation⁺.reflexive-relation (e⁺ (iℓ ⊔ p ⊔ ℓ)))
{(x : I) →
P x →
Σ {ℓ} {ℓ} ((n : ℕ) → Q n x)
(λ f →
(n : ℕ) →
Reflexive-relation._≡_
(Equivalence-relation⁺.reflexive-relation (e⁺ ℓ)) {Q n x}
(down n x (f (suc n))) (f n))}
(λ x x₁ →
(λ y → c .proj₁ y x x₁) ,
(λ y →
Equality-with-J.cong (eq {p ⊔ ℓ} {ℓ}) {(x₂ : P x) → Q y x} {Q y x}
{λ x₂ → down y x (c .proj₁ (suc y) x x₂)} {c .proj₁ y x}
(λ h → h x₁)
(Equality-with-J.cong (eq {iℓ ⊔ p ⊔ ℓ} {p ⊔ ℓ})
{(x₂ : I) (x₃ : P x₂) → Q y x₂} {(x₂ : P x) → Q y x}
{λ x₂ x₃ → down y x₂ (proj₁ c (suc y) x₂ x₃)} {proj₁ c y}
(λ h → h x) (c .proj₂ y))))
(λ i x →
(λ y → c .proj₁ y i x) ,
(λ y →
Equality-with-J.cong (eq {p ⊔ ℓ} {ℓ}) {(x₁ : P i) → Q y i} {Q y i}
{λ x₁ → down y i (c .proj₁ (suc y) i x₁)} {c .proj₁ y i}
(λ h → h x)
(Equality-with-J.cong (eq {iℓ ⊔ p ⊔ ℓ} {p ⊔ ℓ})
{(x₁ : I) → P x₁ → Q y x₁} {P i → Q y i}
{λ i₁ x₁ → down y i₁ (c .proj₁ (suc y) i₁ x₁)} {c .proj₁ y}
(λ h → h i) (c .proj₂ y))))
Note that the terms are fairly small. However, for Agda 2.7.0 it takes several seconds to type-check the proof refl _ (with my current setup).
Bisection points towards @jespercockx's commit 02b7ee0 ("[ #6643 #7090 ] Turn illegal rewrite rules into an error warning"). I don't see why this commit would lead to this problem, but I bisected twice, with and without optimisations, and in both cases this commit was singled out.
I have not created a small test case. I can reproduce the problem by running the following code (in an empty directory):
git clone --single-branch --branch v2.7.0 https://github.com/agda/agda
ln -s agda/test/interaction/RunAgda.hs .
git clone --single-branch --branch v2.1-release https://github.com/agda/agda-stdlib
git clone --single-branch https://github.com/nad/equality
(cd equality && git reset --hard 27a61997801fbdfe4c21c713517da880270f2ae0)
cat <<EOF > libraries
$PWD/agda-stdlib/standard-library.agda-lib
$PWD/equality/equality.agda-lib
EOF
cat <<EOF > bug.agda-lib
depend: equality
include: .
flags:
--cubical-compatible
--erasure
--hidden-argument-puns
--no-import-sorts
--safe
EOF
cat <<EOF > script.hs
#!/usr/bin/env runhaskell
{-# LANGUAGE RecordWildCards #-}
import Control.Monad
import Data.List
import System.Directory
import System.Exit
import System.Process
import System.Timeout
import RunAgda
main :: IO ()
main =
runAgda [ "--no-default-libraries"
, "--library-file=libraries"
] $ \(AgdaCommands { .. }) -> do
-- Ensure that nothing is cached.
exists <- doesDirectoryExist "_build"
when exists $ removeDirectoryRecursive "_build"
echoUntilPrompt
-- Ensure that all dependencies have been loaded.
loadAndEcho "Some-definitions.agda"
-- Type-check the problematic definition.
r <- timeout (3*10^6) $ loadAndEcho "Bug.agda"
case r of
Nothing -> do
putStrLn "Timeout!"
exitFailure
Just ss ->
if any ("(agda2-status-action \"Checked\")" \`isInfixOf\`) ss then
return ()
else
exitWith (ExitFailure 127)
EOF
cat <<EOF > Bug.agda
-- Based on "Non-wellfounded trees in Homotopy Type Theory" by Ahrens,
-- Capriotti and Spadotti.
open import Equality
module _
{e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where
open Derived-definitions-and-properties eq
open import Prelude
open import Container.Indexed eq
open import Equivalence eq as Eq using (_≃_)
open import Extensionality eq
open import Function-universe eq hiding (_∘_)
open import Some-definitions eq
private variable
i ℓ p : Level
-- A variant of the non-dependent universal property.
universal-property-≃ :
{I : Type i} {P : I → Type p} →
Extensionality (i ⊔ p) (i ⊔ p ⊔ ℓ) →
(X : Chain I ℓ) →
(P ⇾ Limit X) ≃ Cone P X
universal-property-≃ {i = iℓ} {p} {ℓ} {P} ext X@(Q , down) =
with-other-inverse equiv from′ from≡from′
where
from′ : Cone P X → P ⇾ Limit X
from′ c i x =
(λ y → c .proj₁ y i x)
, (λ y → ext⁻¹ (ext⁻¹ (c .proj₂ y) i) x)
equiv : (P ⇾ Limit X) ≃ Cone P X
equiv =
P ⇾ Limit X ↝⟨ universal-property X (lower-extensionality p iℓ ext) ⟩
(∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n i x → down n i (f (suc n) i x) ≡ f n i x) ↝⟨ (∃-cong λ _ → ∀-cong (lower-extensionality _ lzero ext) λ _ →
∀-cong (lower-extensionality p iℓ ext) λ _ →
Eq.extensionality-isomorphism (lower-extensionality (iℓ ⊔ p) (iℓ ⊔ p) ext)) ⟩
(∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n i → down n i ∘ f (suc n) i ≡ f n i) ↝⟨ (∃-cong λ _ → ∀-cong (lower-extensionality _ lzero ext) λ _ →
Eq.extensionality-isomorphism (lower-extensionality (iℓ ⊔ p) (iℓ ⊔ p) ext)) ⟩
(∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n → down n ∘⇾ f (suc n) ≡ f n) ↔⟨⟩
Cone P X □
from≡from′ : ∀ c → _≃_.from equiv c ≡ from′ c
from≡from′ c = refl _
EOF
cat <<EOF > Some-definitions.agda
-- Based on "Non-wellfounded trees in Homotopy Type Theory" by Ahrens,
-- Capriotti and Spadotti.
open import Equality
module Some-definitions
{e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where
open Derived-definitions-and-properties eq
open import Prelude
open import Container.Indexed eq
open import Equivalence eq as Eq using (_≃_)
open import Extensionality eq
open import Function-universe eq hiding (_∘_)
open import Tactic.Sigma-cong eq
private variable
a i ℓ p : Level
-- Chains (indexed).
Chain : Type i → ∀ ℓ → Type (i ⊔ lsuc ℓ)
Chain {i} I ℓ =
∃ λ (P : ℕ → I → Type ℓ) → ∀ n → P (suc n) ⇾ P n
-- Limits of chains.
Limit : {I : Type i} → Chain I ℓ → I → Type ℓ
Limit (P , down) i =
∃ λ (f : ∀ n → P n i) →
∀ n → down n i (f (suc n)) ≡ f n
-- A kind of dependent universal property for limits.
universal-property-Π :
{A : Type a} {I : Type i} {g : A → I} →
(X@(P , down) : Chain I ℓ) →
((a : A) → Limit X (g a))
≃
(∃ λ (f : ∀ n (a : A) → P n (g a)) →
∀ n a → down n (g a) (f (suc n) a) ≡ f n a)
universal-property-Π {g} X@(P , down) =
(∀ a → Limit X (g a)) ↔⟨⟩
(∀ a → ∃ λ (f : ∀ n → P n (g a)) →
∀ n → down n (g a) (f (suc n)) ≡ f n) ↔⟨ ΠΣ-comm ⟩
(∃ λ (f : ∀ a n → P n (g a)) →
∀ a n → down n (g a) (f a (suc n)) ≡ f a n) ↝⟨ Σ-cong-refl Π-comm (λ _ → Π-comm) ⟩□
(∃ λ (f : ∀ n a → P n (g a)) →
∀ n a → down n (g a) (f (suc n) a) ≡ f n a) □
-- A universal property for limits.
universal-property :
{I : Type i} {P : I → Type p} →
(X@(Q , down) : Chain I ℓ) →
(P ⇾ Limit X)
↝[ i ∣ p ⊔ ℓ ]
(∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n i x → down n i (f (suc n) i x) ≡ f n i x)
universal-property {P} X@(Q , down) ext =
(P ⇾ Limit X) ↔⟨⟩
(∀ i → P i → Limit X i) ↝⟨ (∀-cong ext λ _ → from-equivalence $ universal-property-Π X) ⟩
(∀ i → ∃ λ (f : ∀ n → P i → Q n i) →
∀ n x → down n i (f (suc n) x) ≡ f n x) ↔⟨ ΠΣ-comm ⟩
(∃ λ (f : ∀ i n → P i → Q n i) →
∀ i n x → down n i (f i (suc n) x) ≡ f i n x) ↝⟨ Σ-cong-refl Π-comm (λ _ → Π-comm) ⟩
(∃ λ (f : ∀ n i → P i → Q n i) →
∀ n i x → down n i (f (suc n) i x) ≡ f n i x) ↔⟨⟩
(∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n i x → down n i (f (suc n) i x) ≡ f n i x) □
-- Cones.
Cone : {I : Type i} → (I → Type p) → Chain I ℓ → Type (i ⊔ p ⊔ ℓ)
Cone P (Q , down) =
∃ λ (f : ∀ n → P ⇾ Q n) →
∀ n → down n ∘⇾ f (suc n) ≡ f n
EOF
chmod u+x script.hs
./script.hs agda
Here agda refers to Agda 2.7.0. When I run this script (with my current setup) the last line of output contains the string Timeout!.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4