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

TTyApp found when kind checking, but it should have been eliminated already #1256

Closed
ramsdell opened this issue Jul 27, 2021 · 2 comments
Closed
Labels
bug Something not working correctly duplicate Essentially the same as another issue

Comments

@ramsdell
Copy link

Here is some buggy code that causes an error. (The curly brackets in the function body should not be there.)

$ cat bug.cry
perm_prop : {n} (fin n) => [n][32] -> Bit
perm_prop p = all (\x -> x < `{n}) p
$ cryptol bug.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸
version 2.10.0
https://cryptol.net :? for help

Loading module Cryptol
Loading module Main
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
%< ---------------------------------------------------

$

@brianhuffman brianhuffman added the bug Something not working correctly label Jul 27, 2021
@brianhuffman
Copy link
Contributor

With a recent development version, it looks like this doesn't panic anymore. I'm going to do a bit more testing to see exactly which versions have the bug.

@brianhuffman brianhuffman added the duplicate Essentially the same as another issue label Jul 27, 2021
@brianhuffman
Copy link
Contributor

Duplicate of #962. It was fixed by #1071.

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

2 participants