Fix parse panic

[robdockins]

Fix parsing/typechecking issues arising from explicit type applications occurring in unexpected places.

This change restricts some programs that were previously accepted, but were rather unusual, I think. E.g.

f`{5}`{Integer}

Is a program that used to be accepted with the same meaning as

f`{5,Integer}

After this patch, the first program with an error indicating that type applications are only allowed on identifiers.

[brianhuffman]

Are empty type applications like f`{} still allowed?

[robdockins]

Yes, those are still allowed. We could rule them out, I suppose.

I think it would just be a matter of removing this line from the parser

cryptol/src/Cryptol/Parser.y

Line 749 in bcc7612

| '{' '}' { at ($1,$2) (TTyApp []) }

Or, we could do it at a later stage and maybe get better error messages.

[yav]

Looks good to me, just maybe add the example, and I am not sure about the paren case, but I am also not sure if it actually matters.

[brianhuffman]

If you want to apply a type to an infix operator, you definitely will need parens, e.g. (+)`{Integer} I suppose that syntax might not use the same "paren" parse AST constructor, but it seems consistent to allow the parens for non-infix identifiers too.

[robdockins]

Yeah, I don't see a compelling reason to rule out things like (name)`{a = Integer}, so I guess we might as well leave it.

[yav]

@brianhuffman I don't think that (+) would result in Parens in the AST, I believe it should just make a different kind of name.

I was confused by the parens because I think of type application as a property of a name rather then expression, because in the current system only named thing can be polymorphic.