Andreas Abel

Now biting: - https://github.com/agda/agda/actions/runs/9740873338/job/26879948881#step:11:38

The problem could be that the parser only catches `IOError`s, but `readFile` throws a custom exception `DecodingError :: ReadException`. https://github.com/agda/agda/blob/20ad6b5d02f7a647e83cc493d8b4e11e22cac8c9/src/full/Agda/Syntax/Parser.hs#L86-L96 We could simply throw a `userError` rather than our hand-rolled...

We are also suffering from this regression in `base-4.20` concerning exception printing: - https://gitlab.haskell.org/ghc/ghc/-/issues/25052

> We could simply throw a `userError` rather than our hand-rolled `DecodingError`, since we never catch the latter. This is actually how it used to be in 8d75579c41308fc33671a96235a83f72add316c2 but it...

This issue is maybe more relevant as `cabal v1-install happy` fails now (since `happy-2.0`). - https://github.com/haskell/happy/issues/315 The error message is quite hermetic: ``` $ cabal v1-install happy ... Completed happy-lib-2.0.2...

> now `cabal v1-install happy` works again. It does so with `cabal-3.12.1.0`. But it fails with `cabal-3.14.1.1`, so this might be a new regression: ``` $ cabal v1-install happy Resolving...

@marcinjangrzybowski wrote: > In recent (not merged yet) [PR to cubical agda ](https://github.com/agda/cubical/pull/1150)I found them really usefull (just checked, and I am using them 147 times) Thanks of the pointer!...

Half a year later we are down to 60 (from 250). ``` /src/full/Agda$ grep -R '[^_][gG]eneric\(Doc\)\?[eE]rror' --include="*.hs" \ --exclude=./TypeChecking/Monad/Base.hs --exclude=./TypeChecking/Errors.hs \ --exclude=./Interaction/Options/Errors.hs --exclude=./TypeChecking/Errors/Names.hs \ | wc 63 667 6311 ```...

2025-10-26: - [x] Syntax/Translation/ReflectedToAbstract.hs:1 - [x] TypeChecking/Generalize.hs:3 - [x] TypeChecking/Primitive/Cubical.hs:1 - [ ] TypeChecking/Rewriting/NonLinPattern.hs:4 - [x] TypeChecking/Rules/Builtin.hs:1 - [ ] TypeChecking/Unquote.hs:4

This issue is finally closed in - #8195