I'm developing a type constructor class and want the constraint forall a. Monoid (m a) (where m :: * -> * ), which is neither legal Haskell, nor supported by GHC.

As a work-around, I used the first encoding suggested in "Simulating Quantified Class Constraints" (Valery Trifonov, Haskell Workshop '03). Add a type class

    class Monoid_f m where
      mempty_f :: forall a. m a
      mappend_f :: forall a. m a -> m a -> m a

and an instance *schema*

    -- instance Monoid_f f where { mempty_f = mempty ; mappend_f = mappend }

to instantiate manually wherever necessary. For instance,

    instance Monoid_f [] where { mempty_f = mempty ; mappend_f = mappend }

The paper's second approach is to replace the schema and multiple instantiations with a single instance.

    instance Monoid_f f => Monoid (f a) where
      { mempty = mempty_f ; mappend = mappend_f }

As the paper points out,

Unfortunately, due to the type variable f in the head of the instance type, this declaration is not in Haskell 98; however, at least two implementations support extensions allowing such declarations.

Sadly, this solution runs into the problem of instance selection based only on head-matching, not back-chaining into constraints. For instance, I'd like also to use the following "conflicting" declaration.

    instance (Applicative f, Monoid a) => Monoid (f a) where
      mempty = pure mempty
      mappend = liftA2 mappend

What's the state of thinking & doing with regard to universally quantified class constraints?

Note that hereditary Harrop formulas do include universally quantified goals. Less ambitiously, I think GHC's type-checker already deals with universally-quantified variables, so perhaps quantified constraints are not a great reach (just guessing).

Cheers, - Conal