Naked type application panics

[yav]

I got confused with the notation for demonting types and wrote a type application instead, which caused a panic:

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

%< --------------------------------------------------- 
  Revision:  a7d352b585507a74440968b3cec46f40b8a047af
  Branch:    master (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.9.1.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.9.1.99-inplace:Cryptol.TypeCheck.Kind
%< --------------------------------------------------- 

[brianhuffman]

Weird! Why does that even parse?

[robdockins]

I think it's one of these strange cases where the parser makes `{ stuff } an expression form and fixes it up later to avoid LALR limitations. The mkEApp operator is expected to munge things around and remove the TTyApp forms.

[brianhuffman]

It seems like whatever post-processing pass we do over the parser AST that deals with TTyApp should only allow type applications to identifiers. Currently cryptol is totally fine with empty type applications anywhere you want, like this:

Cryptol> :t (((True`{}, zero`{Integer})`{}).1)`{}
(((True`{}, zero`{Integer})`{}).1)`{} : Integer

Cryptol also is happy to have multiple adjacent type applications, possibly with some of them empty; the effect is like all the applications are appended together:

Cryptol> :t number`{3}`{}`{}`{}`{}`{Integer}
number`{3}`{}`{}`{}`{}`{Integer} : Integer

I think it would be reasonable to forbid stacked type applications, as you can always just combine them into one like number`{3, Integer}.

[yav]

I unassigned myself for the moment, as I am working on a different part of the code. I'll revisit this if no one else has picked it up in the mean time.