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 (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 (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 (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 (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 (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 (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 ThenCmpSym0) EQSym0) NilSym0 Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) 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 :: 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 (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 :: 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 ThenCmpSym0) 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 ThenCmpSym0) 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 ThenCmpSym0) 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 ThenCmpSym0) 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 ThenCmpSym0) 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 ThenCmpSym0) 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 (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 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210)) = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 @ThenCmpSym0) sThenCmp))) 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 SDecide Nat => Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where 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 (SDecide a, SDecide b, SDecide c, SDecide d) => Data.Type.Equality.TestEquality (SFoo :: Foo a b c d -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance (SDecide a, SDecide b, SDecide c, SDecide d) => Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion 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)