How to better warn users?

[MikaelMayer]

I came across the following case:

module A {
  function fib(n: nat): nat {
    if n <= 1 then n else fib(n-1) + fib(n-2)
  }

  function FibWrapper(n: nat): nat {
    fib(n)
  }
}

module B {
  import opened A
  lemma FibDef(n: nat) {
    assert FibWrapper(n) == fib(n); // Fails
  }

  // Lots of code
  // Uh oh, replicated definition
  function fib(n: nat): nat {
    if n <= 1 then n else fib(n-1) + fib(n-2)
  }
}

The assertion is obvious but it fails., all because resolution picks up a different function and Dafny does not know they are equal.
This caused us some headache today to find.
What should we do?

1. Nothing, just become a bit more expert and remembering that if a name matches a definition, it might not be THAT definition
2. Raise a warning/error if we import opened a module which has a function of the same name (like we would do if there is a duplicate function definition)
3. Emit a proof obligation that the two functions are the same, and ignore the overriden one for resolution.
4. something else

Ideas welcome

[alex-chew]

I think that option 2 "Raise a warning/error if we import opened a module which has a function of the same name (like we would do if there is a duplicate function definition)" is best, and I'm surprised to learn that it's not what's already implemented now.

[RustanLeino]

Definitely not 3. (It would be weird to have such a proof obligation.)

Here are some food for thought:

I like the idea of generating a warning, but I'm not sure what.

import opened is pretty relaxed in a number of ways. For one, anything so imported has lower priority than anything declared in the importing module (which is what option 2 is proposing we generate a warning for). Dafny allows import opened from several difficult modules, even if those modules declare a symbol with the same name--for this, Dafny currently generates a warning (actually, it's an error) if you try to use the symbol.

Option 2 might make sense if shadowing is turned off.

There are other ways that shadowing could occur. For example:

function Fib(n: nat): nat { ... }

class MyClass {
  lemma L() {
    ... Fib ... // this refers to MyClass.Fib, but perhaps the programmer wanted the Fib from the module scope
  }
  function Fib(n: nat): nat { ... }
}