dafny
dafny copied to clipboard
fix: Disambiguation priority not preserved when importing modules
Fixes https://github.com/dafny-lang/dafny/issues/4364.
Description
The author of the issue argues that the types of x
on line 12 and 21 should both be of type int
(currently one is of type T
and one of type int
). I agree that the types should coincide, but believe they should both be T
and not int
. This is my impression since https://dafny.org/latest/DafnyRef/DafnyRef#483-expression-context-name-resolution indicates that one should look for a datatype constructor before matching a function. I believe the difference between documentation and implementation is due to an incorrect triggering of case 2 if there is no surrounding class (that is currentClass is DefaultClassDecl
).
How has this been tested?
I've added two test files that clarify the initial problem documented in the issue.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.