{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -fno-opt-coercion #-}

-- | Valid tuple size
module Debug.RecoverRTTI.Tuple.Size (
    ValidSize(..)
  , TooBig(..)
  , smallerIsValid
  , IsValidSize(..)
  , liftValidSize
  , toValidSize
  ) where

import Data.Proxy
import Data.SOP.Dict

import Debug.RecoverRTTI.Nat
import Debug.RecoverRTTI.Util

{-------------------------------------------------------------------------------
  Not generated
-------------------------------------------------------------------------------}

data ValidSize (n :: Nat) where
  ValidSize :: SNat n -> (forall r. TooBig n -> r) -> ValidSize n

smallerIsValid' :: forall n. ValidSize ('S n) -> ValidSize n
smallerIsValid' :: forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' = \(ValidSize (SS SNat n
n) forall r. TooBig ('S n) -> r
tooBig) -> forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat n
n forall a b. (a -> b) -> a -> b
$ forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux forall r. TooBig ('S n) -> r
tooBig
  where
    aux :: (TooBig ('S n) -> r) -> TooBig n -> r
    aux :: forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
tooBig TooBig n
TooBig = TooBig ('S n) -> r
tooBig (forall (a :: Nat).
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            ('S
                                                                                                                                                                                               a)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig ('S n))

-- | Smaller tuple sizes are always valid
--
-- This function is primarily useful when doing recursion on tuples: we may have
-- in scope evidence that @('S n)@ is a valid tuple size, and need to know that
-- @n@ is a valid tuple size in order to be able to make the recursive call.
smallerIsValid :: forall n r.
     IsValidSize ('S n)
  => Proxy ('S n)
  -> (IsValidSize n => r)
  -> r
smallerIsValid :: forall (n :: Nat) r.
IsValidSize ('S n) =>
Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid Proxy ('S n)
_ IsValidSize n => r
k =
    case forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' ValidSize ('S n)
valid) of
      Dict IsValidSize n
Dict -> IsValidSize n => r
k
  where
    valid :: ValidSize ('S n)
    valid :: ValidSize ('S n)
valid = forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize

-- | Valid tuple sizes
--
-- GHC does not support tuples larger than 62 fields. We do allow for tuples of
-- zero size (which we interpret as unit @()@) and tuples of size one
-- (where @Tuple '[x] ~ x@).
class KnownNat n => IsValidSize n where
  isValidSize :: ValidSize n

{-------------------------------------------------------------------------------
  Generated
-------------------------------------------------------------------------------}

-- | Tuples with too many fields (more than 62)
data TooBig (n :: Nat) where
  TooBig :: TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

-- | Lift term-level evidence to type-level
liftValidSize :: forall n. ValidSize n -> Dict IsValidSize n
liftValidSize :: forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize SNat n
n forall r. TooBig n -> r
notTooBig) = SNat n -> Dict IsValidSize n
go SNat n
n
  where
    go :: SNat n -> Dict IsValidSize n
    go :: SNat n -> Dict IsValidSize n
go SNat n
SZ =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS SNat n
SZ) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS SNat n
SZ)) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS SNat n
SZ))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS SNat n
SZ)))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS SNat n
SZ))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS SNat n
SZ)))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
_))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        forall r. TooBig n -> r
notTooBig (forall (a :: Nat).
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            ('S
                                                                                                                                                                                               a)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig n)

instance IsValidSize 'Z where
  isValidSize :: ValidSize 'Z
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig 'Z -> r
\case

instance IsValidSize ('S 'Z) where
  isValidSize :: ValidSize ('S 'Z)
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S 'Z) -> r
\case

instance IsValidSize ('S ('S 'Z)) where
  isValidSize :: ValidSize ('S ('S 'Z))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S 'Z)) -> r
\case

instance IsValidSize ('S ('S ('S 'Z))) where
  isValidSize :: ValidSize ('S ('S ('S 'Z)))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S 'Z))) -> r
\case

instance IsValidSize ('S ('S ('S ('S 'Z)))) where
  isValidSize :: ValidSize ('S ('S ('S ('S 'Z))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S 'Z)))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S 'Z))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S 'Z)))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S 'Z)))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))) where
  isValidSize :: ValidSize
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))) where
  isValidSize :: ValidSize
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    'Z))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    'Z))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       'Z)))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       'Z)))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          'Z))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          'Z))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             'Z)))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             'Z)))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                'Z))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                'Z))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   'Z)))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   'Z)))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      'Z))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      'Z))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         'Z)))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         'Z)))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            'Z))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            'Z))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               'Z)))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               'Z)))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  'Z))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  'Z))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     'Z)))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     'Z)))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        'Z))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        'Z))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case

-- | Check the given size is a valid tuple size
toValidSize :: Int -> Maybe (Some ValidSize)
toValidSize :: Int -> Maybe (Some ValidSize)
toValidSize = Int -> Maybe (Some ValidSize)
go
  where
    go :: Int -> Maybe (Some ValidSize)
    go :: Int -> Maybe (Some ValidSize)
go Int
0 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @'Z
    go Int
1 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S 'Z)
    go Int
2 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S 'Z))
    go Int
3 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S 'Z)))
    go Int
4 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S 'Z))))
    go Int
5 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S 'Z)))))
    go Int
6 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S 'Z))))))
    go Int
7 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S 'Z)))))))
    go Int
8 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
    go Int
9 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
    go Int
10 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
    go Int
11 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
    go Int
12 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
    go Int
13 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
    go Int
14 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
    go Int
15 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
    go Int
16 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
    go Int
17 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
    go Int
18 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
    go Int
19 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
    go Int
20 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
    go Int
21 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
    go Int
22 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
    go Int
23 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))
    go Int
24 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))
    go Int
25 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))
    go Int
26 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))
    go Int
27 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))
    go Int
28 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))
    go Int
29 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))
    go Int
30 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))
    go Int
31 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))
    go Int
32 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))
    go Int
33 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))
    go Int
34 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))
    go Int
35 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))
    go Int
36 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))
    go Int
37 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))
    go Int
38 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))
    go Int
39 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))
    go Int
40 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))
    go Int
41 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))
    go Int
42 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))
    go Int
43 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))
    go Int
44 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))
    go Int
45 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))
    go Int
46 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))
    go Int
47 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))
    go Int
48 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
49 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
50 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
51 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
52 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
53 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
54 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
55 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
56 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
57 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
58 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
59 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
60 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
61 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
62 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    go Int
_ = forall a. Maybe a
Nothing