"Lower-bounded" universal quantification

[probeiuscorp]

Ideally typeclassing can be flattened, such that in

class Eq a
  eq: a -> a -> Bool

eq has type forall a: Eq. a -> a -> Bool. The problem is the flattening does not work when the typeclass parameter is used multiple times, as eq does. Its current definition would allow usages like this:

eq "Hello" 42

where a is inferred as String + Num. However, a usage like:

eq None $ Some 42

should be allowed, where a is inferred as None + Some Num.

---

A related problem is inspecting type constructors, such as which of these should be valid and how the compiler would know:

type Maybe = a. Some a + None
instance Functor Maybe

type Maybe2 = Maybe
instance Functor Maybe2

type Maybe3 = a. Maybe a
instance Functor Maybe3