I think ultimately the two views of levity that we've been talking diverge along the same lines as the pi vs forall discussion from your Levity polymorphism talk.
I've been focused entirely on situations where forall suffices, and no distinction is needed in how you compile for both levities.
Maybe could be polymorphic using a mere forall in the levity of the boxed argument it carries as it doesn't care what it is, it never forces it, pattern matching on it just gives it back when you pattern match on it.
Eq or Ord could just as easily work over anything boxed. The particular Eq _instance_ needs to care about the levity.
Most of the combinators for working with Maybe do need to care about that levity however.
e.g. consider fmap in Functor, the particular instances would care. Because you ultimately wind up using fmap to build 'f a' values and those need to know how the let binding should work. There seems to be a pi at work there. Correct operational behavior would depend on the levity.
But if we look at what inference should probably grab for the levity of Functor:
you'd get:
class Functor (l : Levity) (l' : Levity') (f :: GC l -> GC l') where
fmap :: forall a b. (a :: GC l) (b :: GC l). (a -> b) -> f a -> f b
Baed on the notion that given current practices, f would cause us to pick a common kind for a and b, and the results of 'f'. Depending on how and if we decided to default to * unless annotated in various situations would drive this closer and closer to the existing Functor by default.
These are indeed distinct functors with distinct operational behavior, and we could implement each of them by supplying separate instances, as the levity would take part in the instance resolution like any other kind argument.
Whether we could expect an average Haskeller to be willing to do so is an entirely different matter.
-Edward