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.

Sign up for GitHub

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

Jump to bottom

Error in function-by-method verification: Type parameter could not be determined #4998

Closed
alex-chew opened this issue Jan 19, 2024 · 0 comments · Fixed by #5068
Closed

Error in function-by-method verification: Type parameter could not be determined #4998

alex-chew opened this issue Jan 19, 2024 · 0 comments · Fixed by #5068
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@alex-chew
Copy link
Contributor

alex-chew commented Jan 19, 2024 •
edited
Loading

Dafny version

4.2.0, 4.3.0, 4.4.0

Code to produce this issue

predicate Foo<A> { true } by method { return true; }

Command to run and resulting output

Tmp.dfy(1,26): Error: type parameter 'A' (inferred to be '?') in the function call to 'Foo' could not be determined

What happened?

It seems that the snippet should verify, but it doesn't. Writing either the predicate by itself, or the method by itself, works as expected.

This behavior occurs in 4.2.0, 4.3.0, and 4.4.0.

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

Mac
@alex-chew alex-chew added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jan 19, 2024
@alex-chew alex-chew changed the title Type parameter Error in function-by-method verification: Type parameter could not be determined Jan 19, 2024
@RustanLeino RustanLeino self-assigned this Feb 8, 2024
@RustanLeino RustanLeino mentioned this issue Feb 8, 2024
Merged
RustanLeino added a commit that referenced this issue Feb 8, 2024
@RustanLeino
fix: Fill in type arguments in implicit function-by-method postcondit…
728433a 
…ion (#5068)

This PR fills in any type arguments `X` to the `result = F<X>(args)`
postcondition that's generated for the method part of a
`function-by-method` declaration.

Fixes #4998 

Reviewer notes: The desugaring of `function-by-method` is done in two
places in the code. I filled in the type arguments in both places.
However, in the second place (which is for `{:test}` functions/methods),
`dafny` would crash if any type parameters were declared (even for type
parameters that were not auto-init `(0)`). Since the `{:test}` was
already not allowed for functions/methods with parameters, I also added
error messages if `{:test}` is used with a function/method with type
parameters.

<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
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Fill in type arguments in implicit function-by-method postcondition RustanLeino/dafny
2 participants
@alex-chew @RustanLeino