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
).