diff --git a/schematic.cabal b/schematic.cabal
index df00704..8d4f654 100644
--- a/schematic.cabal
+++ b/schematic.cabal
@@ -16,6 +16,7 @@ cabal-version:       >=1.10
 library
   exposed-modules:     Data.Schematic
                      , Data.Schematic.DSL
+                     , Data.Schematic.Compat
                      , Data.Schematic.Generator
                      , Data.Schematic.Generator.Regex
                      , Data.Schematic.Instances
@@ -25,6 +26,7 @@ library
                      , Data.Schematic.Migration
                      , Data.Schematic.Path
                      , Data.Schematic.Schema
+                     , Data.Schematic.Constraints
                      , Data.Schematic.Validation
                      , Data.Schematic.Verifier
                      , Data.Schematic.Verifier.Array
@@ -65,7 +67,7 @@ library
                      , TypeOperators
                      , TypeSynonymInstances
                      , UndecidableInstances
-  build-depends:       base >=4.11 && <4.13
+  build-depends:       base >=4.10 && <4.13
                      , bytestring
                      , aeson >= 1
                      , containers
@@ -75,7 +77,8 @@ library
                      , regex-tdfa
                      , regex-tdfa-text
                      , scientific
-                     , singletons >= 2.4
+                     , singletons
+                     -- >= 2.4
                      , smallcheck
                      , tagged
                      , template-haskell
@@ -95,7 +98,7 @@ test-suite spec
   default-language:   Haskell2010
   build-depends:       HUnit
                      , aeson >= 1
-                     , base >=4.11 && <4.13
+                     , base >=4.10 && <4.13
                      , bytestring
                      , containers
                      , hjsonschema
diff --git a/src/Data/Schematic.hs b/src/Data/Schematic.hs
index eba608b..ebe12a1 100644
--- a/src/Data/Schematic.hs
+++ b/src/Data/Schematic.hs
@@ -7,9 +7,10 @@ module Data.Schematic
   , module Data.Schematic.Lens
   , module Data.Schematic.Migration
   , module Data.Schematic.Schema
+  , module Data.Schematic.Constraints
+  , module Data.Schematic.Compat
   , decodeAndValidateJson
   , parseAndValidateJson
-  , parseAndValidateJsonBy
   , parseAndValidateTopVersionJson
   , parseAndValidateWithMList
   , decodeAndValidateVersionedWithMList
@@ -27,6 +28,8 @@ import Data.Aeson as J
 import Data.Aeson.Types as J
 import Data.ByteString.Lazy as BL
 import Data.Functor.Identity as F
+import Data.Schematic.Compat
+import Data.Schematic.Constraints
 import Data.Schematic.DSL
 import Data.Schematic.Helpers
 import Data.Schematic.JsonSchema
@@ -41,7 +44,8 @@ import Data.Text as T
 
 parseAndValidateTopVersionJson
   :: forall proxy (v :: Versioned)
-  .  (SingI (TopVersion (AllVersions v)))
+  . ( SingI (TopVersion (AllVersions v))
+    , FromJSON (JsonRepr (TopVersion (AllVersions v))) )
   => proxy v
   -> J.Value
   -> ParseResult (JsonRepr (TopVersion (AllVersions v)))
@@ -64,13 +68,9 @@ parseAndValidateWithMList
   -> m (ParseResult (JsonRepr (Head revisions)))
 parseAndValidateWithMList MNil v = pure $ parseAndValidateJson v
 parseAndValidateWithMList (Tagged f :&& tl) v =
-  case parseAndValidateJsonBy Proxy v of
+  case parseAndValidateJson v of
     Valid a           -> pure $ Valid a
-    DecodingError _   -> do
-      pr <- parseAndValidateWithMList tl v
-      let pr' = f <$> pr
-      sequence pr'
-    ValidationError _ -> do
+    _   -> do
       pr <- parseAndValidateWithMList tl v
       let pr' = f <$> pr
       sequence pr'
@@ -95,7 +95,8 @@ decodeAndValidateVersionedWithMList _ mlist bs = case decode bs of
   Just x  -> parseAndValidateWithMList mlist x
 
 decodeAndValidateVersionedWithPureMList
-  :: proxy versioned
+  :: FromJSON (JsonRepr (Head (MapSnd (AllVersions versioned))))
+  => proxy versioned
   -> MList F.Identity (MapSnd (AllVersions versioned))
   -> BL.ByteString
   -> ParseResult (JsonRepr (Head (MapSnd (AllVersions versioned))))
diff --git a/src/Data/Schematic/Compat.hs b/src/Data/Schematic/Compat.hs
new file mode 100644
index 0000000..3dd05c1
--- /dev/null
+++ b/src/Data/Schematic/Compat.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP                 #-}
+module Data.Schematic.Compat where
+
+import Data.Singletons.Prelude
+import GHC.TypeLits
+#if MIN_VERSION_base(4,12,0)
+import Data.Vinyl
+#else
+import Data.Kind
+#endif
+
+
+type DeNat = Demote Nat
+-- ^ Demote Nat is depends on version of singletons
+
+demote' :: forall a. (SingI a, SingKind (KindOf a)) => Demote (KindOf a)
+#if MIN_VERSION_singletons(2,4,0)
+type (:+++) a b = (++) a b
+demote' = demote @a
+#else
+type (:+++) a b = (:++) a b
+demote' = fromSing (sing :: Sing a)
+#endif
+
+#if MIN_VERSION_vinyl(0,9,0)
+type RMapCompat fs = RMap fs
+type ReifyConstraintCompat c repr fs = ReifyConstraint c repr fs
+type RecordToListCompat fs = RecordToList fs
+#else
+type RMapCompat fs = (() :: Constraint)
+type ReifyConstraintCompat c fs repr = (() :: Constraint)
+type RecordToListCompat fs = (() :: Constraint)
+#endif
diff --git a/src/Data/Schematic/Constraints.hs b/src/Data/Schematic/Constraints.hs
new file mode 100644
index 0000000..625f63f
--- /dev/null
+++ b/src/Data/Schematic/Constraints.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE EmptyCase #-}
+{-# OPTIONS_GHC -fprint-explicit-kinds #-}
+
+module Data.Schematic.Constraints where
+
+import Data.Schematic.Compat
+import Data.Singletons.Prelude
+import Data.Singletons.TH
+import Data.Singletons.TypeLits
+import Data.Text as T
+import GHC.Generics (Generic)
+
+
+singletons [d|
+  data TextConstraint' s n
+    = TEq n
+    | TLt n
+    | TLe n
+    | TGt n
+    | TGe n
+    | TRegex s
+    | TEnum [s]
+    deriving (Eq, Show, Generic)
+
+  data NumberConstraint' n
+    = NLe n
+    | NLt n
+    | NGt n
+    | NGe n
+    | NEq n
+    deriving (Eq, Show, Generic)
+
+  data ArrayConstraint' n = AEq n deriving (Eq, Show, Generic)
+  |]
+
+type TextConstraintT = TextConstraint' Text DeNat
+type TextConstraint = TextConstraint' Symbol Nat
+type NumberConstraintT = NumberConstraint' DeNat
+type NumberConstraint = NumberConstraint' Nat
+type ArrayConstraintT = ArrayConstraint' DeNat
+type ArrayConstraint = ArrayConstraint' Nat
diff --git a/src/Data/Schematic/DSL.hs b/src/Data/Schematic/DSL.hs
index da16bfd..35c2567 100644
--- a/src/Data/Schematic/DSL.hs
+++ b/src/Data/Schematic/DSL.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE CPP                 #-}
 
 module Data.Schematic.DSL where
 
@@ -18,26 +17,22 @@ import           Data.Vinyl
 import           Data.Vinyl.Functor
 
 
-#if MIN_VERSION_base(4,12,0)
 type Constructor a
   = forall fields b
-  . (fields ~ FieldsOf a, FSubset fields b (FImage fields b), RMap fields)
+  . ( fields ~ FieldsOf a, FSubset fields b (FImage fields b)
+    , ReprObjectConstr fields )
   => Rec (Tagged fields :. FieldRepr) b
   -> JsonRepr ('SchemaObject fields)
-#else
-type Constructor a
-  = forall fields b
-  . (fields ~ FieldsOf a, FSubset fields b (FImage fields b))
-  => Rec (Tagged fields :. FieldRepr) b
-  -> JsonRepr ('SchemaObject fields)
-#endif
+
 withRepr :: Constructor a
 withRepr = ReprObject . rmap (unTagged . getCompose) . fcast
 
 class Representable s where
   constructField :: Sing fn -> Proxy s -> Repr s -> FieldRepr '(fn, s)
 
-instance SingI so => Representable ('SchemaObject so) where
+instance
+  (SingI so, ReprObjectConstr so)
+  => Representable ('SchemaObject so) where
   constructField sfn _ o = withKnownSymbol sfn $ FieldRepr $ ReprObject o
 
 instance (SingI cs, SingI sa) => Representable ('SchemaArray cs sa) where
@@ -55,22 +50,10 @@ instance Representable 'SchemaBoolean where
 instance SingI so => Representable ('SchemaOptional so) where
   constructField sfn _ o = withKnownSymbol sfn $ FieldRepr $ ReprOptional o
 
-instance SingI (h ': tl) => Representable ('SchemaUnion (h ': tl)) where
+instance (SingI (h ': tl), ReprUnionConstr tl)
+  => Representable ('SchemaUnion (h ': tl)) where
   constructField sfn _ u = withKnownSymbol sfn $ FieldRepr $ ReprUnion u
 
-construct :: Sing s -> Repr s -> JsonRepr s
-construct s r = case s of
-  SSchemaObject _          -> ReprObject r
-  SSchemaArray _ _         -> ReprArray r
-  SSchemaText _            -> ReprText r
-  SSchemaNumber _          -> ReprNumber r
-  SSchemaBoolean           -> ReprBoolean r
-  SSchemaOptional _        -> ReprOptional r
-  SSchemaNull              -> ReprNull
-  SSchemaUnion ss          -> case ss of
-    SNil      -> error "unconstructable union"
-    SCons _ _ -> ReprUnion r
-
 type family FieldsOf (s :: Schema) :: [(Symbol, Schema)] where
   FieldsOf ('SchemaObject fs) = fs
 
diff --git a/src/Data/Schematic/Generator.hs b/src/Data/Schematic/Generator.hs
index 59acde4..4d9d8b5 100644
--- a/src/Data/Schematic/Generator.hs
+++ b/src/Data/Schematic/Generator.hs
@@ -1,13 +1,14 @@
 module Data.Schematic.Generator where
 
-import           Data.Maybe
-import           Data.Schematic.Generator.Regex
-import {-# SOURCE #-} Data.Schematic.Schema
-import           Data.Schematic.Verifier
-import           Data.Scientific
-import           Data.Text (Text, pack)
-import qualified Data.Vector as V
-import           Test.SmallCheck.Series
+import Control.Applicative
+import Data.Maybe
+import Data.Schematic.Constraints
+import Data.Schematic.Generator.Regex
+import Data.Schematic.Verifier
+import Data.Scientific
+import Data.Text (Text, pack)
+import Test.SmallCheck.Series
+
 
 maxHigh :: Int
 maxHigh = 30
@@ -30,35 +31,18 @@ textLengthSeries =
 textEnumSeries :: Monad m => [Text] -> Series m Text
 textEnumSeries enum = generate $ \depth -> take depth enum
 
-textSeries :: Monad m => [DemotedTextConstraint] -> Series m Text
-textSeries cs = do
-  let mvcs = verifyTextConstraints cs
-  case mvcs of
-    Just vcs -> do
-      n <- textSeries' vcs
-      pure n
-    Nothing  -> pure "error"
+textSeries :: Monad m => [TextConstraintT] -> Series m Text
+textSeries cs = maybe (pure "error") textSeries' $ verifyTextConstraints cs
 
 textSeries' :: Monad m => [VerifiedTextConstraint] -> Series m Text
 textSeries' [] = pure "sample"
-textSeries' vcs = do
-  let enums = listToMaybe [x | VTEnum x <- vcs]
-  case enums of
-    Just e -> textEnumSeries e
-    Nothing -> do
-      let regexps = listToMaybe [x | VTRegex x _ _ <- vcs]
-      case regexps of
-        Just e  -> regexSeries e
-        Nothing -> textLengthSeries vcs
+textSeries' vcs
+  = fromMaybe (textLengthSeries vcs)
+  $ textEnumSeries <$> listToMaybe [x | VTEnum x <- vcs]
+  <|> regexSeries <$> listToMaybe [x | VTRegex x _ _ <- vcs]
 
-numberSeries :: Monad m => [DemotedNumberConstraint] -> Series m Scientific
-numberSeries cs = do
-  let mvcs = verifyNumberConstraints cs
-  case mvcs of
-    Just vcs -> do
-      n <- numberSeries' vcs
-      pure $ n
-    Nothing -> pure 0
+numberSeries :: Monad m => [NumberConstraintT] -> Series m Scientific
+numberSeries cs = maybe (pure 0) numberSeries' $ verifyNumberConstraints cs
 
 numberSeries' :: Monad m => VerifiedNumberConstraint -> Series m Scientific
 numberSeries' =
@@ -69,23 +53,3 @@ numberSeries' =
           h = fromMaybe maxHigh (fromIntegral <$> mh) - 1
       n <- generate $ \depth -> take depth [l .. h]
       pure $ fromIntegral n
-
-arraySeries
-  :: (Monad m, Serial m (JsonRepr s))
-  => [DemotedArrayConstraint]
-  -> Series m (V.Vector (JsonRepr s))
-arraySeries cs = do
-  let mvcs = verifyArrayConstraint cs
-  case mvcs of
-    Just vcs -> arraySeries' vcs
-    Nothing  -> pure V.empty
-
-arraySeries'
-  :: forall m s. (Monad m, Serial m (JsonRepr s))
-  => Maybe VerifiedArrayConstraint
-  -> Series m (V.Vector (JsonRepr s))
-arraySeries' ml = do
-  objs <- V.replicateM (maybe minRepeat f ml) (series :: Series m (JsonRepr s))
-  pure $ objs
-  where
-    f (VAEq l) = fromIntegral l
diff --git a/src/Data/Schematic/Helpers.hs b/src/Data/Schematic/Helpers.hs
index 9620e7b..808fcdb 100644
--- a/src/Data/Schematic/Helpers.hs
+++ b/src/Data/Schematic/Helpers.hs
@@ -1,6 +1,6 @@
 module Data.Schematic.Helpers where
 
-import Data.Schematic.Schema
+import Data.Schematic.Constraints
 import GHC.TypeLits
 
 
diff --git a/src/Data/Schematic/Instances.hs b/src/Data/Schematic/Instances.hs
index c3a5080..dcc7d7f 100644
--- a/src/Data/Schematic/Instances.hs
+++ b/src/Data/Schematic/Instances.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module Data.Schematic.Instances where
diff --git a/src/Data/Schematic/JsonSchema.hs b/src/Data/Schematic/JsonSchema.hs
index 1a4ae82..581d67a 100644
--- a/src/Data/Schematic/JsonSchema.hs
+++ b/src/Data/Schematic/JsonSchema.hs
@@ -1,8 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE OverloadedLabels #-}
-{-# LANGUAGE TemplateHaskell #-}
-
 module Data.Schematic.JsonSchema
   ( toJsonSchema
   , toJsonSchema'
@@ -14,6 +9,7 @@ import Data.Foldable as F
 import Data.HashMap.Strict as H
 import Data.List as L
 import Data.List.NonEmpty as NE
+import Data.Schematic.Constraints
 import Data.Schematic.Schema as S
 import Data.Set as Set
 import Data.Singletons
@@ -26,40 +22,40 @@ import JSONSchema.Validator.Draft4 as D4
 draft4 :: Text
 draft4 = "http://json-schema.org/draft-04/schema#"
 
-textConstraint :: DemotedTextConstraint -> State D4.Schema ()
-textConstraint (DTEq n) = modify $ \s -> s
+textConstraint :: TextConstraintT -> State D4.Schema ()
+textConstraint (TEq n) = modify $ \s -> s
   { _schemaMinLength = pure $ fromIntegral n
   , _schemaMaxLength = pure $ fromIntegral n }
-textConstraint (DTLt n) = modify $ \s -> s
+textConstraint (TLt n) = modify $ \s -> s
   { _schemaMaxLength = pure . fromIntegral $ n + 1 }
-textConstraint (DTLe n) = modify $ \s -> s
+textConstraint (TLe n) = modify $ \s -> s
   { _schemaMaxLength = pure . fromIntegral $ n }
-textConstraint (DTGt n) =
+textConstraint (TGt n) =
   let n' = if n == 0 then 0 else n - 1
   in modify $ \s -> s { _schemaMinLength = pure . fromIntegral $ n' }
-textConstraint (DTGe n) = modify $ \s -> s
+textConstraint (TGe n) = modify $ \s -> s
   { _schemaMinLength = pure . fromIntegral $ n }
-textConstraint (DTRegex r) = modify $ \s -> s { _schemaPattern = pure r }
-textConstraint (DTEnum ss) =
+textConstraint (TRegex r) = modify $ \s -> s { _schemaPattern = pure r }
+textConstraint (TEnum ss) =
   let ss' = if F.length ss == 0 then [] else NE.fromList $ J.String <$> ss
   in modify $ \s -> s { _schemaEnum = pure ss' }
 
-numberConstraint :: DemotedNumberConstraint -> State D4.Schema ()
-numberConstraint (DNLe n) = modify $ \s -> s
+numberConstraint :: NumberConstraintT -> State D4.Schema ()
+numberConstraint (NLe n) = modify $ \s -> s
   { _schemaMaximum = pure . fromIntegral $ n }
-numberConstraint (DNLt n) = modify $ \s -> s
+numberConstraint (NLt n) = modify $ \s -> s
   { _schemaMaximum = pure . fromIntegral $ n + 1 }
-numberConstraint (DNGt n) = modify $ \s -> s
+numberConstraint (NGt n) = modify $ \s -> s
   { _schemaMinimum = pure . fromIntegral $ n }
-numberConstraint (DNGe n) =
+numberConstraint (NGe n) =
   let n' = if n == 0 then 0 else n - 1
   in modify $ \s -> s { _schemaMinimum = pure . fromIntegral $ n' }
-numberConstraint (DNEq n) = modify $ \s -> s
+numberConstraint (NEq n) = modify $ \s -> s
   { _schemaMinimum = pure $ fromIntegral n
   , _schemaMaximum = pure $ fromIntegral n }
 
-arrayConstraint :: DemotedArrayConstraint -> State D4.Schema ()
-arrayConstraint (DAEq _) = pure ()
+arrayConstraint :: ArrayConstraintT -> State D4.Schema ()
+arrayConstraint (AEq _) = pure ()
 
 toJsonSchema
   :: forall proxy schema
@@ -71,41 +67,41 @@ toJsonSchema _ = do
   pure $ js { _schemaVersion = pure draft4 }
 
 toJsonSchema'
-  :: DemotedSchema
+  :: SchemaT
   -> Maybe D4.Schema
 toJsonSchema' = \case
-  DSchemaText tcs ->
+  SchemaText tcs ->
     pure $ execState (traverse_ textConstraint tcs) $ emptySchema
       { _schemaType = pure $ TypeValidatorString D4.SchemaString }
-  DSchemaNumber ncs ->
+  S.SchemaNumber ncs ->
     pure $ execState (traverse_ numberConstraint ncs) $ emptySchema
       { _schemaType = pure $ TypeValidatorString D4.SchemaNumber }
-  DSchemaBoolean -> pure $ emptySchema
+  S.SchemaBoolean -> pure $ emptySchema
     { _schemaType = pure $ TypeValidatorString D4.SchemaBoolean }
-  DSchemaObject objs -> do
+  S.SchemaObject objs -> do
     res <- for objs $ \(n,s) -> do
       s' <- toJsonSchema' s
       pure (n, s')
     let
       nonOpt = \case
-        (_, DSchemaOptional _) -> False
-        _                      -> True
+        (_, SchemaOptional _) -> False
+        _                     -> True
     pure $ emptySchema
       { _schemaType       = pure $ TypeValidatorString D4.SchemaObject
       , _schemaRequired   = pure $ Set.fromList $ fst <$> L.filter nonOpt objs
       , _schemaProperties = pure $ H.fromList res }
-  DSchemaArray acs sch -> do
+  S.SchemaArray acs sch -> do
     res <- toJsonSchema' sch
     pure $ execState (traverse_ arrayConstraint acs) $ emptySchema
       { _schemaType  = pure $ TypeValidatorString D4.SchemaArray
       , _schemaItems = pure $ ItemsObject res }
-  DSchemaNull -> pure $ emptySchema
+  S.SchemaNull -> pure $ emptySchema
     { _schemaType = pure $ TypeValidatorString D4.SchemaNull }
-  DSchemaOptional sch -> do
-    snull <- toJsonSchema' DSchemaNull
+  SchemaOptional sch -> do
+    snull <- toJsonSchema' S.SchemaNull
     sres <- toJsonSchema' sch
     pure $ emptySchema { _schemaOneOf = pure (snull :| [sres]) }
-  DSchemaUnion sch -> do
+  SchemaUnion sch -> do
     schemaUnion <- traverse toJsonSchema' sch >>= \case
       [] -> Nothing
       x  -> Just x
diff --git a/src/Data/Schematic/Lens.hs b/src/Data/Schematic/Lens.hs
index a51423a..8453432 100644
--- a/src/Data/Schematic/Lens.hs
+++ b/src/Data/Schematic/Lens.hs
@@ -1,8 +1,3 @@
-{-# LANGUAGE UndecidableSuperClasses #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE InstanceSigs #-}
-
 module Data.Schematic.Lens
   ( FIndex
   , FElem(..)
@@ -33,7 +28,7 @@ import Data.Vector as V
 import Data.Vinyl
 import Data.Vinyl.Functor
 import Data.Vinyl.TypeLevel (Nat(..))
-import GHC.TypeLits (Symbol, KnownSymbol)
+import GHC.TypeLits (KnownSymbol, Symbol)
 
 
 -- | A partial relation that gives the index of a value in a list.
@@ -176,7 +171,7 @@ arrayRepr
 arrayRepr = iso (\(FieldRepr (ReprArray a)) -> a) (FieldRepr . ReprArray)
 
 objectRepr
-  :: (KnownSymbol fn, SingI fields)
+  :: (KnownSymbol fn, SingI fields, ReprObjectConstr fields)
   => Iso' (FieldRepr '(fn, ('SchemaObject fields))) (Rec FieldRepr fields)
 objectRepr = iso (\(FieldRepr (ReprObject o)) -> o) (FieldRepr . ReprObject)
 
@@ -185,13 +180,14 @@ optionalRepr
   => Iso' (FieldRepr '(fn, ('SchemaOptional schema))) (Maybe (JsonRepr schema))
 optionalRepr = iso (\(FieldRepr (ReprOptional r)) -> r) (FieldRepr . ReprOptional)
 
-obj :: Iso' (JsonRepr ('SchemaObject fields)) (Rec FieldRepr fields)
+obj :: ReprObjectConstr fields => Iso' (JsonRepr ('SchemaObject fields)) (Rec FieldRepr fields)
 obj = iso (\(ReprObject r) -> r) ReprObject
 
 arr :: Iso' (JsonRepr ('SchemaArray cs schema)) (V.Vector (JsonRepr schema))
 arr = iso (\(ReprArray r) -> r) ReprArray
 
-uni :: Iso' (JsonRepr ('SchemaUnion (h ': tl))) (Union JsonRepr (h ': tl))
+uni :: ReprUnionConstr tl
+  => Iso' (JsonRepr ('SchemaUnion (h ': tl))) (Union JsonRepr (h ': tl))
 uni = iso (\(ReprUnion u) -> u) ReprUnion
 
 txt :: Iso' (JsonRepr ('SchemaText cs)) Text
diff --git a/src/Data/Schematic/Migration.hs b/src/Data/Schematic/Migration.hs
index b8cc197..e210543 100644
--- a/src/Data/Schematic/Migration.hs
+++ b/src/Data/Schematic/Migration.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE TemplateHaskell     #-}
 
 module Data.Schematic.Migration where
 
+import Data.Aeson
 import Data.Kind
+import Data.Schematic.Compat
 import Data.Schematic.DSL
 import Data.Schematic.Lens
 import Data.Schematic.Path
@@ -43,8 +43,8 @@ type family SchemaByKey (fs :: [(Symbol, Schema)]) (s :: Symbol) :: Schema where
   SchemaByKey ( '(a, s) ': tl) fn = SchemaByKey tl fn
 
 type family DeleteKey (acc :: [(Symbol, Schema)]) (fn :: Symbol) (fs :: [(Symbol, Schema)]) :: [(Symbol, Schema)] where
-  DeleteKey acc fn ('(fn, a) ': tl) = acc ++ tl
-  DeleteKey acc fn (fna ': tl) = acc ++ (fna ': tl)
+  DeleteKey acc fn ('(fn, a) ': tl) = acc :+++ tl
+  DeleteKey acc fn (fna ': tl) = acc :+++ (fna ': tl)
 
 type family UpdateKey
   (fn :: Symbol)
@@ -148,33 +148,29 @@ data instance Sing (v :: Versioned) where
 type DataMigration s m h = Tagged s (JsonRepr h -> m (JsonRepr s))
 
 data MList :: (Type -> Type) -> [Schema] -> Type where
-  MNil :: (Monad m, SingI s, TopLevel s) => MList m '[s]
+  MNil :: (Monad m, SingI s, TopLevel s, FromJSON (JsonRepr s)) => MList m '[s]
   (:&&)
-    :: (TopLevel s, SingI s)
+    :: (TopLevel s, SingI s, FromJSON (JsonRepr h), FromJSON (JsonRepr s))
     => DataMigration s m h
     -> MList m (h ': tl)
     -> MList m (s ': h ': tl)
 
 infixr 7 :&&
 
-#if MIN_VERSION_base(4,12,0)
 migrateObject
-  :: forall m fs fh. (FSubset fs fs (FImage fs fs), Monad m, RMap fh, RMap fs)
+  :: forall m fs fh
+  . ( FSubset fs fs (FImage fs fs), Monad m
+    , ReprObjectConstr fh, ReprObjectConstr fs )
   => (Rec (Tagged fs :. FieldRepr) fh -> m (Rec (Tagged fs :. FieldRepr) fs))
-  -> Tagged ('SchemaObject fs) (JsonRepr ('SchemaObject fh) -> m (JsonRepr ('SchemaObject fs)))
-#else
-migrateObject
-  :: forall m fs fh. (FSubset fs fs (FImage fs fs), Monad m)
-  => (Rec (Tagged fs :. FieldRepr) fh -> m (Rec (Tagged fs :. FieldRepr) fs))
-  -> Tagged ('SchemaObject fs) (JsonRepr ('SchemaObject fh) -> m (JsonRepr ('SchemaObject fs)))
-#endif
+  -> Tagged ('SchemaObject fs)
+    (JsonRepr ('SchemaObject fh) -> m (JsonRepr ('SchemaObject fs)))
 migrateObject f = Tagged $ \(ReprObject r) -> do
   res <- f $ rmap (Compose . Tagged) r
   pure $ withRepr @('SchemaObject fs) res
 
 shrinkObject
   :: forall rs ss m
-  . ( Monad m, FSubset rs ss (FImage rs ss) )
+  . ( Monad m, FSubset rs ss (FImage rs ss), ReprObjectConstr rs )
   => Tagged
     ('SchemaObject rs)
     (JsonRepr ('SchemaObject ss) -> m (JsonRepr ('SchemaObject rs)))
diff --git a/src/Data/Schematic/Path.hs b/src/Data/Schematic/Path.hs
index 566448e..070f527 100644
--- a/src/Data/Schematic/Path.hs
+++ b/src/Data/Schematic/Path.hs
@@ -1,39 +1,31 @@
 module Data.Schematic.Path where
 
 import Data.Foldable as F
+import Data.Monoid ((<>))
+import Data.Schematic.Compat
 import Data.Singletons.Prelude
+import Data.Singletons.TH
 import Data.Singletons.TypeLits
 import Data.Text as T
 
 
-data PathSegment = Key Symbol | Ix Nat
+singletons [d|
+  data PathSegment' s n = Key s | Ix n
+    deriving Show
+  |]
 
-data instance Sing (jp :: PathSegment) where
-  SKey :: (SingI k) => Sing (k :: Symbol) -> Sing ('Key k)
-  SIx :: (SingI n) => Sing (n :: Nat) -> Sing ('Ix n)
-
-data DemotedPathSegment = DKey Text | DIx Integer
-  deriving (Show)
+type PathSegment = PathSegment' Symbol Nat
+type DemotedPathSegment = PathSegment' Text DeNat
 
 -- | Textual representation of json path.
 newtype JSONPath = JSONPath Text
   deriving (Show)
 
-demotePath :: Sing (ps :: [PathSegment]) -> [DemotedPathSegment]
-demotePath = go []
-  where
-    go :: [DemotedPathSegment] -> Sing (ps :: [PathSegment]) -> [DemotedPathSegment]
-    go acc SNil = acc
-    go acc (SCons p ps) = go (acc ++ [demotePathSeg p]) ps
-    demotePathSeg :: Sing (ps :: PathSegment) -> DemotedPathSegment
-    demotePathSeg (SKey s) = DKey $ T.pack $ withKnownSymbol s $ symbolVal s
-    demotePathSeg (SIx n) = DIx $ withKnownNat n $ fromIntegral $ natVal n
-
 demotedPathToText :: [DemotedPathSegment] -> JSONPath
 demotedPathToText = JSONPath . F.foldl' renderPathSegment ""
   where
-    renderPathSegment acc (DKey t) = acc <> "." <> t
-    renderPathSegment acc (DIx n)  = acc <> "[" <> T.pack (show n) <> "]"
+    renderPathSegment acc (Key t) = acc <> "." <> t
+    renderPathSegment acc (Ix n)  = acc <> "[" <> T.pack (show n) <> "]"
 
 pathToText :: Sing (ps :: [PathSegment]) -> JSONPath
-pathToText = demotedPathToText . demotePath
+pathToText = demotedPathToText . fromSing
diff --git a/src/Data/Schematic/Schema.hs b/src/Data/Schematic/Schema.hs
index c2bb7c2..1333cfd 100644
--- a/src/Data/Schematic/Schema.hs
+++ b/src/Data/Schematic/Schema.hs
@@ -1,7 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE CPP                 #-}
-{-# LANGUAGE OverloadedLists     #-}
-{-# LANGUAGE OverloadedStrings   #-}
 {-# OPTIONS_GHC -fprint-explicit-kinds #-}
 
 module Data.Schematic.Schema where
@@ -10,282 +8,53 @@ import           Control.Applicative ((<|>))
 import           Control.Monad
 import           Data.Aeson as J
 import           Data.Aeson.Types as J
+import           Data.Char as C
 import           Data.HashMap.Strict as H
 import           Data.Kind
 import           Data.Maybe
+import           Data.Schematic.Compat
+import           Data.Schematic.Constraints
 import           Data.Schematic.Generator
+import           Data.Schematic.Generator.Regex
 import           Data.Schematic.Instances ()
+import           Data.Schematic.Verifier.Array
 import           Data.Scientific
-import           Data.Singletons.Prelude.List hiding (All, Union)
 import           Data.Singletons.TH
 import           Data.Singletons.TypeLits
 import           Data.Text as T
 import           Data.Union
 import           Data.Vector as V
 import           Data.Vinyl hiding (Dict)
-import qualified Data.Vinyl.TypeLevel as V
 import           GHC.Exts
 import           GHC.Generics (Generic)
-import           GHC.TypeLits
-  (SomeNat(..), SomeSymbol(..), someNatVal, someSymbolVal)
+import           GHC.TypeLits as TL
 import           Prelude as P
-import           Test.SmallCheck.Series
-
-
-type family CRepr (s :: Schema) :: Type where
-  CRepr ('SchemaText cs)  = TextConstraint
-  CRepr ('SchemaNumber cs) = NumberConstraint
-  CRepr ('SchemaObject fs) = (String, Schema)
-  CRepr ('SchemaArray ar s) = ArrayConstraint
-
-data TextConstraint
-  = TEq Nat
-  | TLt Nat
-  | TLe Nat
-  | TGt Nat
-  | TGe Nat
-  | TRegex Symbol
-  | TEnum [Symbol]
-  deriving (Generic)
-
-instance SingKind TextConstraint where
-  type Demote TextConstraint = DemotedTextConstraint
-  fromSing = \case
-    STEq n -> withKnownNat n (DTEq . fromIntegral $ natVal n)
-    STLt n -> withKnownNat n (DTLt . fromIntegral $ natVal n)
-    STLe n -> withKnownNat n (DTLe . fromIntegral $ natVal n)
-    STGt n -> withKnownNat n (DTGt . fromIntegral $ natVal n)
-    STGe n -> withKnownNat n (DTGe . fromIntegral $ natVal n)
-    STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
-    STEnum s -> let
-      d :: Sing (s :: [Symbol]) -> [Text]
-      d SNil               = []
-      d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
-      in DTEnum $ d s
-  toSing = \case
-    DTEq n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DTLt n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DTLe n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DTGt n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DTGe n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DTRegex s -> case someSymbolVal (T.unpack s) of
-      SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
-    DTEnum ss -> case toSing ss of
-      SomeSing l -> SomeSing (STEnum l)
-
-data DemotedTextConstraint
-  = DTEq Integer
-  | DTLt Integer
-  | DTLe Integer
-  | DTGt Integer
-  | DTGe Integer
-  | DTRegex Text
-  | DTEnum [Text]
-  deriving (Generic, Eq, Show)
-
-data instance Sing (tc :: TextConstraint) where
-  STEq :: Sing n -> Sing ('TEq n)
-  STLt :: Sing n -> Sing ('TLt n)
-  STLe :: Sing n -> Sing ('TLe n)
-  STGt :: Sing n -> Sing ('TGt n)
-  STGe :: Sing n -> Sing ('TGe n)
-  STRegex :: Sing s -> Sing ('TRegex s)
-  STEnum :: Sing ss -> Sing ('TEnum ss)
-
-instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
-instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
-instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
-instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
-instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
-instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
-instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
-
-instance Eq (Sing ('TEq n)) where _ == _ = True
-instance Eq (Sing ('TLt n)) where _ == _ = True
-instance Eq (Sing ('TLe n)) where _ == _ = True
-instance Eq (Sing ('TGt n)) where _ == _ = True
-instance Eq (Sing ('TGe n)) where _ == _ = True
-instance Eq (Sing ('TRegex t)) where _ == _ = True
-instance Eq (Sing ('TEnum ss)) where _ == _ = True
-
-data NumberConstraint
-  = NLe Nat
-  | NLt Nat
-  | NGt Nat
-  | NGe Nat
-  | NEq Nat
-  deriving (Generic)
-
-data DemotedNumberConstraint
-  = DNLe Integer
-  | DNLt Integer
-  | DNGt Integer
-  | DNGe Integer
-  | DNEq Integer
-  deriving (Generic, Eq, Show)
-
-data instance Sing (nc :: NumberConstraint) where
-  SNEq :: Sing n -> Sing ('NEq n)
-  SNGt :: Sing n -> Sing ('NGt n)
-  SNGe :: Sing n -> Sing ('NGe n)
-  SNLt :: Sing n -> Sing ('NLt n)
-  SNLe :: Sing n -> Sing ('NLe n)
-
-instance KnownNat n => SingI ('NEq n) where sing = SNEq sing
-instance KnownNat n => SingI ('NGt n) where sing = SNGt sing
-instance KnownNat n => SingI ('NGe n) where sing = SNGe sing
-instance KnownNat n => SingI ('NLt n) where sing = SNLt sing
-instance KnownNat n => SingI ('NLe n) where sing = SNLe sing
-
-instance Eq (Sing ('NEq n)) where _ == _ = True
-instance Eq (Sing ('NLt n)) where _ == _ = True
-instance Eq (Sing ('NLe n)) where _ == _ = True
-instance Eq (Sing ('NGt n)) where _ == _ = True
-instance Eq (Sing ('NGe n)) where _ == _ = True
-
-instance SingKind NumberConstraint where
-  type Demote NumberConstraint = DemotedNumberConstraint
-  fromSing = \case
-    SNEq n -> withKnownNat n (DNEq . fromIntegral $ natVal n)
-    SNGt n -> withKnownNat n (DNGt . fromIntegral $ natVal n)
-    SNGe n -> withKnownNat n (DNGe . fromIntegral $ natVal n)
-    SNLt n -> withKnownNat n (DNLt . fromIntegral $ natVal n)
-    SNLe n -> withKnownNat n (DNLe . fromIntegral $ natVal n)
-  toSing = \case
-    DNEq n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DNGt n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DNGe n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DNLt n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-    DNLe n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-
-data ArrayConstraint
-  = AEq Nat
-  deriving (Generic)
-
-data DemotedArrayConstraint
-  = DAEq Integer
-  deriving (Generic, Eq, Show)
-
-data instance Sing (ac :: ArrayConstraint) where
-  SAEq :: Sing n -> Sing ('AEq n)
-
-instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
-
-instance Eq (Sing ('AEq n)) where _ == _ = True
-
-instance SingKind ArrayConstraint where
-  type Demote ArrayConstraint = DemotedArrayConstraint
-  fromSing = \case
-    SAEq n -> withKnownNat n (DAEq . fromIntegral $ natVal n)
-  toSing = \case
-    DAEq n -> case someNatVal n of
-      Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
-      Nothing                       -> error "Negative singleton nat"
-
-data Schema
-  = SchemaText [TextConstraint]
-  | SchemaBoolean
-  | SchemaNumber [NumberConstraint]
-  | SchemaObject [(Symbol, Schema)]
-  | SchemaArray [ArrayConstraint] Schema
-  | SchemaNull
-  | SchemaOptional Schema
-  | SchemaUnion [Schema]
-  deriving (Generic)
-
-data DemotedSchema
-  = DSchemaText [DemotedTextConstraint]
-  | DSchemaNumber [DemotedNumberConstraint]
-  | DSchemaBoolean
-  | DSchemaObject [(Text, DemotedSchema)]
-  | DSchemaArray [DemotedArrayConstraint] DemotedSchema
-  | DSchemaNull
-  | DSchemaOptional DemotedSchema
-  | DSchemaUnion [DemotedSchema]
-  deriving (Generic, Eq, Show)
-
-data instance Sing (schema :: Schema) where
-  SSchemaText :: Sing tcs -> Sing ('SchemaText tcs)
-  SSchemaNumber :: Sing ncs -> Sing ('SchemaNumber ncs)
-  SSchemaBoolean :: Sing 'SchemaBoolean
-  SSchemaArray :: Sing acs -> Sing schema -> Sing ('SchemaArray acs schema)
-  SSchemaObject :: Sing fields -> Sing ('SchemaObject fields)
-  SSchemaOptional :: Sing s -> Sing ('SchemaOptional s)
-  SSchemaNull :: Sing 'SchemaNull
-  SSchemaUnion :: Sing ss -> Sing ('SchemaUnion ss)
-
-instance SingI sl => SingI ('SchemaText sl) where
-  sing = SSchemaText sing
-instance SingI sl => SingI ('SchemaNumber sl) where
-  sing = SSchemaNumber sing
-instance SingI 'SchemaNull where
-  sing = SSchemaNull
-instance SingI 'SchemaBoolean where
-  sing = SSchemaBoolean
-instance (SingI ac, SingI s) => SingI ('SchemaArray ac s) where
-  sing = SSchemaArray sing sing
-instance SingI stl => SingI ('SchemaObject stl) where
-  sing = SSchemaObject sing
-instance SingI s => SingI ('SchemaOptional s) where
-  sing = SSchemaOptional sing
-instance SingI s => SingI ('SchemaUnion s) where
-  sing = SSchemaUnion sing
-
-instance Eq (Sing ('SchemaText cs)) where _ == _ = True
-instance Eq (Sing ('SchemaNumber cs)) where _ == _ = True
-instance Eq (Sing 'SchemaNull) where _ == _ = True
-instance Eq (Sing 'SchemaBoolean) where _ == _ = True
-instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
-instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
-instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
-instance Eq (Sing ('SchemaUnion s)) where _ == _ = True
-
-instance SingKind Schema where
-  type Demote Schema = DemotedSchema
-  fromSing = \case
-    SSchemaText cs -> DSchemaText $ fromSing cs
-    SSchemaNumber cs -> DSchemaNumber $ fromSing cs
-    SSchemaBoolean -> DSchemaBoolean
-    SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
-    SSchemaOptional s -> DSchemaOptional $ fromSing s
-    SSchemaNull -> DSchemaNull
-    SSchemaObject cs -> DSchemaObject $ fromSing cs
-    SSchemaUnion ss -> DSchemaUnion $ fromSing ss
-  toSing = \case
-    DSchemaText cs -> case toSing cs of
-      SomeSing scs -> SomeSing $ SSchemaText scs
-    DSchemaNumber cs -> case toSing cs of
-      SomeSing scs -> SomeSing $ SSchemaNumber scs
-    DSchemaBoolean -> SomeSing $ SSchemaBoolean
-    DSchemaArray cs sch -> case (toSing cs, toSing sch) of
-      (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
-    DSchemaOptional sch -> case toSing sch of
-      SomeSing ssch -> SomeSing $ SSchemaOptional ssch
-    DSchemaNull -> SomeSing SSchemaNull
-    DSchemaObject cs -> case toSing cs of
-      SomeSing scs -> SomeSing $ SSchemaObject scs
-    DSchemaUnion ss -> case toSing ss of
-      SomeSing sss -> SomeSing $ SSchemaUnion sss
+import           Test.SmallCheck.Series as S
+#if !MIN_VERSION_base(4,12,0)
+import qualified Data.Vinyl.TypeLevel as V
+#endif
+import           Data.Monoid ((<>))
+
+
+singletons [d|
+  data Schema' s n
+    = SchemaText [TextConstraint' s n]
+    | SchemaBoolean
+    | SchemaNumber [NumberConstraint' n]
+    | SchemaObject [(s, Schema' s n)]
+    | SchemaArray [ArrayConstraint' n] (Schema' s n)
+    | SchemaNull
+    | SchemaOptional (Schema' s n)
+    | SchemaUnion [Schema' s n]
+    deriving (Show, Generic)
+  |]
+
+type SchemaT = Schema' Text (Demote Nat)
+type Schema = Schema' Symbol Nat
+
+schemaTypeStr :: forall (sch :: Schema). SingI sch => String
+schemaTypeStr =
+  P.map C.toLower $ P.drop 6 $ P.head $ P.words $ show $ (demote' @sch)
 
 data FieldRepr :: (Symbol, Schema) -> Type where
   FieldRepr
@@ -302,7 +71,7 @@ knownFieldName
   .  KnownSymbol fieldName
   => proxy '(fieldName, schema)
   -> Text
-knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
+knownFieldName _ = demote' @fieldName
 
 knownFieldSchema
   :: forall proxy fieldName schema
@@ -312,9 +81,8 @@ knownFieldSchema
 knownFieldSchema _ = sing
 
 deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
-
-instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
-  FieldRepr a == FieldRepr b = a == b
+deriving instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema))
+deriving instance Ord (JsonRepr schema) => Ord (FieldRepr '(name, schema))
 
 instance
   ( KnownSymbol name
@@ -323,9 +91,16 @@ instance
   => Serial m (FieldRepr '(name, schema)) where
   series = FieldRepr <$> series
 
-type family USubsets (u :: [k]) :: Constraint where
-  USubsets '[] = ()
-  USubsets (h ': tl) = (USubset tl (h ': tl) (V.RImage tl (h ': tl)), USubsets tl)
+#if MIN_VERSION_base(4,12,0)
+type ReprObjectConstr fs =
+  ( RMap fs, RecordToList fs, ReifyConstraint Show FieldRepr fs
+  , Eq (Rec FieldRepr fs), Ord (Rec FieldRepr fs))
+#else
+type ReprObjectConstr fs =
+  (V.RecAll FieldRepr fs Show, Eq (Rec FieldRepr fs))
+#endif
+type ReprUnionConstr tl =
+  (Show (Union JsonRepr tl), Eq (Union JsonRepr tl), Ord (Union JsonRepr tl))
 
 data JsonRepr :: Schema -> Type where
   ReprText :: Text -> JsonRepr ('SchemaText cs)
@@ -333,93 +108,20 @@ data JsonRepr :: Schema -> Type where
   ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
   ReprNull :: JsonRepr 'SchemaNull
   ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
-  ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
   ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
-  ReprUnion :: Union JsonRepr (h ': tl) -> JsonRepr ('SchemaUnion (h ': tl))
-
-instance (Monad m, Serial m Text, SingI cs)
-  => Serial m (JsonRepr ('SchemaText cs)) where
-  series = decDepth $ fmap ReprText $ textSeries $ fromSing (sing :: Sing cs)
-
-instance (Monad m, Serial m Scientific, SingI cs)
-  => Serial m (JsonRepr ('SchemaNumber cs)) where
-  series = decDepth $ fmap ReprNumber
-    $ numberSeries $ fromSing (sing :: Sing cs)
-
-instance Monad m => Serial m (JsonRepr 'SchemaNull) where
-  series = cons0 ReprNull
-
-instance (Serial m (JsonRepr s), Serial m (V.Vector (JsonRepr s)), SingI cs)
-  => Serial m (JsonRepr ('SchemaArray cs s)) where
-  series = decDepth $ fmap ReprArray
-    $ arraySeries $ fromSing (sing :: Sing cs)
-
-instance (Serial m (JsonRepr s))
-  => Serial m (JsonRepr ('SchemaOptional s)) where
-  series = cons1 ReprOptional
-
-instance (Monad m, Serial m (Rec FieldRepr fs))
-  => Serial m (JsonRepr ('SchemaObject fs)) where
-  series = cons1 ReprObject
-
--- | Move to the union package
-instance Show (JsonRepr ('SchemaText cs)) where
-  show (ReprText t) = "ReprText " P.++ show t
+  ReprUnion :: ReprUnionConstr tl
+    => Union JsonRepr (h ': tl) -> JsonRepr ('SchemaUnion (h ': tl))
+  ReprObject :: ReprObjectConstr fs
+    => Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
 
-instance Show (JsonRepr ('SchemaNumber cs)) where
-  show (ReprNumber n) = "ReprNumber " P.++ show n
-
-instance Show (JsonRepr 'SchemaBoolean) where
-  show (ReprBoolean n) = "ReprBoolean " P.++ show n
-
-instance Show (JsonRepr 'SchemaNull) where show _ = "ReprNull"
-
-instance Show (JsonRepr s) => Show (JsonRepr ('SchemaArray acs s)) where
-  show (ReprArray v) = "ReprArray " P.++ show v
+deriving instance Show (JsonRepr sch)
+deriving instance Eq (JsonRepr sch)
 
+-- due to issue https://gitlab.haskell.org/ghc/ghc/issues/8128
 #if MIN_VERSION_base(4,12,0)
-instance
-  ( V.RecAll FieldRepr fs Show, RMap fs, ReifyConstraint Show FieldRepr fs
-  , RecordToList fs )
-  => Show (JsonRepr ('SchemaObject fs)) where
-  show (ReprObject fs) = "ReprObject " P.++ show fs
-#else
-instance V.RecAll FieldRepr fs Show => Show (JsonRepr ('SchemaObject fs)) where
-  show (ReprObject fs) = "ReprObject " P.++ show fs
-#endif
-
-instance Show (JsonRepr s) => Show (JsonRepr ('SchemaOptional s)) where
-  show (ReprOptional s) = "ReprOptional " P.++ show s
-
-instance Show (Union JsonRepr (h ': tl))
-  => Show (JsonRepr ('SchemaUnion (h ': tl))) where
-  show (ReprUnion s) = "ReprUnion " P.++ show s
-
-instance Eq (Rec FieldRepr fs) => Eq (JsonRepr ('SchemaObject fs)) where
-  ReprObject a == ReprObject b = a == b
-
-instance Eq (JsonRepr ('SchemaText cs)) where
-  ReprText a == ReprText b = a == b
-
-instance Eq (JsonRepr ('SchemaNumber cs)) where
-  ReprNumber a == ReprNumber b = a == b
-
-instance Eq (JsonRepr 'SchemaBoolean) where
-  ReprBoolean a == ReprBoolean b = a == b
-
-instance Eq (JsonRepr 'SchemaNull) where
-  ReprNull == ReprNull = True
-
-instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaArray as s)) where
-  ReprArray a == ReprArray b = a == b
-
-instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaOptional s)) where
-  ReprOptional a == ReprOptional b = a == b
-
-instance Eq (Union JsonRepr (h ': tl))
-  => Eq (JsonRepr ('SchemaUnion (h ': tl))) where
-  ReprUnion a == ReprUnion b = a == b
+deriving instance Ord (JsonRepr sch)
 
+#else
 instance Ord (Rec FieldRepr fs) => Ord (JsonRepr ('SchemaObject fs)) where
   ReprObject a `compare` ReprObject b = a `compare` b
 
@@ -444,6 +146,46 @@ instance Ord (JsonRepr s) => Ord (JsonRepr ('SchemaOptional s)) where
 instance Ord (Union JsonRepr (h ': tl))
   => Ord (JsonRepr ('SchemaUnion (h ': tl))) where
   ReprUnion a `compare` ReprUnion b = a `compare` b
+#endif
+
+instance (Monad m, Serial m Text, SingI cs)
+  => Serial m (JsonRepr ('SchemaText cs)) where
+  series = decDepth $ fmap ReprText $ textSeries $ fromSing (sing :: Sing cs)
+
+instance (Monad m, Serial m Scientific, SingI cs)
+  => Serial m (JsonRepr ('SchemaNumber cs)) where
+  series = decDepth $ fmap ReprNumber
+    $ numberSeries $ fromSing (sing :: Sing cs)
+
+instance Monad m => Serial m (JsonRepr 'SchemaNull) where
+  series = cons0 ReprNull
+
+arraySeries
+  :: (Monad m, Serial m (JsonRepr s))
+  => [ArrayConstraintT] -> S.Series m (V.Vector (JsonRepr s))
+arraySeries cs = maybe (pure V.empty) arraySeries' $ verifyArrayConstraint cs
+
+arraySeries'
+  :: forall m s. (Monad m, Serial m (JsonRepr s))
+  => Maybe VerifiedArrayConstraint -> S.Series m (V.Vector (JsonRepr s))
+arraySeries' ml =
+  V.replicateM (maybe minRepeat f ml) (series :: S.Series m (JsonRepr s))
+  where
+    f (VAEq l) = fromIntegral l
+
+instance (Serial m (JsonRepr s), Serial m (V.Vector (JsonRepr s)), SingI cs)
+  => Serial m (JsonRepr ('SchemaArray cs s)) where
+  series = decDepth $ fmap ReprArray
+    $ arraySeries $ fromSing (sing :: Sing cs)
+
+instance (Serial m (JsonRepr s))
+  => Serial m (JsonRepr ('SchemaOptional s)) where
+  series = cons1 ReprOptional
+
+instance
+  ( Monad m, Serial m (Rec FieldRepr fs), ReprObjectConstr fs)
+  => Serial m (JsonRepr ('SchemaObject fs)) where
+  series = cons1 ReprObject
 
 instance IsList (JsonRepr ('SchemaArray cs s)) where
   type Item (JsonRepr ('SchemaArray cs s)) = JsonRepr s
@@ -462,7 +204,7 @@ instance IsString (JsonRepr ('SchemaText cs)) where
   fromString = ReprText . fromString
 
 fromOptional
-  :: SingI s
+  :: (SingI s, FromJSON (JsonRepr s))
   => Sing ('SchemaOptional s)
   -> J.Value
   -> Parser (Maybe (JsonRepr s))
@@ -478,7 +220,8 @@ parseUnion _ val = parseJSON val
 instance FromJSON (Union JsonRepr '[]) where
   parseJSON = fail "empty union"
 
-instance (SingI a, FromJSON (Union JsonRepr as)) => FromJSON (Union JsonRepr (a ': as)) where
+instance (SingI a, FromJSON (JsonRepr a), FromJSON (Union JsonRepr as))
+  => FromJSON (Union JsonRepr (a ': as)) where
   parseJSON val = (This <$> parseJSON val)
     <|> (That <$> (parseJSON val :: Parser (Union JsonRepr as)))
 
@@ -486,49 +229,57 @@ instance ToJSON (Union JsonRepr as) where
   toJSON (This fa) = toJSON fa
   toJSON (That u)  = toJSON u
 
-instance SingI schema => J.FromJSON (JsonRepr schema) where
-  parseJSON value = case sing :: Sing schema of
-    SSchemaText _          -> withText "String" (pure . ReprText) value
-    SSchemaNumber _        -> withScientific "Number" (pure . ReprNumber) value
-    SSchemaBoolean         -> ReprBoolean <$> parseJSON value
-    SSchemaNull            -> case value of
-      J.Null -> pure ReprNull
-      _      -> typeMismatch "Null" value
-    so@(SSchemaOptional s) -> withSingI s $ ReprOptional <$> fromOptional so value
-    SSchemaArray sa sb     -> withSingI sa $ withSingI sb
-      $ withArray "Array" (fmap ReprArray . traverse parseJSON) value
-    SSchemaObject fs       -> do
-      let
-        demoteFields :: SList s -> H.HashMap Text J.Value -> Parser (Rec FieldRepr s)
-        demoteFields SNil _ = pure RNil
-        demoteFields (SCons (STuple2 (n :: Sing fn) s) tl) h = withKnownSymbol n $ do
-          let fieldName = T.pack $ symbolVal (Proxy @fn)
-          fieldRepr <- case s of
-            SSchemaText so -> case H.lookup fieldName h of
-              Just v  -> withSingI so $ FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No text field: " P.++ show fieldName
-            SSchemaNumber so -> case H.lookup fieldName h of
-              Just v  -> withSingI so $ FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No number field: " P.++ show fieldName
-            SSchemaBoolean -> case H.lookup fieldName h of
-              Just v  -> FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No boolean field: " P.++ show fieldName
-            SSchemaNull -> case H.lookup fieldName h of
-              Just v  -> FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No null field: " P.++ show fieldName
-            SSchemaArray sa sb -> case H.lookup fieldName h of
-              Just v  -> withSingI sa $ withSingI sb $ FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No array field: " P.++ show fieldName
-            SSchemaObject so -> case H.lookup fieldName h of
-              Just v  -> withSingI so $ FieldRepr <$> parseJSON v
-              Nothing -> fail $ "No object field" P.++ show fieldName
-            SSchemaOptional so -> case H.lookup fieldName h of
-              Just v -> withSingI so $ FieldRepr <$> parseJSON v
-              Nothing -> withSingI so $ pure $ FieldRepr $ ReprOptional Nothing
-            SSchemaUnion ss -> withSingI ss $ FieldRepr <$> parseUnion ss value
-          (fieldRepr :&) <$> demoteFields tl h
-      ReprObject <$> withObject "Object" (demoteFields fs) value
-    SSchemaUnion ss -> parseUnion ss value
+instance J.FromJSON (JsonRepr ('SchemaText cs)) where
+  parseJSON = withText "String" (pure . ReprText)
+
+instance J.FromJSON (JsonRepr ('SchemaNumber cs)) where
+  parseJSON = withScientific "Number" (pure . ReprNumber)
+
+instance J.FromJSON (JsonRepr 'SchemaBoolean) where
+  parseJSON = fmap ReprBoolean . parseJSON
+
+instance J.FromJSON (JsonRepr 'SchemaNull) where
+  parseJSON value = case value of
+    J.Null -> pure ReprNull
+    _      -> typeMismatch "Null" value
+
+instance
+  J.FromJSON (JsonRepr s) =>  J.FromJSON (JsonRepr ('SchemaOptional s)) where
+  parseJSON = fmap ReprOptional . parseJSON
+
+instance
+  J.FromJSON (JsonRepr sb) => J.FromJSON (JsonRepr ('SchemaArray sa sb)) where
+  parseJSON = withArray "Array" (fmap ReprArray . traverse parseJSON)
+
+instance
+  ( SingI x, ReprUnionConstr xs
+  , FromJSON (Union JsonRepr xs), FromJSON (JsonRepr x) )
+  => J.FromJSON (JsonRepr ('SchemaUnion (x ': xs))) where
+  parseJSON = fmap ReprUnion . parseJSON
+
+class FromHashMap (xs :: [(Symbol, Schema)]) where
+  fromHashMap :: H.HashMap Text J.Value -> Parser (Rec FieldRepr xs)
+
+instance FromHashMap '[] where
+  fromHashMap _ = pure RNil
+
+instance
+  (KnownSymbol n, SingI s, FromHashMap xs, FromJSON (JsonRepr s))
+  => FromHashMap ( '(n,s) ': xs) where
+  fromHashMap h = do
+    fr <- case H.lookup fn h of
+      Nothing -> case (sing :: Sing s) of
+        SSchemaOptional _ -> pure $ FieldRepr @s $ ReprOptional Nothing
+        _ -> fail $ "No " <> schemaTypeStr @s <> " field: " <> show fn
+      Just v -> FieldRepr @s <$> parseJSON v
+    frs <- fromHashMap @xs h
+    pure $ fr :& frs
+    where
+      fn = demote' @n
+
+instance (FromHashMap rs, ReprObjectConstr rs)
+  => J.FromJSON (JsonRepr ('SchemaObject rs)) where
+  parseJSON = fmap ReprObject . withObject "Object" fromHashMap
 
 instance J.ToJSON (JsonRepr a) where
   toJSON ReprNull         = J.Null
@@ -551,9 +302,10 @@ instance J.ToJSON (JsonRepr a) where
         fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
   toJSON (ReprUnion u) = toJSON u
 
-class FalseConstraint a
+-- class FalseConstraint a
 
 type family TopLevel (schema :: Schema) :: Constraint where
   TopLevel ('SchemaArray acs s) = ()
   TopLevel ('SchemaObject o)    = ()
-  TopLevel spec                 = 'True ~ 'False
+  TopLevel spec                 = TypeError ('TL.Text "Only Object or Array"
+    ':$$: 'TL.Text "   should be on the top level")
diff --git a/src/Data/Schematic/Schema.hs-boot b/src/Data/Schematic/Schema.hs-boot
deleted file mode 100644
index e0444f5..0000000
--- a/src/Data/Schematic/Schema.hs-boot
+++ /dev/null
@@ -1,87 +0,0 @@
-module Data.Schematic.Schema where
-
-import           Data.Kind
-import           Data.Maybe
-import           Data.Schematic.Instances ()
-import           Data.Scientific
-import           Data.Singletons.TH
-import           Data.Singletons.TypeLits
-import           Data.Text as T
-import           Data.Union
-import           Data.Vector as V
-import           Data.Vinyl hiding (Dict)
-import           Prelude as P
-
-data TextConstraint
-  = TEq Nat
-  | TLt Nat
-  | TLe Nat
-  | TGt Nat
-  | TGe Nat
-  | TRegex Symbol
-  | TEnum [Symbol]
-
-data DemotedTextConstraint
-  = DTEq Integer
-  | DTLt Integer
-  | DTLe Integer
-  | DTGt Integer
-  | DTGe Integer
-  | DTRegex Text
-  | DTEnum [Text]
-
-data NumberConstraint
-  = NLe Nat
-  | NLt Nat
-  | NGt Nat
-  | NGe Nat
-  | NEq Nat
-
-data DemotedNumberConstraint
-  = DNLe Integer
-  | DNLt Integer
-  | DNGt Integer
-  | DNGe Integer
-  | DNEq Integer
-
-data ArrayConstraint
-  = AEq Nat
-
-data DemotedArrayConstraint
-  = DAEq Integer
-
-data Schema
-  = SchemaText [TextConstraint]
-  | SchemaBoolean
-  | SchemaNumber [NumberConstraint]
-  | SchemaObject [(Symbol, Schema)]
-  | SchemaArray [ArrayConstraint] Schema
-  | SchemaNull
-  | SchemaOptional Schema
-  | SchemaUnion [Schema]
-
-data DemotedSchema
-  = DSchemaText [DemotedTextConstraint]
-  | DSchemaNumber [DemotedNumberConstraint]
-  | DSchemaBoolean
-  | DSchemaObject [(Text, DemotedSchema)]
-  | DSchemaArray [DemotedArrayConstraint] DemotedSchema
-  | DSchemaNull
-  | DSchemaOptional DemotedSchema
-  | DSchemaUnion [DemotedSchema]
-
-data FieldRepr :: (Symbol, Schema) -> Type where
-  FieldRepr
-    :: (SingI schema, KnownSymbol name)
-    => JsonRepr schema
-    -> FieldRepr '(name, schema)
-
-data JsonRepr :: Schema -> Type where
-  ReprText :: Text -> JsonRepr ('SchemaText cs)
-  ReprNumber :: Scientific -> JsonRepr ('SchemaNumber cs)
-  ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
-  ReprNull :: JsonRepr 'SchemaNull
-  ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
-  ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
-  ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
-  ReprUnion :: Union JsonRepr (h ': tl) -> JsonRepr ('SchemaUnion (h ': tl))
diff --git a/src/Data/Schematic/Validation.hs b/src/Data/Schematic/Validation.hs
index c7605f6..6210c25 100644
--- a/src/Data/Schematic/Validation.hs
+++ b/src/Data/Schematic/Validation.hs
@@ -6,18 +6,17 @@ import Data.Aeson
 import Data.Aeson.Types
 import Data.Foldable
 import Data.Functor.Identity
-import Data.Monoid
+import Data.Monoid ((<>))
+import Data.Schematic.Constraints
 import Data.Schematic.Path
 import Data.Schematic.Schema
 import Data.Scientific
 import Data.Singletons.Prelude
-import Data.Singletons.TypeLits
 import Data.Text as T
 import Data.Traversable
 import Data.Union
 import Data.Vector as V
 import Data.Vinyl
-import Data.Vinyl.TypeLevel
 import Prelude as P
 import Text.Regex.TDFA
 
@@ -38,7 +37,7 @@ instance (TopLevel a, SingI a, FromJSON (JsonRepr a))
 
 isValid :: ParseResult a -> Bool
 isValid (Valid _) = True
-isValid _ = False
+isValid _         = False
 
 isDecodingError :: ParseResult a -> Bool
 isDecodingError (DecodingError _) = True
@@ -53,151 +52,91 @@ validateTextConstraint
   -> Text
   -> Sing (tcs :: TextConstraint)
   -> Validation ()
-validateTextConstraint (JSONPath path) t = \case
-  STEq n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen == (fromIntegral $ T.length t)
-      errMsg    = "length should be == " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STLt n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen > (fromIntegral $ T.length t)
-      errMsg    = "length should be < " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STLe n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen >= (fromIntegral $ T.length t)
-      errMsg    = "length should be <= " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STGt n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen < (fromIntegral $ T.length t)
-      errMsg    = "length should be > " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STGe n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen <= (fromIntegral $ T.length t)
-      errMsg    = "length should be >= " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STRegex r -> do
-    let
-      regex     = withKnownSymbol r $ fromSing r
-      predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
-      errMsg    = "must match " <> regex
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  STEnum ss -> do
-    let
-      matching :: Sing (s :: [Symbol]) -> Bool
-      matching SNil              = False
-      matching (SCons s@SSym fs) = T.pack (symbolVal s) == t || matching fs
-      errMsg = "must be one of " <> T.pack (show (fromSing ss))
-      warn   = vWarning $ mmSingleton path (pure errMsg)
-    unless (matching ss) warn
+validateTextConstraint (JSONPath path) t s =
+  case (fromSing s :: TextConstraintT) of
+    TEq n -> checkLength n (==) "=="
+    TLt n -> checkLength n (<) "<"
+    TLe n -> checkLength n (<=) "<="
+    TGt n -> checkLength n (>) ">"
+    TGe n -> checkLength n (>=) ">="
+    TRegex r -> unless
+      (matchTest (makeRegex (T.unpack r) :: Regex) $ T.unpack t)
+      $ vWarning $ mmSingleton path $ pure $ path <> " must match " <> r
+    TEnum ss -> unless (t `P.elem` ss) $ vWarning $ mmSingleton path
+      $ pure $ path <> " must be one of " <> T.pack (show ss)
+  where
+    checkLength n f sf =
+      unless (f (fromIntegral $ T.length t) n)
+        $ vWarning $ mmSingleton path $ pure
+          $ "length of " <> path <> " should be " <> sf
+            <> " " <> T.pack (show n)
 
 validateNumberConstraint
   :: JSONPath
   -> Scientific
   -> Sing (tcs :: NumberConstraint)
   -> Validation ()
-validateNumberConstraint (JSONPath path) num = \case
-  SNEq n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = fromIntegral nlen == num
-      errMsg    = "should be == " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  SNGt n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = num > fromIntegral nlen
-      errMsg    = "should be > " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  SNGe n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = num >= fromIntegral nlen
-      errMsg    = "should be >= " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  SNLt n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = num < fromIntegral nlen
-      errMsg    = "should be < " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
-  SNLe n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = num <= fromIntegral nlen
-      errMsg    = "should be <= " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
+validateNumberConstraint (JSONPath path) num s =
+  case (fromSing s :: NumberConstraintT) of
+    NEq n -> checkVal n (==) "=="
+    NLt n -> checkVal n (<) "<"
+    NLe n -> checkVal n (<=) "<="
+    NGt n -> checkVal n (>) ">"
+    NGe n -> checkVal n (>=) ">="
+  where
+    checkVal n f sf =
+      unless (f num $ fromIntegral n)
+        $ vWarning $ mmSingleton path $ pure
+          $ path <> " should be " <> sf <> " " <> T.pack (show n)
 
 validateArrayConstraint
   :: JSONPath
   -> V.Vector a
   -> Sing (tcs :: ArrayConstraint)
   -> Validation ()
-validateArrayConstraint (JSONPath path) v = \case
-  SAEq n -> do
-    let
-      nlen      = withKnownNat n $ natVal n
-      predicate = nlen == fromIntegral (V.length v)
-      errMsg    = "length should be == " <> T.pack (show nlen)
-      warn      = vWarning $ mmSingleton path (pure errMsg)
-    unless predicate warn
+validateArrayConstraint (JSONPath path) v s =
+  case (fromSing s :: ArrayConstraintT) of
+   AEq n -> unless (V.length v == fromIntegral n)
+    $ vWarning $ mmSingleton path $ pure
+      $ "length of " <> path <> " should be == " <> T.pack (show n)
+
+class ValidateConstraint t c where
+  validateConstraint
+    :: [DemotedPathSegment] -> t -> Sing (a::c) -> Validation ()
+
+instance ValidateConstraint Text TextConstraint where
+  validateConstraint = validateTextConstraint . demotedPathToText
+
+instance ValidateConstraint Scientific NumberConstraint where
+  validateConstraint = validateNumberConstraint . demotedPathToText
+
+instance ValidateConstraint (V.Vector a) ArrayConstraint where
+  validateConstraint = validateArrayConstraint . demotedPathToText
+
+validateConstraints
+  :: ValidateConstraint t c
+  => [DemotedPathSegment] -> t -> Sing (cs :: [c]) -> Validation ()
+validateConstraints _ _ SNil = pure ()
+validateConstraints dp t (SCons c cs) = do
+  validateConstraint dp t c >> validateConstraints dp t cs
 
 validateJsonRepr
   :: Sing schema
   -> [DemotedPathSegment]
   -> JsonRepr schema
   -> Validation ()
-validateJsonRepr sschema dpath jr = case jr of
+validateJsonRepr sschema dpath = \case
   ReprText t -> case sschema of
-    SSchemaText scs -> do
-      let
-        process :: Sing (cs :: [TextConstraint]) -> Validation ()
-        process SNil         = pure ()
-        process (SCons c cs) = do
-          validateTextConstraint (demotedPathToText dpath) t c
-          process cs
-      process scs
+    SSchemaText scs -> validateConstraints dpath t scs
   ReprNumber n -> case sschema of
-    SSchemaNumber scs -> do
-      let
-        process :: Sing (cs :: [NumberConstraint]) -> Validation ()
-        process SNil         = pure ()
-        process (SCons c cs) = do
-          validateNumberConstraint (demotedPathToText dpath) n c
-          process cs
-      process scs
-  ReprNull -> pure ()
+    SSchemaNumber scs -> validateConstraints dpath n scs
+  ReprNull  -> pure ()
   ReprBoolean _ -> pure ()
   ReprArray v -> case sschema of
     SSchemaArray acs s -> do
-      let
-        process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
-        process SNil         = pure ()
-        process (SCons c cs) = do
-          validateArrayConstraint (demotedPathToText dpath) v c
-          process cs
-      process acs
+      validateConstraints dpath v acs
       for_ (V.indexed v) $ \(ix, jr') -> do
-        let newPath = dpath <> pure (DIx $ fromIntegral ix)
+        let newPath = dpath <> pure (Ix $ fromIntegral ix)
         validateJsonRepr s newPath jr'
   ReprOptional d -> case sschema of
     SSchemaOptional ss -> case d of
@@ -209,49 +148,17 @@ validateJsonRepr sschema dpath jr = case jr of
         go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
         go RNil                     = pure ()
         go (f@(FieldRepr d) :& ftl) = do
-          let newPath = dpath <> [DKey (knownFieldName f)]
+          let newPath = dpath <> [Key (knownFieldName f)]
           validateJsonRepr (knownFieldSchema f) newPath d
           go ftl
-  ReprUnion _ -> pure () -- FIXME
-    -- case sschema of
-    --   SSchemaUnion ss -> case ss of
-    --     SCons s stl -> case umatch' s u of
-    --       Nothing -> case urestrict u of
-    --         Nothing ->
-    --           fail "impossible to produce subUnion, please report this as a bug"
-    --         Just x -> do
-    --           let
-    --             JSONPath path = demotedPathToText dpath
-    --           case stl of
-    --             SNil -> void $ vWarning $ mmSingleton path
-    --               $ pure "union handling error, please report this as bug"
-    --             SCons s' stl' ->
-    --               validateJsonRepr (SSchemaUnion (SCons s' stl')) dpath
-    --                 $ toUnion (SCons s' stl') x
-    --       Just x  -> validateJsonRepr s dpath x
-
--- subUnion
---   :: Sing (s ': stl)
---   -> (  USubset stl (s ': stl) (RImage stl (s ': stl))
---      => Union f (s ': stl)
---      -> Maybe (Union f stl) )
--- subUnion (SCons s stl) = urestrict
-
--- withUSubset
---   :: Sing (s ': stl)
---   -> (USubset stl (s ': stl) (RImage stl (s ': stl)) => Maybe (Union f stl))
---   -> Maybe (Union f stl)
--- withUSubset (SCons s stl) r = r
-
-toUnion
-  :: USubset s' (s ': ss) (RImage s' (s ': ss))
-  => Sing (s ': ss)
-  -> Union JsonRepr s'
-  -> JsonRepr ('SchemaUnion (s ': ss))
-toUnion _ = ReprUnion . urelax
-
-umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
-umatch' _ u = umatch u
+  ReprUnion ru -> case sschema of
+    SSchemaUnion su -> validateUnion su ru
+    where
+      validateUnion :: Sing us -> Union JsonRepr us -> Validation ()
+      validateUnion ss r  = case (ss,r) of
+        (SCons s _, This v)     -> validateJsonRepr s dpath v
+        (SCons _ stl, That r')  -> validateUnion stl r'
+        (SNil,_) -> fail "Invalid union. Please report this as a bug"
 
 parseAndValidateJson
   :: forall schema
@@ -268,10 +175,3 @@ parseAndValidateJson v =
       in case res of
         Left em  -> ValidationError em
         Right () -> Valid jsonRepr
-
-parseAndValidateJsonBy
-  :: (FromJSON (JsonRepr schema), TopLevel schema, SingI schema)
-  => proxy schema
-  -> Value
-  -> ParseResult (JsonRepr schema)
-parseAndValidateJsonBy _ = parseAndValidateJson
diff --git a/src/Data/Schematic/Verifier/Array.hs b/src/Data/Schematic/Verifier/Array.hs
index 7280f55..71a3b32 100644
--- a/src/Data/Schematic/Verifier/Array.hs
+++ b/src/Data/Schematic/Verifier/Array.hs
@@ -1,14 +1,14 @@
 module Data.Schematic.Verifier.Array where
 
-import {-# SOURCE #-} Data.Schematic.Schema
+import Data.Schematic.Compat
+import Data.Schematic.Constraints
 import Data.Schematic.Verifier.Common
 
+
 data VerifiedArrayConstraint =
-  VAEq Integer
+  VAEq DeNat
   deriving (Show)
 
-verifyArrayConstraint ::
-     [DemotedArrayConstraint] -> Maybe (Maybe VerifiedArrayConstraint)
-verifyArrayConstraint cs = do
-  x <- verifyDNEq [x | DAEq x <- cs]
-  pure $ VAEq <$> x
+verifyArrayConstraint
+  :: [ArrayConstraintT] -> Maybe (Maybe VerifiedArrayConstraint)
+verifyArrayConstraint cs = fmap VAEq <$> verifyNEq [x | AEq x <- cs]
diff --git a/src/Data/Schematic/Verifier/Common.hs b/src/Data/Schematic/Verifier/Common.hs
index d334878..9406b76 100644
--- a/src/Data/Schematic/Verifier/Common.hs
+++ b/src/Data/Schematic/Verifier/Common.hs
@@ -1,41 +1,43 @@
 module Data.Schematic.Verifier.Common where
 
 import Data.List (nub)
+import Data.Schematic.Compat
 
-simplifyNumberConstraint :: ([Integer] -> Integer) -> [Integer] -> Maybe Integer
+
+simplifyNumberConstraint :: ([DeNat] -> DeNat) -> [DeNat] -> Maybe DeNat
 simplifyNumberConstraint f =
   \case
     [] -> Nothing
     x -> Just $ f x
 
-simplifyDNLs :: [Integer] -> Maybe Integer
-simplifyDNLs = simplifyNumberConstraint minimum
+simplifyNLs :: [DeNat] -> Maybe DeNat
+simplifyNLs = simplifyNumberConstraint minimum
 
-simplifyDNGs :: [Integer] -> Maybe Integer
-simplifyDNGs = simplifyNumberConstraint maximum
+simplifyNGs :: [DeNat] -> Maybe DeNat
+simplifyNGs = simplifyNumberConstraint maximum
 
-verifyDNEq :: [Integer] -> Maybe (Maybe Integer)
-verifyDNEq x =
+verifyNEq :: [DeNat] -> Maybe (Maybe DeNat)
+verifyNEq x =
   case nub x of
     []      -> Just Nothing
     [y]     -> Just $ Just y
     (_:_:_) -> Nothing
 
-verify3 :: Maybe Integer -> Maybe Integer -> Maybe Integer -> Maybe ()
+verify3 :: Maybe DeNat -> Maybe DeNat -> Maybe DeNat -> Maybe ()
 verify3 (Just x) (Just y) (Just z) =
   if x < y && y < z
     then Just ()
     else Nothing
 verify3 _ _ _ = Just ()
 
-verify2 :: Maybe Integer -> Maybe Integer -> Maybe ()
+verify2 :: Maybe DeNat -> Maybe DeNat -> Maybe ()
 verify2 (Just x) (Just y) =
   if x < y
     then Just ()
     else Nothing
 verify2 _ _ = Just ()
 
-verifyEquations :: Maybe Integer -> Maybe Integer -> Maybe Integer -> Maybe ()
+verifyEquations :: Maybe DeNat -> Maybe DeNat -> Maybe DeNat -> Maybe ()
 verifyEquations mgt meq mlt = do
   verify3 mgt meq mlt
   verify2 mgt meq
diff --git a/src/Data/Schematic/Verifier/Number.hs b/src/Data/Schematic/Verifier/Number.hs
index a8d239b..5e41cc9 100644
--- a/src/Data/Schematic/Verifier/Number.hs
+++ b/src/Data/Schematic/Verifier/Number.hs
@@ -1,29 +1,31 @@
 module Data.Schematic.Verifier.Number where
 
-import {-# SOURCE #-} Data.Schematic.Schema
+import Data.Schematic.Compat
+import Data.Schematic.Constraints
 import Data.Schematic.Verifier.Common
 
-toStrictNumber :: [DemotedNumberConstraint] -> [DemotedNumberConstraint]
+
+toStrictNumber :: [NumberConstraintT] -> [NumberConstraintT]
 toStrictNumber = map f
   where
-    f (DNLe x) = DNLt (x + 1)
-    f (DNGe x) = DNGt (x - 1)
-    f x        = x
+    f (NLe x) = NLt (x + 1)
+    f (NGe x) = NGt (x - 1)
+    f x       = x
 
 data VerifiedNumberConstraint
-  = VNEq Integer
-  | VNBounds (Maybe Integer) (Maybe Integer)
+  = VNEq DeNat
+  | VNBounds (Maybe DeNat) (Maybe DeNat)
   deriving (Show)
 
 verifyNumberConstraints
-  :: [DemotedNumberConstraint]
+  :: [NumberConstraintT]
   -> Maybe VerifiedNumberConstraint
 verifyNumberConstraints cs' = do
   let
     cs = toStrictNumber cs'
-    mlt = simplifyDNLs [x | DNLt x <- cs]
-    mgt = simplifyDNGs [x | DNGt x <- cs]
-  meq <- verifyDNEq [x | DNEq x <- cs]
+    mlt = simplifyNLs [x | NLt x <- cs]
+    mgt = simplifyNGs [x | NGt x <- cs]
+  meq <- verifyNEq [x | NEq x <- cs]
   verifyEquations mgt meq mlt
   Just $
     case meq of
diff --git a/src/Data/Schematic/Verifier/Text.hs b/src/Data/Schematic/Verifier/Text.hs
index 485db87..0c0b5de 100644
--- a/src/Data/Schematic/Verifier/Text.hs
+++ b/src/Data/Schematic/Verifier/Text.hs
@@ -2,37 +2,39 @@ module Data.Schematic.Verifier.Text where
 
 import Control.Monad
 import Data.Maybe
-import {-# SOURCE #-} Data.Schematic.Schema
+import Data.Schematic.Compat
+import Data.Schematic.Constraints
 import Data.Schematic.Verifier.Common
 import Data.Text (Text, unpack)
 import Text.Regex.TDFA.Pattern
 import Text.Regex.TDFA.ReadRegex (parseRegex)
 
-toStrictTextLength :: [DemotedTextConstraint] -> [DemotedTextConstraint]
+
+toStrictTextLength :: [TextConstraintT] -> [TextConstraintT]
 toStrictTextLength = map f
   where
-    f (DTLe x) = DTLt (x + 1)
-    f (DTGe x) = DTGt (x - 1)
-    f x        = x
+    f (TLe x) = TLt (x + 1)
+    f (TGe x) = TGt (x - 1)
+    f x       = x
 
 data VerifiedTextConstraint
-  = VTEq Integer
-  | VTBounds (Maybe Integer) (Maybe Integer)
-  | VTRegex Text Integer (Maybe Integer)
+  = VTEq DeNat
+  | VTBounds (Maybe DeNat) (Maybe DeNat)
+  | VTRegex Text DeNat (Maybe DeNat)
   | VTEnum [Text]
   deriving (Show)
 
 verifyTextLengthConstraints
-  :: [DemotedTextConstraint]
+  :: [TextConstraintT]
   -> Maybe (Maybe VerifiedTextConstraint)
 verifyTextLengthConstraints cs' = do
   let
     cs = toStrictTextLength cs'
-    mlt = simplifyDNLs [x | DTLt x <- cs]
-    mgt = simplifyDNGs [x | DTGt x <- cs]
-  meq <- verifyDNEq [x | DTEq x <- cs]
+    mlt = simplifyNLs [x | TLt x <- cs]
+    mgt = simplifyNGs [x | TGt x <- cs]
+  meq <- verifyNEq [x | TEq x <- cs]
   verifyEquations mgt meq mlt
-  case all isNothing ([mgt, meq, mlt] :: [Maybe Integer]) of
+  case all isNothing ([mgt, meq, mlt] :: [Maybe DeNat]) of
     True -> Just Nothing
     _    ->
       Just $
@@ -86,10 +88,10 @@ maxRegexLength p =
     _                  -> Just 0
 
 verifyTextRegexConstraint
-  :: [DemotedTextConstraint]
+  :: [TextConstraintT]
   -> Maybe (Maybe VerifiedTextConstraint)
 verifyTextRegexConstraint cs = do
-  let regexps = [x | DTRegex x <- cs]
+  let regexps = [x | TRegex x <- cs]
   case regexps of
     []  -> Just Nothing
     [x] -> do
@@ -98,23 +100,23 @@ verifyTextRegexConstraint cs = do
     _   -> Nothing
 
 verifyTextEnumConstraint
-  :: [DemotedTextConstraint]
+  :: [TextConstraintT]
   -> Maybe (Maybe VerifiedTextConstraint)
 verifyTextEnumConstraint cs = do
-  let enums = concat [x | DTEnum x <- cs]
+  let enums = concat [x | TEnum x <- cs]
   case enums of
     [] -> Just Nothing
     x  -> Just $ Just $ VTEnum x
 
 verifyTextConstraints
-  :: [DemotedTextConstraint]
+  :: [TextConstraintT]
   -> Maybe [VerifiedTextConstraint]
 verifyTextConstraints cs = do
   regexp <- verifyTextRegexConstraint cs
   void $
     case regexp of
       Just (VTRegex _ l mh) ->
-        verifyTextLengthConstraints (DTGe l : cs ++ maybeToList (DTLe <$> mh))
+        verifyTextLengthConstraints (TGe l : cs ++ maybeToList (TLe <$> mh))
       _                     -> pure Nothing
   lengths <- verifyTextLengthConstraints cs
   enums <- verifyTextEnumConstraint cs
diff --git a/stack.yaml b/stack.yaml
index 8b81f4c..3babde0 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,4 +1,6 @@
-resolver: lts-12.0
+# resolver: lts-13.7
+# resolver: lts-12.0
+resolver: lts-10.0
 extra-deps:
   - hjsonpointer-1.4.0@rev:0
   - hjsonschema-1.9.0@rev:0
diff --git a/test/HelpersSpec.hs b/test/HelpersSpec.hs
index 65d2255..dff1243 100644
--- a/test/HelpersSpec.hs
+++ b/test/HelpersSpec.hs
@@ -1,17 +1,16 @@
 {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
-
-{-# LANGUAGE LambdaCase #-}
-
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds         #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module HelpersSpec (spec, main) where
 
 import Control.Lens
 import Data.ByteString.Lazy.Lens
 import Data.Foldable
-import Data.Monoid
+import Data.Monoid ((<>))
 import Data.Schematic
 import Data.Text as T
 import Data.Text.Lens
diff --git a/test/JsonSchemaSpec.hs b/test/JsonSchemaSpec.hs
index 312c919..762ac8b 100644
--- a/test/JsonSchemaSpec.hs
+++ b/test/JsonSchemaSpec.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LambdaCase        #-}
 
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE OverloadedLists   #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds         #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module JsonSchemaSpec (spec, main) where
 
diff --git a/test/LensSpec.hs b/test/LensSpec.hs
index b28d1c0..a15ef99 100644
--- a/test/LensSpec.hs
+++ b/test/LensSpec.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE OverloadedLists   #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds         #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module LensSpec (spec, main) where
 
 import Control.Lens
-import Data.Proxy
 import Data.Schematic
 import Data.Vinyl
 import Test.Hspec
@@ -301,7 +301,6 @@ spec :: Spec
 spec = do
   let
     newFooVal = FieldRepr $ ReprArray [ReprNumber 15]
-    fooProxy  = Proxy @"foo"
   it "gets the field from an object" $ do
     fget @"foo" objectData `shouldBe` arrayField
   it "sets the object field" $ do
diff --git a/test/SchemaSpec.hs b/test/SchemaSpec.hs
index 3ce30ad..50720b9 100644
--- a/test/SchemaSpec.hs
+++ b/test/SchemaSpec.hs
@@ -1,33 +1,29 @@
 {-# OPTIONS_GHC -fprint-potential-instances #-}
-
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE OverloadedLists #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
+
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE OverloadedLists     #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeApplications    #-}
 
 module SchemaSpec (spec, main) where
 
 import Control.Lens
 import Data.Aeson
 import Data.ByteString.Lazy
-import Data.Functor.Identity
+import Data.Monoid ((<>))
 import Data.Proxy
 import Data.Schematic
-import Data.Schematic.Generator
-import Data.Singletons
-import Data.Tagged
 import Data.Vinyl
 import Test.Hspec
 import Test.Hspec.SmallCheck
 import Test.SmallCheck as SC
-import Test.SmallCheck.Drivers as SC
 import Test.SmallCheck.Series as SC
 
-import Debug.Trace
 
 type SchemaExample = 'SchemaObject
   '[ '("foo", 'SchemaArray '[ 'AEq 1] ('SchemaNumber '[ 'NGt 10]))
@@ -37,6 +33,12 @@ type SchemaExample2 = 'SchemaObject
   '[ '("foo", 'SchemaArray '[ 'AEq 2] ('SchemaText '[ 'TGt 10]))
    , '("bar", 'SchemaOptional ('SchemaText '[ 'TRegex "[0-9]+"]))]
 
+type SchemaExample3 = 'SchemaUnion '[SchemaExample]
+
+type SchemaExample4 = 'SchemaObject
+  '[ '("baz3", SchemaExample3)
+  ,  '("baz1", SchemaExample)]
+
 jsonExample :: JsonRepr SchemaExample
 jsonExample = withRepr @SchemaExample
    $ field @"bar" (Just "bar")
@@ -45,7 +47,7 @@ jsonExample = withRepr @SchemaExample
 
 type AddQuuz =
   'Migration "add_field_quuz"
-   '[ 'Diff '[] ('AddKey "quuz" (SchemaNumber '[])) ]
+   '[ 'Diff '[] ('AddKey "quuz" ('SchemaNumber '[])) ]
 
 type DeleteQuuz =
   'Migration "remove_field_quuz"
@@ -80,6 +82,12 @@ schemaJson = "{\"foo\": [13], \"bar\": null}"
 schemaJson2 :: ByteString
 schemaJson2 = "{\"foo\": [3], \"bar\": null}"
 
+schemaJson3 :: ByteString
+schemaJson3 = schemaJson
+
+schemaJson4 :: ByteString
+schemaJson4 = "{\"baz1\": "<>schemaJson<>", \"baz3\": "<>schemaJson3<>"}"
+
 schemaJsonSeries :: Monad m => SC.Series m (JsonRepr SchemaExample)
 schemaJsonSeries = series
 
@@ -93,7 +101,7 @@ spec = do
   it "decode/encode JsonRepr properly" $
     decode (encode jsonExample) == Just jsonExample
   it "validates correct representation" $
-    ((decodeAndValidateJson schemaJson) :: ParseResult (JsonRepr SchemaExample))
+    ((decodeAndValidateJson schemaJson4) :: ParseResult (JsonRepr SchemaExample4))
       `shouldSatisfy` isValid
   it "returns decoding error on structurally incorrect input" $
     ((decodeAndValidateJson "{}") :: ParseResult (JsonRepr SchemaExample))