Why is UndecidableInstances not required here, for instance C1

Trying this in other contexts requires the extension (which seems right), but not here:

{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Data.Kind (Type)

class (forall a. c a => c (f a)) => C1 c f
-- Why can I do this without UndecidableInstances?:
instance (forall a. c a => c (f a)) => C1 c f
-- As opposed to requiring
--instance C1 Eq Maybe

---------- below just demonstrates using above

data AnnBoolExpFld backend leaf =
    AVAggregationPredicates Int (AggregationPredicates backend leaf)

class (C1 Eq (AggregationPredicates b)) => Backend b where
  type AggregationPredicates b :: Type -> Type

instance Backend Int where
  type AggregationPredicates Int = Maybe

deriving instance (Eq a, Backend b) =>  Eq (AnnBoolExpFld b a)

main = print $
  AVAggregationPredicates 1 (Just 1) == (AVAggregationPredicates 1 (Just 1) :: AnnBoolExpFld Int Int )

EDIT: some relevant discussion here https://www.reddit.com/r/haskell/comments/1eh2ic8/comment/lgsgr95/

It may be this issue. Termination checking is buggy for type classes with invisible arguments (including polykinded type classes). With the inferred type:

type C1 :: (k -> Constraint) -> (k -> k) -> Constraint

the instance is accepted. If you add an explicit kind signature, like type C1 :: (Type -> Constraint) -> (Type -> Type) -> Constraint, the instance is rejected with the expected error:

Foo.hs:10:10: error:
    • The constraint ‘c (f a)’
        is no smaller than the instance head ‘C1 c f’
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘C1 c f’
   |
10 | instance (forall a. c a => c (f a)) => C1 c f
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^