@@ -15,7 +15,7 @@ import Data.Maybe
1515import Data.Schematic.Instances ()
1616import Data.Schematic.Utils
1717import Data.Scientific
18−import Data.Singletons.Prelude.List
18+import Data.Singletons.Prelude.List hiding (All)
1919import Data.Singletons.TH
2020import Data.Singletons.TypeLits
2121import Data.Text as T
@@ -27,6 +27,10 @@ import Prelude as P
2727import Test.SmallCheck.Series
2828
2929
30+type family All (c :: k -> Constraint) (s :: [k]) :: Constraint where
31+ All c '[] = ()
32+ All c (a ': as) = (c a, All c as)
33+
3034type family CRepr (s :: Schema) :: Type where
3135 CRepr ('SchemaText cs) = TextConstraint
3236 CRepr ('SchemaNumber cs) = NumberConstraint
@@ -38,22 +42,27 @@ data TextConstraint
3842 | TLe Nat
3943 | TGt Nat
4044 | TRegex Symbol
45+ | TEnum [Symbol]
4146 deriving (Generic)
4247
4348data instance Sing (tc :: TextConstraint) where
44− STEq :: Sing n -> Sing ('TEq n)
45− STLe :: Sing n -> Sing ('TLe n)
46− STGt :: Sing n -> Sing ('TGt n)
47− STRegex :: Sing s -> Sing ('TRegex s)
48−
49−instance Known (Sing n) => Known (Sing ('TEq n)) where known = STEq known
50−instance Known (Sing n) => Known (Sing ('TGt n)) where known = STGt known
51−instance Known (Sing n) => Known (Sing ('TLe n)) where known = STLe known
52−instance Known (Sing s) => Known (Sing ('TRegex s)) where known = STRegex known
49+ STEq :: (KnownNat n) => Sing n -> Sing ('TEq n)
50+ STLe :: (KnownNat n) => Sing n -> Sing ('TLe n)
51+ STGt :: (KnownNat n) => Sing n -> Sing ('TGt n)
52+ STRegex :: (KnownSymbol s, Known (Sing s)) => Sing s -> Sing ('TRegex s)
53+ STEnum :: (All KnownSymbol ss, Known (Sing ss)) => Sing ss -> Sing ('TEnum ss)
54+
55+instance (KnownNat n) => Known (Sing ('TEq n)) where known = STEq known
56+instance (KnownNat n) => Known (Sing ('TGt n)) where known = STGt known
57+instance (KnownNat n) => Known (Sing ('TLe n)) where known = STLe known
58+instance (KnownSymbol s, Known (Sing s)) => Known (Sing ('TRegex s)) where known = STRegex known
59+instance (All KnownSymbol ss, Known (Sing ss)) => Known (Sing ('TEnum ss)) where known = STEnum known
5360
5461instance Eq (Sing ('TEq n)) where _ == _ = True
5562instance Eq (Sing ('TLe n)) where _ == _ = True
5663instance Eq (Sing ('TGt n)) where _ == _ = True
64+instance Eq (Sing ('TRegex t)) where _ == _ = True
65+instance Eq (Sing ('TEnum ss)) where _ == _ = True
5766
5867data NumberConstraint
5968 = NLe Nat
@@ -62,13 +71,13 @@ data NumberConstraint
6271 deriving (Generic)
6372
6473data instance Sing (nc :: NumberConstraint) where
65− SNEq :: Sing n -> Sing ('NEq n)
66− SNGt :: Sing n -> Sing ('NGt n)
67− SNLe :: Sing n -> Sing ('NLe n)
74+ SNEq :: KnownNat n => Sing n -> Sing ('NEq n)
75+ SNGt :: KnownNat n => Sing n -> Sing ('NGt n)
76+ SNLe :: KnownNat n => Sing n -> Sing ('NLe n)
6877
69−instance Known (Sing n) => Known (Sing ('NEq n)) where known = SNEq known
70−instance Known (Sing n) => Known (Sing ('NGt n)) where known = SNGt known
71−instance Known (Sing n) => Known (Sing ('NLe n)) where known = SNLe known
78+instance KnownNat n => Known (Sing ('NEq n)) where known = SNEq known
79+instance KnownNat n => Known (Sing ('NGt n)) where known = SNGt known
80+instance KnownNat n => Known (Sing ('NLe n)) where known = SNLe known
7281
7382instance Eq (Sing ('NEq n)) where _ == _ = True
7483instance Eq (Sing ('NLe n)) where _ == _ = True
@@ -79,9 +88,9 @@ data ArrayConstraint
7988 deriving (Generic)
8089
8190data instance Sing (ac :: ArrayConstraint) where
82− SAEq :: Sing n -> Sing ('AEq n)
91+ SAEq :: KnownNat n => Sing n -> Sing ('AEq n)
8392
84−instance Known (Sing n) => Known (Sing ('AEq n)) where known = SAEq known
93+instance KnownNat n => Known (Sing ('AEq n)) where known = SAEq known
8594
8695instance Eq (Sing ('AEq n)) where _ == _ = True
8796
@@ -123,11 +132,24 @@ instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
123132instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
124133
125134data FieldRepr :: (Symbol, Schema) -> Type where
126− FieldRepr :: KnownSymbol name => JsonRepr schema -> FieldRepr '(name, schema)
127−
128−type family MapSnd (cs :: [(Symbol, Schema)]) :: [Schema] where
129− MapSnd '[] = '[]
130− MapSnd ( '(fn, schema) ': as) = schema ': MapSnd as
135+ FieldRepr
136+ :: (Known (Sing schema), KnownSymbol name)
137+ => JsonRepr schema
138+ -> FieldRepr '(name, schema)
139+
140+knownFieldName
141+ :: forall proxy (fieldName :: Symbol) schema
142+ . KnownSymbol fieldName
143+ => proxy '(fieldName, schema)
144+ -> Text
145+knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
146+
147+knownFieldSchema
148+ :: forall proxy fieldName schema
149+ . Known (Sing schema)
150+ => proxy '(fieldName, schema)
151+ -> Sing schema
152+knownFieldSchema _ = known
131153
132154deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
133155
@@ -136,6 +158,7 @@ instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
136158
137159instance
138160 ( KnownSymbol name
161+ , Known (Sing schema)
139162 , Serial m (JsonRepr schema) )
140163 => Serial m (FieldRepr '(name, schema)) where
141164 series = FieldRepr <$> series
@@ -269,9 +292,9 @@ instance J.ToJSON (JsonRepr a) where
269292 RNil -> []
270293 fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
271294
272−class FalseConstraint
295+class FalseConstraint a
273296
274−type family TopLevel (spec :: Schema) :: Constraint where
275− TopLevel ('SchemaArray a e) = ()
276− TopLevel ('SchemaObject o) = ()
277− TopLevel spec = FalseConstraint
297+type family TopLevel (schema :: Schema) :: Constraint where
298+ TopLevel ('SchemaArray acs s) = ()
299+ TopLevel ('SchemaObject o) = ()
300+ TopLevel spec = FalseConstraint spec