Andreas Abel

I am realizing this with `make AGDA_BIN=agda-quicker fail`: ``` MultipleFixityDecl: OK (0.12s) MultipleFrontEnds: Golden value differs from actual value. Accept actual value as new golden value? [yn] n FAIL Golden...

`--double-check` broken by `--sized-types`

1

Double checking does not succeed with sized types, as they do not follow the same blocking logic: https://github.com/agda/agda/blob/4f78cac7071f662601c08707e6000ce7e2b5b9f4/src/full/Agda/TypeChecking/MetaVars.hs#L527C65-L531 TODO: - Investigate and document why this special blocking logic is necessary....

Allow unification when types are not equal but have a common supertype?

4

This was accepted by Agda-2.5.2 (and versions below) but is rejected in 2.5.3: ```agda {-# OPTIONS --sized-types #-} {-# OPTIONS --experimental-irrelevance #-} {-# BUILTIN SIZEUNIV SizeUniv #-} {-# BUILTIN SIZE...

Refactor the sort system

1

Working on PRs #6623, #6641 and #6652 (in connection with PropOmega) I saw that operations on sorts are distributed over several modules (like `Syntax.Internal`, `TC.Sort`, `TC.Substitute`, `TC.Conversion`) and were partially...

Reopen PR "Add `record where` syntax sugar (#6603)"

3

This reopens - #6603 and continues the discussion started there. There is a few points to discuss and address in the proposed `record where` feature: 1. The currently implemented semantics...

Revert cyclic computation of ranges (and ban `mdo` from this code base)

2

https://github.com/agda/agda/blob/ee1b7beb3d45d507ff0ec60c5f1f7a18d6772063/src/full/Agda/Interaction/Imports.hs#L133-L146 This change in 2.6.3 caused the `SrcFile` component of ranges to be black holes during parsing, making stuff not `Show`able and causing regression #7301. - #7301 This regression shows...

no termination error with `--double-check`

5

This is a strange case: turning on `--double-check` makes the termination error go away. Should be investigated. ```agda {-# OPTIONS --no-syntax-based-termination #-} {-# OPTIONS --type-based-termination #-} {-# OPTIONS --cubical-compatible #-}...

Fix #5269: agda-bisect: WIP: Support v2-cabal via v2-build and cabal-plan

1

Fix #5269: use v2-cabal in agda-bisect. Problems: - call agda so that it finds its data dir

TBT skips termination checking for record types and then hangs: ```agda {-# OPTIONS --syntax-based-termination #-} -- OR: no-syntax-based... {-# OPTIONS --type-based-termination #-} -- Andreas, 2022-03-10, issue #5823, reported by oisdk...

TBT: internal error in function `smallerOrEq`

5

This code triggers an internal error in `Agda.Termination.TypeBased.Checking.smallerOrEq`: ```agda {-# OPTIONS --no-syntax-based-termination #-} {-# OPTIONS --type-based-termination #-} {-# OPTIONS --sized-types #-} open import Agda.Builtin.Size open import Agda.Builtin.Equality data Empty :...