Cannot include opaque types in datatype definitions with higher-order functions

[danmatichuk]

The following program fails the export consistency check:

module M1 {
  type T

  datatype D<U> = D(h : T -> int)
}

With the error message: formal type parameter 'T' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'T' as '!T')

This is, in general, a necessary check for soundness (although there is no way to declare T appropriately to make this valid), but in particular it makes it impossible to export this type as provides.

module M1 {
  export reveals D provides T

  type T = int

  datatype D<U> = D(h : T ~> int)
}