{-# 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' :: ValidSize ('S n) -> ValidSize n
smallerIsValid' = \(ValidSize (SS SNat n
n) forall r. TooBig ('S n) -> r
tooBig) -> SNat n -> (forall r. TooBig n -> r) -> ValidSize n
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat n
n ((forall r. TooBig n -> r) -> ValidSize n)
-> (forall r. TooBig n -> r) -> ValidSize n
forall a b. (a -> b) -> a -> b
$ (TooBig ('S n) -> r) -> TooBig n -> r
forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
forall r. TooBig ('S n) -> r
tooBig
  where
    aux :: (TooBig ('S n) -> r) -> TooBig n -> r
    aux :: (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
tooBig TooBig n
TooBig = TooBig ('S n) -> r
tooBig (TooBig ('S n)
forall (n :: 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
                                                                                                                                                                                               n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
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 :: Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid Proxy ('S n)
_ IsValidSize n => r
k =
    case ValidSize n -> Dict IsValidSize n
forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize ('S n) -> ValidSize n
forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' ValidSize ('S n)
valid) of
      Dict IsValidSize n
Dict -> r
IsValidSize n => r
k
  where
    valid :: ValidSize ('S n)
    valid :: ValidSize ('S n)
valid = ValidSize ('S n)
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 :: 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 =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS SNat n
SZ) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS SNat n
SZ)) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS SNat n
SZ))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS SNat n
SZ)))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS SNat n
SZ))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS SNat n
SZ)))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))) =
        Dict IsValidSize n
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)))))))) =
        Dict IsValidSize n
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))))))))) =
        Dict IsValidSize n
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)))))))))) =
        Dict IsValidSize n
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))))))))))) =
        Dict IsValidSize n
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)))))))))))) =
        Dict IsValidSize n
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))))))))))))) =
        Dict IsValidSize n
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)))))))))))))) =
        Dict IsValidSize n
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))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
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
_))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        TooBig n -> Dict IsValidSize n
forall r. TooBig n -> r
notTooBig (TooBig n
forall (n :: 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
                                                                                                                                                                                               n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig n)

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

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

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

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

instance IsValidSize ('S ('S ('S ('S 'Z)))) where
  isValidSize :: ValidSize ('S ('S ('S ('S 'Z))))
isValidSize = SNat ('S ('S ('S ('S 'Z))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S 'Z))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
 -> ValidSize ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S 'Z)))) -> r
forall r. 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 = SNat ('S ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
forall r. 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 = SNat ('S ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
forall r. 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 = SNat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
forall r. 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 = SNat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
forall r. 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 = SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
forall r.
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 = SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
forall r.
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 = SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
  -> r)
 -> ValidSize
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
forall r.
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 = SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
  -> r)
 -> ValidSize
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
forall r.
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 = SNat
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
forall r.
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 = SNat
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
    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)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
    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)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))
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
forall r.
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 = SNat
  ('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))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('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))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('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)))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('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)))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('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))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('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))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('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)))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('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)))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('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))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('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))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('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)))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('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)))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('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))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('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))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('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)))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('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)))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('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))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('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))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('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)))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('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)))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('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))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('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))))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('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)))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('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)))))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('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))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('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))))))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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)))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('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)))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('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)))))))))))))))))))))))))))))))))))))
forall (n :: Nat). KnownNat n => SNat n
singNat ((forall r.
  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)
 -> 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))))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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)))))))))))))))))))))))))))))))))))))
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
forall r.
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 = SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('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))))))))))))))))))))))))))))))))))))))
-> (forall r.
    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)
-> 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))))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S