singletons-base-3.5.1: tests/compile-and-dump/Singletons/OrdDeriving.golden
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 @Nat @Nat 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 @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = A a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) ASym3KindInference ())
type ASym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family ASym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
ASym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = A a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type BSym0 :: forall a
b
c
d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
data BSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
where
BSym0KindInference :: SameKind (Apply BSym0 arg) (BSym1 arg) =>
BSym0 a0123456789876543210
type instance Apply @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = B a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) BSym3KindInference ())
type BSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family BSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
BSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = B a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type CSym0 :: forall a
b
c
d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
data CSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
where
CSym0KindInference :: SameKind (Apply CSym0 arg) (CSym1 arg) =>
CSym0 a0123456789876543210
type instance Apply @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = C a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) CSym3KindInference ())
type CSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family CSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
CSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = C a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type DSym0 :: forall a
b
c
d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
data DSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
where
DSym0KindInference :: SameKind (Apply DSym0 arg) (DSym1 arg) =>
DSym0 a0123456789876543210
type instance Apply @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = D a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) DSym3KindInference ())
type DSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family DSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
DSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = D a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type ESym0 :: forall a
b
c
d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
data ESym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
where
ESym0KindInference :: SameKind (Apply ESym0 arg) (ESym1 arg) =>
ESym0 a0123456789876543210
type instance Apply @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = E a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) ESym3KindInference ())
type ESym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family ESym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
ESym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = E a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type FSym0 :: forall a
b
c
d. (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
data FSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))
where
FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) =>
FSym0 a0123456789876543210
type instance Apply @a @((~>) b ((~>) c ((~>) d (Foo a b c d)))) 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 @b @((~>) c ((~>) d (Foo a b c d))) (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 @c @((~>) d (Foo a b c d)) (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 @d @(Foo a b c d) (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = F a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) FSym3KindInference ())
type FSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d
type family FSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where
FSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool
type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where
TFHelper_0123456789876543210 Zero Zero = TrueSym0
TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0
TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0
TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210
instance PEq Nat where
type (==) a a = TFHelper_0123456789876543210 a a
type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
Compare_0123456789876543210 Zero (Succ _) = LTSym0
Compare_0123456789876543210 (Succ _) Zero = GTSym0
instance POrd Nat where
type Compare a a = Compare_0123456789876543210 a a
type TFHelper_0123456789876543210 :: forall a b c d. Foo a b c d
-> Foo a b c d -> Bool
type family TFHelper_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Bool where
TFHelper_0123456789876543210 @a @b @c @d (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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 @c @d (A _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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 @c @d (B _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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 @c @d (C _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (D a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (D b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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 @c @d (D _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (E a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (E b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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 @c @d (E _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = FalseSym0
TFHelper_0123456789876543210 @a @b @c @d (F a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (F b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = 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)))
instance PEq (Foo a b c d) where
type (==) a a = TFHelper_0123456789876543210 a a
type Compare_0123456789876543210 :: forall a b c d. Foo a b c d
-> Foo a b c d -> Ordering
type family Compare_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Ordering where
Compare_0123456789876543210 @a @b @c @d (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (D a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (D b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (E a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (E b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (F a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: Foo a b c d) (F b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 :: Foo a b c d) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))))
Compare_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (A _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (B _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (C _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (D _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (E _ _ _ _ :: Foo a b c d) (F _ _ _ _ :: Foo a b c d) = LTSym0
Compare_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (A _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (B _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (C _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (D _ _ _ _ :: Foo a b c d) = GTSym0
Compare_0123456789876543210 @a @b @c @d (F _ _ _ _ :: Foo a b c d) (E _ _ _ _ :: Foo a b c d) = GTSym0
instance POrd (Foo a b c d) where
type Compare a a = Compare_0123456789876543210 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))
= (\cases (SomeSing c) -> SomeSing (SSucc c))
(toSing b :: SomeSing Nat)
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))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SA c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
toSing
(B (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SB c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
toSing
(C (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SC c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
toSing
(D (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SD c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
toSing
(E (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SE c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
toSing
(F (b :: Demote a) (b :: Demote b) (b :: Demote c) (b :: Demote d))
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SF c c c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
(toSing b :: SomeSing c) (toSing b :: SomeSing d)
instance SEq Nat => SEq Nat where
(%==) 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 SZero SZero
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare
(SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
(SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil)
sCompare SZero (SSucc _) = SLT
sCompare (SSucc _) SZero = SGT
instance (SEq a, SEq b, SEq c, SEq d) => SEq (Foo a b c d) where
(%==)
(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
(SA (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SA (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare
(SB (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SB (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare
(SC (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SC (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare
(SD (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SD (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare
(SE (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SE (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare
(SF (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SF (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))))
sCompare (SA _ _ _ _) (SB _ _ _ _) = SLT
sCompare (SA _ _ _ _) (SC _ _ _ _) = SLT
sCompare (SA _ _ _ _) (SD _ _ _ _) = SLT
sCompare (SA _ _ _ _) (SE _ _ _ _) = SLT
sCompare (SA _ _ _ _) (SF _ _ _ _) = SLT
sCompare (SB _ _ _ _) (SA _ _ _ _) = SGT
sCompare (SB _ _ _ _) (SC _ _ _ _) = SLT
sCompare (SB _ _ _ _) (SD _ _ _ _) = SLT
sCompare (SB _ _ _ _) (SE _ _ _ _) = SLT
sCompare (SB _ _ _ _) (SF _ _ _ _) = SLT
sCompare (SC _ _ _ _) (SA _ _ _ _) = SGT
sCompare (SC _ _ _ _) (SB _ _ _ _) = SGT
sCompare (SC _ _ _ _) (SD _ _ _ _) = SLT
sCompare (SC _ _ _ _) (SE _ _ _ _) = SLT
sCompare (SC _ _ _ _) (SF _ _ _ _) = SLT
sCompare (SD _ _ _ _) (SA _ _ _ _) = SGT
sCompare (SD _ _ _ _) (SB _ _ _ _) = SGT
sCompare (SD _ _ _ _) (SC _ _ _ _) = SGT
sCompare (SD _ _ _ _) (SE _ _ _ _) = SLT
sCompare (SD _ _ _ _) (SF _ _ _ _) = SLT
sCompare (SE _ _ _ _) (SA _ _ _ _) = SGT
sCompare (SE _ _ _ _) (SB _ _ _ _) = SGT
sCompare (SE _ _ _ _) (SC _ _ _ _) = SGT
sCompare (SE _ _ _ _) (SD _ _ _ _) = SGT
sCompare (SE _ _ _ _) (SF _ _ _ _) = SLT
sCompare (SF _ _ _ _) (SA _ _ _ _) = SGT
sCompare (SF _ _ _ _) (SB _ _ _ _) = SGT
sCompare (SF _ _ _ _) (SC _ _ _ _) = SGT
sCompare (SF _ _ _ _) (SD _ _ _ _) = SGT
sCompare (SF _ _ _ _) (SE _ _ _ _) = SGT
instance SDecide Nat => SDecide Nat where
(%~) SZero SZero = Proved Refl
(%~) SZero (SSucc _) = Disproved (\case)
(%~) (SSucc _) SZero = Disproved (\case)
(%~) (SSucc a) (SSucc b)
= (\cases
(Proved Refl) -> Proved Refl
(Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b)
instance Eq (SNat (z :: Nat)) where
(==) _ _ = True
instance SDecide Nat =>
GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat
-> Type) where
GHC.Internal.Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance SDecide Nat =>
GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat
-> Type) where
GHC.Internal.Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance (SDecide a, SDecide b, SDecide c, SDecide d) =>
SDecide (Foo a b c d) where
(%~) (SA a a a a) (SA b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
(%~) (SA _ _ _ _) (SB _ _ _ _) = Disproved (\case)
(%~) (SA _ _ _ _) (SC _ _ _ _) = Disproved (\case)
(%~) (SA _ _ _ _) (SD _ _ _ _) = Disproved (\case)
(%~) (SA _ _ _ _) (SE _ _ _ _) = Disproved (\case)
(%~) (SA _ _ _ _) (SF _ _ _ _) = Disproved (\case)
(%~) (SB _ _ _ _) (SA _ _ _ _) = Disproved (\case)
(%~) (SB a a a a) (SB b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
(%~) (SB _ _ _ _) (SC _ _ _ _) = Disproved (\case)
(%~) (SB _ _ _ _) (SD _ _ _ _) = Disproved (\case)
(%~) (SB _ _ _ _) (SE _ _ _ _) = Disproved (\case)
(%~) (SB _ _ _ _) (SF _ _ _ _) = Disproved (\case)
(%~) (SC _ _ _ _) (SA _ _ _ _) = Disproved (\case)
(%~) (SC _ _ _ _) (SB _ _ _ _) = Disproved (\case)
(%~) (SC a a a a) (SC b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
(%~) (SC _ _ _ _) (SD _ _ _ _) = Disproved (\case)
(%~) (SC _ _ _ _) (SE _ _ _ _) = Disproved (\case)
(%~) (SC _ _ _ _) (SF _ _ _ _) = Disproved (\case)
(%~) (SD _ _ _ _) (SA _ _ _ _) = Disproved (\case)
(%~) (SD _ _ _ _) (SB _ _ _ _) = Disproved (\case)
(%~) (SD _ _ _ _) (SC _ _ _ _) = Disproved (\case)
(%~) (SD a a a a) (SD b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
(%~) (SD _ _ _ _) (SE _ _ _ _) = Disproved (\case)
(%~) (SD _ _ _ _) (SF _ _ _ _) = Disproved (\case)
(%~) (SE _ _ _ _) (SA _ _ _ _) = Disproved (\case)
(%~) (SE _ _ _ _) (SB _ _ _ _) = Disproved (\case)
(%~) (SE _ _ _ _) (SC _ _ _ _) = Disproved (\case)
(%~) (SE _ _ _ _) (SD _ _ _ _) = Disproved (\case)
(%~) (SE a a a a) (SE b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
(%~) (SE _ _ _ _) (SF _ _ _ _) = Disproved (\case)
(%~) (SF _ _ _ _) (SA _ _ _ _) = Disproved (\case)
(%~) (SF _ _ _ _) (SB _ _ _ _) = Disproved (\case)
(%~) (SF _ _ _ _) (SC _ _ _ _) = Disproved (\case)
(%~) (SF _ _ _ _) (SD _ _ _ _) = Disproved (\case)
(%~) (SF _ _ _ _) (SE _ _ _ _) = Disproved (\case)
(%~) (SF a a a a) (SF b b b b)
= (\cases
(Proved Refl) (Proved Refl) (Proved Refl) (Proved Refl)
-> Proved Refl
(Disproved contra) _ _ _ -> Disproved (\cases Refl -> contra Refl)
_ (Disproved contra) _ _ -> Disproved (\cases Refl -> contra Refl)
_ _ (Disproved contra) _ -> Disproved (\cases Refl -> contra Refl)
_ _ _ (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
((%~) a b) ((%~) a b) ((%~) a b) ((%~) a b)
instance Eq (SFoo (z :: Foo a b c d)) where
(==) _ _ = True
instance (SDecide a, SDecide b, SDecide c, SDecide d) =>
GHC.Internal.Data.Type.Equality.TestEquality (SFoo :: Foo a b c d
-> Type) where
GHC.Internal.Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance (SDecide a, SDecide b, SDecide c, SDecide d) =>
GHC.Internal.Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d
-> Type) where
GHC.Internal.Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance Ord (SNat (z :: Nat)) where
compare _ _ = EQ
instance Ord (SFoo (z :: Foo a b c d)) where
compare _ _ = EQ
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing
instance SingI1 Succ where
liftSing = SSucc
instance SingI (SuccSym0 :: (~>) Nat Nat) where
sing = singFun1 @SuccSym0 SSucc
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (A (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SA sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (A (n :: a) (n :: b) (n :: c)) where
liftSing = SA sing sing sing
instance (SingI n, SingI n) => SingI2 (A (n :: a) (n :: b)) where
liftSing2 = SA sing sing
instance SingI (ASym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @ASym0 SA
instance SingI d =>
SingI (ASym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(ASym1 (d :: a)) (SA (sing @d))
instance SingI1 (ASym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(ASym1 (d :: a)) (SA s)
instance (SingI d, SingI d) =>
SingI (ASym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(ASym2 (d :: a) (d :: b)) (SA (sing @d) (sing @d))
instance SingI d =>
SingI1 (ASym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(ASym2 (d :: a) (d :: b)) (SA (sing @d) s)
instance SingI2 (ASym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(ASym2 (d :: a) (d :: b)) (SA s s)
instance (SingI d, SingI d, SingI d) =>
SingI (ASym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(ASym3 (d :: a) (d :: b) (d :: c))
(SA (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (ASym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(ASym3 (d :: a) (d :: b) (d :: c)) (SA (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (ASym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(ASym3 (d :: a) (d :: b) (d :: c)) (SA (sing @d) s s)
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (B (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SB sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (B (n :: a) (n :: b) (n :: c)) where
liftSing = SB sing sing sing
instance (SingI n, SingI n) => SingI2 (B (n :: a) (n :: b)) where
liftSing2 = SB sing sing
instance SingI (BSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @BSym0 SB
instance SingI d =>
SingI (BSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(BSym1 (d :: a)) (SB (sing @d))
instance SingI1 (BSym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(BSym1 (d :: a)) (SB s)
instance (SingI d, SingI d) =>
SingI (BSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(BSym2 (d :: a) (d :: b)) (SB (sing @d) (sing @d))
instance SingI d =>
SingI1 (BSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(BSym2 (d :: a) (d :: b)) (SB (sing @d) s)
instance SingI2 (BSym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(BSym2 (d :: a) (d :: b)) (SB s s)
instance (SingI d, SingI d, SingI d) =>
SingI (BSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(BSym3 (d :: a) (d :: b) (d :: c))
(SB (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (BSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(BSym3 (d :: a) (d :: b) (d :: c)) (SB (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (BSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(BSym3 (d :: a) (d :: b) (d :: c)) (SB (sing @d) s s)
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (C (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SC sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (C (n :: a) (n :: b) (n :: c)) where
liftSing = SC sing sing sing
instance (SingI n, SingI n) => SingI2 (C (n :: a) (n :: b)) where
liftSing2 = SC sing sing
instance SingI (CSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @CSym0 SC
instance SingI d =>
SingI (CSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(CSym1 (d :: a)) (SC (sing @d))
instance SingI1 (CSym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(CSym1 (d :: a)) (SC s)
instance (SingI d, SingI d) =>
SingI (CSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(CSym2 (d :: a) (d :: b)) (SC (sing @d) (sing @d))
instance SingI d =>
SingI1 (CSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(CSym2 (d :: a) (d :: b)) (SC (sing @d) s)
instance SingI2 (CSym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(CSym2 (d :: a) (d :: b)) (SC s s)
instance (SingI d, SingI d, SingI d) =>
SingI (CSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(CSym3 (d :: a) (d :: b) (d :: c))
(SC (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (CSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(CSym3 (d :: a) (d :: b) (d :: c)) (SC (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (CSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(CSym3 (d :: a) (d :: b) (d :: c)) (SC (sing @d) s s)
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (D (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SD sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (D (n :: a) (n :: b) (n :: c)) where
liftSing = SD sing sing sing
instance (SingI n, SingI n) => SingI2 (D (n :: a) (n :: b)) where
liftSing2 = SD sing sing
instance SingI (DSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @DSym0 SD
instance SingI d =>
SingI (DSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(DSym1 (d :: a)) (SD (sing @d))
instance SingI1 (DSym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(DSym1 (d :: a)) (SD s)
instance (SingI d, SingI d) =>
SingI (DSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(DSym2 (d :: a) (d :: b)) (SD (sing @d) (sing @d))
instance SingI d =>
SingI1 (DSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(DSym2 (d :: a) (d :: b)) (SD (sing @d) s)
instance SingI2 (DSym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(DSym2 (d :: a) (d :: b)) (SD s s)
instance (SingI d, SingI d, SingI d) =>
SingI (DSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(DSym3 (d :: a) (d :: b) (d :: c))
(SD (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (DSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(DSym3 (d :: a) (d :: b) (d :: c)) (SD (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (DSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(DSym3 (d :: a) (d :: b) (d :: c)) (SD (sing @d) s s)
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (E (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SE sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (E (n :: a) (n :: b) (n :: c)) where
liftSing = SE sing sing sing
instance (SingI n, SingI n) => SingI2 (E (n :: a) (n :: b)) where
liftSing2 = SE sing sing
instance SingI (ESym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @ESym0 SE
instance SingI d =>
SingI (ESym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(ESym1 (d :: a)) (SE (sing @d))
instance SingI1 (ESym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(ESym1 (d :: a)) (SE s)
instance (SingI d, SingI d) =>
SingI (ESym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(ESym2 (d :: a) (d :: b)) (SE (sing @d) (sing @d))
instance SingI d =>
SingI1 (ESym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(ESym2 (d :: a) (d :: b)) (SE (sing @d) s)
instance SingI2 (ESym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(ESym2 (d :: a) (d :: b)) (SE s s)
instance (SingI d, SingI d, SingI d) =>
SingI (ESym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(ESym3 (d :: a) (d :: b) (d :: c))
(SE (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (ESym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(ESym3 (d :: a) (d :: b) (d :: c)) (SE (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (ESym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(ESym3 (d :: a) (d :: b) (d :: c)) (SE (sing @d) s s)
instance (SingI n, SingI n, SingI n, SingI n) =>
SingI (F (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = SF sing sing sing sing
instance (SingI n, SingI n, SingI n) =>
SingI1 (F (n :: a) (n :: b) (n :: c)) where
liftSing = SF sing sing sing
instance (SingI n, SingI n) => SingI2 (F (n :: a) (n :: b)) where
liftSing2 = SF sing sing
instance SingI (FSym0 :: (~>) a ((~>) b ((~>) c ((~>) d (Foo a b c d))))) where
sing = singFun4 @FSym0 SF
instance SingI d =>
SingI (FSym1 (d :: a) :: (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
sing = singFun3 @(FSym1 (d :: a)) (SF (sing @d))
instance SingI1 (FSym1 :: a
-> (~>) b ((~>) c ((~>) d (Foo a b c d)))) where
liftSing (s :: Sing (d :: a)) = singFun3 @(FSym1 (d :: a)) (SF s)
instance (SingI d, SingI d) =>
SingI (FSym2 (d :: a) (d :: b) :: (~>) c ((~>) d (Foo a b c d))) where
sing = singFun2 @(FSym2 (d :: a) (d :: b)) (SF (sing @d) (sing @d))
instance SingI d =>
SingI1 (FSym2 (d :: a) :: b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing (s :: Sing (d :: b))
= singFun2 @(FSym2 (d :: a) (d :: b)) (SF (sing @d) s)
instance SingI2 (FSym2 :: a
-> b -> (~>) c ((~>) d (Foo a b c d))) where
liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b))
= singFun2 @(FSym2 (d :: a) (d :: b)) (SF s s)
instance (SingI d, SingI d, SingI d) =>
SingI (FSym3 (d :: a) (d :: b) (d :: c) :: (~>) d (Foo a b c d)) where
sing
= singFun1
@(FSym3 (d :: a) (d :: b) (d :: c))
(SF (sing @d) (sing @d) (sing @d))
instance (SingI d, SingI d) =>
SingI1 (FSym3 (d :: a) (d :: b) :: c -> (~>) d (Foo a b c d)) where
liftSing (s :: Sing (d :: c))
= singFun1
@(FSym3 (d :: a) (d :: b) (d :: c)) (SF (sing @d) (sing @d) s)
instance SingI d =>
SingI2 (FSym3 (d :: a) :: b -> c -> (~>) d (Foo a b c d)) where
liftSing2 (s :: Sing (d :: b)) (s :: Sing (d :: c))
= singFun1 @(FSym3 (d :: a) (d :: b) (d :: c)) (SF (sing @d) s s)