Refinement export sets are shared?

[xtrm0]

In dafny3.3. I would expect module MB to just export M0, but it seems that the export set 'All' is being shared between MA and MB. I was trying to have Imports as a baseclass with a lot of import opened and then using it on child classes to not have to duplicate the imports, but it doesn't work.

Is this a bug, and is there another way to avoid duplicating the imports?

module M0 {}

module Imports {
  import opened M0
  export All provides M0
  export reveals *
}

module MA refines Imports {
  export All ... provides AAA
  export extends All

  predicate AAA() { true }
}

module MB refines Imports {
  export extends All
}

Output:

# dafny /version
Dafny 3.3.0.31104
# dafny /dafnyVerify:1 /compile:0 test/file3.dfy /trace
Parsing test/file3.dfy 
test/file3.dfy(13,12): Error: 'AAA' must be a member of 'MB' to be exported

This doesn't error:

module M0 {}

module Imports {
  import opened M0
  export All provides M0
  export reveals *
}

module MA refines Imports {
  export All ... provides AAA
  export extends All

  predicate AAA() { true }
}

Output:

# dafny /version
Dafny 3.3.0.31104
# dafny /dafnyVerify:1 /compile:0 test/file3.dfy /trace
Parsing test/file3.dfy 
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.0074818 s]

Dafny program verifier finished with 0 verified, 0 errors

Neither does this:

module M0 {}

module Imports {
  import opened M0
  export All provides M0
  export reveals *
}

module MB refines Imports {
  export extends All
}

module MA refines Imports {
  export All ... provides AAA
  export extends All

  predicate AAA() { true }
}

Output:

# dafny /version
Dafny 3.3.0.31104
# dafny /dafnyVerify:1 /compile:0 test/file3.dfy /trace
Parsing test/file3.dfy 
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.0074818 s]

Dafny program verifier finished with 0 verified, 0 errors

[MikaelMayer]

The following doesn't error either:

module M0 {}

module Imports {
  import opened M0
  export All provides M0
  export reveals *
}

module MA refines Imports {
  export All ... provides AAA
  export extends All

  predicate AAA() { true }
}

module MB refines Imports {
  export extends All

  predicate AAA() { false }
}

But I'm not sure what are the specifications of exporting, providing, extending and importing. Can someone please help @xtrm0 with this?