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

sum-types: Fix lint checking for case expressions #1615

Closed
RyanGlScott opened this issue Jan 24, 2024 · 0 comments
Closed

sum-types: Fix lint checking for case expressions #1615

RyanGlScott opened this issue Jan 24, 2024 · 0 comments
Assignees
Labels
bug Something not working correctly enums Issues related to enums typechecker Issues related to type-checking Cryptol code.

Comments

@RyanGlScott
Copy link
Contributor

On the sum-types branch (#1602), if you write this:

// Foo.cry
enum Foo = MkFoo

f : Foo -> ()
f l =
  case l of
    MkFoo -> ()
// Foo.icry
:set coreLint=true
:l Foo.cry

Then running cryptol on Foo.icry will crash:

$ cabal run exe:cryptol -- -b Foo.icry 
Loading module Cryptol
Loading module Cryptol
{n, a, b, c} n == min n n
{a, n} (fin n) => inf == inf * (1 * (1 * 1))
{a, n} (fin n) => n / 2 == n - n /^ 2
{n, a, b} n == min n n
{n} (n >= 1, fin n) => (fin n, n >= 1)
Loading module Main
cryptol: src/Cryptol/TypeCheck/Sanity.hs:(212,3)-(338,56): Non-exhaustive patterns in case

We need to implement an ECase case in Cryptol.Typecheck.Sanity.exprSchema.

@RyanGlScott RyanGlScott added bug Something not working correctly typechecker Issues related to type-checking Cryptol code. enums Issues related to enums labels Jan 24, 2024
@yav yav self-assigned this Jan 31, 2024
yav added a commit that referenced this issue Jan 31, 2024
@yav yav closed this as completed Jan 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly enums Issues related to enums typechecker Issues related to type-checking Cryptol code.
Projects
None yet
Development

No branches or pull requests

2 participants