DataValues.golden

Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| pr = Pair (Succ Zero) ([Zero])
          complex = Pair (Pair (Just Zero) Zero) False
          tuple = (False, Just Zero, True)
          aList = [Zero, Succ Zero, Succ (Succ Zero)]
          
          data Pair a b
            = Pair a b
            deriving Show |]
  ======>
    data Pair a b
      = Pair a b
      deriving Show
    pr = Pair (Succ Zero) [Zero]
    complex = Pair (Pair (Just Zero) Zero) False
    tuple = (False, Just Zero, True)
    aList = [Zero, Succ Zero, Succ (Succ Zero)]
    type PairSym0 :: forall a b. (~>) a ((~>) b (Pair a b))
    data PairSym0 :: (~>) a ((~>) b (Pair a b))
      where
        PairSym0KindInference :: SameKind (Apply PairSym0 arg) (PairSym1 arg) =>
                                 PairSym0 a0123456789876543210
    type instance Apply @a @((~>) b (Pair a b)) PairSym0 a0123456789876543210 = PairSym1 a0123456789876543210
    instance SuppressUnusedWarnings PairSym0 where
      suppressUnusedWarnings = snd ((,) PairSym0KindInference ())
    type PairSym1 :: forall a b. a -> (~>) b (Pair a b)
    data PairSym1 (a0123456789876543210 :: a) :: (~>) b (Pair a b)
      where
        PairSym1KindInference :: SameKind (Apply (PairSym1 a0123456789876543210) arg) (PairSym2 a0123456789876543210 arg) =>
                                 PairSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @b @(Pair a b) (PairSym1 a0123456789876543210) a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (PairSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) PairSym1KindInference ())
    type PairSym2 :: forall a b. a -> b -> Pair a b
    type family PairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where
      PairSym2 a0123456789876543210 a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
    type family AListSym0 where
      AListSym0 = AList
    type family TupleSym0 where
      TupleSym0 = Tuple
    type family ComplexSym0 where
      ComplexSym0 = Complex
    type family PrSym0 where
      PrSym0 = Pr
    type family AList where
      AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
    type family Tuple where
      Tuple = Apply (Apply (Apply Tuple3Sym0 FalseSym0) (Apply JustSym0 ZeroSym0)) TrueSym0
    type family Complex where
      Complex = Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
    type family Pr where
      Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0)
    type ShowsPrec_0123456789876543210 :: forall a
                                                 b. GHC.Num.Natural.Natural
                                                    -> Pair a b -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210 @a @b (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210 @a @b (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Pair arg_0123456789876543210 arg_0123456789876543210 :: Pair a b) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
    instance PShow (Pair a b) where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    sAList :: Sing @_ AList
    sTuple :: Sing @_ Tuple
    sComplex :: Sing @_ Complex
    sPr :: Sing @_ Pr
    sAList
      = applySing
          (applySing (singFun2 @(:@#@$) SCons) SZero)
          (applySing
             (applySing
                (singFun2 @(:@#@$) SCons)
                (applySing (singFun1 @SuccSym0 SSucc) SZero))
             (applySing
                (applySing
                   (singFun2 @(:@#@$) SCons)
                   (applySing
                      (singFun1 @SuccSym0 SSucc)
                      (applySing (singFun1 @SuccSym0 SSucc) SZero)))
                SNil))
    sTuple
      = applySing
          (applySing
             (applySing (singFun3 @Tuple3Sym0 STuple3) SFalse)
             (applySing (singFun1 @JustSym0 SJust) SZero))
          STrue
    sComplex
      = applySing
          (applySing
             (singFun2 @PairSym0 SPair)
             (applySing
                (applySing
                   (singFun2 @PairSym0 SPair)
                   (applySing (singFun1 @JustSym0 SJust) SZero))
                SZero))
          SFalse
    sPr
      = applySing
          (applySing
             (singFun2 @PairSym0 SPair)
             (applySing (singFun1 @SuccSym0 SSucc) SZero))
          (applySing (applySing (singFun2 @(:@#@$) SCons) SZero) SNil)
    data SPair :: forall a b. Pair a b -> Type
      where
        SPair :: forall a b (n :: a) (n :: b).
                 (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b)
    type instance Sing @(Pair a b) = SPair
    instance (SingKind a, SingKind b) => SingKind (Pair a b) where
      type Demote (Pair a b) = Pair (Demote a) (Demote b)
      fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
      toSing (Pair (b :: Demote a) (b :: Demote b))
        = (\cases (SomeSing c) (SomeSing c) -> SomeSing (SPair c c))
            (toSing b :: SomeSing a) (toSing b :: SomeSing b)
    instance (SShow a, SShow b) => SShow (Pair a b) where
      sShowsPrec
        (sP_0123456789876543210 :: Sing p_0123456789876543210)
        (SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
               (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (applySing
                  (singFun3 @ShowParenSym0 sShowParen)
                  (applySing
                     (applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
                     (sFromInteger (sing :: Sing 10))))
               (applySing
                  (applySing
                     (singFun3 @(.@#@$) (%.))
                     (applySing
                        (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Pair ")))
                  (applySing
                     (applySing
                        (singFun3 @(.@#@$) (%.))
                        (applySing
                           (applySing
                              (singFun3 @ShowsPrecSym0 sShowsPrec)
                              (sFromInteger (sing :: Sing 11)))
                           sArg_0123456789876543210))
                     (applySing
                        (applySing
                           (singFun3 @(.@#@$) (%.)) (singFun1 @ShowSpaceSym0 sShowSpace))
                        (applySing
                           (applySing
                              (singFun3 @ShowsPrecSym0 sShowsPrec)
                              (sFromInteger (sing :: Sing 11)))
                           sArg_0123456789876543210)))))
            sA_0123456789876543210
    deriving instance (Data.Singletons.ShowSing.ShowSing a,
                       Data.Singletons.ShowSing.ShowSing b) =>
                      Show (SPair (z :: Pair a b))
    instance (SingI n, SingI n) => SingI (Pair (n :: a) (n :: b)) where
      sing = SPair sing sing
    instance SingI n => SingI1 (Pair (n :: a)) where
      liftSing = SPair sing
    instance SingI2 Pair where
      liftSing2 = SPair
    instance SingI (PairSym0 :: (~>) a ((~>) b (Pair a b))) where
      sing = singFun2 @PairSym0 SPair
    instance SingI d =>
             SingI (PairSym1 (d :: a) :: (~>) b (Pair a b)) where
      sing = singFun1 @(PairSym1 (d :: a)) (SPair (sing @d))
    instance SingI1 (PairSym1 :: a -> (~>) b (Pair a b)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(PairSym1 (d :: a)) (SPair s)