It does feel a little clunky. The current definition of "Eq1" is "class (forall a. Eq a => Eq (f a)) => Eq1 (f :: Type -> Type)", but I noticed that if we write type Eq1' :: (Type -> Type) -> Constraint type Eq1' f = forall a. (Eq a) => Eq (f a) func :: (Eq a, Eq1' f) => [f a] -> Bool func = allEqual That works with no problem. I wonder if they would ever redefine "Eq1" in that way or if that would cause any problems