packages feed

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))