Impossible to specify type characteristics when export provides

[MikaelMayer]

Dafny version

4.2.0

Code to produce this issue

module DatatypeHider {
  export provides Test, Test.Number

  datatype Test = Test(i: nat)
  {
    function Number(): nat {
      i
    }
  }
}
module DatatypeUser {
  import opened DatatypeHider

  predicate Test() {
    forall t: Test :: true // Error: a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 't' (of type 'Test') may contain references
  }
}

Command to run and resulting output

dafny verify

What happened?

I'm exporting a datatype but I want to hide its constructors.
I would still export the fact that this datatype is not allocated though, otherwise, I can't quantify on all of them.
I did not find a mechanism to do that. We should be able to do something like

export provides Test(!new)

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

Windows