The proper type for callCC would be rank-3. The current form is an under-approximation that only allows you to choose to use the continuation at one type.
Going higher rank (usefully) is still pretty straight-forward. There is the Mendler-style encoding of functors that gets used every once in a while in recursion-schemes work. It adds a rank to get rid of a Functor constraint. This is basically replacing a functor f with (forall b. (a -> b) -> f b), which is the same as the Yoneda f a newtype.
For more information, see some of the lovely examples in
https://www.ioc.ee/~tarmo/papers/msfp08.pdf like
update ::
(forall c’. (forall y’. (y’ -> c’) -> (y’ -> Mu f) -> f y’ -> c’)
-> y -> c’)
-> (Mu f -> c)
-> (forall c’. (forall y’. (y’ -> c) -> (y’ -> c’) -> f y’ -> c’)
-> y -> c’)
-Edward