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

Match expression type inference is incorrect #3333

Closed
keyboardDrummer opened this issue Jan 6, 2023 · 0 comments · Fixed by #3334
Closed

Match expression type inference is incorrect #3333

keyboardDrummer opened this issue Jan 6, 2023 · 0 comments · Fixed by #3334
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jan 6, 2023

Dafny version

3.10.0

Code to produce this issue

newtype uint16 = x: int | 0 <= x < 0x1_0000
datatype Datatype = A | B
{
  function method Foo(): uint16 {
    match this
    case A => 1
    case B => 2
  }
}

Command to run and resulting output

dafny verify filename.dfy

Dafny program verifier finished with 2 verified, 0 errors

What happened?

I expect to get an error, since newtypes cannot be automatically converted to their basetype.

filename.dfy(5,18): Error: Function body type mismatch (expected uint16, got int)
1 resolution/type errors detected in filename.dfy

What type of operating system are you experiencing the problem on?

Mac

@keyboardDrummer keyboardDrummer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jan 6, 2023
@keyboardDrummer keyboardDrummer self-assigned this Jan 6, 2023
keyboardDrummer added a commit that referenced this issue Jan 6, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
Fixes #3333

The actual fix was already accidentally made in
#2734, this PR is just adding a
test case and a release note, and removing some obsolete code.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant