Panic when evaluating literal type.

[linesthatinterlace]

Cryptol asked me to raise this bug: as you can see, I simply input `{0 - 1} at the REPL, and it asked me to submit a bug.

cryptol> `{0 -1}
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  a506732dc63cf5bd78f18ac7ac525926c805a2b6
  Branch:    HEAD (uncommited files present)
  Location:  doCheckType
  Message:   TTyApp found when kind checking, but it should have been eliminated already
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.10.0.99-inplace:Cryptol.TypeCheck.Kind
%< --------------------------------------------------- 

[linesthatinterlace]

Actually, it's not actually the - that is causing it, I was wrong, it's the use of the curly braces (should be parentheses). Not sure why it crashes!

[yav]

The correct notation is to use parens instead of braces, and we had a bug in the parser, which has now been fixed (should be in the release from a few days ago).

Cryptol> `{0-1}

[error] at <interactive>:1:2--1:7:
  Unexpected bare type application.
  Perhaps you meant `( ... ) instead.

[robdockins]

Yup, same as #962

[linesthatinterlace]

Sorry for the duplicate! I'll go get the new release.

…

On Wed, 31 Mar 2021, 18:36 robdockins, ***@***.***> wrote: Yup, same as #962 <#962> — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1142 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AIDTA6F4W3R3CIOTHNGAX53TGNMQXANCNFSM42FDMPTQ> .

[robdockins]

No worries! It's interesting that we've had this bug for a long time, I think, but somehow 4 different people noticed it just in the last few months.