(Sorry for the late reply.) apfelmus@quantentunnel.de wrote:
I'd really like to write
class (forall a . Ord p a) => OrdPolicy p where
but I guess that's (currently) not possible.
Actually, it seems that something like this can be achieved, at some price. First, I change the statement ;-) to class (forall a . Ord a => Ord p a) => OrdPolicy p since I guess this is what you really want. Then, we reify the Ord class with a GADT: data O a where O :: Ord a => O a Then, we reify the forall, using GADT+impredicativity: data O1 p where O1:: (forall a . Ord a => O (p a)) -> O1 p We can express the constraint with a class OrdAll, providing the GADT proof: class OrdAll p where ordAll :: O1 p Instances are easy to define, I think: instance OrdAll [] where ordAll = O1 O Your class becomes then: class OrdAll p => OrdPolicy p where ... Actually, using this is not exactly nice, since you have to 'instantiate' the forall on your own. For example, fooSort :: forall p a . (OrdPolicy p, Ord a) => [p a] -> [p a] fooSort = case ordAll of O1 o -> case o of (O :: O (p a)) -> sort * * * Actually, a simpler (untested) approach could be: class OrdAll p where ordAll :: Ord a => O (p a) This would make the O1 hack useless. Regards, Zun.