Andreas Abel

`--no-syntax-based-termination` turns on `--type-based-termination`, but should not

2

`--no-syntax-based-termination` turns on `--type-based-termination`, but should not: ```agda {-# OPTIONS --no-type-based-termination #-} {-# OPTIONS --no-syntax-based-termination #-} -- Turns on TBT -- {-# OPTIONS -v term.tbt:50 #-} -- look TBT over...

```agda {-# OPTIONS --no-syntax-based-termination #-} {-# OPTIONS --type-based-termination #-} module TypeBasedTermination.CopatternNonterminating where open import Agda.Builtin.Equality record Stream (A : Set) : Set where coinductive field head : A tail :...

The syntax-based termination checker forbids `T` because it makes Agda loop. ```agda {-# OPTIONS --type-based-termination #-} {-# OPTIONS --sized-types #-} module TypeBasedTermination.BoundedSizeNoMatch where open import Agda.Builtin.Size open import Agda.Builtin.Equality --...

Agda seems to loop on this example: ```agda {-# OPTIONS --type-based-termination #-} data ⊥ : Set where data T (A : Set) : Set where sup : (A → T...

--type-based-termination does not process postulates

3

The `mapRose` example passes with defined `List` and `mapList` but fails when we turn them into postulates: ```agda {-# OPTIONS --type-based-termination #-} {-# OPTIONS --no-syntax-based-termination #-} {-# OPTIONS -v term.tbt:50...

TBT accepts this, but this is questionable, since it seems to assume too much about postulates: ```agda {-# OPTIONS --type-based-termination #-} record U : Set where coinductive field force :...

With `nest : forall i -> Nat i -> Nat i` the `nest` function termination checks, but the size preservation analysis seems to come too late to certify termination of...

Shape-irrelevance without-K broken by Agda 2.6.2

2

(AIM XXXVIII playing with cubical equality proofs for sized coinduction.) This (ICFP 2017 paper definition) is no longer accepted by Agda >= 2.6.2: ```agda {-# OPTIONS --without-K --sized-types --experimental-irrelevance #-}...

https://github.com/agda/agda/blob/cc78a51ffffb5b46c4ed4cf7fe7db8df60b5981f/test/Fail/Issue5468.err#L1-L3 The correct range would be `33,1-12`. Currently, attention is directed to a pattern which is not actually the cause of the error.

Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole

6

Module `Data.List.Relation.Binary.Subset.Setoid` is parametrized on a `Setoid`, but its _Properties_ module not: https://github.com/agda/agda-stdlib/blob/bfd7a7bda8ee55e8d319600c974a3ca7151d752b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda#L9 Instead, each function is parametrized there individually, via anonymous modules. Is there a reason why it is...