Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

doCheckType panic #1050

Closed
ramsdell opened this issue Jan 27, 2021 · 5 comments
Closed

doCheckType panic #1050

ramsdell opened this issue Jan 27, 2021 · 5 comments
Assignees
Labels
bug Something not working correctly duplicate Essentially the same as another issue

Comments

@ramsdell
Copy link

I received this output from Cryptol 2.10.0.

$ cryptol bug.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸
version 2.10.0
https://cryptol.net :? for help

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

%< ---------------------------------------------------
Revision: 3cab6e6
Branch: release-2.10.0 (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-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/TypeCheck/Kind.hs:391:24 in cryptol-2.10.0-inplace:Cryptol.TypeCheck.Kind
%< ---------------------------------------------------

$

bug.cry.txt

@robdockins robdockins added the bug Something not working correctly label Jan 27, 2021
@robdockins
Copy link
Contributor

I think this is the same issues #962 and #1045

@weaversa
Copy link
Collaborator

Yeah, the example here mistakenly uses braces instead of parens.

@weaversa
Copy link
Collaborator

Specifically,

else if i < `{v1 + o1} then

should be

else if i < `(v1 + o1) then

@weaversa
Copy link
Collaborator

This seems like a pretty easy mistake to make. I'm surprised we haven't run into this before.

@ramsdell
Copy link
Author

Oh man, that is a little embarrassing. The panic through me completely off from looking where I needed to. So this issue becomes a request for a better error message when one uses curly brackets instead of parentheses as I did.

@robdockins robdockins added the duplicate Essentially the same as another issue label Feb 9, 2021
robdockins added a commit that referenced this issue Feb 10, 2021
We now reject situations where the user writes a type application
on a term that is not an identifier, and we correctly unwind
and reapply tuple and field selectors.

Fixes #962
Fixes #1045
Fixes #1050
@robdockins robdockins self-assigned this Feb 12, 2021
robdockins added a commit that referenced this issue Feb 16, 2021
We now reject situations where the user writes a type application
on a term that is not an identifier, and we correctly unwind
and reapply tuple and field selectors.

Fixes #962
Fixes #1045
Fixes #1050
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly duplicate Essentially the same as another issue
Projects
None yet
Development

No branches or pull requests

3 participants