singletons-base-3.2: tests/compile-and-dump/Singletons/T536.golden
Singletons/T536.hs:(0,0)-(0,0): Splicing declarations
let
customPromote :: Name -> Name
customPromote n
| n == ''Message = ''PMessage
| n == 'MkMessage = 'PMkMessage
| n == ''Text = ''Symbol
| otherwise = promotedDataTypeOrConName defaultOptions n
customDefun :: Name -> Int -> Name
customDefun n sat
= defunctionalizedName defaultOptions (customPromote n) sat
in
withOptions
defaultOptions
{promotedDataTypeOrConName = customPromote,
defunctionalizedName = customDefun}
$ do decs1 <- genSingletons [''Message]
decs2 <- singletons
[d| hello :: Message
hello = MkMessage "hello" |]
decs3 <- singDecideInstances [''Message]
decs4 <- showSingInstances [''Message]
return $ decs1 ++ decs2 ++ decs3 ++ decs4
======>
type PMkMessageSym0 :: (Data.Singletons.~>) Symbol PMessage
data PMkMessageSym0 :: (Data.Singletons.~>) Symbol PMessage
where
PMkMessageSym0KindInference :: Data.Singletons.SameKind (Data.Singletons.Apply PMkMessageSym0 arg) (PMkMessageSym1 arg) =>
PMkMessageSym0 a0123456789876543210
type instance Data.Singletons.Apply PMkMessageSym0 a0123456789876543210 = 'PMkMessage a0123456789876543210
instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings PMkMessageSym0 where
Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
= snd ((,) PMkMessageSym0KindInference ())
type PMkMessageSym1 :: Symbol -> PMessage
type family PMkMessageSym1 (a0123456789876543210 :: Symbol) :: PMessage where
PMkMessageSym1 a0123456789876543210 = 'PMkMessage a0123456789876543210
type SMessage :: PMessage -> Type
data SMessage :: PMessage -> Type
where
SMkMessage :: forall (n :: Symbol).
(Data.Singletons.Sing n) -> SMessage ('PMkMessage n :: PMessage)
type instance Data.Singletons.Sing @PMessage = SMessage
instance Data.Singletons.SingKind PMessage where
type Data.Singletons.Demote PMessage = Message
Data.Singletons.fromSing (SMkMessage b)
= MkMessage (Data.Singletons.fromSing b)
Data.Singletons.toSing
(MkMessage (b :: Data.Singletons.Demote Symbol))
= case Data.Singletons.toSing b :: Data.Singletons.SomeSing Symbol
of
Data.Singletons.SomeSing c
-> Data.Singletons.SomeSing (SMkMessage c)
instance Data.Singletons.SingI n =>
Data.Singletons.SingI ('PMkMessage (n :: Symbol)) where
Data.Singletons.sing = SMkMessage Data.Singletons.sing
instance Data.Singletons.SingI1 'PMkMessage where
Data.Singletons.liftSing = SMkMessage
instance Data.Singletons.SingI (PMkMessageSym0 :: (Data.Singletons.~>) Symbol PMessage) where
Data.Singletons.sing
= Data.Singletons.singFun1 @PMkMessageSym0 SMkMessage
hello :: Message
hello = MkMessage "hello"
type HelloSym0 :: PMessage
type family HelloSym0 :: PMessage where
HelloSym0 = Hello
type Hello :: PMessage
type family Hello :: PMessage where
Hello = Data.Singletons.Apply PMkMessageSym0 (FromString "hello")
sHello :: (Data.Singletons.Sing (HelloSym0 :: PMessage) :: Type)
sHello
= Data.Singletons.applySing
(Data.Singletons.singFun1 @PMkMessageSym0 SMkMessage)
(sFromString
(Data.Singletons.sing :: Data.Singletons.Sing "hello"))
instance Data.Singletons.Decide.SDecide Text =>
Data.Singletons.Decide.SDecide PMessage where
(Data.Singletons.Decide.%~) (SMkMessage a) (SMkMessage b)
= case (Data.Singletons.Decide.%~) a b of
Data.Singletons.Decide.Proved Data.Type.Equality.Refl
-> Data.Singletons.Decide.Proved Data.Type.Equality.Refl
Data.Singletons.Decide.Disproved contra
-> Data.Singletons.Decide.Disproved
(\ refl
-> case refl of
Data.Type.Equality.Refl -> contra Data.Type.Equality.Refl)
instance Data.Singletons.Decide.SDecide Text =>
Data.Type.Equality.TestEquality (SMessage :: PMessage
-> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance Data.Singletons.Decide.SDecide Text =>
Data.Type.Coercion.TestCoercion (SMessage :: PMessage
-> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
deriving instance Data.Singletons.ShowSing.ShowSing Text =>
Show (SMessage (z :: PMessage))