From ddd521134e92163da009c222d52605fc0c69843b Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Thu, 23 Apr 2026 19:21:01 +0200 Subject: [PATCH 1/2] Fixes for agda/agda#8533: eta equality is no longer inferred - `Data.Record` needs a `ETA_EQUALITY` pragma to suppress the `UnguardedEtaRecord` warning. - `Reflection.AST.Traversal` needs an explicit declaration of `no-eta-equality`. This was previously inferred. --- src/Data/Record.agda | 2 ++ src/Reflection/AST/Traversal.agda | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Data/Record.agda b/src/Data/Record.agda index 709ce69a67..8a9c6d5f39 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -62,6 +62,8 @@ mutual -- Record is a record type to ensure that the signature can be -- inferred from a value of type Record Sig. + {-# ETA_EQUALITY #-} -- Suppress warning UnguardedEtaRecord + record Record {s} (Sig : Signature s) : Set s where eta-equality inductive diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda index 2598b75c1a..913bc5b8f7 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -27,7 +27,7 @@ open RawApplicative AppF -- compute the length of the context everytime it's needed. record Cxt : Set where constructor _,_ - pattern + no-eta-equality; pattern field len : ℕ context : List (String × Arg Term) From dc53645772f399aa73e8748628e61af726da6201 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 28 Apr 2026 11:48:55 +0200 Subject: [PATCH 2/2] CI: update experimental to Agda commit f3697415 --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index a623879445..b928bd538b 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -76,7 +76,7 @@ jobs: if [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}"; + echo "AGDA_COMMIT=f3697415ac835c4e0898fb7eb0a5a46e313c2065" >> "${GITHUB_ENV}"; echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}" else # Pick Agda version for master