Lifting an instance of an element to a type-level list instance with functionnal dependencies

Let's suppose I have a Coproduct data type whose constructor has kind Coproduct :: [*] -> * . I also have a class

class MyFun s x | x -> s where
  myFun :: s -> x

Whenever I have a list of types xsthat contains some type x, I want to get an instance of the form instance MyFun s x => MyFun s (Coproduct xs)

My attempts

I've written the following type families :

type family SplitAt (x :: a) (xs :: [a]) :: ([a], [a]) where
  SplitAt x '[] = '( '[] , '[] )
  SplitAt x (x ': q) = '( '[], q)
  SplitAt x (y ': q) = '( y ': Fst (SplitAt x q), Snd (SplitAt y q))

type family ConcatWith (x :: a) (s :: ([a], [a])) :: [a] where
  ConcatWith x '( '[], xs) = x ': xs
  ConcatWith x '(y ': q, xs) = y ': ConcatWith x '(q, xs)

type family Fst (p :: (a, b)) :: a where
  Fst '(a, b) = a

type family Snd (p :: (a, b)) :: b where
  Snd '(a, b) = b

Attempt 1 : Now I would like to write the following instance :

instance (MyFun s x, b ~ ConcatWith x (SplitAt x xs)) => MyFun s (Coproduct b) where
  myFun = -- irrelevant code after this

However, I get this error :

Illegal instance declaration for ‘MyFun s 
(Coproduct b)’
        The liberal coverage condition fails in class 
‘MyFun’
          for functional dependency: ‘m -> s’
        Reason: lhs type ‘Coproduct b’ does not 
determine rhs type ‘s’
        Un-determined variable: s
    • In the instance declaration for ‘MyFun s 
(Coproduct b)’

I understand why I get this error : GHC fails to see that the list b must contain xsomewhere and therefore fails to retrieves the functional dependency inherited from the instance for x.

Attempt 2 : I also tried to achieve the same thing using the TypeFamilies extension, by writing

class MyFun x where
  type ArgMyFun x
  myFun :: ArgMyFun x -> x

instance (MyFun x, b ~  ConcatWith x (SplitAt x xs)) => MyFun (Coproduct b) where
  type ArgMyFun (Coproduct (ConcatWith b)) = ArgMyFun x
  myFun = -- ...

But again, this (understandably) fails

error:
    The RHS of an associated type declaration 
mentions out-of-scope variable ‘x’
      All such variables must be bound on the LHS

Again, the error message couldn't be clearer and I understand why this doesn't work.

Hack 1 :

The only (atrocious) workaround I managed to find is the following instance for functional dependencies :

instance (MyFun s x)
  => MyFun s (Either x (Coproduct xs)) where
  myFun x = --...

which artificially puts x explicitely in the type and then only use the Rightpart of Either. However, this is obviously ugly and not what I was aiming for.

Functional dependencies just don't work very well, and you should probably avoid them. For example, the following program implements a possible ElemDep instance for Coproducts using overlapping instances, and the example main illustrates that GHC will happily let you violate the functional dependency. (I think it's an example of issue 10675.)

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}

type Coproduct :: [*] -> *
data Coproduct tys where
  Inject :: x -> Coproduct (x:xs)
  Reject :: Coproduct xs -> Coproduct (x:xs)
deriving instance (Show x, Show (Coproduct xs)) => Show (Coproduct (x:xs))
deriving instance (Show (Coproduct '[]))

class ElemDep x xs | xs -> x where
  inject :: x -> xs
instance {-# OVERLAPPING #-} ElemDep x (Coproduct (x ': xs)) where
  inject = Inject
instance {-# OVERLAPPABLE #-} ElemDep x (Coproduct xs) => ElemDep x (Coproduct (y ': xs)) where
  inject = Reject . inject

main = do
  print (inject 15    :: Coproduct '[Int, Bool])
  print (inject False :: Coproduct '[Int, Bool])

I still don't think I understand what you're trying to do, even after all the discussion in the comments, but if you've got some situation where every possible Coproduct xs has a specific x in xs that you want to select for your ElemDep class, I think your best bet is to use type families:

class ElemDep xs where
  type family Injector xs
  inject :: Injector xs -> xs

and, critically, write a complete type program to programmatically calculate the appropriate x for a given Coproduct xs by deferring to a standalone type family:

-- instance for coproducts
instance ElemDep (Coproduct xs) where
  type Injector (Coproduct xs) = CoproductInjector xs

-- delegated injector type for coproducts
type CoproductInjector :: [*] -> *
type family CoproductInjector xs where
  CoproductInjector ((x, y) ': xs) = (x, y)
  CoproductInjector (Bool ': x ': xs) = x
  CoproductInjector (x ': xs) = CoproductInjector xs

This example finds the first pair in the list, or the first type that follows a Bool type. It's nonsense of course, but it illustrates that you can write any sort of reasonable type program to do the job. Even an exhaustive list of cases might be an option:

type CoproductInjector :: [*] -> *
type family CoproductInjector xs where
  CoproductInjector '[Int, Bool] = Int
  CoproductInjector '[Bool] = Bool
  CoproductInjector '[Bool, Int] = Int

(One thing you certainly can't do is write a type program to find the first type x that has a MyFun instance. Types can't be calculated based on the existence or absence of instances. You'll have to come up with some other type-level method of determining x.)

Anyway, once you've got that taken care of, it's possible to write a reasonable instance. You'll need a helper class, basically a variant of my first example without the fundep and tailored to coproducts:

class CoproductElemDep x xs where
  coproductInject :: x -> Coproduct xs
instance {-# OVERLAPPING #-} CoproductElemDep x (x ': xs) where
  coproductInject = Inject
instance {-# OVERLAPPABLE #-} CoproductElemDep x xs => CoproductElemDep x (y ': xs) where
  coproductInject = Reject . coproductInject

and then the Coproduct instance for ElemDep can be written:

instance (CoproductElemDep (CoproductInjector xs) xs) => ElemDep (Coproduct xs) where
  type Injector (Coproduct xs) = CoproductInjector xs
  inject = coproductInject

The full code, with some examples:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

type Coproduct :: [*] -> *
data Coproduct tys where
  Inject :: x -> Coproduct (x:xs)
  Reject :: Coproduct xs -> Coproduct (x:xs)
deriving instance (Show x, Show (Coproduct xs)) => Show (Coproduct (x:xs))
deriving instance (Show (Coproduct '[]))

class ElemDep xs where
  type family Injector xs
  inject :: Injector xs -> xs

class CoproductElemDep x xs where
  coproductInject :: x -> Coproduct xs
instance {-# OVERLAPPING #-} CoproductElemDep x (x ': xs) where
  coproductInject = Inject
instance {-# OVERLAPPABLE #-} CoproductElemDep x xs => CoproductElemDep x (y ': xs) where
  coproductInject = Reject . coproductInject

instance (CoproductElemDep (CoproductInjector xs) xs) => ElemDep (Coproduct xs) where
  type Injector (Coproduct xs) = CoproductInjector xs
  inject = coproductInject

-- type program to find x to inject into coproducts
type CoproductInjector :: [*] -> *
type family CoproductInjector xs where
  CoproductInjector ((x, y) ': xs) = (x, y)
  CoproductInjector (Bool ': x ': xs) = x
  CoproductInjector (x ': xs) = CoproductInjector xs

-- other instances for injection
instance ElemDep Double where
  type Injector Double = Int
  inject = fromIntegral

main = do
  -- injects Int into Double
  print (inject 8     :: Double)
  -- injects (Int,Int) into Coproduct (first pair)
  print (inject (1,2) :: Coproduct '[Double, (Char,String,Bool), (Int,Int), Bool, Double])
  -- injects String into Coproduct (first type after Bool)
  print (inject "hello" :: Coproduct '[Int, Bool, String, Bool, Double])