{-# LANGUAGE 
    MultiParamTypeClasses,FunctionalDependencies,FlexibleInstances,FlexibleContexts,
    UndecidableInstances,OverlappingInstances,NoMonomorphismRestriction,Rank2Types,
    TypeOperators,EmptyDataDecls,KindSignatures,TypeFamilies
    #-}
module FunDepError (x) where 

data O = O deriving Show
data S n = S n deriving Show

class Sub a b c | a b -> c where
  sub :: a -> b -> c
instance Sub n n O where sub _ _ = O
instance Sub (S n) n (S O) where sub _ _ = S O
instance Sub (S (S n)) n (S (S O)) where sub _ _ = S (S O)
instance Sub (S (S (S n))) n (S (S (S O))) where sub _ _ = S (S (S O))


data xs :> x = xs :> x
data Nil = Nil


class HList xs n | xs -> n where
  len :: xs -> n
instance HList xs n => HList (xs :> x) (S n) where
  len ~(xs :> x) = S (len xs)
instance HList Nil O where
  len _ = O


class Pickup xs n s | xs n -> s where
  pickup :: xs -> n -> s
instance (HList xs l, Sub l (S n) m, PickupR xs m s)
    => Pickup xs n s where
  pickup xs n = pickupR xs (sub (len xs) (S n))

class PickupR xs n s | xs n -> s where
  pickupR :: xs -> n -> s
instance xs ~ (xs':>t) => PickupR xs O t where
  pickupR (_ :> t) _ = t
instance (PickupR xs' n t, xs ~ (xs':>s')) => PickupR xs (S n) t where
  pickupR (xs' :> _) (S n) = pickupR xs' n

class Update xs n t xs' | xs n t -> xs' where
  update :: xs -> n -> t -> xs'
instance (HList xs l, Sub l (S n) m, UpdateR xs m t xs') 
 => Update xs n t xs' where
  update xs n t = updateR xs (sub (len xs) (S n)) t

class UpdateR xs n t xs' | xs n t -> xs' where
  updateR ::  xs -> n -> t -> xs'
instance UpdateR (xs:>s) O t (xs:>t) where
  updateR (xs:>_) _ t = xs :> t
instance UpdateR xs n t xs' => UpdateR (xs:>s) (S n) t (xs':>s) where
  updateR (xs:>s) (S n) t = updateR xs n t :> s

newtype F a = F a
data U = U
newtype a :-> b = Arr { ext :: a -> IO b }


newtype LLC t ii jj a = LLC { run' :: ii -> IO (jj,a) }

run :: forall a n jj. (forall t. LLC t Nil Nil a) -> IO a
run s = case s of LLC m -> m Nil >>= \(_,a) -> return a

newtype Var n = Var n

infixr 6 :->

class Consume ii jj where
  consume :: ii -> jj
instance Consume Nil Nil where
  consume _ = Nil
instance Consume ii jj => Consume (ii:>F a) (jj:>F a) where
  consume (ii:>i) = consume ii :> i
instance Consume ii jj => Consume (ii:>F a) (jj:>U) where
  consume (ii:>_) = consume ii :> U

lam :: (HList ii n, Consume ii jj) => (Var n -> LLC t (ii:>F a) (jj:>U) b) -> LLC t ii jj (a :-> b)
lam f = LLC (\ii -> return (consume ii, Arr $ \a -> run' (f (Var $ len ii)) (ii:>F a) >>= \(_,b) -> return b))

var :: (Pickup ii n (F a), Update ii n U jj) => Var n -> LLC t ii jj a
var (Var n) = LLC (\ii -> return (update ii n U, case pickup ii n of F x -> x))

x = lam (\a -> lam (\b -> var a))