Fix: Making default export set opaque no longer crashing the resolver on inductive datatypes

[MikaelMayer]

This PR fixes #4334

Looking at the debugger, it arrives at the line that I deleted with the fact that it's not an AbstractTypeDecl, but an InductiveTypeDecl. It just happen that it is no visible in the default scope because there is an export declaration. So there should be no reason to assume it should be an AbstractTypeDecl in my opinion, but I might be missing something. as well.

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

[RustanLeino]

This does not look like the right fix to me. I think the problem is that

rtd.AsTopLevelDecl.IsVisibleInScope(scope)

on L170 is returning false when rtd is Sort. I would expect it to return true, since Sort is visible in every module and export set that includes the body of the predicate. So, my sense is that there's something wrong with the scope information.

Here is a shorter repro (please include both in the eventual test file):

module Crash {
  export Body // rename this to "Crash" and everything works
    reveals *

  datatype Sort =
    | Int
    | Re

  predicate True() {
    forall arg: Sort :: true
  }
}

The problem occurs only if the export set has a name that's different than the name of the enclosing module. I don't understand that part.

Another possible clue: The problem occurs the fourth time the SubsetConstraintGhostChecker is called. (Side note: The call that starts these tests, at the end of method ResolveTopLevelDecls_Core, should probably be enclosed in an if (reporter.Count(ErrorLevel.Error) == prevErrorCount).) The four calls are:

• for the systems module (object, array, ...)
• for module Crash
• for the module created from the export set in Crash, to test the export consistency
• the outermost module (called _module internally).

Evidently, the traversal through the outermost module continues traversing inside its submodules. I'm not sure that's desired. (If not, then perhaps that's the bug.) But even if this is desired, then it seems the scope information is not right when it gets to traversing inside the submodule. I don't understand how the name of the export set could affect this in any way, but apparently it does.