module Data.Schematic.Utils where
import Data.Proxy
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Data.Vinyl hiding (Dict)
class Known a where
known :: a
instance Known (Proxy a) where
known = Proxy
instance KnownNat n => Known (Sing n) where
known = SNat
instance KnownSymbol s => Known (Sing s) where
known = SSym
instance (Known (Sing a), Known (Sing b)) => Known (Sing '(a,b)) where
known = STuple2 known known
instance Known (Sing '[]) where known = SNil
instance (Known (Sing a), Known (Sing as)) => Known (Sing (a ': as)) where
known = SCons known known
instance Known (Rec Sing '[]) where
known = RNil
instance (Known (Sing a), Known (Rec Sing tl)) => Known (Rec Sing (a ': tl)) where
known = known :& known
data Dict c where
Dict :: c => Dict c
instance c => Known (Dict c) where
known = Dict