{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeApplications #-}

import Data.Proxy
import GHC.TypeLits
import Data.Constraint
import Unsafe.Coerce

data Box (xs::[*]) = forall n a . (KnownNat n, Elem n xs ~ a) => Box (Proxy n) a


type family Elem (n::Nat) (xs::[k]) = result where
  Elem 0 (a ': _)  = a
  Elem n (a ': as) = Elem (n-1) as

type family ForAll (cxt :: * -> Constraint) (xs :: [k]) :: Constraint where
  ForAll ctx '[] = ()
  ForAll ctx (x ': xs) = (ctx x, ForAll ctx xs)

data CBox ctx (xs::[*]) where
  Z :: CBox ctx '[]
  S :: Dict (ctx a) -> CBox ctx as -> CBox ctx (a ': as)

class MkCBox ctx xs where mkCB :: Proxy ctx -> Proxy xs -> CBox ctx xs
instance MkCBox ctx '[] where mkCB _ _ =  Z
instance (ctx x, MkCBox ctx xs) => MkCBox ctx (x ': xs) where mkCB ctx p = S Dict (mkCB ctx (Proxy :: Proxy xs))

ithCBox :: forall ctx xs n a . (KnownNat n, Elem n xs ~ a) => Proxy n -> CBox ctx xs -> Dict (ctx a)
ithCBox pn cb = go i cb
  where i = natVal pn
        go :: Integer -> CBox ctx zs -> Dict (ctx a)
        go 0 (S d _) = unsafeCoerce d
        go i (S _ r) = go (i-1) r
        go _ _ = error "Wooooo!"

applyCBox :: Proxy ctx -> CBox ctx xs -> Box xs -> (forall a. ctx a => a -> t) -> t
applyCBox _ cbox box f = case box of
  Box p x -> case ithCBox p cbox of
               Dict -> f x

withBox :: (MkCBox ctx xs, ForAll ctx xs) => Proxy ctx -> Box xs -> (forall a. ctx a => a -> t) -> t
withBox ctx box = applyCBox ctx cbox box where cbox = mkCB ctx (Proxy :: Proxy xs)


{-
type family ForAll1 (cxt :: * -> Constraint) (xs :: [k]) :: [Constraint] where
  ForAll1 ctx '[] = '[]
  ForAll1 ctx (x ': xs) = (ctx x) ': (ForAll1 ctx xs)

type family ForAll2 (cxt :: * -> Constraint) (xs :: [k]) :: [(*,Constraint)] where
  ForAll2 ctx '[] = '[]
  ForAll2 ctx (x ': xs) = '(x, ctx x) ': (ForAll2 ctx xs)

class MkD (c::Constraint) a where mkD :: proxy a -> Dict c
instance ctx => MkD ctx (a ': as) where mkD _ = Dict
instance MkD (ctx a) as => MkD (ctx a) (b ': as) where mkD p = mkD (Proxy :: Proxy as)

class MkD (ctx a) a => A (ctx :: * -> Constraint) (a :: *)
instance MkD (ctx a) a => A ctx a
-}

{-
q :: forall ctx xs t. ForAll (A ctx) xs => Proxy (ctx :: * -> Constraint) -> Box xs -> (forall a. ctx a => a -> t) -> t
q pctx box f = case box of
    Box (n::Proxy n) (x::a) -> case mkD (Proxy :: Proxy (Elem n xs)) of
      (Dict :: Dict (ctx a)) -> f x
-}

{-
t :: Proxy xs -> ctx -> (Proxy n -> (foral a . ctx a => a -> t) -> t)
t
-}

{-
class Has ctx x xs
instance ctx x => Has ctx x (x ':xs)
instance Has ctx x xs => Has ctx x (y ':xs)
-}

{-
q :: (ForAll ctx xs, Elem (n::Nat) xs ~ a, Has ctx a xs) => Proxy ctx -> Proxy xs -> Proxy n -> Proxy a -> Dict (ctx a)
q _ _ _ _ = Dict
-}

p :: ((a ': as) ~ xs, ForAll ctx xs) => Proxy ctx -> Proxy xs -> Dict (ctx a)
p _ _ = Dict