Andreas Abel

Clauses do not reduce up to eta during termination checking. This is distilled from a real world example by @jonashoefer: ```agda postulate A : Set B : A → Set...

- **Replace SafeFlagPragma with early check for unsafe options**

Unguarded eta records can make Agda loop

1

From: https://github.com/agda/agda/issues/7467#issuecomment-2326548333 ```agda data ⊥ : Set where record R : Set where eta-equality; inductive field f : R f : R → ⊥ f () -- Agda loops here...

PR #5267 redux: Make more options infective

2

This is a reopening of PR #5267 - #5267 This PR was removed from 2.7.0 since some design questions are still open. The PR made e.g. `--type-in-type` infective so that...

Require ETA pragma instead of eta-equality directive in unguarded records

1

Fixes #7477. - #7477 From: https://github.com/agda/agda/issues/7467#issuecomment-2327177373 > should overwrite the user directive, mark it as dead code, cast an [error] warning and point the user toward the ETA pragma. This...

Extend the emptiness check to all pattern records?

7

Lifted from #7442. The lack of eta for the following record `R` makes it fail the emptiness check. ```agda data ⊥ : Set where record R : Set where no-eta-equality;...

Deprecate idiom brackets?

4

Idiom brackets were added to Agda in 2016. Personally, I think they are a questionable feature (I will explain below why I think so) and I think we should reevaluate...

In the situation `agda -c M.agda`, when `M.agda` can be just deserialized, any `{-# OPTIONS -v ... #-}` in this files are ignored.

Lift relevance restriction in record-expression-to-copatterns translation?

6

The record-expression-to-copatterns translation currently does not kick in for records with irrelevant fields: https://github.com/agda/agda/blob/d854cc9aebe80012c00ec75fa68ccad63efa57b4/src/full/Agda/TypeChecking/RecordPatterns.hs#L301 Do we need this restriction? Note that Agda happily accepts a definition by copatterns with irrelevant...

Don't project fields that depend shape-irrelevantly on an irrelevant field

1

@anuyts writes (lifted from https://github.com/agda/agda/issues/6703#issuecomment-1607103761): Without `--experimental-irrelevance`, further fields' types cannot really depend on an irrelevant field's value (they have to use it irrelevantly AND their type is of course...