Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7225 below:

Named errors instead of Generic[Doc]Error · Issue #7225 · agda/agda · GitHub

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: Link from error messages to documentation? #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. GenericError #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 INJECTIVE_FOR_INFERENCE silently ignored on non-functions #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
• TypeChecking/SizedTypes.hs:1
• TypeChecking/SizedTypes/Solve.hs:5
• TypeChecking/Telescope/Path.hs:1 No reproducer for error raised in telePiPath #7226
• TypeChecking/Unquote.hs:22
• TypeChecking/With.hs:5

Suggested prioritization:

1. type checker
2. scope checker
3. interaction
4. compiler

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4