Export sets should transitively consider subset types

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

module A {
  type uint8 = int
  type Converted = seq<uint8>

  function Convert(s : string) : (ret : Converted)
}

module B {
  import A
  export provides
    A,
    DEFAULT_VALUE
  const DEFAULT_VALUE := A.Convert("DEFAULT_VALUE")
}

Command to run and resulting output

Paste in VSCode in latest-nightly

What happened?

Raised while checking export set B: Type or type parameter is not declared in this scope: uint8 (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules)
This export set is not consistent: B

There should be no error.

What type of operating system are you experiencing the problem on?

Windows