Andreas Abel

I built with GHC 9.10 locally, it seems that only warnings are affected, so 2.6.4.3 could be revised for GHC 9.10 as well.

CI Stack Windows fails to install build-tools (permission denied)

1

Last successful build: https://github.com/agda/agda/actions/runs/8509770751/job/23306000462#step:10:1384 > Installing executable happy in C:\sr\snapshots\dd11c2a9\bin https://github.com/agda/agda/actions/runs/8509770751/job/23306000462#step:1:9 - runner version: '2.314.1' - Image: windows-2022 Version: 20240322.1.0 First failing build: https://github.com/agda/agda/actions/runs/8733365593/job/23961919676#step:10:1402 > Installing executable happy in C:\sr\snapshots\dd11c2a9\bin...

OptionWarnings are emitted twice

2

OptionWarnings are emitted twice, e.g.: https://github.com/agda/agda/blob/05138510ac152b6fbb6130467502095073ba07cb/test/Succeed/LossyUnification.warn#L1-L6 Suspected reason: We are calling `setOptionsFromPragma` several times during processing a file. https://github.com/agda/agda/blob/05138510ac152b6fbb6130467502095073ba07cb/src/full/Agda/TypeChecking/Monad/Options.hs#L208-L212 Found while working on: - #7219

The testsuite does not cover this error atm: https://github.com/agda/agda/blob/8c52e3f71c890314c1436a55193256d2b1a43f35/src/full/Agda/TypeChecking/Telescope/Path.hs#L44-L52

Named errors instead of Generic[Doc]Error

1

We have currently short of 250 places where we throw a `GenericError` or `GenericDocError`. ``` /src/full/Agda$ grep -R '[^_][gG]eneric\(Doc\)\?[eE]rror' --include="*.hs" \ --exclude=./TypeChecking/Monad/Base.hs --exclude=./TypeChecking/Errors.hs \ | wc 247 2584 25145 ```...

Typechecker produces unsolvable constraints

1

I would expect Agda to only do safe steps in constraint solving. But in this example I get unsolvable constraints if I do not supply the hidden argument (`{B =...

Agda prints hidden function type in hidden argument as `{{...` and then fails to parse it

2

Agda prints hidden function type in hidden argument as `{{...` and then fails to parse it. Example: `f {{x : A} -> B}`. This is dual to the existing problem...

Fix #6703: lift relevance restriction in recordExpressionToCopatterns

2

Not sure why this restriction was there in the first place, because Agda accepts irrelevant projections on the lhs by default: ```agda record R : Set where field .f :...

According to https://matrix.hackage.haskell.org/#/package/fb versions 2.0.0 and 1.2.x do not build: ``` $ cabal install fb-2.0.0 ... In order, the following will be built (use -v for more details): ... -...

This fails: ``` cabal install hi ``` This works: ``` $ cabal install hi --constraint="optparse-applicative