For `import opened M` where `M` is a module that declares a top-level `M`, let `M` in the importer refer to that top-level `M` instead of referring to the module `M`.

Fixes dafny-lang#1996

# Conflicts:
#	RELEASE_NOTES.md

The resolution change introduced by the previous commit silently changes the
meaning of existing Dafny programs.  This commit 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 this 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.

# Conflicts:
#	RELEASE_NOTES.md