How to export members of opened module in Dafny?

I can't get the following example to pass resolution in Dafny:

module A{
  export all reveals *
  export provides P // I don't want to reveal the implementation of P by default
  type P<!T(==)> = iset<T>
}

module B{
  import opened A`all
  export provides Test

  function Test(): P<nat>
}

Basically, I would like the function Test() to be provided by default from B and the type P to also be provided, not revealed.
I can't find in the documentation how to achieve that.

You need to say more in the export set of B. Here's a way you can do it:

module A{
  export all
    reveals *
  export
    provides P // I don't want to reveal the implementation of P by default

  type P<!T(==)> = iset<T>
}

module B {
  export
    provides Test, JustP

  import JustP = A
  import opened Everything = A`all

  function Test(): P<nat> {
    iset{} // module B knows what P is, because it imports A`all
  }
}

module Client {
  import B

  method M() {
    var p: B.JustP.P<nat>; // Client can use P, but only as an opaque type
    p := iset{}; // error: Client does not know what P is
  }
}

You can also change

  import opened Everything = A`all

to just

  import Everything = A`all

if you also change the signature of B.Test to

function Test(): Everything.P<nat>

But, for reasons I don't understand, if you change the "everything" import declaration to

  import opened A`all

then you don't get the desired effect of hiding the definition of P from Client (this may be a bug).