Bulat Ziganshin wrote:

sequence :: [m a] -> m [a] | Monad m

I think translations of higher rank signatures using this syntax could be: foo :: (forall a. a-> a) ->b -> c -> (b,c) ==> foo :: (a -> a | a) -> b -> c -> (b, c) using the rule that we just write the variable by itself to indicate the quantification point. With restricted quantification, bar :: forall m a b. MonadIO m => (forall n. MonadIO n => a -> n b) -> a -> m b ==> bar :: (a -> n b | n, MonadIO n) -> a -> m b | a, b, m, MonadIO m Perhaps some rules could be devised to automatically determine the quantification point of each variable so it might even be possible to write the above as: bar :: (a -> n b | MonadIO n) -> a -> m b | MonadIO m though for MPTC it's no longer clear from a restriction which variable(s) are being introduced and which are being used as the basis for restricting them, hence explicit quantification as above is probably unavoidable for the general case. Neil Mitchell wrote:

How about name, context, value as the three elements:

class <name> | <context> where <value> data <name> | <context> = <value> type <name> | <context> = <value> <name> | <context> :: <value>

This would give: sequence | Monad m :: [m a] -> m [a] But this wouldn't work because here the context is separated from the rest of the type by :: whereas from the higher rank examples above it's clear that the context, which is nothing more than a(restricted) quantifier, needs to be part of the type itself. Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com