Andreas Abel

Investigating #6685 I noticed that PR #5319 introduced a semantics change introduced which we did not document explicitly: ```agda private module A where module B where module B' = B...

This is the current specification of `-i`: https://github.com/agda/agda/blob/3c239ef6eddf3f0502c5fe42f81f2b038b76717f/doc/user-manual/tools/command-line-options.rst?plain=1#L184-L186 Rather sad, I'd expect to be informed about the following there: - [x] `-i` is monoidal, i.e., can be supplied many times,...

Size of the Agda git repo (dev only)

13

Since recently, I noticed that `git pull` usually pulls in around 8MB. (Of course, not consecutive pulls, but whenever I return to Agda development the next day or a couple...

The GHC backend does not seem to update existing MAlonzo/RTS.hs

1

Observed the following behavior: - edited `src/data/MAlonzo/src/MAlonzo/RTE.hs` - ran `make install-bin` - ran `make compiler-test` It used the old, existing `MALonzo/RTE.hs` (dating 2021), giving `-Werror=star-is-type` errors with GHC 9.6.1. I...

E.g.: https://github.com/agda/agda/actions/runs/4506148531/jobs/7932946851#step:10:42 ``` +ret > ExitFailure 42 +out > { compiling Issue2908.foo +out > Issue2908.foo = λ a → let b = a + a in seq b 0 +out...

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...