Undeclared top-level issue

[MikaelMayer]

The following code

type Foo

module bar {
  class C {
    var baz : Foo
  }
}

produces the error

Type Error Error
(6,14): Error: Undeclared top-level type or type parameter: Foo (did you forget to qualify a name or declare a module import 'opened'?) 

In this particular case, the error message should not mention "undeclared top-level type" because it assumes Dafny looked into the top-level types and could not see Foo, but it's a top-level type.
Here are the alternatives on how we could fix it:

• Remove "top-level" from the error message
• Reverse the importing rule for the top-level module: children of a top-level module should be able to import their default parent module's definitions
• Add the message (also, children can't import the definitions of their parents)

[cpitclaudel]

Remove "top-level" from the error message

I think top-level here means "unqualified" (so it's the use of Foo that's "top-level", not its definition)
(I don't find it very clear and I like the idea of removing it)