This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE | |
DataKinds, | |
DeriveGeneric, | |
PolyKinds, | |
StandaloneDeriving, | |
TypeFamilies, | |
UndecidableInstances #-} | |
module T where | |
import Data.Kind (Constraint, Type) | |
import Data.Void | |
import GHC.Generics | |
import GHC.TypeLits | |
data KeyValueX x = | |
KVX (X "KVX" x) String (DataX x) | | |
KeyValueX (X "KeyValueX" x) | |
deriving Generic | |
data DataX x = | |
NullX (X "NullX" x) | | |
IntX (X "IntX" x) Int | | |
NumX (X "NumX" x) Double | | |
BoolX (X "BoolX" x) Bool | | |
StringX (X "StringX" x) String | | |
ArrayX (X "ArrayX" x) [DataX x] | | |
ObjectX (X "ObjectX" x) [KeyValueX x] | | |
DataX (X "DataX" x) | |
deriving Generic | |
-- | |
type family X (s :: k) (x :: l) :: Type | |
-- | |
type ForAllX c x = (AllX c (CNames (DataX x)) x, AllX c (CNames (KeyValueX x)) x) | |
deriving instance ForAllX Eq x => Eq (DataX x) | |
deriving instance ForAllX Eq x => Eq (KeyValueX x) | |
-- | |
data UD | |
type X s UD = XUD s | |
type family XUD (s :: Symbol) :: Type where | |
XUD "KeyValueX" = Void | |
XUD "DataX" = Void | |
XUD _ = () | |
-- | |
type CNames a = GCNames (Rep a) | |
type family GCNames (f :: Type -> Type) :: [Symbol] where | |
GCNames (M1 D c f) = GCNames f | |
GCNames (f :+: g) = GCNames f ++ GCNames g | |
GCNames (M1 C (MetaCons name _ _) f) = '[name] | |
type family (xs :: [k]) ++ (ys :: [k]) :: [k] where | |
'[] ++ ys = ys | |
(x ': xs) ++ ys = x ': (xs ++ ys) | |
type family AllX (c :: Type -> Constraint) (xs :: [Symbol]) (x :: l) :: Constraint where | |
AllX c '[] x = () | |
AllX c (s ': ss) x = (c (X s x), AllX c ss x) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment