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 = Zero type SuccSym1 (t0123456789876543210 :: Nat) = Succ t0123456789876543210 instance SuppressUnusedWarnings SuccSym0 where suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ()) data SuccSym0 :: (~>) Nat Nat where SuccSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) => SuccSym0 t0123456789876543210 type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210 type ASym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = A t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ASym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ASym3KindInference) ()) data ASym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where ASym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ASym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (ASym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => ASym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (ASym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = A t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ASym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ASym2KindInference) ()) data ASym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where ASym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ASym2 t0123456789876543210 t0123456789876543210) arg) (ASym3 t0123456789876543210 t0123456789876543210 arg) => ASym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (ASym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = ASym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ASym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ASym1KindInference) ()) data ASym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where ASym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ASym1 t0123456789876543210) arg) (ASym2 t0123456789876543210 arg) => ASym1 t0123456789876543210 t0123456789876543210 type instance Apply (ASym1 t0123456789876543210) t0123456789876543210 = ASym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings ASym0 where suppressUnusedWarnings = snd (((,) ASym0KindInference) ()) data ASym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where ASym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply ASym0 arg) (ASym1 arg) => ASym0 t0123456789876543210 type instance Apply ASym0 t0123456789876543210 = ASym1 t0123456789876543210 type BSym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = B t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (BSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) BSym3KindInference) ()) data BSym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where BSym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (BSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (BSym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => BSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (BSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = B t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (BSym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) BSym2KindInference) ()) data BSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where BSym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (BSym2 t0123456789876543210 t0123456789876543210) arg) (BSym3 t0123456789876543210 t0123456789876543210 arg) => BSym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (BSym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = BSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (BSym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) BSym1KindInference) ()) data BSym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where BSym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (BSym1 t0123456789876543210) arg) (BSym2 t0123456789876543210 arg) => BSym1 t0123456789876543210 t0123456789876543210 type instance Apply (BSym1 t0123456789876543210) t0123456789876543210 = BSym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings BSym0 where suppressUnusedWarnings = snd (((,) BSym0KindInference) ()) data BSym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where BSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply BSym0 arg) (BSym1 arg) => BSym0 t0123456789876543210 type instance Apply BSym0 t0123456789876543210 = BSym1 t0123456789876543210 type CSym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = C t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (CSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) CSym3KindInference) ()) data CSym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where CSym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (CSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (CSym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => CSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (CSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = C t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (CSym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) CSym2KindInference) ()) data CSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where CSym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (CSym2 t0123456789876543210 t0123456789876543210) arg) (CSym3 t0123456789876543210 t0123456789876543210 arg) => CSym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (CSym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = CSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (CSym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) CSym1KindInference) ()) data CSym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where CSym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (CSym1 t0123456789876543210) arg) (CSym2 t0123456789876543210 arg) => CSym1 t0123456789876543210 t0123456789876543210 type instance Apply (CSym1 t0123456789876543210) t0123456789876543210 = CSym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings CSym0 where suppressUnusedWarnings = snd (((,) CSym0KindInference) ()) data CSym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where CSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply CSym0 arg) (CSym1 arg) => CSym0 t0123456789876543210 type instance Apply CSym0 t0123456789876543210 = CSym1 t0123456789876543210 type DSym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = D t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (DSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) DSym3KindInference) ()) data DSym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where DSym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (DSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (DSym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => DSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (DSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = D t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (DSym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) DSym2KindInference) ()) data DSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where DSym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (DSym2 t0123456789876543210 t0123456789876543210) arg) (DSym3 t0123456789876543210 t0123456789876543210 arg) => DSym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (DSym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = DSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (DSym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) DSym1KindInference) ()) data DSym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where DSym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (DSym1 t0123456789876543210) arg) (DSym2 t0123456789876543210 arg) => DSym1 t0123456789876543210 t0123456789876543210 type instance Apply (DSym1 t0123456789876543210) t0123456789876543210 = DSym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings DSym0 where suppressUnusedWarnings = snd (((,) DSym0KindInference) ()) data DSym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where DSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply DSym0 arg) (DSym1 arg) => DSym0 t0123456789876543210 type instance Apply DSym0 t0123456789876543210 = DSym1 t0123456789876543210 type ESym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = E t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ESym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ESym3KindInference) ()) data ESym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where ESym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ESym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (ESym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => ESym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (ESym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = E t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ESym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ESym2KindInference) ()) data ESym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where ESym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ESym2 t0123456789876543210 t0123456789876543210) arg) (ESym3 t0123456789876543210 t0123456789876543210 arg) => ESym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (ESym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = ESym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (ESym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) ESym1KindInference) ()) data ESym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where ESym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (ESym1 t0123456789876543210) arg) (ESym2 t0123456789876543210 arg) => ESym1 t0123456789876543210 t0123456789876543210 type instance Apply (ESym1 t0123456789876543210) t0123456789876543210 = ESym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings ESym0 where suppressUnusedWarnings = snd (((,) ESym0KindInference) ()) data ESym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where ESym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply ESym0 arg) (ESym1 arg) => ESym0 t0123456789876543210 type instance Apply ESym0 t0123456789876543210 = ESym1 t0123456789876543210 type FSym4 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) (t0123456789876543210 :: d0123456789876543210) = F t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (FSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) FSym3KindInference) ()) data FSym3 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) (t0123456789876543210 :: c0123456789876543210) :: forall d0123456789876543210. (~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) where FSym3KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (FSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) arg) (FSym4 t0123456789876543210 t0123456789876543210 t0123456789876543210 arg) => FSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (FSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210) t0123456789876543210 = F t0123456789876543210 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (FSym2 t0123456789876543210 t0123456789876543210) where suppressUnusedWarnings = snd (((,) FSym2KindInference) ()) data FSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) :: forall c0123456789876543210 d0123456789876543210. (~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)) where FSym2KindInference :: forall t0123456789876543210 t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (FSym2 t0123456789876543210 t0123456789876543210) arg) (FSym3 t0123456789876543210 t0123456789876543210 arg) => FSym2 t0123456789876543210 t0123456789876543210 t0123456789876543210 type instance Apply (FSym2 t0123456789876543210 t0123456789876543210) t0123456789876543210 = FSym3 t0123456789876543210 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (FSym1 t0123456789876543210) where suppressUnusedWarnings = snd (((,) FSym1KindInference) ()) data FSym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))) where FSym1KindInference :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply (FSym1 t0123456789876543210) arg) (FSym2 t0123456789876543210 arg) => FSym1 t0123456789876543210 t0123456789876543210 type instance Apply (FSym1 t0123456789876543210) t0123456789876543210 = FSym2 t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd (((,) FSym0KindInference) ()) data FSym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 ((~>) c0123456789876543210 ((~>) d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)))) where FSym0KindInference :: forall t0123456789876543210 arg. SameKind (Apply FSym0 arg) (FSym1 arg) => FSym0 t0123456789876543210 type instance Apply FSym0 t0123456789876543210 = FSym1 t0123456789876543210 type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]) Compare_0123456789876543210 Zero (Succ _) = LTSym0 Compare_0123456789876543210 (Succ _) Zero = GTSym0 type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym1KindInference) ()) data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering where Compare_0123456789876543210Sym1KindInference :: forall a0123456789876543210 a0123456789876543210 arg. 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_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym0KindInference) ()) data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering) where Compare_0123456789876543210Sym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210 instance POrd Nat where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a 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)) '[])))) 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)) '[])))) 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)) '[])))) 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)) '[])))) 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)) '[])))) 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)) '[])))) 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_0123456789876543210Sym2 (a0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (a0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym1KindInference) ()) data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) :: (~>) (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering where Compare_0123456789876543210Sym1KindInference :: forall a0123456789876543210 a0123456789876543210 arg. 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_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym0KindInference) ()) data Compare_0123456789876543210Sym0 :: forall a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210. (~>) (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) ((~>) (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering) where Compare_0123456789876543210Sym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210 instance POrd (Foo a b c d) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where Equals_0123456789876543210 Zero Zero = TrueSym0 Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0 instance PEq Nat where type (==) a b = Equals_0123456789876543210 a b type family Equals_0123456789876543210 (a :: Foo a b c d) (b :: Foo a b c d) :: Bool where Equals_0123456789876543210 (A a a a a) (A b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (B a a a a) (B b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (C a a a a) (C b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (D a a a a) (D b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (E a a a a) (E b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (F a a a a) (F b b b b) = (&&) ((==) a b) ((&&) ((==) a b) ((&&) ((==) a b) ((==) a b))) Equals_0123456789876543210 (_ :: Foo a b c d) (_ :: Foo a b c d) = FalseSym0 instance PEq (Foo a b c d) where type (==) a b = Equals_0123456789876543210 a b data instance Sing :: Nat -> GHC.Types.Type where SZero :: Sing Zero SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n) type SNat = (Sing :: Nat -> GHC.Types.Type) 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 instance Sing :: Foo a b c d -> GHC.Types.Type where SA :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (A n n n n) SB :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (B n n n n) SC :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (C n n n n) SD :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (D n n n n) SE :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (E n n n n) SF :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). (Sing (n :: a)) -> (Sing (n :: b)) -> (Sing (n :: c)) -> (Sing (n :: d)) -> Sing (F n n n n) type SFoo = (Sing :: Foo a b c d -> GHC.Types.Type) 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 SOrd Nat => SOrd Nat where sCompare :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) -> GHC.Types.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 (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) -> GHC.Types.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 SEq Nat => SEq Nat where (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse (%==) (SSucc a) (SSucc b) = ((%==) a) b 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 (SEq a, SEq b, SEq c, SEq d) => SEq (Foo a b c d) where (%==) (SA a a a a) (SA b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) (%==) (SA _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SA _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SB a a a a) (SB b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) (%==) (SB _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SB _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SC a a a a) (SC b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) (%==) (SC _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SC _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SD a a a a) (SD b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) (%==) (SD _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SD _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SE _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SE a a a a) (SE b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) (%==) (SE _ _ _ _) (SF _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SA _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SB _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SC _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SD _ _ _ _) = SFalse (%==) (SF _ _ _ _) (SE _ _ _ _) = SFalse (%==) (SF a a a a) (SF b b b b) = ((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%&&) (((%==) a) b)) (((%==) a) b))) 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 SingI Zero where sing = SZero instance SingI n => SingI (Succ (n :: Nat)) where sing = SSucc sing instance SingI (SuccSym0 :: (~>) Nat Nat) where sing = (singFun1 @SuccSym0) SSucc instance SingI (TyCon1 Succ :: (~>) Nat Nat) where sing = (singFun1 @(TyCon1 Succ)) 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 (ASym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @ASym0) SA instance SingI (TyCon4 A :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 A)) 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 SingI d => SingI (TyCon3 (A (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (A (d :: a)))) (SA (sing @d)) 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, SingI d) => SingI (TyCon2 (A (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (A (d :: a) (d :: b)))) ((SA (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (A (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (A (d :: a) (d :: b) (d :: c)))) (((SA (sing @d)) (sing @d)) (sing @d)) 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 (BSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @BSym0) SB instance SingI (TyCon4 B :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 B)) 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 SingI d => SingI (TyCon3 (B (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (B (d :: a)))) (SB (sing @d)) 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, SingI d) => SingI (TyCon2 (B (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (B (d :: a) (d :: b)))) ((SB (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (B (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (B (d :: a) (d :: b) (d :: c)))) (((SB (sing @d)) (sing @d)) (sing @d)) 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 (CSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @CSym0) SC instance SingI (TyCon4 C :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 C)) 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 SingI d => SingI (TyCon3 (C (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (C (d :: a)))) (SC (sing @d)) 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, SingI d) => SingI (TyCon2 (C (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (C (d :: a) (d :: b)))) ((SC (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (C (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (C (d :: a) (d :: b) (d :: c)))) (((SC (sing @d)) (sing @d)) (sing @d)) 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 (DSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @DSym0) SD instance SingI (TyCon4 D :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 D)) 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 SingI d => SingI (TyCon3 (D (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (D (d :: a)))) (SD (sing @d)) 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, SingI d) => SingI (TyCon2 (D (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (D (d :: a) (d :: b)))) ((SD (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (D (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (D (d :: a) (d :: b) (d :: c)))) (((SD (sing @d)) (sing @d)) (sing @d)) 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 (ESym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @ESym0) SE instance SingI (TyCon4 E :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 E)) 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 SingI d => SingI (TyCon3 (E (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (E (d :: a)))) (SE (sing @d)) 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, SingI d) => SingI (TyCon2 (E (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (E (d :: a) (d :: b)))) ((SE (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (E (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (E (d :: a) (d :: b) (d :: c)))) (((SE (sing @d)) (sing @d)) (sing @d)) 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 (FSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @FSym0) SF instance SingI (TyCon4 F :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where sing = (singFun4 @(TyCon4 F)) 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 SingI d => SingI (TyCon3 (F (d :: a)) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where sing = (singFun3 @(TyCon3 (F (d :: a)))) (SF (sing @d)) 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, SingI d) => SingI (TyCon2 (F (d :: a) (d :: b)) :: (~>) c ((~>) d (Foo a b c d))) where sing = (singFun2 @(TyCon2 (F (d :: a) (d :: b)))) ((SF (sing @d)) (sing @d)) 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, SingI d) => SingI (TyCon1 (F (d :: a) (d :: b) (d :: c)) :: (~>) d (Foo a b c d)) where sing = (singFun1 @(TyCon1 (F (d :: a) (d :: b) (d :: c)))) (((SF (sing @d)) (sing @d)) (sing @d))