singletons-base-3.5: tests/compile-and-dump/Singletons/T136.golden
Singletons/T136.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| instance Enum BiNat where
succ [] = [True]
succ (False : as) = True : as
succ (True : as) = False : succ as
pred [] = error "pred 0"
pred (False : as) = True : pred as
pred (True : as) = False : as
toEnum i
| i < 0 = error "negative toEnum"
| i == 0 = []
| otherwise = succ (toEnum (pred i))
fromEnum [] = 0
fromEnum (False : as) = 2 * fromEnum as
fromEnum (True : as) = 1 + 2 * fromEnum as |]
======>
instance Enum BiNat where
succ [] = [True]
succ (False : as) = (True : as)
succ (True : as) = (False : succ as)
pred [] = error "pred 0"
pred (False : as) = (True : pred as)
pred (True : as) = (False : as)
toEnum i
| (i < 0) = error "negative toEnum"
| (i == 0) = []
| otherwise = succ (toEnum (pred i))
fromEnum [] = 0
fromEnum (False : as) = (2 * fromEnum as)
fromEnum (True : as) = (1 + (2 * fromEnum as))
type Succ_0123456789876543210 :: [Bool] -> [Bool]
type family Succ_0123456789876543210 (a :: [Bool]) :: [Bool] where
Succ_0123456789876543210 '[] = Apply (Apply (:@#@$) TrueSym0) NilSym0
Succ_0123456789876543210 ('(:) 'False as) = Apply (Apply (:@#@$) TrueSym0) as
Succ_0123456789876543210 ('(:) 'True as) = Apply (Apply (:@#@$) FalseSym0) (Apply SuccSym0 as)
type Pred_0123456789876543210 :: [Bool] -> [Bool]
type family Pred_0123456789876543210 (a :: [Bool]) :: [Bool] where
Pred_0123456789876543210 '[] = Apply ErrorSym0 "pred 0"
Pred_0123456789876543210 ('(:) 'False as) = Apply (Apply (:@#@$) TrueSym0) (Apply PredSym0 as)
Pred_0123456789876543210 ('(:) 'True as) = Apply (Apply (:@#@$) FalseSym0) as
type family LamCases_0123456789876543210 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_0123456789876543210 where
LamCases_0123456789876543210 i arg_0123456789876543210 'True = NilSym0
LamCases_0123456789876543210 i arg_0123456789876543210 'False = Apply SuccSym0 (Apply ToEnumSym0 (Apply PredSym0 i))
data LamCases_0123456789876543210Sym0 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 i0123456789876543210 arg_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_0123456789876543210 where
LamCases_0123456789876543210 i arg_0123456789876543210 'True = Apply ErrorSym0 "negative toEnum"
LamCases_0123456789876543210 i arg_0123456789876543210 'False = Apply (LamCases_0123456789876543210Sym0 i arg_0123456789876543210) (Apply (Apply (==@#@$) i) (FromInteger 0))
data LamCases_0123456789876543210Sym0 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 i0123456789876543210 arg_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 i0123456789876543210 arg_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_0123456789876543210 where
LamCases_0123456789876543210 arg_0123456789876543210 i = Apply (LamCases_0123456789876543210Sym0 i arg_0123456789876543210) (Apply (Apply (<@#@$) i) (FromInteger 0))
data LamCases_0123456789876543210Sym0 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 arg_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 arg_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 arg_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 arg_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural
-> [Bool]
type family ToEnum_0123456789876543210 (a :: GHC.Num.Natural.Natural) :: [Bool] where
ToEnum_0123456789876543210 arg_0123456789876543210 = Apply (LamCases_0123456789876543210Sym0 arg_0123456789876543210) arg_0123456789876543210
type FromEnum_0123456789876543210 :: [Bool]
-> GHC.Num.Natural.Natural
type family FromEnum_0123456789876543210 (a :: [Bool]) :: GHC.Num.Natural.Natural where
FromEnum_0123456789876543210 '[] = FromInteger 0
FromEnum_0123456789876543210 ('(:) 'False as) = Apply (Apply (*@#@$) (FromInteger 2)) (Apply FromEnumSym0 as)
FromEnum_0123456789876543210 ('(:) 'True as) = Apply (Apply (+@#@$) (FromInteger 1)) (Apply (Apply (*@#@$) (FromInteger 2)) (Apply FromEnumSym0 as))
instance PEnum [Bool] where
type Succ a = Succ_0123456789876543210 a
type Pred a = Pred_0123456789876543210 a
type ToEnum a = ToEnum_0123456789876543210 a
type FromEnum a = FromEnum_0123456789876543210 a
instance SEnum [Bool] where
sSucc SNil
= applySing (applySing (singFun2 @(:@#@$) SCons) STrue) SNil
sSucc (SCons SFalse (sAs :: Sing as))
= applySing (applySing (singFun2 @(:@#@$) SCons) STrue) sAs
sSucc (SCons STrue (sAs :: Sing as))
= applySing
(applySing (singFun2 @(:@#@$) SCons) SFalse)
(applySing (singFun1 @SuccSym0 sSucc) sAs)
sPred SNil
= applySing (singFun1 @ErrorSym0 sError) (sing :: Sing "pred 0")
sPred (SCons SFalse (sAs :: Sing as))
= applySing
(applySing (singFun2 @(:@#@$) SCons) STrue)
(applySing (singFun1 @PredSym0 sPred) sAs)
sPred (SCons STrue (sAs :: Sing as))
= applySing (applySing (singFun2 @(:@#@$) SCons) SFalse) sAs
sToEnum (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
= applySing
(singFun1
@(LamCases_0123456789876543210Sym0 arg_0123456789876543210)
(\cases
(sI :: Sing i)
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 i arg_0123456789876543210)
(\cases
STrue
-> applySing
(singFun1 @ErrorSym0 sError) (sing :: Sing "negative toEnum")
SFalse
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 i arg_0123456789876543210)
(\cases
STrue -> SNil
SFalse
-> applySing
(singFun1 @SuccSym0 sSucc)
(applySing
(singFun1 @ToEnumSym0 sToEnum)
(applySing (singFun1 @PredSym0 sPred) sI))))
(applySing
(applySing (singFun2 @(==@#@$) (%==)) sI)
(sFromInteger (sing :: Sing 0)))))
(applySing
(applySing (singFun2 @(<@#@$) (%<)) sI)
(sFromInteger (sing :: Sing 0)))))
sArg_0123456789876543210
sFromEnum SNil = sFromInteger (sing :: Sing 0)
sFromEnum (SCons SFalse (sAs :: Sing as))
= applySing
(applySing
(singFun2 @(*@#@$) (%*)) (sFromInteger (sing :: Sing 2)))
(applySing (singFun1 @FromEnumSym0 sFromEnum) sAs)
sFromEnum (SCons STrue (sAs :: Sing as))
= applySing
(applySing
(singFun2 @(+@#@$) (%+)) (sFromInteger (sing :: Sing 1)))
(applySing
(applySing
(singFun2 @(*@#@$) (%*)) (sFromInteger (sing :: Sing 2)))
(applySing (singFun1 @FromEnumSym0 sFromEnum) sAs))