{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.TypeMap.Internal.Unsafe
( module Data.TypeMap.Internal.Unsafe
, module Unsafe
) where
import Data.Coerce
import Data.Proxy as Unsafe (Proxy(..))
#if MIN_VERSION_base(4,10,0)
import GHC.Exts as Unsafe (Any)
#else
import GHC.Prim as Unsafe (Any)
#endif
import GHC.TypeLits as Unsafe (KnownNat)
import GHC.TypeLits (type (+), natVal)
import Unsafe.Coerce as Unsafe
type family Index (a :: k) (d :: [(k, *)]) where
Index a ('(a, _) ': _) = 0
Index a (_ ': d) = 1 + Index a d
type family Lookup (a :: k) (d :: [(k, *)]) where
Lookup a ('(a, b) ': _) = b
Lookup a (_ ': d) = Lookup a d
type family Snoc (d :: [k]) (a :: k) where
Snoc '[] a = '[a]
Snoc (x ': d) a = x ': Snoc d a
type family Last (d :: [k]) where
Last (x ': '[]) = x
Last (_ ': d) = Last d
type family Init (d :: [k]) where
Init (_ ': '[]) = '[]
Init (x ': d) = x ': Init d
unsafeIndex
:: forall a d f m
. (KnownNat (Index a d), Coercible (f Any) (m d))
=> (forall c. f c -> Int -> c)
-> m d -> Lookup a d
unsafeIndex :: (forall c. f c -> Int -> c) -> m d -> Lookup a d
unsafeIndex forall c. f c -> Int -> c
index = (f Any -> Any) -> m d -> Lookup a d
forall a b. a -> b
unsafeCoerce ((f Any -> Int -> Any) -> Int -> f Any -> Any
forall a b c. (a -> b -> c) -> b -> a -> c
flip f Any -> Int -> Any
forall c. f c -> Int -> c
index Int
na)
where
na :: Int
na = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Index a d) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Index a d)
forall k (t :: k). Proxy t
Proxy @(Index a d))) :: Int
unsafeCons
:: forall a d b f m
. (Coercible (f Any) (m d), Coercible (f Any) (m ('(a, b) ': d)))
=> (forall c. c -> f c -> f c)
-> b -> m d -> m ('(a, b) ': d)
unsafeCons :: (forall c. c -> f c -> f c) -> b -> m d -> m ('(a, b) : d)
unsafeCons = \forall c. c -> f c -> f c
x -> (Any -> f Any -> f Any) -> b -> m d -> m ('(a, b) : d)
forall a b. a -> b
unsafeCoerce Any -> f Any -> f Any
forall c. c -> f c -> f c
x
unsafeSnoc
:: forall a d b f m
. (Last d ~ '(a, b), Coercible (f Any) (m (Init d)), Coercible (f Any) (m d))
=> (forall c. f c -> c -> f c)
-> m (Init d) -> b -> m d
unsafeSnoc :: (forall c. f c -> c -> f c) -> m (Init d) -> b -> m d
unsafeSnoc = \forall c. f c -> c -> f c
x -> (f Any -> Any -> f Any) -> m (Init d) -> b -> m d
forall a b. a -> b
unsafeCoerce f Any -> Any -> f Any
forall c. f c -> c -> f c
x