Agda: Lack of unicode support in locale may result in uncaught IOException

[ajrouvoet]

I'm experiencing some type-checking performance issues (2.6.0.1, still present on the 2.6.1 release branch) that are hard to debug.

Running with the new -vprofile.definitions:10 reveals a mysterious note about and 'commitBuffer', with a large portion of the total time missing:

Total                                                                             410,437ms 
Miscellaneous                                                                      90,003ms 
JVM.Defaults.Syntax.Bytecode.label                                                243,552ms 
JVM.Defaults.Syntax.Bytecode.<stdout>: commitBuffer: invalid argument (invalid character)

This seems to be at least a bug with the new profile flags?

I think that the large amount of time used by type-checking here is (mostly) due to instance search.
Are there flags that help me get some more insight into how much time was spent in this module/definition on instance search?

[nad]

Agda uses the current locale settings for output (or something similar on Windows). I suspect that you can fix the output by switching to a locale with full Unicode support.

We get similar reports now and then. I wonder if we could catch the error and give a better error message.

[nad]

I wonder if we could catch the error and give a better error message.

One can trigger the error message above in the following way (at least on my machine):

$ cat Test.hs
main = putStrLn "∀"
$ ghc --make Test.hs
[1 of 1] Compiling Main             ( Test.hs, Test.o )
Linking Test ...
$ LC_CTYPE=C ./Test
Test: <stdout>: commitBuffer: invalid argument (invalid character)

The error can be caught in a somewhat imprecise way:

$ cat Test.hs
{-# LANGUAGE ScopedTypeVariables #-}

import Data.List
import Control.Exception

main =
  putStrLn "∀" `catch` \(e :: IOException) ->
    let s = show e in
    if "invalid argument (invalid character)" `isSuffixOf` s
    then putStr $ s ++ "\n" ++ message
    else throw e

message = unlines
  [ ""
  , "This error may be due to the use of a locale or code page that does not"
  , "support some character used in the program being type-checked."
  , ""
  , "If you are using a Unix-like system, try <something>."
  , ""
  , "If you are using Windows, try <something else>."
  ]
$ ghc --make Test.hs
[1 of 1] Compiling Main             ( Test.hs, Test.o )
Linking Test ...
$ LC_CTYPE=C ./Test
<stdout>: commitBuffer: invalid argument (invalid character)

This error may be due to the use of a locale or code page that does not
support some character used in the program being type-checked.

If you are using a Unix-like system, try <something>.

If you are using Windows, try <something else>.

An alternative would be to use a text encoding that drops all code points that trigger this problem. However, I think this might confuse users. An error message has the advantage that you know that something is wrong.