Exporting opened modules with conflicting symbols leads to Contract.Assert failure

[robin-aws]

Minimal reproduction below. As documented in the reference manual, it isn't an error to open modules with overlapping symbols. But attempting to re-export them seems to confuse the resolver.

module Foo {
  datatype T = T()
}

module Bar {
  datatype T = T()
}

module Consumer {

  import opened Foo
  import opened Bar

  export provides Foo, Bar
}

Stack trace below. Note that no published release of Dafny seems to hit this. It only occurs if I build Dafny from source. This seems to imply that the assertion being violated is not actually checked in the published releases.

Process terminated. Assertion failed.
   at Microsoft.Dafny.Type.NormalizeExpand(Boolean keepConstraints) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/DafnyAst.cs:line 791
   at Microsoft.Dafny.UserDefinedType.Equals(Type that, Boolean keepConstraints) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/DafnyAst.cs:line 2980
   at Microsoft.Dafny.Resolver.ResolveOpenedImportsWorker(ModuleSignature sig, ModuleDefinition moduleDef, ModuleDecl im, HashSet`1 importedSigs, Boolean useCompileSignatures) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 1789
   at Microsoft.Dafny.Resolver.ResolveOpenedImports(ModuleSignature sig, ModuleDefinition moduleDef, Boolean useCompileSignatures, Resolver resolver) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 1735
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 993
   at Microsoft.Dafny.Resolver.CheckModuleExportConsistency(ModuleDefinition m) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 1378
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 491
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/DafnyMain.cs:line 165
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/DafnyMain.cs:line 113
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyDriver.cs:line 265
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyDriver.cs:line 57
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyDriver.cs:line 36
   at System.Threading.ThreadHelper.ThreadStart_Context(Object state)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.ThreadHelper.ThreadStart()

[robin-aws]

I suspect what's confusing the code is having a symbol both implicitly defined by an import opened statement but also exported with provides, which should make it an OpaqueTypeDecl. Having two definitions of the same symbol is necessary to trigger the bug only because it causes an equality check between the two types, which in turn calls NormalizeExpand and exposes the inconsistency in both definitions.

[RustanLeino]

The problem arises when the scope import openeds two types of the same name. This ambiguous-name situation is allowed, as long as no use of the types is ambiguous. If the type are referred to by qualified names, then there is no ambiguous use. The other case where there is no ambiguity is when both types refer to the same type (for example, both may be synonyms for int).

The crash reported in this Issue happens during this type-equality test, because the method that performs the type-equality requires the types to be visible.