-
- {-# 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
-