[TYPES] System F and Type Generativity

[George Kuan]

ML datatypes and opaque sealing are the source of type generativity in
the ML module system. This generativity is sometimes modeled using
existential types. However, a more direct modeling of generativity
would be to consider generativity as a special operator G in a variant
of System F that takes a type expression and produces a new unique
type unequal to all others. This would be essentially a type-level
effect. Are there any variants of System F that include such an
extension?

- George