singletons-2.4: tests/compile-and-dump/Singletons/OrdDeriving.ghc84.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 (t :: Nat) = Succ t
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
data SuccSym0 (l :: TyFun Nat Nat)
= forall arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0KindInference
type instance Apply SuccSym0 l = Succ l
type ASym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
A t t t t
instance SuppressUnusedWarnings ASym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ASym3KindInference) GHC.Tuple.())
data ASym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (ASym3 l l l) arg) (ASym4 l l l arg) =>
ASym3KindInference
type instance Apply (ASym3 l l l) l = A l l l l
instance SuppressUnusedWarnings ASym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ASym2KindInference) GHC.Tuple.())
data ASym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ASym2 l l) arg) (ASym3 l l arg) =>
ASym2KindInference
type instance Apply (ASym2 l l) l = ASym3 l l l
instance SuppressUnusedWarnings ASym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ASym1KindInference) GHC.Tuple.())
data ASym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ASym1 l) arg) (ASym2 l arg) =>
ASym1KindInference
type instance Apply (ASym1 l) l = ASym2 l l
instance SuppressUnusedWarnings ASym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ASym0KindInference) GHC.Tuple.())
data ASym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply ASym0 arg) (ASym1 arg) =>
ASym0KindInference
type instance Apply ASym0 l = ASym1 l
type BSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
B t t t t
instance SuppressUnusedWarnings BSym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) BSym3KindInference) GHC.Tuple.())
data BSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (BSym3 l l l) arg) (BSym4 l l l arg) =>
BSym3KindInference
type instance Apply (BSym3 l l l) l = B l l l l
instance SuppressUnusedWarnings BSym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) BSym2KindInference) GHC.Tuple.())
data BSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (BSym2 l l) arg) (BSym3 l l arg) =>
BSym2KindInference
type instance Apply (BSym2 l l) l = BSym3 l l l
instance SuppressUnusedWarnings BSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) BSym1KindInference) GHC.Tuple.())
data BSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (BSym1 l) arg) (BSym2 l arg) =>
BSym1KindInference
type instance Apply (BSym1 l) l = BSym2 l l
instance SuppressUnusedWarnings BSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) BSym0KindInference) GHC.Tuple.())
data BSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply BSym0 arg) (BSym1 arg) =>
BSym0KindInference
type instance Apply BSym0 l = BSym1 l
type CSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
C t t t t
instance SuppressUnusedWarnings CSym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) CSym3KindInference) GHC.Tuple.())
data CSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (CSym3 l l l) arg) (CSym4 l l l arg) =>
CSym3KindInference
type instance Apply (CSym3 l l l) l = C l l l l
instance SuppressUnusedWarnings CSym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) CSym2KindInference) GHC.Tuple.())
data CSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (CSym2 l l) arg) (CSym3 l l arg) =>
CSym2KindInference
type instance Apply (CSym2 l l) l = CSym3 l l l
instance SuppressUnusedWarnings CSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) CSym1KindInference) GHC.Tuple.())
data CSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (CSym1 l) arg) (CSym2 l arg) =>
CSym1KindInference
type instance Apply (CSym1 l) l = CSym2 l l
instance SuppressUnusedWarnings CSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) CSym0KindInference) GHC.Tuple.())
data CSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply CSym0 arg) (CSym1 arg) =>
CSym0KindInference
type instance Apply CSym0 l = CSym1 l
type DSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
D t t t t
instance SuppressUnusedWarnings DSym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) DSym3KindInference) GHC.Tuple.())
data DSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (DSym3 l l l) arg) (DSym4 l l l arg) =>
DSym3KindInference
type instance Apply (DSym3 l l l) l = D l l l l
instance SuppressUnusedWarnings DSym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) DSym2KindInference) GHC.Tuple.())
data DSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (DSym2 l l) arg) (DSym3 l l arg) =>
DSym2KindInference
type instance Apply (DSym2 l l) l = DSym3 l l l
instance SuppressUnusedWarnings DSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) DSym1KindInference) GHC.Tuple.())
data DSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (DSym1 l) arg) (DSym2 l arg) =>
DSym1KindInference
type instance Apply (DSym1 l) l = DSym2 l l
instance SuppressUnusedWarnings DSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) DSym0KindInference) GHC.Tuple.())
data DSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply DSym0 arg) (DSym1 arg) =>
DSym0KindInference
type instance Apply DSym0 l = DSym1 l
type ESym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
E t t t t
instance SuppressUnusedWarnings ESym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ESym3KindInference) GHC.Tuple.())
data ESym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (ESym3 l l l) arg) (ESym4 l l l arg) =>
ESym3KindInference
type instance Apply (ESym3 l l l) l = E l l l l
instance SuppressUnusedWarnings ESym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ESym2KindInference) GHC.Tuple.())
data ESym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ESym2 l l) arg) (ESym3 l l arg) =>
ESym2KindInference
type instance Apply (ESym2 l l) l = ESym3 l l l
instance SuppressUnusedWarnings ESym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ESym1KindInference) GHC.Tuple.())
data ESym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ESym1 l) arg) (ESym2 l arg) =>
ESym1KindInference
type instance Apply (ESym1 l) l = ESym2 l l
instance SuppressUnusedWarnings ESym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) ESym0KindInference) GHC.Tuple.())
data ESym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply ESym0 arg) (ESym1 arg) =>
ESym0KindInference
type instance Apply ESym0 l = ESym1 l
type FSym4 (t :: a0123456789876543210) (t :: b0123456789876543210) (t :: c0123456789876543210) (t :: d0123456789876543210) =
F t t t t
instance SuppressUnusedWarnings FSym3 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) FSym3KindInference) GHC.Tuple.())
data FSym3 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: c0123456789876543210) (l :: TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210))
= forall arg. SameKind (Apply (FSym3 l l l) arg) (FSym4 l l l arg) =>
FSym3KindInference
type instance Apply (FSym3 l l l) l = F l l l l
instance SuppressUnusedWarnings FSym2 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) FSym2KindInference) GHC.Tuple.())
data FSym2 (l :: a0123456789876543210) (l :: b0123456789876543210) (l :: TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (FSym2 l l) arg) (FSym3 l l arg) =>
FSym2KindInference
type instance Apply (FSym2 l l) l = FSym3 l l l
instance SuppressUnusedWarnings FSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) FSym1KindInference) GHC.Tuple.())
data FSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply (FSym1 l) arg) (FSym2 l arg) =>
FSym1KindInference
type instance Apply (FSym1 l) l = FSym2 l l
instance SuppressUnusedWarnings FSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) FSym0KindInference) GHC.Tuple.())
data FSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (TyFun c0123456789876543210 (TyFun d0123456789876543210 (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210)
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply FSym0 arg) (FSym1 arg) =>
FSym0KindInference
type instance Apply FSym0 l = FSym1 l
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 (t :: Nat) (t :: Nat) =
Compare_0123456789876543210 t t
instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym1 (l :: Nat) (l :: TyFun Nat Ordering)
= forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
Compare_0123456789876543210Sym1KindInference
type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym0 (l :: TyFun Nat (TyFun Nat Ordering
-> GHC.Types.Type))
= forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0KindInference
type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
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 (t :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (t :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) =
Compare_0123456789876543210 t t
instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym1 (l :: Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (l :: TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering)
= forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
Compare_0123456789876543210Sym1KindInference
type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym0 (l :: TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) (TyFun (Foo a0123456789876543210 b0123456789876543210 c0123456789876543210 d0123456789876543210) Ordering
-> GHC.Types.Type))
= forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0KindInference
type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
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 (z :: Nat)
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 (z :: Foo a b c d)
where
SA :: forall (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 (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 (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 (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 (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 (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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
(((GHC.Tuple.(,,,) (toSing b :: SomeSing a))
(toSing b :: SomeSing b))
(toSing b :: SomeSing c))
(toSing b :: SomeSing d)
of {
GHC.Tuple.(,,,) (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 (TyFun Nat Ordering
-> GHC.Types.Type)
-> 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) (TyFun (Foo a b c d) Ordering
-> GHC.Types.Type)
-> 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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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
(((GHC.Tuple.(,,,) (((%~) a) b)) (((%~) a) b)) (((%~) a) b))
(((%~) a) b)
of
GHC.Tuple.(,,,) (Proved Refl)
(Proved Refl)
(Proved Refl)
(Proved Refl)
-> Proved Refl
GHC.Tuple.(,,,) (Disproved contra) _ _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ (Disproved contra) _ _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ (Disproved contra) _
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
GHC.Tuple.(,,,) _ _ _ (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 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, 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, 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, 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, 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, SingI n) =>
SingI (F (n :: a) (n :: b) (n :: c) (n :: d)) where
sing = (((SF sing) sing) sing) sing