Type system whose implicit conversions form a bounded lattice?

I've been working on an "OOP inspired" type system (for the Zeolite Programming Language) that has a particular feature that I haven't encountered before: The implicit conversions between types (e.g., automatic conversion to a parent type) form a bounded lattice (L,≤).

Specifically:

• a ≤ b means "a automatically converts to b".
• a ∧ b can be used covariantly as a, b, or both, e.g., you can call the functions of a or b on a variable of type a∧b. (Any value that can already be used as both a and b can be assigned.)
• a ∨ b is the dual of a∧b, and can store any value of type a or type b. (Can only be used as something that both a and b can convert to, e.g., a common parent. Mostly included for completeness, but it can be useful for restricting a variable to particular implementations of an interface.)
• Any type can convert to the upper bound ∧∅.
• The lower bound ∨∅ can convert to any type. (No such object exists, but it can serve as a "universal" missing value.)

The primary motivation for this is to have first-class variable types that require the functionality of multiple interfaces without having to contrive a common parent, and without needing a type parameter.

This has been of limited use on its own, but it has been fairly useful in conjunction with declaration-site variance for params in generic types. Other than a few solvable issues related to function dispatching and the complexity of type checking, it hasn't been particularly problematic, and it hasn't caused my programs to degenerate into complete nonsense.

I've seen a few tangentially-related properties in other type systems:

• In Java, you can have a param such as T extends A & B, which means that T must be able to do anything that A or B can do; however, this isn't a first-class type, e.g., you can't use extends A & B as a variable type. (My type system also allows param constraints, which is completely separate.)
• Haskell allows universal qualification such as forall a. (Eq a, Ord a) => a, but this serves a similar purpose to that of the previous example. In particular, it just restricts what type you can substitute in for a; the substitution is still required.
• The type system of Haskell contains all finite products and coproducts, e.g. data T = T A B and data T = TA A | TB B, but it isn't even a preorder because the type relationships are functions rather than automatic conversions. (Also note that coproducts in Haskell can be deconstructed via pattern matching, which is not a feature of my type system.)

I'd like to find more information about this property of a type system, but it seems like something that wouldn't work in most languages. Specifically, I'd like to know if it imposes some catastrophic limitation on the type system, or if there are minor changes that would make it a more powerful tool to use in programs.

Edit:

I've thought about Java a bit more, and I now have a better idea of what the similarities and differences are. tl;dr: It's still different enough to not be that helpful of a comparison.

• The presence/absence of constraints on param T define a "meta-type" for T, if you look at T as a variable that holds a type.
• T extends A & B means that sup T = A∧B. You can assign any type T2 to T as long as T2≤A and T2≤B. (Assuming that T2 is meet prime, which it usually is.)
• T super A & B means that inf T = A∨B. You can assign any type T2 to T as long as A≤T2 and B≤T2. (Assuming that T2 is join prime, which it usually is.)
• Without constraints, ∨∅ ≤ T ≤ ∧∅.
• As far as I know, something like A∧(B∨C) isn't possible, and doesn't really make sense.