Closed
Description
Compiling Agda 2.6.4.1 on GHC 9.4.5 with the cabal flags debug, debug-parsing, and debug-serialisation enabled leads to the following erros:
src/full/Agda/Main.hs:291:5: error:
• No instance for (Data.String.IsString (t0 -> [a0] -> [[Char]]))
arising from the literal ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"’
(maybe you haven't applied a function to enough arguments?)
• In the second argument of ‘(:)’, namely
‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
"debug-serialisation: extra debug info during serialisation into '.agdai' files"
[]’
In the expression:
"debug: enable debug printing ('-v' verbosity flags)"
: "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
"debug-serialisation: extra debug info during serialisation into '.agdai' files"
[]
In an equation for ‘flags’:
flags
= "debug: enable debug printing ('-v' verbosity flags)"
: "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
"debug-serialisation: extra debug info during serialisation into '.agdai' files"
[]
|
291 | "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/full/Agda/Main.hs:294:5: error:
• Ambiguous type variable ‘t0’ arising from the literal ‘"debug-serialisation: extra debug info during serialisation into '.agdai' files"’
prevents the constraint ‘(Data.String.IsString
t0)’ from being solved.
Probable fix: use a type annotation to specify what ‘t0’ should be.
Potentially matching instances:
instance (Data.String.IsString a, MonadIO m) =>
Data.String.IsString (TCMT m a)
-- Defined at src/full/Agda/TypeChecking/Monad/Base.hs:5350:10
instance (a ~ Char) => Data.String.IsString [a]
-- Defined in ‘Data.String’
...plus 33 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"’, namely
‘"debug-serialisation: extra debug info during serialisation into '.agdai' files"’
In the second argument of ‘(:)’, namely
‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
"debug-serialisation: extra debug info during serialisation into '.agdai' files"
[]’
In the expression:
"debug: enable debug printing ('-v' verbosity flags)"
: "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
"debug-serialisation: extra debug info during serialisation into '.agdai' files"
[]
|
294 | "debug-serialisation: extra debug info during serialisation into '.agdai' files"
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^