feat!: New behavior for opened import where module contains homonymous top-level declaration

[RustanLeino]

This PR changes the behavior of import opened M = M (and its shorthand import opened M) for a module that contains a top-level declaration M. To motivate and describe the change, it's helpful to start with what Dafny did previously.

Opened import

Consider a "library" module

module M {
  const X...
  ...
}

and a "client" module

module Client {
  import opened M
  ...
}

The import opened declaration adds M as a local name in Client, and this M refers to the module being imported. In addition, since the import is opened, the top-level names declares in module M are spilled into the module Client. This means that the client can refer to the constant as either X or M.X.

There are some restrictions:

• If the client declares a local name X, then that X takes precedence over the import-opened X. This means that the client has to write M.X to refer to that constant.
• If the client does not declare another local name X, but the client also does import opened N, where N is a module that declares an X, then the name X is ambiguous in the client. This is allowed by Dafny, but the client module cannot write just X, but has to use the qualified name M.X or N.X to indicate which X it wants to refer to.

Previous behavior

Suppose the library module contains a top-level declaration with the same name as the module:

module M {
  type M...
  ...
}

A client that does import opened M introduces the local name M, and this name takes precedence over the import-opened name M. Thus, in the client module, M refers to the imported module, and the only way to refer to the type inside that module is to write M.M.

Even though this gives rise to simple, consistent rules, it sometimes causes programs to have to invent more names. For example, for a library module that primarily exports one type, say Option, it would be natural to use the same name (Option) for the name of the module. However, that means clients have to write Option.Option to refer to the type, even if the module is imported as opened.

New behavior

To better serve the special case of naming a module and its primary top-level declaration the same, this PR introduces an exception to the standard rules given above. The exception is that if a client does import opened M where module M contains a top-level declaration M, then the client, in effect, gets a local name M that refers to the M in module M.

For example, a library module

module Option {
  datatype Option<T> = None | Some(value: T)
  function Certainly<T>(t: T): Option<T> {
    Some(t)
  }
}

can be used as follows:

module Client
  import opened Option

  function Find<X>(s: seq<X>, key: X): Option<int>
  ...
}

Note, however, that this means the import-opened module cannot be referred to directly (unless it is renamed). For example, the only way the client module can refer to another member in the imported module, say Certainly, is to not use any qualification. That is, Option.Certainly would give an error (since Option refers to the type and Certainly is not a member of that type), and the client instead must write just Certainly (which works only if no other name in the client takes precedence and there is no ambiguity).

Since import opened M makes M a local name--either to the imported module, as before, or to a top-level declaration in the imported module--it does not introduce any ambiguity with other import-opened symbols. For example, in the example

module M {
  type M
}
module N {
  type M
}
module Client {
  import opened M
  import opened N
  
  method Test(m: M) // M unambiguously refers to the type M in module M
}

Renaming imports

Dafny allows an import declaration to introduce a local name that is different from the name of the module being imported. This is done as

import opened LocalName = ModuleName

(with or without the opened modifier). By default, import opened M just means import opened M = M (again, with or without the opened modifier). The new behavior applies only if the local name is the same as the name of the module being imported. For example, this PR does not change the behavior for import opened LocalNameForM = M.

TODO: The description here should be copied into the reference manual.

Fixes #1996

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[cpitclaudel]

The resolution change introduced by the previous commit silently changed the
meaning of existing Dafny programs. I have pushed a commit that does its best to detect these
cases and raise resolution errors instead.

To illustrate the technique, consider the following example:

module Option {
  static const a := 1
  datatype Option = … { static const a := 2 }
}

module X {
  import opened Option
  method M() { print Option.a; }
}

This program printed 1 in previous versions of Dafny. It would print 2 with the
new resolution strategy introduced in the previous commit. To avoid that, the program
is rejected instead.

To do so, we keep track of shadowing in a separate table:

• Source/DafnyCore/AST/TopLevelDeclarations.cs (ModuleSignature): Add a new
  field ShadowedImportedModules.
• Source/DafnyCore/Resolver.cs (ResolveOpenedImports): Keep track of
  shadowed modules.

This table is used in ResolveDotSuffix:

• Source/DafnyCore/Resolver.cs (ResolveNameSegment): Return name of shadowed
  module, if any, as an out parameter
  (ResolveDotSuffix): Before returning, make sure that the same name could not
  have been resolved in the parent module.

The check is performed in CheckForAmbiguityInShadowedImportedModule, which
runs a simplified version of resolution of a name in a module:

• Source/DafnyCore/Resolver.cs (CheckForAmbiguityInShadowedImportedModule):
  Error out if the shadowed module contains a conflicting name (a name that would
  previously would have been instead of the one that the new resolution algorithm
  picks).
  (NameConflictsWithModuleContents): Determine whether a conflicting name exists.
  The check is an over-approximation: it disallows certain cases in which the old
  program would not have compiled due to ambiguity, for example.

Two subtle additional difficulties:

• Constructors are visible in a datatype and in its parent module. This means
  that without special care we would disallow expressions like Option.Some.

• Code that was previously ambiguous now compiles unambiguously. One specific
  example is datatype constructors: previously, if two datatypes in a module
  defined same-named constructors, references to Module.Constructor were
  ambiguous. Now, if one of the datatype has the same name as the module, then
  such references are legal and unambiguously resolve to the constructors of that
  datatype.

[davidcok]

I opened issue 2757, assigned to me, to document this change in the RM.

[RustanLeino]

bahvior -> behavior

[davidcok]

The two instances of 'open' should be 'opened'