singletons-2.5: tests/compile-and-dump/Singletons/OrdDeriving.ghc86.template
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))