Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations singletons [d| data Nat = Zero | Succ Nat deriving (Eq, Ord) data Foo a b c d = A a b c d | B a b c d | C a b c d | D a b c d | E a b c d | F a b c d deriving (Eq, Ord) |] ======> data Nat = Zero | Succ Nat deriving (Eq, Ord) data Foo a b c d = A a b c d | B a b c d | C a b c d | D a b c d | E a b c d | F a b c d deriving (Eq, Ord) type ZeroSym0 :: Nat type family ZeroSym0 :: Nat where ZeroSym0 = Zero type SuccSym0 :: (~>) Nat Nat data SuccSym0 :: (~>) Nat Nat where SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) => SuccSym0 a0123456789876543210 type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210 instance SuppressUnusedWarnings SuccSym0 where suppressUnusedWarnings = snd ((,) SuccSym0KindInference ()) type SuccSym1 :: Nat -> Nat type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where SuccSym1 a0123456789876543210 = Succ a0123456789876543210 type ASym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data ASym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where ASym0KindInference :: SameKind (Apply ASym0 arg) (ASym1 arg) => ASym0 a0123456789876543210 type instance Apply ASym0 a0123456789876543210 = ASym1 a0123456789876543210 instance SuppressUnusedWarnings ASym0 where suppressUnusedWarnings = snd ((,) ASym0KindInference ()) type ASym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data ASym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where ASym1KindInference :: SameKind (Apply (ASym1 a0123456789876543210) arg) (ASym2 a0123456789876543210 arg) => ASym1 a0123456789876543210 a0123456789876543210 type instance Apply (ASym1 a0123456789876543210) a0123456789876543210 = ASym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ASym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ASym1KindInference ()) type ASym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data ASym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where ASym2KindInference :: SameKind (Apply (ASym2 a0123456789876543210 a0123456789876543210) arg) (ASym3 a0123456789876543210 a0123456789876543210 arg) => ASym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ASym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ASym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ASym2KindInference ()) type ASym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data ASym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where ASym3KindInference :: SameKind (Apply (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (ASym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = A a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ASym3KindInference ()) type ASym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family ASym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where ASym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = A a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type BSym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data BSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where BSym0KindInference :: SameKind (Apply BSym0 arg) (BSym1 arg) => BSym0 a0123456789876543210 type instance Apply BSym0 a0123456789876543210 = BSym1 a0123456789876543210 instance SuppressUnusedWarnings BSym0 where suppressUnusedWarnings = snd ((,) BSym0KindInference ()) type BSym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data BSym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where BSym1KindInference :: SameKind (Apply (BSym1 a0123456789876543210) arg) (BSym2 a0123456789876543210 arg) => BSym1 a0123456789876543210 a0123456789876543210 type instance Apply (BSym1 a0123456789876543210) a0123456789876543210 = BSym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BSym1KindInference ()) type BSym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data BSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where BSym2KindInference :: SameKind (Apply (BSym2 a0123456789876543210 a0123456789876543210) arg) (BSym3 a0123456789876543210 a0123456789876543210 arg) => BSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (BSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BSym2KindInference ()) type BSym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data BSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where BSym3KindInference :: SameKind (Apply (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (BSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = B a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BSym3KindInference ()) type BSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family BSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where BSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = B a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type CSym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data CSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where CSym0KindInference :: SameKind (Apply CSym0 arg) (CSym1 arg) => CSym0 a0123456789876543210 type instance Apply CSym0 a0123456789876543210 = CSym1 a0123456789876543210 instance SuppressUnusedWarnings CSym0 where suppressUnusedWarnings = snd ((,) CSym0KindInference ()) type CSym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data CSym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where CSym1KindInference :: SameKind (Apply (CSym1 a0123456789876543210) arg) (CSym2 a0123456789876543210 arg) => CSym1 a0123456789876543210 a0123456789876543210 type instance Apply (CSym1 a0123456789876543210) a0123456789876543210 = CSym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (CSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CSym1KindInference ()) type CSym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data CSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where CSym2KindInference :: SameKind (Apply (CSym2 a0123456789876543210 a0123456789876543210) arg) (CSym3 a0123456789876543210 a0123456789876543210 arg) => CSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (CSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (CSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CSym2KindInference ()) type CSym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data CSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where CSym3KindInference :: SameKind (Apply (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (CSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = C a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CSym3KindInference ()) type CSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family CSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where CSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = C a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type DSym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data DSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where DSym0KindInference :: SameKind (Apply DSym0 arg) (DSym1 arg) => DSym0 a0123456789876543210 type instance Apply DSym0 a0123456789876543210 = DSym1 a0123456789876543210 instance SuppressUnusedWarnings DSym0 where suppressUnusedWarnings = snd ((,) DSym0KindInference ()) type DSym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data DSym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where DSym1KindInference :: SameKind (Apply (DSym1 a0123456789876543210) arg) (DSym2 a0123456789876543210 arg) => DSym1 a0123456789876543210 a0123456789876543210 type instance Apply (DSym1 a0123456789876543210) a0123456789876543210 = DSym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (DSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) DSym1KindInference ()) type DSym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data DSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where DSym2KindInference :: SameKind (Apply (DSym2 a0123456789876543210 a0123456789876543210) arg) (DSym3 a0123456789876543210 a0123456789876543210 arg) => DSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (DSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (DSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) DSym2KindInference ()) type DSym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data DSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where DSym3KindInference :: SameKind (Apply (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (DSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = D a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) DSym3KindInference ()) type DSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family DSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where DSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = D a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type ESym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data ESym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where ESym0KindInference :: SameKind (Apply ESym0 arg) (ESym1 arg) => ESym0 a0123456789876543210 type instance Apply ESym0 a0123456789876543210 = ESym1 a0123456789876543210 instance SuppressUnusedWarnings ESym0 where suppressUnusedWarnings = snd ((,) ESym0KindInference ()) type ESym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data ESym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where ESym1KindInference :: SameKind (Apply (ESym1 a0123456789876543210) arg) (ESym2 a0123456789876543210 arg) => ESym1 a0123456789876543210 a0123456789876543210 type instance Apply (ESym1 a0123456789876543210) a0123456789876543210 = ESym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ESym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ESym1KindInference ()) type ESym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data ESym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where ESym2KindInference :: SameKind (Apply (ESym2 a0123456789876543210 a0123456789876543210) arg) (ESym3 a0123456789876543210 a0123456789876543210 arg) => ESym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ESym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ESym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ESym2KindInference ()) type ESym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data ESym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where ESym3KindInference :: SameKind (Apply (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (ESym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = E a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ESym3KindInference ()) type ESym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family ESym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where ESym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = E a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type FSym0 :: forall a b c d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) data FSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d)))) where FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) => FSym0 a0123456789876543210 type instance Apply FSym0 a0123456789876543210 = FSym1 a0123456789876543210 instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd ((,) FSym0KindInference ()) type FSym1 :: forall a b c d. a -> (~>) b ((~>) c ((~>) d (Foo a b c d))) data FSym1 (a0123456789876543210 :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d))) where FSym1KindInference :: SameKind (Apply (FSym1 a0123456789876543210) arg) (FSym2 a0123456789876543210 arg) => FSym1 a0123456789876543210 a0123456789876543210 type instance Apply (FSym1 a0123456789876543210) a0123456789876543210 = FSym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (FSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym1KindInference ()) type FSym2 :: forall a b c d. a -> b -> (~>) c ((~>) d (Foo a b c d)) data FSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) c ((~>) d (Foo a b c d)) where FSym2KindInference :: SameKind (Apply (FSym2 a0123456789876543210 a0123456789876543210) arg) (FSym3 a0123456789876543210 a0123456789876543210 arg) => FSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (FSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (FSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym2KindInference ()) type FSym3 :: forall a b c d. a -> b -> c -> (~>) d (Foo a b c d) data FSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: (~>) d (Foo a b c d) where FSym3KindInference :: SameKind (Apply (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (FSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) => FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = F a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym3KindInference ()) type FSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d type family FSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where FSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where TFHelper_0123456789876543210 Zero Zero = TrueSym0 TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0 TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0 TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool) data TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym0KindInference ()) type TFHelper_0123456789876543210Sym1 :: Nat -> (~>) Nat Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Nat -> Nat -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq Nat where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Nat -> Nat -> Ordering type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0 Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0) Compare_0123456789876543210 Zero (Succ _) = LTSym0 Compare_0123456789876543210 (Succ _) Zero = GTSym0 type Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering) data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering) where Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Compare_0123456789876543210Sym0KindInference ()) type Compare_0123456789876543210Sym1 :: Nat -> (~>) Nat Ordering data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering where Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) => Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: Nat -> Nat -> Ordering type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd Nat where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type TFHelper_0123456789876543210 :: Foo a b c d -> Foo a b c d -> Bool type family TFHelper_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Bool where TFHelper_0123456789876543210 (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (A _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (A _ _ _ _) (C _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (A _ _ _ _) (D _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (A _ _ _ _) (E _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (A _ _ _ _) (F _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (B _ _ _ _) (A _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (B _ _ _ _) (C _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (B _ _ _ _) (D _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (B _ _ _ _) (E _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (B _ _ _ _) (F _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (C _ _ _ _) (A _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (C _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (C _ _ _ _) (D _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (C _ _ _ _) (E _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (C _ _ _ _) (F _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (D _ _ _ _) (A _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (D _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (D _ _ _ _) (C _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (D a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (D b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (D _ _ _ _) (E _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (D _ _ _ _) (F _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (E _ _ _ _) (A _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (E _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (E _ _ _ _) (C _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (E _ _ _ _) (D _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (E a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (E b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (E _ _ _ _) (F _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F _ _ _ _) (A _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F _ _ _ _) (C _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F _ _ _ _) (D _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F _ _ _ _) (E _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (F a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (F b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) type TFHelper_0123456789876543210Sym0 :: (~>) (Foo a b c d) ((~>) (Foo a b c d) Bool) data TFHelper_0123456789876543210Sym0 :: (~>) (Foo a b c d) ((~>) (Foo a b c d) Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym0KindInference ()) type TFHelper_0123456789876543210Sym1 :: Foo a b c d -> (~>) (Foo a b c d) Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Foo a b c d) :: (~>) (Foo a b c d) Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Foo a b c d -> Foo a b c d -> Bool type family TFHelper_0123456789876543210Sym2 @a @b @c @d (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Foo a b c d) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Foo a b c d -> Foo a b c d -> Ordering type family Compare_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Ordering where Compare_0123456789876543210 (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (D a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (D b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (E a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (E b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (F a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (F b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (A _ _ _ _) (B _ _ _ _) = LTSym0 Compare_0123456789876543210 (A _ _ _ _) (C _ _ _ _) = LTSym0 Compare_0123456789876543210 (A _ _ _ _) (D _ _ _ _) = LTSym0 Compare_0123456789876543210 (A _ _ _ _) (E _ _ _ _) = LTSym0 Compare_0123456789876543210 (A _ _ _ _) (F _ _ _ _) = LTSym0 Compare_0123456789876543210 (B _ _ _ _) (A _ _ _ _) = GTSym0 Compare_0123456789876543210 (B _ _ _ _) (C _ _ _ _) = LTSym0 Compare_0123456789876543210 (B _ _ _ _) (D _ _ _ _) = LTSym0 Compare_0123456789876543210 (B _ _ _ _) (E _ _ _ _) = LTSym0 Compare_0123456789876543210 (B _ _ _ _) (F _ _ _ _) = LTSym0 Compare_0123456789876543210 (C _ _ _ _) (A _ _ _ _) = GTSym0 Compare_0123456789876543210 (C _ _ _ _) (B _ _ _ _) = GTSym0 Compare_0123456789876543210 (C _ _ _ _) (D _ _ _ _) = LTSym0 Compare_0123456789876543210 (C _ _ _ _) (E _ _ _ _) = LTSym0 Compare_0123456789876543210 (C _ _ _ _) (F _ _ _ _) = LTSym0 Compare_0123456789876543210 (D _ _ _ _) (A _ _ _ _) = GTSym0 Compare_0123456789876543210 (D _ _ _ _) (B _ _ _ _) = GTSym0 Compare_0123456789876543210 (D _ _ _ _) (C _ _ _ _) = GTSym0 Compare_0123456789876543210 (D _ _ _ _) (E _ _ _ _) = LTSym0 Compare_0123456789876543210 (D _ _ _ _) (F _ _ _ _) = LTSym0 Compare_0123456789876543210 (E _ _ _ _) (A _ _ _ _) = GTSym0 Compare_0123456789876543210 (E _ _ _ _) (B _ _ _ _) = GTSym0 Compare_0123456789876543210 (E _ _ _ _) (C _ _ _ _) = GTSym0 Compare_0123456789876543210 (E _ _ _ _) (D _ _ _ _) = GTSym0 Compare_0123456789876543210 (E _ _ _ _) (F _ _ _ _) = LTSym0 Compare_0123456789876543210 (F _ _ _ _) (A _ _ _ _) = GTSym0 Compare_0123456789876543210 (F _ _ _ _) (B _ _ _ _) = GTSym0 Compare_0123456789876543210 (F _ _ _ _) (C _ _ _ _) = GTSym0 Compare_0123456789876543210 (F _ _ _ _) (D _ _ _ _) = GTSym0 Compare_0123456789876543210 (F _ _ _ _) (E _ _ _ _) = GTSym0 type Compare_0123456789876543210Sym0 :: (~>) (Foo a b c d) ((~>) (Foo a b c d) Ordering) data Compare_0123456789876543210Sym0 :: (~>) (Foo a b c d) ((~>) (Foo a b c d) Ordering) where Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Compare_0123456789876543210Sym0KindInference ()) type Compare_0123456789876543210Sym1 :: Foo a b c d -> (~>) (Foo a b c d) Ordering data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Foo a b c d) :: (~>) (Foo a b c d) Ordering where Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) => Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: Foo a b c d -> Foo a b c d -> Ordering type family Compare_0123456789876543210Sym2 @a @b @c @d (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (Foo a b c d) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a data SNat :: Nat -> Type where SZero :: SNat (Zero :: Nat) SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat) type instance Sing @Nat = SNat instance SingKind Nat where type Demote Nat = Nat fromSing SZero = Zero fromSing (SSucc b) = Succ (fromSing b) toSing Zero = SomeSing SZero toSing (Succ (b :: Demote Nat)) = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c) data SFoo :: forall a b c d. Foo a b c d -> Type where SA :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (A n n n n :: Foo a b c d) SB :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (B n n n n :: Foo a b c d) SC :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (C n n n n :: Foo a b c d) SD :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (D n n n n :: Foo a b c d) SE :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (E n n n n :: Foo a b c d) SF :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> SFoo (F n n n n :: Foo a b c d) type instance Sing @(Foo a b c d) = SFoo instance (SingKind a, SingKind b, SingKind c, SingKind d) => SingKind (Foo a b c d) where type Demote (Foo a b c d) = Foo (Demote a) (Demote b) (Demote c) (Demote d) fromSing (SA b b b b) = A (fromSing b) (fromSing b) (fromSing b) (fromSing b) fromSing (SB b b b b) = B (fromSing b) (fromSing b) (fromSing b) (fromSing b) fromSing (SC b b b b) = C (fromSing b) (fromSing b) (fromSing b) (fromSing b) fromSing (SD b b b b) = D (fromSing b) (fromSing b) (fromSing b) (fromSing b) fromSing (SE b b b b) = E (fromSing b) (fromSing b) (fromSing b) (fromSing b) fromSing (SF b b b b) = F (fromSing b) (fromSing b) (fromSing b) (fromSing b) toSing (A (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SA c c c c) toSing (B (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SB c c c c) toSing (C (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SC c c c c) toSing (D (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SD c c c c) toSing (E (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SE c c c c) toSing (F (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d)) = case (,,,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) (toSing b :: SomeSing c) (toSing b :: SomeSing d) of (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SF c c c c) instance SEq Nat => SEq Nat where (%==) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse (%==) (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SOrd Nat => SOrd Nat where sCompare :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) -> Type) t1) t2) sCompare SZero SZero = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) SNil sCompare (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil) sCompare SZero (SSucc _) = SLT sCompare (SSucc _) SZero = SGT instance (SEq a, SEq b, SEq c, SEq d) => SEq (Foo a b c d) where (%==) :: forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Bool) -> Type) t1) t2) (%==) (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SA (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) (%==) (SA _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SB (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SB (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) (%==) (SB _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SC (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SC (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) (%==) (SC _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SD (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SD (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) (%==) (SD _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SE (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SE (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) (%==) (SE _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SF (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SF (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210))) instance (SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (Foo a b c d) where sCompare :: forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Ordering) -> Type) t1) t2) sCompare (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SA (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SB (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SB (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SC (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SC (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SD (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SD (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SE (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SE (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SF (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SF (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(:@#@$) SCons) (applySing (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210) sB_0123456789876543210)) SNil)))) sCompare (SA _ _ _ _) (SB _ _ _ _) = SLT sCompare (SA _ _ _ _) (SC _ _ _ _) = SLT sCompare (SA _ _ _ _) (SD _ _ _ _) = SLT sCompare (SA _ _ _ _) (SE _ _ _ _) = SLT sCompare (SA _ _ _ _) (SF _ _ _ _) = SLT sCompare (SB _ _ _ _) (SA _ _ _ _) = SGT sCompare (SB _ _ _ _) (SC _ _ _ _) = SLT sCompare (SB _ _ _ _) (SD _ _ _ _) = SLT sCompare (SB _ _ _ _) (SE _ _ _ _) = SLT sCompare (SB _ _ _ _) (SF _ _ _ _) = SLT sCompare (SC _ _ _ _) (SA _ _ _ _) = SGT sCompare (SC _ _ _ _) (SB _ _ _ _) = SGT sCompare (SC _ _ _ _) (SD _ _ _ _) = SLT sCompare (SC _ _ _ _) (SE _ _ _ _) = SLT sCompare (SC _ _ _ _) (SF _ _ _ _) = SLT sCompare (SD _ _ _ _) (SA _ _ _ _) = SGT sCompare (SD _ _ _ _) (SB _ _ _ _) = SGT sCompare (SD _ _ _ _) (SC _ _ _ _) = SGT sCompare (SD _ _ _ _) (SE _ _ _ _) = SLT sCompare (SD _ _ _ _) (SF _ _ _ _) = SLT sCompare (SE _ _ _ _) (SA _ _ _ _) = SGT sCompare (SE _ _ _ _) (SB _ _ _ _) = SGT sCompare (SE _ _ _ _) (SC _ _ _ _) = SGT sCompare (SE _ _ _ _) (SD _ _ _ _) = SGT sCompare (SE _ _ _ _) (SF _ _ _ _) = SLT sCompare (SF _ _ _ _) (SA _ _ _ _) = SGT sCompare (SF _ _ _ _) (SB _ _ _ _) = SGT sCompare (SF _ _ _ _) (SC _ _ _ _) = SGT sCompare (SF _ _ _ _) (SD _ _ _ _) = SGT sCompare (SF _ _ _ _) (SE _ _ _ _) = SGT instance SDecide Nat => SDecide Nat where (%~) SZero SZero = Proved Refl (%~) SZero (SSucc _) = Disproved (\ x -> case x of {}) (%~) (SSucc _) SZero = Disproved (\ x -> case x of {}) (%~) (SSucc a) (SSucc b) = case (%~) a b of Proved Refl -> Proved Refl Disproved contra -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance Eq (SNat (z :: Nat)) where (==) _ _ = True instance SDecide Nat => GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance (SDecide a, SDecide b, SDecide c, SDecide d) => SDecide (Foo a b c d) where (%~) (SA a a a a) (SA b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) (%~) (SA _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SA _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SA _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SA _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SA _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SB _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SB a a a a) (SB b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) (%~) (SB _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SB _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SB _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SB _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SC _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SC _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SC a a a a) (SC b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) (%~) (SC _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SC _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SC _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SD _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SD _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SD _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SD a a a a) (SD b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) (%~) (SD _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SD _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SE _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SE _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SE _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SE _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SE a a a a) (SE b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) (%~) (SE _ _ _ _) (SF _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF _ _ _ _) (SA _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF _ _ _ _) (SB _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF _ _ _ _) (SC _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF _ _ _ _) (SD _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF _ _ _ _) (SE _ _ _ _) = Disproved (\ x -> case x of {}) (%~) (SF a a a a) (SF b b b b) = case (,,,) ((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b) of (,,,) (Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl) -> Proved Refl (,,,) (Disproved contra) _ _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ (Disproved contra) _ _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ (Disproved contra) _ -> Disproved (\ refl -> case refl of Refl -> contra Refl) (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance Eq (SFoo (z :: Foo a b c d)) where (==) _ _ = True instance (SDecide a, SDecide b, SDecide c, SDecide d) => GHC.Internal.Data.Type.Equality.TestEquality (SFoo :: Foo a b c d -> Type) where GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance (SDecide a, SDecide b, SDecide c, SDecide d) => GHC.Internal.Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d -> Type) where GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SNat (z :: Nat)) where compare _ _ = EQ instance Ord (SFoo (z :: Foo a b c d)) where compare _ _ = EQ instance SingI Zero where sing = SZero instance SingI n => SingI (Succ (n :: Nat)) where sing = SSucc sing instance SingI1 Succ where liftSing = SSucc instance SingI (SuccSym0 :: (~>) Nat Nat) where sing = singFun1 @SuccSym0 SSucc instance (SingI n, SingI n, SingI n, SingI n) => SingI (A (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SA sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (A (n :: a) (n :: b) (n :: c)) where liftSing = SA sing sing sing instance (SingI n, SingI n) => SingI2 (A (n :: a) (n :: b)) where liftSing2 = SA sing sing instance SingI (ASym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @ASym0 SA instance SingI d => SingI (ASym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(ASym1 (d :: a)) (SA (sing @d)) instance SingI1 (ASym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(ASym1 (d :: a)) (SA s) instance (SingI d, SingI d) => SingI (ASym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(ASym2 (d :: a) (d :: b)) (SA (sing @d) (sing @d)) instance SingI d => SingI1 (ASym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(ASym2 (d :: a) (d :: b)) (SA (sing @d) s) instance SingI2 (ASym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(ASym2 (d :: a) (d :: b)) (SA s s) instance (SingI d, SingI d, SingI d) => SingI (ASym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(ASym3 (d :: a) (d :: b) (d :: c)) (SA (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (ASym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(ASym3 (d :: a) (d :: b) (d :: c)) (SA (sing @d) (sing @d) s) instance SingI d => SingI2 (ASym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(ASym3 (d :: a) (d :: b) (d :: c)) (SA (sing @d) s s) instance (SingI n, SingI n, SingI n, SingI n) => SingI (B (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SB sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (B (n :: a) (n :: b) (n :: c)) where liftSing = SB sing sing sing instance (SingI n, SingI n) => SingI2 (B (n :: a) (n :: b)) where liftSing2 = SB sing sing instance SingI (BSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @BSym0 SB instance SingI d => SingI (BSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(BSym1 (d :: a)) (SB (sing @d)) instance SingI1 (BSym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(BSym1 (d :: a)) (SB s) instance (SingI d, SingI d) => SingI (BSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(BSym2 (d :: a) (d :: b)) (SB (sing @d) (sing @d)) instance SingI d => SingI1 (BSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(BSym2 (d :: a) (d :: b)) (SB (sing @d) s) instance SingI2 (BSym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(BSym2 (d :: a) (d :: b)) (SB s s) instance (SingI d, SingI d, SingI d) => SingI (BSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(BSym3 (d :: a) (d :: b) (d :: c)) (SB (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (BSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(BSym3 (d :: a) (d :: b) (d :: c)) (SB (sing @d) (sing @d) s) instance SingI d => SingI2 (BSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(BSym3 (d :: a) (d :: b) (d :: c)) (SB (sing @d) s s) instance (SingI n, SingI n, SingI n, SingI n) => SingI (C (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SC sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (C (n :: a) (n :: b) (n :: c)) where liftSing = SC sing sing sing instance (SingI n, SingI n) => SingI2 (C (n :: a) (n :: b)) where liftSing2 = SC sing sing instance SingI (CSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @CSym0 SC instance SingI d => SingI (CSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(CSym1 (d :: a)) (SC (sing @d)) instance SingI1 (CSym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(CSym1 (d :: a)) (SC s) instance (SingI d, SingI d) => SingI (CSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(CSym2 (d :: a) (d :: b)) (SC (sing @d) (sing @d)) instance SingI d => SingI1 (CSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(CSym2 (d :: a) (d :: b)) (SC (sing @d) s) instance SingI2 (CSym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(CSym2 (d :: a) (d :: b)) (SC s s) instance (SingI d, SingI d, SingI d) => SingI (CSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(CSym3 (d :: a) (d :: b) (d :: c)) (SC (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (CSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(CSym3 (d :: a) (d :: b) (d :: c)) (SC (sing @d) (sing @d) s) instance SingI d => SingI2 (CSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(CSym3 (d :: a) (d :: b) (d :: c)) (SC (sing @d) s s) instance (SingI n, SingI n, SingI n, SingI n) => SingI (D (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SD sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (D (n :: a) (n :: b) (n :: c)) where liftSing = SD sing sing sing instance (SingI n, SingI n) => SingI2 (D (n :: a) (n :: b)) where liftSing2 = SD sing sing instance SingI (DSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @DSym0 SD instance SingI d => SingI (DSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(DSym1 (d :: a)) (SD (sing @d)) instance SingI1 (DSym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(DSym1 (d :: a)) (SD s) instance (SingI d, SingI d) => SingI (DSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(DSym2 (d :: a) (d :: b)) (SD (sing @d) (sing @d)) instance SingI d => SingI1 (DSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(DSym2 (d :: a) (d :: b)) (SD (sing @d) s) instance SingI2 (DSym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(DSym2 (d :: a) (d :: b)) (SD s s) instance (SingI d, SingI d, SingI d) => SingI (DSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(DSym3 (d :: a) (d :: b) (d :: c)) (SD (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (DSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(DSym3 (d :: a) (d :: b) (d :: c)) (SD (sing @d) (sing @d) s) instance SingI d => SingI2 (DSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(DSym3 (d :: a) (d :: b) (d :: c)) (SD (sing @d) s s) instance (SingI n, SingI n, SingI n, SingI n) => SingI (E (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SE sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (E (n :: a) (n :: b) (n :: c)) where liftSing = SE sing sing sing instance (SingI n, SingI n) => SingI2 (E (n :: a) (n :: b)) where liftSing2 = SE sing sing instance SingI (ESym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @ESym0 SE instance SingI d => SingI (ESym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(ESym1 (d :: a)) (SE (sing @d)) instance SingI1 (ESym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(ESym1 (d :: a)) (SE s) instance (SingI d, SingI d) => SingI (ESym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(ESym2 (d :: a) (d :: b)) (SE (sing @d) (sing @d)) instance SingI d => SingI1 (ESym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(ESym2 (d :: a) (d :: b)) (SE (sing @d) s) instance SingI2 (ESym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(ESym2 (d :: a) (d :: b)) (SE s s) instance (SingI d, SingI d, SingI d) => SingI (ESym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(ESym3 (d :: a) (d :: b) (d :: c)) (SE (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (ESym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(ESym3 (d :: a) (d :: b) (d :: c)) (SE (sing @d) (sing @d) s) instance SingI d => SingI2 (ESym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(ESym3 (d :: a) (d :: b) (d :: c)) (SE (sing @d) s s) instance (SingI n, SingI n, SingI n, SingI n) => SingI (F (n :: a) (n :: b) (n :: c) (n :: d)) where sing = SF sing sing sing sing instance (SingI n, SingI n, SingI n) => SingI1 (F (n :: a) (n :: b) (n :: c)) where liftSing = SF sing sing sing instance (SingI n, SingI n) => SingI2 (F (n :: a) (n :: b)) where liftSing2 = SF sing sing instance SingI (FSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = singFun4 @FSym0 SF instance SingI d => SingI (FSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = singFun3 @(FSym1 (d :: a)) (SF (sing @d)) instance SingI1 (FSym1 :: a -> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where liftSing (s :: Sing (d :: a)) = singFun3 @(FSym1 (d :: a)) (SF s) instance (SingI d, SingI d) => SingI (FSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where sing = singFun2 @(FSym2 (d :: a) (d :: b)) (SF (sing @d) (sing @d)) instance SingI d => SingI1 (FSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where liftSing (s :: Sing (d :: b)) = singFun2 @(FSym2 (d :: a) (d :: b)) (SF (sing @d) s) instance SingI2 (FSym2 :: a -> b -> (~>) c ((~>) d (Foo a b c d))) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun2 @(FSym2 (d :: a) (d :: b)) (SF s s) instance (SingI d, SingI d, SingI d) => SingI (FSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where sing = singFun1 @(FSym3 (d :: a) (d :: b) (d :: c)) (SF (sing @d) (sing @d) (sing @d)) instance (SingI d, SingI d) => SingI1 (FSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where liftSing (s :: Sing (d :: c)) = singFun1 @(FSym3 (d :: a) (d :: b) (d :: c)) (SF (sing @d) (sing @d) s) instance SingI d => SingI2 (FSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c)) = singFun1 @(FSym3 (d :: a) (d :: b) (d :: c)) (SF (sing @d) s s)