attempt to use DataKinds

Foo.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Prelude hiding ((-))

import GHC.TypeLits (Nat, type (-), type (<=))
import Data.Proxy (Proxy(Proxy))

class Foo (n :: Nat) x y | n x -> y, x y -> n where
  foo :: Proxy n -> x -> y

instance Foo 0 x x where
  foo _ x = x

reduce :: Proxy n -> Proxy (n - 1)
reduce _ = Proxy

instance (Foo (n - 1) x y, 1 <= n) => Foo n (a,x) y where
  foo n (_,x) = foo (reduce n) x

-- > :l Foo
-- *Foo> foo (Proxy :: Proxy 2) ((1,(2,3)) :: (Int,(Int,Int)))
-- 3
--

Foo2.hs

-- In order to write Eq1, could be solved by introducing additional types,
-- or using typeable:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
--In order to write type classes:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
-- In order to have parameter 'c' in IFoo, that is only on left hand side,
-- I think it could be avioded somehow, but do not see an easy way right now.
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy

-- Our own type equality, :~: will not work as we wan it's negation,
-- exists somewhere in singletons package
type family Eq1 a b :: Bool where
  Eq1 a a = True
  Eq1 a b = False

-- Class that will allow to get tail of the type we want
class Foo a b where
  foo :: Proxy b -> a -> b

-- Only one instance, because we want o catch all cases,
-- downside: foo (Proxy ::a) (a) will not work, if this
-- is needed you may to this trick again.
instance (IFoo x b c, c ~ (Eq1 x b)) => Foo (a,x) b where
  foo p (a,x) = ifoo' Proxy p x
    where ifoo' :: (IFoo x b c, (Eq1 x b) ~ c) => Proxy c -> Proxy b -> x -> b
          ifoo' = ifoo

--  Internal class
class IFoo a b (c::Bool) where
  ifoo :: Proxy c -> Proxy b -> a -> b

instance Foo a b => IFoo a b False where
  ifoo _ p a = foo p a

instance IFoo a a True where
  ifoo _ _ x = x
  
  {-
  *Main> foo (Proxy :: Proxy Int) (1::Int,(2::Int,3::Int))
3
*Main> foo (Proxy :: Proxy (Int,Int)) (1::Int,(2::Int,3::Int))
(2,3)
*Main> foo (Proxy :: Proxy (Int,(Int,Int))) (1::Int,(2::Int,3::Int))

<interactive>:74:1:
    No instance for (Foo Int (Int, (Int, Int)))
      arising from a use of ‘foo’
-}