GHC accepts ambiguous type

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, PolyKinds, ConstraintKinds, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}

import Data.Kind (Constraint)

class ElimList (c :: k -> Constraint) (l :: [k]) where
    elimList :: f '[] -> (forall (x :: k) (xs :: [k]). c x => ElimList c xs => f xs -> f (x : xs)) -> f l

GHC-9.0, 9.2 and 9.4 accept the following, GHC-8.10 and previous doens't.

The type is ambiguous, as c can vary. It's made clear if we want to define instances for that class:

instance ElimList c '[] where
    elimList fNil _ = fNil

instance (c x, ElimList c xs) => ElimList c (x : xs) where
    elimList fNil fCons = fCons (elimList fNil fCons)

the nil case is fine, but the recursive case (as all other use-sites of elimList) fail with

Ambiguous.hs:15:34: error:
    • Could not deduce (ElimList c0 xs)
        arising from a use of ‘elimList’

and have to be "fixed" by using type-applications:

instance (c x, ElimList c xs) => ElimList c (x : xs) where
    elimList fNil fCons = fCons (elimList @_ @c fNil fCons)

(first argument is k).