AutomaticInjection.hs

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wall #-}

import Data.Proxy

data Sum (fs :: [* -> *]) a where
  Sum :: Either (f a) (Sum fs a) -> Sum (f ': fs) a

data IsHead :: k -> [k] -> * where
  IsHead :: IsHead f (f : fs)
  NotHead :: Inject f fs => IsHead f (f' : fs)

class Inject (f :: * -> *) (fs :: [* -> *]) where
  inject :: f a -> Sum fs a

type family IsEq (a :: k) (b :: k) :: Bool where
  IsEq a a = 'True
  IsEq a b = 'False

class ComputeIsHead' (f :: * -> *) (f' :: * -> *) (fs :: [* -> *]) (isEq :: Bool) where
  computeIsHead' :: Proxy f -> Proxy f' -> Proxy fs -> Proxy isEq -> IsHead f (f' : fs)

instance ComputeIsHead' f f fs 'True where
  computeIsHead' _ _ _ _ = IsHead

instance Inject f fs => ComputeIsHead' f f' fs 'False where
  computeIsHead' _ _ _ _ = NotHead

class ComputeIsHead f f' fs where
  computeIsHead :: IsHead f (f' : fs)

instance ComputeIsHead' f f' fs (IsEq f f') => ComputeIsHead f f' fs where
  computeIsHead = computeIsHead' (Proxy :: Proxy f)
                                 (Proxy :: Proxy f')
                                 (Proxy :: Proxy fs)
                                 (Proxy :: Proxy (IsEq f f'))

instance ComputeIsHead f f' fs => Inject f (f' : fs) where
  inject :: forall a. f a -> Sum (f' : fs) a
  inject fa = case computeIsHead :: IsHead f (f' : fs) of
                IsHead  -> Sum $ Left fa
                NotHead -> lift (inject fa)
    where
      lift :: Sum fs a -> Sum (f' : fs) a
      lift = Sum . Right

test1 :: Sum [IO, Maybe] ()
test1 = inject (print "hi")

test2 :: Sum [IO, Maybe] ()
test2 = inject (Just ())

-- Error: No instance for (Inject [] '[]) arising from a use of ‘inject’
-- test3 :: Sum [IO, Maybe] ()
-- test3 = inject [()]