singletons-2.1: tests/compile-and-dump/Singletons/T136.ghc80.template
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 GHC.Types.[] = [True]
succ (False GHC.Types.: as) = (True GHC.Types.: as)
succ (True GHC.Types.: as) = (False GHC.Types.: (succ as))
pred GHC.Types.[] = error "pred 0"
pred (False GHC.Types.: as) = (True GHC.Types.: (pred as))
pred (True GHC.Types.: as) = (False GHC.Types.: as)
toEnum i
| (i < 0) = error "negative toEnum"
| (i == 0) = []
| otherwise = succ (toEnum (pred i))
fromEnum GHC.Types.[] = 0
fromEnum (False GHC.Types.: as) = (2 * (fromEnum as))
fromEnum (True GHC.Types.: as) = (1 + (2 * (fromEnum as)))
type family Succ_0123456789 (a :: [Bool]) :: [Bool] where
Succ_0123456789 '[] = Apply (Apply (:$) TrueSym0) '[]
Succ_0123456789 ((:) False as) = Apply (Apply (:$) TrueSym0) as
Succ_0123456789 ((:) True as) = Apply (Apply (:$) FalseSym0) (Apply SuccSym0 as)
type Succ_0123456789Sym1 (t :: [Bool]) = Succ_0123456789 t
instance SuppressUnusedWarnings Succ_0123456789Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Succ_0123456789Sym0KindInference GHC.Tuple.())
data Succ_0123456789Sym0 (l :: TyFun [Bool] [Bool])
= forall arg. KindOf (Apply Succ_0123456789Sym0 arg) ~ KindOf (Succ_0123456789Sym1 arg) =>
Succ_0123456789Sym0KindInference
type instance Apply Succ_0123456789Sym0 l = Succ_0123456789Sym1 l
type family Pred_0123456789 (a :: [Bool]) :: [Bool] where
Pred_0123456789 '[] = Apply ErrorSym0 "pred 0"
Pred_0123456789 ((:) False as) = Apply (Apply (:$) TrueSym0) (Apply PredSym0 as)
Pred_0123456789 ((:) True as) = Apply (Apply (:$) FalseSym0) as
type Pred_0123456789Sym1 (t :: [Bool]) = Pred_0123456789 t
instance SuppressUnusedWarnings Pred_0123456789Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Pred_0123456789Sym0KindInference GHC.Tuple.())
data Pred_0123456789Sym0 (l :: TyFun [Bool] [Bool])
= forall arg. KindOf (Apply Pred_0123456789Sym0 arg) ~ KindOf (Pred_0123456789Sym1 arg) =>
Pred_0123456789Sym0KindInference
type instance Apply Pred_0123456789Sym0 l = Pred_0123456789Sym1 l
type family Case_0123456789 i arg_0123456789 t where
Case_0123456789 i arg_0123456789 True = '[]
Case_0123456789 i arg_0123456789 False = Apply SuccSym0 (Apply ToEnumSym0 (Apply PredSym0 i))
type family Case_0123456789 i arg_0123456789 t where
Case_0123456789 i arg_0123456789 True = Apply ErrorSym0 "negative toEnum"
Case_0123456789 i arg_0123456789 False = Case_0123456789 i arg_0123456789 (Apply (Apply (:==$) i) (FromInteger 0))
type family Case_0123456789 arg_0123456789 t where
Case_0123456789 arg_0123456789 i = Case_0123456789 i arg_0123456789 (Apply (Apply (:<$) i) (FromInteger 0))
type family ToEnum_0123456789 (a :: GHC.Types.Nat) :: [Bool] where
ToEnum_0123456789 arg_0123456789 = Case_0123456789 arg_0123456789 arg_0123456789
type ToEnum_0123456789Sym1 (t :: GHC.Types.Nat) =
ToEnum_0123456789 t
instance SuppressUnusedWarnings ToEnum_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) ToEnum_0123456789Sym0KindInference GHC.Tuple.())
data ToEnum_0123456789Sym0 (l :: TyFun GHC.Types.Nat [Bool])
= forall arg. KindOf (Apply ToEnum_0123456789Sym0 arg) ~ KindOf (ToEnum_0123456789Sym1 arg) =>
ToEnum_0123456789Sym0KindInference
type instance Apply ToEnum_0123456789Sym0 l = ToEnum_0123456789Sym1 l
type family FromEnum_0123456789 (a :: [Bool]) :: GHC.Types.Nat where
FromEnum_0123456789 '[] = FromInteger 0
FromEnum_0123456789 ((:) False as) = Apply (Apply (:*$) (FromInteger 2)) (Apply FromEnumSym0 as)
FromEnum_0123456789 ((:) True as) = Apply (Apply (:+$) (FromInteger 1)) (Apply (Apply (:*$) (FromInteger 2)) (Apply FromEnumSym0 as))
type FromEnum_0123456789Sym1 (t :: [Bool]) = FromEnum_0123456789 t
instance SuppressUnusedWarnings FromEnum_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) FromEnum_0123456789Sym0KindInference GHC.Tuple.())
data FromEnum_0123456789Sym0 (l :: TyFun [Bool] GHC.Types.Nat)
= forall arg. KindOf (Apply FromEnum_0123456789Sym0 arg) ~ KindOf (FromEnum_0123456789Sym1 arg) =>
FromEnum_0123456789Sym0KindInference
type instance Apply FromEnum_0123456789Sym0 l = FromEnum_0123456789Sym1 l
instance PEnum (KProxy :: KProxy [Bool]) where
type Succ (a :: [Bool]) = Apply Succ_0123456789Sym0 a
type Pred (a :: [Bool]) = Apply Pred_0123456789Sym0 a
type ToEnum (a :: GHC.Types.Nat) = Apply ToEnum_0123456789Sym0 a
type FromEnum (a :: [Bool]) = Apply FromEnum_0123456789Sym0 a
instance SEnum (KProxy :: KProxy [Bool]) where
sSucc ::
forall (t0 :: [Bool]).
Sing t0
-> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool]
-> GHC.Types.Type) t0 :: [Bool])
sPred ::
forall (t0 :: [Bool]).
Sing t0
-> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool]
-> GHC.Types.Type) t0 :: [Bool])
sToEnum ::
forall (t0 :: GHC.Types.Nat).
Sing t0
-> Sing (Apply (ToEnumSym0 :: TyFun GHC.Types.Nat [Bool]
-> GHC.Types.Type) t0 :: [Bool])
sFromEnum ::
forall (t0 :: [Bool]).
Sing t0
-> Sing (Apply (FromEnumSym0 :: TyFun [Bool] GHC.Types.Nat
-> GHC.Types.Type) t0 :: GHC.Types.Nat)
sSucc SNil
= let
lambda :: t0 ~ '[] => Sing (Apply SuccSym0 t0 :: [Bool])
lambda
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue) SNil
in lambda
sSucc (SCons SFalse sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) FalseSym0) as =>
Sing as -> Sing (Apply SuccSym0 t0 :: [Bool])
lambda as
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue) as
in lambda sAs
sSucc (SCons STrue sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) TrueSym0) as =>
Sing as -> Sing (Apply SuccSym0 t0 :: [Bool])
lambda as
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) SFalse)
(applySing (singFun1 (Proxy :: Proxy SuccSym0) sSucc) as)
in lambda sAs
sPred SNil
= let
lambda :: t0 ~ '[] => Sing (Apply PredSym0 t0 :: [Bool])
lambda = sError (sing :: Sing "pred 0")
in lambda
sPred (SCons SFalse sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) FalseSym0) as =>
Sing as -> Sing (Apply PredSym0 t0 :: [Bool])
lambda as
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) STrue)
(applySing (singFun1 (Proxy :: Proxy PredSym0) sPred) as)
in lambda sAs
sPred (SCons STrue sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) TrueSym0) as =>
Sing as -> Sing (Apply PredSym0 t0 :: [Bool])
lambda as
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) SFalse) as
in lambda sAs
sToEnum sArg_0123456789
= let
lambda ::
forall arg_0123456789.
t0 ~ arg_0123456789 =>
Sing arg_0123456789 -> Sing (Apply ToEnumSym0 t0 :: [Bool])
lambda arg_0123456789
= case arg_0123456789 of {
sI
-> let
lambda ::
forall i.
i ~ arg_0123456789 =>
Sing i -> Sing (Case_0123456789 arg_0123456789 i :: [Bool])
lambda i
= case
applySing
(applySing (singFun2 (Proxy :: Proxy (:<$)) (%:<)) i)
(sFromInteger (sing :: Sing 0))
of {
STrue
-> let
lambda ::
TrueSym0 ~ Apply (Apply (:<$) i) (FromInteger 0) =>
Sing (Case_0123456789 i arg_0123456789 TrueSym0 :: [Bool])
lambda = sError (sing :: Sing "negative toEnum")
in lambda
SFalse
-> let
lambda ::
FalseSym0 ~ Apply (Apply (:<$) i) (FromInteger 0) =>
Sing (Case_0123456789 i arg_0123456789 FalseSym0 :: [Bool])
lambda
= case
applySing
(applySing
(singFun2 (Proxy :: Proxy (:==$)) (%:==)) i)
(sFromInteger (sing :: Sing 0))
of {
STrue
-> let
lambda ::
TrueSym0 ~ Apply (Apply (:==$) i) (FromInteger 0) =>
Sing (Case_0123456789 i arg_0123456789 TrueSym0 :: [Bool])
lambda = SNil
in lambda
SFalse
-> let
lambda ::
FalseSym0 ~ Apply (Apply (:==$) i) (FromInteger 0) =>
Sing (Case_0123456789 i arg_0123456789 FalseSym0 :: [Bool])
lambda
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) sSucc)
(applySing
(singFun1
(Proxy :: Proxy ToEnumSym0) sToEnum)
(applySing
(singFun1
(Proxy :: Proxy PredSym0) sPred)
i))
in lambda } ::
Sing (Case_0123456789 i arg_0123456789 (Apply (Apply (:==$) i) (FromInteger 0)) :: [Bool])
in lambda } ::
Sing (Case_0123456789 i arg_0123456789 (Apply (Apply (:<$) i) (FromInteger 0)) :: [Bool])
in lambda sI } ::
Sing (Case_0123456789 arg_0123456789 arg_0123456789 :: [Bool])
in lambda sArg_0123456789
sFromEnum SNil
= let
lambda :: t0 ~ '[] => Sing (Apply FromEnumSym0 t0 :: GHC.Types.Nat)
lambda = sFromInteger (sing :: Sing 0)
in lambda
sFromEnum (SCons SFalse sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) FalseSym0) as =>
Sing as -> Sing (Apply FromEnumSym0 t0 :: GHC.Types.Nat)
lambda as
= applySing
(applySing
(singFun2 (Proxy :: Proxy (:*$)) (%:*))
(sFromInteger (sing :: Sing 2)))
(applySing (singFun1 (Proxy :: Proxy FromEnumSym0) sFromEnum) as)
in lambda sAs
sFromEnum (SCons STrue sAs)
= let
lambda ::
forall as.
t0 ~ Apply (Apply (:$) TrueSym0) as =>
Sing as -> Sing (Apply FromEnumSym0 t0 :: GHC.Types.Nat)
lambda as
= applySing
(applySing
(singFun2 (Proxy :: Proxy (:+$)) (%:+))
(sFromInteger (sing :: Sing 1)))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:*$)) (%:*))
(sFromInteger (sing :: Sing 2)))
(applySing (singFun1 (Proxy :: Proxy FromEnumSym0) sFromEnum) as))
in lambda sAs