Named errors instead of Generic[Doc]Error

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

The mid-term plan is to replace these by properly named errors. The name of the error can then be printed as part of the error message. Expected benefits:

We can mechanically check whether each error has a trigger in the testsuite.
We can mechanically check whether each error is covered by the documentation.
We can have a wiki with a page for each error, with the error message linking to it (or we link to the docs). See: #659

Steps to implement:

Prevent new instances of Generic[Doc]Error in our code base, while working off the old ones. This could be ensured by a watchdog in the CI.
For each Generic[Doc]Error (see e.g. #7223):
- Check for a reproducer in the test suite. Add one if missing.
- Check if there exists a suitable named error yet that could cover that error message.
- If not, introduce a new named error.

The current list of occurrences is (2024-04-15):

/src/full/Agda[issue-7181]$ 
grep -Rc '[^_][gG]eneric\(Doc\)\?[eE]rror' --include="*.hs" \
  --exclude=./TypeChecking/Monad/Base.hs --exclude=./TypeChecking/Errors.hs \
  | grep -v ':0' | sort

[ ] Compiler/Backend.hs:3
[ ] Compiler/JS/Compiler.hs:2
[ ] Compiler/MAlonzo/Compiler.hs:4
[ ] Compiler/MAlonzo/HaskellTypes.hs:2
[ ] Compiler/MAlonzo/Pragmas.hs:6
[ ] Compiler/MAlonzo/Primitives.hs:1
[ ] Compiler/ToTreeless.hs:1
[ ] Interaction/BasicOps.hs:6
[ ] Interaction/FindFile.hs:2
[ ] Interaction/Highlighting/Dot/Backend.hs:2
[ ] Interaction/InteractionTop.hs:3
[ ] Interaction/MakeCase.hs:13
[ ] Syntax/DoNotation.hs:2
[ ] Syntax/IdiomBrackets.hs:4
[ ] Syntax/Scope/Monad.hs:1
[ ] Syntax/Translation/ConcreteToAbstract.hs:58
[ ] Syntax/Translation/ReflectedToAbstract.hs:1
[ ] TypeChecking/Coverage/Cubical.hs:3
[ ] TypeChecking/Generalize.hs:3
[ ] TypeChecking/InstanceArguments.hs:3
[ ] TypeChecking/Irrelevance.hs:1
[ ] TypeChecking/Lock.hs:1
[ ] TypeChecking/MetaVars/Occurs.hs:5
[ ] TypeChecking/Modalities.hs:2
[ ] TypeChecking/Monad/MetaVars.hs:1
[ ] TypeChecking/Monad/Options.hs:3
[ ] TypeChecking/Monad/Signature.hs:3
[ ] TypeChecking/Monad/State.hs:2
[ ] TypeChecking/Patterns/Abstract.hs:2
[ ] TypeChecking/Positivity.hs:1
[ ] TypeChecking/Primitive/Cubical.hs:2
[ ] TypeChecking/Primitive/Cubical/Base.hs:1
[ ] TypeChecking/Quote.hs:3
[ ] TypeChecking/Rewriting.hs:1
[ ] TypeChecking/Rewriting/NonLinPattern.hs:4
[ ] TypeChecking/Rules/Application.hs:3
[ ] TypeChecking/Rules/Builtin.hs:15
[ ] TypeChecking/Rules/Data.hs:3
[ ] TypeChecking/Rules/Decl.hs:12 #7245
[ ] TypeChecking/Rules/Def.hs:1
[ ] TypeChecking/Rules/Display.hs:4
[ ] TypeChecking/Rules/LHS.hs:7
[ ] TypeChecking/Rules/Record.hs:2
[ ] TypeChecking/Rules/Term.hs:13
[ ] TypeChecking/Serialise/Base.hs:1
[x] TypeChecking/SizedTypes.hs:1
[ ] TypeChecking/SizedTypes/Solve.hs:5
[ ] TypeChecking/Telescope/Path.hs:1 #7226
[ ] TypeChecking/Unquote.hs:22
[ ] TypeChecking/With.hs:5

Suggested prioritization:

type checker
scope checker
interaction
compiler

agda / agda

Named errors instead of Generic[Doc]Error #7225