{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
module Data.TypedEncoding.Common.Types.SomeEnc where
import Data.TypedEncoding.Common.Types.Enc
import Data.TypedEncoding.Common.Class.Util
import Data.TypedEncoding.Common.Types.SomeAnnotation
import Data.TypedEncoding.Common.Types.CheckedEnc
data SomeEnc conf str where
MkSomeEnc :: SymbolList xs => Enc xs conf str -> SomeEnc conf str
withSomeEnc :: SomeEnc conf str -> (forall xs . SymbolList xs => Enc xs conf str -> r) -> r
withSomeEnc (MkSomeEnc enc) f = f enc
toSome :: SymbolList xs => Enc xs conf str -> SomeEnc conf str
toSome = MkSomeEnc
someToChecked :: SomeEnc conf str -> CheckedEnc conf str
someToChecked se = withSomeEnc se toCheckedEnc
checkedToSome :: CheckedEnc conf str -> SomeEnc conf str
checkedToSome (UnsafeMkCheckedEnc xs c s) = withSomeAnnotation (someAnnValue xs) (\p -> MkSomeEnc (UnsafeMkEnc p c s))
instance (Show c, Displ str) => Displ (SomeEnc c str) where
displ (MkSomeEnc en) =
"Some (" ++ displ en ++ ")"