Give clearer error messages about why Cryptol rejects non-Latin-1 Unicode characters

[RyanGlScott]

Cryptol only supports character and string literals where each character can fit within a single byte, i.e., where all characters come from the Latin-1 character encoding. There are many Unicode characters that fall outside of Latin-1, however, and Cryptol currently gives a rather confusing error message when you attempt to use such characters. For example, if you attempt to write a string with the ω character, Cryptol will give this error:

[error] at Primitive/Asymmetric/Signature/ML_DSA/Specification.cry:137:27--137:77:
  • Unsolvable constraint:
      8 >= 10
        arising from
        use of literal or demoted expression
        at Primitive/Asymmetric/Signature/ML_DSA/Specification.cry:137:27--137:77

This only makes sense if you realize that (1) character literals desugar to calls to number (e.g., ω desugars to number`{969,[8]}), and (2) the 8 >= 10 part arises due to ω needing at least 10 bits to represent, but the maximum bits character literals are allowed is 8. It would be nice if the error message could explain this to avoid confusion in the future.