import Prelude hiding ((!!))
import GHC.TypeLits
import Data.Proxy
import qualified Data.Map as M
 
newtype Map (k :: [Nat]) v = Map [v]
  deriving Show

empty :: Map '[] a
empty = Map []

add :: Proxy k -> v -> Map ks v -> Map (k ': ks) v
add _ v (Map xs) = Map (v:xs)

class KnownNat k => Ke (k :: Nat) (ks :: [Nat]) v where
  (!!) :: Proxy k -> Map ks v -> v

instance KnownNat k => Ke k (k ': ks) v where
  _ !! (Map (x:_)) = x

instance Ke k ks v => Ke k (h ': ks) v where
  k' !! (Map (_:xs)) = k' !! (Map xs :: Map ks v)

g :: Map [3, 10, 1] String
g = add (undefined :: Proxy 3)  "baz"
  $ add (undefined :: Proxy 10) "bar"
  $ add (undefined :: Proxy 1)  "foo"
  $ empty

v1 = (undefined :: Proxy 10) !! g
v2 = (undefined :: Proxy 3) !! g
v3 = (undefined :: Proxy 1) !! g
-- Type Error: v4 = (undefined :: Sing 2) !! g


--

data SMap (k :: [Symbol]) v = SMap [v] (M.Map String v)
  deriving Show

class KnownSymbol k => Ma (k :: Symbol) (ks :: [Symbol]) v where
  (!) :: Proxy k -> SMap ks v -> v
  (!?) :: Proxy k -> SMap ks v -> Maybe v

instance KnownSymbol k => Ma k (k ': ks) v where
  _ !  (SMap (x:_) _) = x
  _ !? (SMap (x:_) _) = Just x

instance Ma k ks v => Ma k (h ': ks) v where
  k' !  (SMap (_:xs) m) = k' ! (SMap xs m :: SMap ks v)
  k' !? (SMap (_:xs) m) = k' !? (SMap xs m :: SMap ks v)

instance KnownSymbol k => Ma k '[] v where
  _  !  (SMap _ _) = undefined
  k' !? (SMap _ m) = M.lookup (symbolVal k') m

emptys :: SMap '[] a
emptys = SMap [] M.empty

adds :: Proxy k -> v -> SMap ks v -> SMap (k ': ks) v
adds _ v (SMap xs m) = SMap (v:xs) m

addo :: String -> v -> SMap ks v -> SMap ks v
addo k v (SMap vs m) = SMap vs $ M.insert k v m
type HTTPHeaders = SMap ["connection", "accept", "host"] String

httpIn :: HTTPHeaders
httpIn = adds (undefined :: Proxy "connection") "keep-alive"
       $ adds (undefined :: Proxy "accept")     "text/plain"
       $ adds (undefined :: Proxy "host")       "maxs.io"
       $ addo "content-length"                  "9001"
       $ emptys

m1 = (undefined :: Proxy "host") ! httpIn
m2 = (undefined :: Proxy "content-length") !? httpIn
