[TYPES] Looking for a type system

[David Rajchenbach-Teller]

Dear list,

I've been working for a few months on a type system for applied system
security. I've started with dependent types and progressively managed to
trim it down to something which, with a few simplifications, has the
following grammar:

T ::= T -> T
      |    P                    (primitive type)
      |   forall a T   (polymorphism)
      |   a                     (type variable)
      |   K(T)               (constructor)
      |   T union T     (set union)

Now, I'd say that all of the above is very common stuff except for the
union (let me stress that this is set union, not disjoint union). As
that construction seems quite natural, I cannot help but assume that
such a type system has been amply studied.

Could anyone help me put a name on that type system so that I can look
for some literature?

Thanks,
 David,
   Who already feels foolish for asking, because the answer is bound to
be somewhere on the lambda-cube or so

-- 
David Teller-Rajchenbach
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations. 
-- 
David Teller-Rajchenbach
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations.