An opaque type should only be export-provided

[RustanLeino]

Currently, Dafny allows an opaque type to be listed both in the provides list and the reveals list of an export set. There's no difference between these two. Therefore, to be consistent with other restrictions, it seems logical to forbid an opaque type from being listed in a reveals clause. (Ror example, compare with a method declaration, which is not allowed in a reveals clause.)

Example:

module M {
  export A
    provides OpaqueType
  export B
    reveals OpaqueType // this ought not to be allowed

  type OpaqueType
}