singletons-base-3.5: 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 @ErrorMessage @((~>) ErrorMessage ErrorMessage) (:$$:@#@$) 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 @ErrorMessage @ErrorMessage ((:$$:@#@$$) 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 @ErrorMessage @((~>) ErrorMessage ErrorMessage) (:<>:@#@$) 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 @ErrorMessage @ErrorMessage ((:<>:@#@$$) 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 @[Bool] @ErrorMessage 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 @ErrorMessage @((~>) ErrorMessage ErrorMessage) (<>:@#@$) 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 @ErrorMessage @ErrorMessage ((<>:@#@$$) 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 @ErrorMessage @((~>) ErrorMessage ErrorMessage) ($$:@#@$) 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 @ErrorMessage @ErrorMessage (($$:@#@$$) 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 ((<>:) t t :: ErrorMessage) :: Type)
(%$$:) ::
(forall (t :: ErrorMessage) (t :: ErrorMessage).
Sing t -> Sing t -> Sing (($$:) t t :: ErrorMessage) :: Type)
(%<>:) (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 SingI1 ((<>:@#@$$) :: ErrorMessage
-> (~>) ErrorMessage ErrorMessage) where
liftSing (s :: Sing (d :: ErrorMessage))
= singFun1 @((<>:@#@$$) (d :: ErrorMessage)) ((%<>:) s)
instance SingI (($$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = singFun2 @($$:@#@$) (%$$:)
instance SingI d =>
SingI (($$:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= singFun1 @(($$:@#@$$) (d :: ErrorMessage)) ((%$$:) (sing @d))
instance SingI1 (($$:@#@$$) :: ErrorMessage
-> (~>) ErrorMessage ErrorMessage) where
liftSing (s :: Sing (d :: ErrorMessage))
= singFun1 @(($$:@#@$$) (d :: ErrorMessage)) ((%$$:) s)
data SErrorMessage :: ErrorMessage -> 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))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%$$:) c c))
(toSing b :: SomeSing ErrorMessage)
(toSing b :: SomeSing ErrorMessage)
toSing
((:<>:) (b :: Demote ErrorMessage) (b :: Demote ErrorMessage))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%<>:) c c))
(toSing b :: SomeSing ErrorMessage)
(toSing b :: SomeSing ErrorMessage)
toSing (EM (b :: Demote [Bool]))
= (\cases (SomeSing c) -> SomeSing (SEM c))
(toSing b :: SomeSing [Bool])
instance (SingI n, SingI n) =>
SingI ((:$$:) (n :: ErrorMessage) (n :: ErrorMessage)) where
sing = (:%$$:) sing sing
instance SingI n => SingI1 ((:$$:) (n :: ErrorMessage)) where
liftSing = (:%$$:) sing
instance SingI2 (:$$:) where
liftSing2 = (:%$$:)
instance SingI ((:$$:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = singFun2 @(:$$:@#@$) (:%$$:)
instance SingI d =>
SingI ((:$$:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= singFun1 @((:$$:@#@$$) (d :: ErrorMessage)) ((:%$$:) (sing @d))
instance SingI1 ((:$$:@#@$$) :: ErrorMessage
-> (~>) ErrorMessage ErrorMessage) where
liftSing (s :: Sing (d :: ErrorMessage))
= singFun1 @((:$$:@#@$$) (d :: ErrorMessage)) ((:%$$:) s)
instance (SingI n, SingI n) =>
SingI ((:<>:) (n :: ErrorMessage) (n :: ErrorMessage)) where
sing = (:%<>:) sing sing
instance SingI n => SingI1 ((:<>:) (n :: ErrorMessage)) where
liftSing = (:%<>:) sing
instance SingI2 (:<>:) where
liftSing2 = (:%<>:)
instance SingI ((:<>:@#@$) :: (~>) ErrorMessage ((~>) ErrorMessage ErrorMessage)) where
sing = singFun2 @(:<>:@#@$) (:%<>:)
instance SingI d =>
SingI ((:<>:@#@$$) (d :: ErrorMessage) :: (~>) ErrorMessage ErrorMessage) where
sing
= singFun1 @((:<>:@#@$$) (d :: ErrorMessage)) ((:%<>:) (sing @d))
instance SingI1 ((:<>:@#@$$) :: ErrorMessage
-> (~>) ErrorMessage ErrorMessage) where
liftSing (s :: Sing (d :: ErrorMessage))
= singFun1 @((:<>:@#@$$) (d :: ErrorMessage)) ((:%<>:) s)
instance SingI n => SingI (EM (n :: [Bool])) where
sing = SEM sing
instance SingI1 EM where
liftSing = SEM
instance SingI (EMSym0 :: (~>) [Bool] ErrorMessage) where
sing = singFun1 @EMSym0 SEM