{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Data.TypedEncoding.Combinators.Promotion where
import Data.TypedEncoding.Common.Class
import Data.TypedEncoding.Common.Util.TypeLits
import Data.TypedEncoding.Common.Types (Enc(..) )
import Data.TypedEncoding.Combinators.Unsafe (withUnsafeCoerce)
demoteFlattenTop :: forall y x xs c str . (IsSuperset y x ~ 'True) => Enc (x ': y ': xs) c str -> Enc (x ': xs) c str
demoteFlattenTop :: Enc @[Symbol] ((':) @Symbol x ((':) @Symbol y xs)) c str
-> Enc @[Symbol] ((':) @Symbol x xs) c str
demoteFlattenTop = (str -> str)
-> Enc @[Symbol] ((':) @Symbol x ((':) @Symbol y xs)) c str
-> Enc @[Symbol] ((':) @Symbol x xs) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
promoteUnFlattenTop :: forall y x xs c str . (IsSuperset y x ~ 'True) => Enc (x ': xs) c str -> Enc (x ': y ': xs) c str
promoteUnFlattenTop :: Enc @[Symbol] ((':) @Symbol x xs) c str
-> Enc @[Symbol] ((':) @Symbol x ((':) @Symbol y xs)) c str
promoteUnFlattenTop = (str -> str)
-> Enc @[Symbol] ((':) @Symbol x xs) c str
-> Enc @[Symbol] ((':) @Symbol x ((':) @Symbol y xs)) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
demoteRemoveTop :: forall y x xs c str . (IsSuperset y x ~ 'True) => Enc (y ': x ' : xs) c str -> Enc (x ': xs) c str
demoteRemoveTop :: Enc @[Symbol] ((':) @Symbol y ((':) @Symbol x xs)) c str
-> Enc @[Symbol] ((':) @Symbol x xs) c str
demoteRemoveTop = (str -> str)
-> Enc @[Symbol] ((':) @Symbol y ((':) @Symbol x xs)) c str
-> Enc @[Symbol] ((':) @Symbol x xs) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
promoteAddTop :: forall y x xs c str . (IsSuperset y x ~ 'True) => Enc (x ': xs) c str -> Enc (y ': x ' : xs) c str
promoteAddTop :: Enc @[Symbol] ((':) @Symbol x xs) c str
-> Enc @[Symbol] ((':) @Symbol y ((':) @Symbol x xs)) c str
promoteAddTop = (str -> str)
-> Enc @[Symbol] ((':) @Symbol x xs) c str
-> Enc @[Symbol] ((':) @Symbol y ((':) @Symbol x xs)) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
demoteRemoveBot :: (UnSnoc xs ~ '(,) ys y, UnSnoc ys ~ '(,) zs x, IsSuperset y x ~ 'True) => Enc xs c str -> Enc ys c str
demoteRemoveBot :: Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str
demoteRemoveBot = (str -> str) -> Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
promoteAddBot :: forall y x xs c str ys . (UnSnoc xs ~ '(,) ys x, IsSuperset y x ~ 'True) => Enc xs c str -> Enc (Snoc xs y) c str
promoteAddBot :: Enc @[Symbol] xs c str -> Enc @[Symbol] (Snoc @Symbol xs y) c str
promoteAddBot = (str -> str)
-> Enc @[Symbol] xs c str
-> Enc @[Symbol] (Snoc @Symbol xs y) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
demoteFlattenBot :: (UnSnoc xs ~ '(,) ys x, UnSnoc ys ~ '(,) zs y, IsSuperset y x ~ 'True) => Enc xs c str -> Enc (Snoc zs x) c str
demoteFlattenBot :: Enc @[Symbol] xs c str -> Enc @[Symbol] (Snoc @Symbol zs x) c str
demoteFlattenBot = (str -> str)
-> Enc @[Symbol] xs c str
-> Enc @[Symbol] (Snoc @Symbol zs x) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id
promoteUnFlattenBot :: forall y x xs c str ys . (UnSnoc xs ~ '(,) ys x, IsSuperset y x ~ 'True) => Enc xs c str -> Enc (Snoc (Snoc ys y) x) c str
promoteUnFlattenBot :: Enc @[Symbol] xs c str
-> Enc @[Symbol] (Snoc @Symbol (Snoc @Symbol ys y) x) c str
promoteUnFlattenBot = (str -> str)
-> Enc @[Symbol] xs c str
-> Enc @[Symbol] (Snoc @Symbol (Snoc @Symbol ys y) x) c str
forall k1 k2 s1 s2 (e1 :: k1) c (e2 :: k2).
(s1 -> s2) -> Enc @k1 e1 c s1 -> Enc @k2 e2 c s2
withUnsafeCoerce str -> str
forall a. a -> a
id