dafny icon indicating copy to clipboard operation
dafny copied to clipboard

fix: Disambiguation priority not preserved when importing modules

Open stefan-aws opened this issue 9 months ago • 0 comments

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.

stefan-aws avatar May 28 '24 14:05 stefan-aws