singletons-base-3.0: tests/compile-and-dump/Singletons/T200.golden
Singletons/T200.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| ($$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
x $$: y = x :$$: y
(<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
x <>: y = x :<>: y
data ErrorMessage
= ErrorMessage :$$: ErrorMessage |
ErrorMessage :<>: ErrorMessage |
EM [Bool] |]
======>
data ErrorMessage
= ErrorMessage :$$: ErrorMessage |
ErrorMessage :<>: ErrorMessage |
EM [Bool]
($$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
($$:) x y = (x :$$: y)
(<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
(<>:) x y = (x :<>: y)
type (:$$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
data (:$$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
where
(::$$:@#@$###) :: SameKind (Apply (:$$:@#@$) arg) ((:$$:@#@$$) arg) =>
(:$$:@#@$) a0123456789876543210
type instance Apply (:$$:@#@$) a0123456789876543210 = (:$$:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:$$:@#@$) where
suppressUnusedWarnings = snd (((,) (::$$:@#@$###)) ())
type (:$$:@#@$$) :: ErrorMessage -> (~>) ErrorMessage ErrorMessage
data (:$$:@#@$$) (a0123456789876543210 :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage
where
(::$$:@#@$$###) :: SameKind (Apply ((:$$:@#@$$) a0123456789876543210) arg) ((:$$:@#@$$$) a0123456789876543210 arg) =>
(:$$:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:$$:@#@$$) a0123456789876543210) a0123456789876543210 = (:$$:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:$$:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::$$:@#@$$###)) ())
type (:$$:@#@$$$) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family (:$$:@#@$$$) (a0123456789876543210 :: ErrorMessage) (a0123456789876543210 :: ErrorMessage) :: ErrorMessage where
(:$$:@#@$$$) a0123456789876543210 a0123456789876543210 = (:$$:) a0123456789876543210 a0123456789876543210
type (:<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
data (:<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
where
(::<>:@#@$###) :: SameKind (Apply (:<>:@#@$) arg) ((:<>:@#@$$) arg) =>
(:<>:@#@$) a0123456789876543210
type instance Apply (:<>:@#@$) a0123456789876543210 = (:<>:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:<>:@#@$) where
suppressUnusedWarnings = snd (((,) (::<>:@#@$###)) ())
type (:<>:@#@$$) :: ErrorMessage -> (~>) ErrorMessage ErrorMessage
data (:<>:@#@$$) (a0123456789876543210 :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage
where
(::<>:@#@$$###) :: SameKind (Apply ((:<>:@#@$$) a0123456789876543210) arg) ((:<>:@#@$$$) a0123456789876543210 arg) =>
(:<>:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:<>:@#@$$) a0123456789876543210) a0123456789876543210 = (:<>:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:<>:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::<>:@#@$$###)) ())
type (:<>:@#@$$$) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family (:<>:@#@$$$) (a0123456789876543210 :: ErrorMessage) (a0123456789876543210 :: ErrorMessage) :: ErrorMessage where
(:<>:@#@$$$) a0123456789876543210 a0123456789876543210 = (:<>:) a0123456789876543210 a0123456789876543210
type EMSym0 :: (~>) [Bool] ErrorMessage
data EMSym0 :: (~>) [Bool] ErrorMessage
where
EMSym0KindInference :: SameKind (Apply EMSym0 arg) (EMSym1 arg) =>
EMSym0 a0123456789876543210
type instance Apply EMSym0 a0123456789876543210 = EM a0123456789876543210
instance SuppressUnusedWarnings EMSym0 where
suppressUnusedWarnings = snd (((,) EMSym0KindInference) ())
type EMSym1 :: [Bool] -> ErrorMessage
type family EMSym1 (a0123456789876543210 :: [Bool]) :: ErrorMessage where
EMSym1 a0123456789876543210 = EM a0123456789876543210
type (<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
data (<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
where
(:<>:@#@$###) :: SameKind (Apply (<>:@#@$) arg) ((<>:@#@$$) arg) =>
(<>:@#@$) a0123456789876543210
type instance Apply (<>:@#@$) a0123456789876543210 = (<>:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (<>:@#@$) where
suppressUnusedWarnings = snd (((,) (:<>:@#@$###)) ())
type (<>:@#@$$) :: ErrorMessage -> (~>) ErrorMessage ErrorMessage
data (<>:@#@$$) (a0123456789876543210 :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage
where
(:<>:@#@$$###) :: SameKind (Apply ((<>:@#@$$) a0123456789876543210) arg) ((<>:@#@$$$) a0123456789876543210 arg) =>
(<>:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((<>:@#@$$) a0123456789876543210) a0123456789876543210 = (<>:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((<>:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (:<>:@#@$$###)) ())
type (<>:@#@$$$) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family (<>:@#@$$$) (a0123456789876543210 :: ErrorMessage) (a0123456789876543210 :: ErrorMessage) :: ErrorMessage where
(<>:@#@$$$) a0123456789876543210 a0123456789876543210 = (<>:) a0123456789876543210 a0123456789876543210
type ($$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
data ($$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)
where
(:$$:@#@$###) :: SameKind (Apply ($$:@#@$) arg) (($$:@#@$$) arg) =>
($$:@#@$) a0123456789876543210
type instance Apply ($$:@#@$) a0123456789876543210 = ($$:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings ($$:@#@$) where
suppressUnusedWarnings = snd (((,) (:$$:@#@$###)) ())
type ($$:@#@$$) :: ErrorMessage -> (~>) ErrorMessage ErrorMessage
data ($$:@#@$$) (a0123456789876543210 :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage
where
(:$$:@#@$$###) :: SameKind (Apply (($$:@#@$$) a0123456789876543210) arg) (($$:@#@$$$) a0123456789876543210 arg) =>
($$:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply (($$:@#@$$) a0123456789876543210) a0123456789876543210 = ($$:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (($$:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (:$$:@#@$$###)) ())
type ($$:@#@$$$) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family ($$:@#@$$$) (a0123456789876543210 :: ErrorMessage) (a0123456789876543210 :: ErrorMessage) :: ErrorMessage where
($$:@#@$$$) a0123456789876543210 a0123456789876543210 = ($$:) a0123456789876543210 a0123456789876543210
type (<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family (<>:) (a :: ErrorMessage) (a :: ErrorMessage) :: ErrorMessage where
(<>:) x y = Apply (Apply (:<>:@#@$) x) y
type ($$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
type family ($$:) (a :: ErrorMessage) (a :: ErrorMessage) :: ErrorMessage where
($$:) x y = Apply (Apply (:$$:@#@$) x) y
(%<>:) ::
forall (t :: ErrorMessage) (t :: ErrorMessage).
Sing t
-> Sing t -> Sing (Apply (Apply (<>:@#@$) t) t :: ErrorMessage)
(%$$:) ::
forall (t :: ErrorMessage) (t :: ErrorMessage).
Sing t
-> Sing t -> Sing (Apply (Apply ($$:@#@$) t) t :: ErrorMessage)
(%<>:) (sX :: Sing x) (sY :: Sing y)
= (applySing ((applySing ((singFun2 @(:<>:@#@$)) (:%<>:))) sX)) sY
(%$$:) (sX :: Sing x) (sY :: Sing y)
= (applySing ((applySing ((singFun2 @(:$$:@#@$)) (:%$$:))) sX)) sY
instance SingI ((<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = (singFun2 @(<>:@#@$)) (%<>:)
instance SingI d =>
SingI ((<>:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= (singFun1 @((<>:@#@$$) (d :: ErrorMessage))) ((%<>:) (sing @d))
instance SingI (($$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = (singFun2 @($$:@#@$)) (%$$:)
instance SingI d =>
SingI (($$:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= (singFun1 @(($$:@#@$$) (d :: ErrorMessage))) ((%$$:) (sing @d))
data SErrorMessage :: ErrorMessage -> GHC.Types.Type
where
(:%$$:) :: forall (n :: ErrorMessage) (n :: ErrorMessage).
(Sing n) -> (Sing n) -> SErrorMessage ((:$$:) n n :: ErrorMessage)
(:%<>:) :: forall (n :: ErrorMessage) (n :: ErrorMessage).
(Sing n) -> (Sing n) -> SErrorMessage ((:<>:) n n :: ErrorMessage)
SEM :: forall (n :: [Bool]).
(Sing n) -> SErrorMessage (EM n :: ErrorMessage)
type instance Sing @ErrorMessage = SErrorMessage
instance SingKind ErrorMessage where
type Demote ErrorMessage = ErrorMessage
fromSing ((:%$$:) b b) = ((:$$:) (fromSing b)) (fromSing b)
fromSing ((:%<>:) b b) = ((:<>:) (fromSing b)) (fromSing b)
fromSing (SEM b) = EM (fromSing b)
toSing
((:$$:) (b :: Demote ErrorMessage) (b :: Demote ErrorMessage))
= case
((,) (toSing b :: SomeSing ErrorMessage))
(toSing b :: SomeSing ErrorMessage)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:%$$:) c) c) }
toSing
((:<>:) (b :: Demote ErrorMessage) (b :: Demote ErrorMessage))
= case
((,) (toSing b :: SomeSing ErrorMessage))
(toSing b :: SomeSing ErrorMessage)
of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:%<>:) c) c) }
toSing (EM (b :: Demote [Bool]))
= case toSing b :: SomeSing [Bool] of {
SomeSing c -> SomeSing (SEM c) }
instance (SingI n, SingI n) =>
SingI ((:$$:) (n :: ErrorMessage) (n :: ErrorMessage)) where
sing = ((:%$$:) sing) sing
instance SingI ((:$$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = (singFun2 @(:$$:@#@$)) (:%$$:)
instance SingI d =>
SingI ((:$$:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= (singFun1 @((:$$:@#@$$) (d :: ErrorMessage))) ((:%$$:) (sing @d))
instance (SingI n, SingI n) =>
SingI ((:<>:) (n :: ErrorMessage) (n :: ErrorMessage)) where
sing = ((:%<>:) sing) sing
instance SingI ((:<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = (singFun2 @(:<>:@#@$)) (:%<>:)
instance SingI d =>
SingI ((:<>:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= (singFun1 @((:<>:@#@$$) (d :: ErrorMessage))) ((:%<>:) (sing @d))
instance SingI n => SingI (EM (n :: [Bool])) where
sing = SEM sing
instance SingI (EMSym0 :: (~>) [Bool] ErrorMessage) where
sing = (singFun1 @EMSym0) SEM