singletons-2.3: tests/compile-and-dump/Singletons/OrdDeriving.ghc82.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 family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where
Equals_0123456789876543210 Zero Zero = TrueSym0
Equals_0123456789876543210 (Succ a) (Succ b) = (:==) a b
Equals_0123456789876543210 (a :: Nat) (b :: Nat) = FalseSym0
instance PEq Nat where
type (:==) (a :: Nat) (b :: Nat) = Equals_0123456789876543210 a b
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 family Equals_0123456789876543210 (a :: Foo k k k k) (b :: Foo k k k k) :: 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 (a :: Foo k k k k) (b :: Foo k k k k) = FalseSym0
instance PEq (Foo k k k k) where
type (:==) (a :: Foo k k k k) (b :: Foo k k k k) = Equals_0123456789876543210 a b
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 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (Succ _z_0123456789876543210) 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 :: Nat) (a :: Nat) = 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 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (A _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (B _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (C _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (D _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = GTSym0
Compare_0123456789876543210 (F _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) (E _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210 _z_0123456789876543210) = 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 :: Foo a b c d) (a :: Foo a b c d) = Apply (Apply Compare_0123456789876543210Sym0 a) a
data instance Sing (z :: Nat)
= z ~ Zero => SZero |
forall (n :: Nat). z ~ Succ n => SSucc (Sing (n :: Nat))
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)
= case toSing b :: SomeSing Nat of {
SomeSing c -> SomeSing (SSucc c) }
instance SEq Nat where
(%:==) SZero SZero = STrue
(%:==) SZero (SSucc _) = SFalse
(%:==) (SSucc _) SZero = SFalse
(%:==) (SSucc a) (SSucc b) = ((%:==) a) b
instance SDecide Nat where
(%~) SZero SZero = Proved Refl
(%~) SZero (SSucc _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SSucc _) SZero
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SSucc a) (SSucc b)
= case ((%~) a) b of
Proved Refl -> Proved Refl
Disproved contra
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
data instance Sing (z :: Foo a b c d)
= forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ A n n n n =>
SA (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d)) |
forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ B n n n n =>
SB (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d)) |
forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ C n n n n =>
SC (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d)) |
forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ D n n n n =>
SD (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d)) |
forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ E n n n n =>
SE (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d)) |
forall (n :: a) (n :: b) (n :: c) (n :: d). z ~ F n n n n =>
SF (Sing (n :: a)) (Sing (n :: b)) (Sing (n :: c)) (Sing (n :: d))
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 b b b)
= 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 b b b)
= 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 b b b)
= 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 b b b)
= 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 b b b)
= 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 b b b)
= 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 (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SA _ _ _ _) (SC _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SA _ _ _ _) (SD _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SA _ _ _ _) (SE _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SA _ _ _ _) (SF _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SB _ _ _ _) (SA _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SB _ _ _ _) (SD _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SB _ _ _ _) (SE _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SB _ _ _ _) (SF _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SC _ _ _ _) (SA _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SC _ _ _ _) (SB _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SC _ _ _ _) (SE _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SC _ _ _ _) (SF _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SD _ _ _ _) (SA _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SD _ _ _ _) (SB _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SD _ _ _ _) (SC _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SD _ _ _ _) (SF _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SE _ _ _ _) (SA _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SE _ _ _ _) (SB _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SE _ _ _ _) (SC _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SE _ _ _ _) (SD _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SF _ _ _ _) (SA _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SF _ _ _ _) (SB _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SF _ _ _ _) (SC _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SF _ _ _ _) (SD _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SF _ _ _ _) (SE _ _ _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 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 :: TyFun Nat Ordering
-> GHC.Types.Type) t2 :: Ordering)
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 :: TyFun (Foo a b c d) Ordering
-> GHC.Types.Type) t2 :: Ordering)
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 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