Disambiguation priority not preserved when importing modules

[xumingkuan]

Dafny version

4.1.0

Code to produce this issue

module A {
  datatype T = foo(int)
  function foo(x: int): int {
    x * x
  }
  method M() {
    var x := foo(100);
    print x, "\n";
  }
}

module B {
  import opened A
  method M() {
    var x := foo(100);
    print x, "\n";
  }
}

method Main() {
  A.M();
  B.M();
}

Command to run and resulting output

output:
Dafny program verifier finished with 1 verified, 0 errors
10000
100

(If "print" doesn't work, you can also write `assert x == 10000;` in both methods. The one in `A` passes and the one in `B` does not type check.)

What happened?

In A, foo is resolved correctly to the function because it has a higher priority than the datatype constructor.

In B, however, such priorities are not preserved when we import the module A. foo is resolved as a datatype constructor instead.

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

Mac

[stefan-aws]

Following https://dafny.org/latest/DafnyRef/DafnyRef#483-expression-context-name-resolution, I'd expect that in both cases the type of x should be T (instead of int as you suggest). Here's another example:

module A {
  function foo(x: int): int {
    x * x
  }

  datatype T = foo(int)

  method M() {
    var x := foo(100);
    assert x is int;
  }
}

module B {
  import opened A
  
  method M() {
    var x := foo(100);
    assert x is T;
  }
}

[xumingkuan]

Following https://dafny.org/latest/DafnyRef/DafnyRef#483-expression-context-name-resolution, I'd expect that in both cases the type of x should be T (instead of int as you suggest).

Thanks for the fix! I suggested int just because module A did not involve importing opened modules so I thought that should be the correct behavior. It is better to follow the documentation.

Just to make sure I understand the documentation correctly, foo in datatype T = foo(int) falls into the following rule,

3. If there is no Suffix, then look for a datatype constructor, if unambiguous.

and foo in function foo(x: int): int falls into the following rule,

5. Module-level (static) functions and methods

right? And does this mean everything from an opened module will come after everything in the original module?

In each module, names from opened modules are also potential matches, but only after names declared in the module.

For example, is this the correct behavior?

module A {
  datatype T = foo(int)

  method M() {
    var x := foo(100);
    assert x is T;
  }
}

module B {
  import opened A
  
  function foo(x: int): int {
    x * x
  }

  method M() {
    var x := foo(100);
    assert x is int;
  }
}

[stefan-aws]

As for your first two questions, yes, that is how I understand it too. I don't think the last example should verify though. From the perspective of B, you'll still have one datatype (from A) and one function (from B) with the same name, thus the datatype will take priority (that is, I'd expect x is T in both cases). I'd think preference should be given to declarations in the local module over the opened one only when you have say two functions with the same name:

module A {
  function foo(x: int): int {
    x
  }

  method M() {
    var x := foo(100);
    assert x == 100;
  }
}

module B {
  import opened A
  
  function foo(x: int): int {
    x * x
  }

  method M() {
    var x := foo(100);
    assert x == 10000;
  }
}

If you have two datatype constructors with the same name, Dafny will report an error that asks for further clarification:

module A {
  datatype T = foo(int)

  method M() {
    var x := foo(100);
    assert x is T;
  }
}

module B {
  import opened A

  datatype U = foo(int)

  method M() {
    var x := foo(100); // ERROR: the name 'foo' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'U.foo')
  }
}