T197b.golden

Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| infixr 9 `Pair`, `MkPair`
          
          data a :*: b = a :*: b
          data Pair a b = MkPair a b |]
  ======>
    data (:*:) a b = a :*: b
    data Pair a b = MkPair a b
    infixr 9 `Pair`
    infixr 9 `MkPair`
    type (:*:@#@$) :: forall a b. (~>) a ((~>) b ((:*:) a b))
    data (:*:@#@$) :: (~>) a ((~>) b ((:*:) a b))
      where
        (::*:@#@$###) :: SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) =>
                         (:*:@#@$) a0123456789876543210
    type instance Apply @a @((~>) b ((:*:) a b)) (:*:@#@$) a0123456789876543210 = (:*:@#@$$) a0123456789876543210
    instance SuppressUnusedWarnings (:*:@#@$) where
      suppressUnusedWarnings = snd ((,) (::*:@#@$###) ())
    type (:*:@#@$$) :: forall a b. a -> (~>) b ((:*:) a b)
    data (:*:@#@$$) (a0123456789876543210 :: a) :: (~>) b ((:*:) a b)
      where
        (::*:@#@$$###) :: SameKind (Apply ((:*:@#@$$) a0123456789876543210) arg) ((:*:@#@$$$) a0123456789876543210 arg) =>
                          (:*:@#@$$) a0123456789876543210 a0123456789876543210
    type instance Apply @b @((:*:) a b) ((:*:@#@$$) a0123456789876543210) a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((:*:@#@$$) a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ())
    type (:*:@#@$$$) :: forall a b. a -> b -> (:*:) a b
    type family (:*:@#@$$$) @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (:*:) a b where
      (:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
    type MkPairSym0 :: forall a b. (~>) a ((~>) b (Pair a b))
    data MkPairSym0 :: (~>) a ((~>) b (Pair a b))
      where
        MkPairSym0KindInference :: SameKind (Apply MkPairSym0 arg) (MkPairSym1 arg) =>
                                   MkPairSym0 a0123456789876543210
    type instance Apply @a @((~>) b (Pair a b)) MkPairSym0 a0123456789876543210 = MkPairSym1 a0123456789876543210
    instance SuppressUnusedWarnings MkPairSym0 where
      suppressUnusedWarnings = snd ((,) MkPairSym0KindInference ())
    infixr 9 type `MkPairSym0`
    type MkPairSym1 :: forall a b. a -> (~>) b (Pair a b)
    data MkPairSym1 (a0123456789876543210 :: a) :: (~>) b (Pair a b)
      where
        MkPairSym1KindInference :: SameKind (Apply (MkPairSym1 a0123456789876543210) arg) (MkPairSym2 a0123456789876543210 arg) =>
                                   MkPairSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @b @(Pair a b) (MkPairSym1 a0123456789876543210) a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MkPairSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MkPairSym1KindInference ())
    infixr 9 type `MkPairSym1`
    type MkPairSym2 :: forall a b. a -> b -> Pair a b
    type family MkPairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where
      MkPairSym2 a0123456789876543210 a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210
    infixr 9 type `MkPairSym2`
    infixr 9 data `SMkPair`
    data (%:*:) :: forall a b. (:*:) a b -> Type
      where
        (:%*:) :: forall a b (n :: a) (n :: b).
                  (Sing n) -> (Sing n) -> (%:*:) ((:*:) n n :: (:*:) a b)
    type instance Sing @((:*:) a b) = (%:*:)
    instance (SingKind a, SingKind b) => SingKind ((:*:) a b) where
      type Demote ((:*:) a b) = (:*:) (Demote a) (Demote b)
      fromSing ((:%*:) b b) = (:*:) (fromSing b) (fromSing b)
      toSing ((:*:) (b :: Demote a) (b :: Demote b))
        = (\cases (SomeSing c) (SomeSing c) -> SomeSing ((:%*:) c c))
            (toSing b :: SomeSing a) (toSing b :: SomeSing b)
    data SPair :: forall a b. Pair a b -> Type
      where
        SMkPair :: forall a b (n :: a) (n :: b).
                   (Sing n) -> (Sing n) -> SPair (MkPair 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 (SMkPair b b) = MkPair (fromSing b) (fromSing b)
      toSing (MkPair (b :: Demote a) (b :: Demote b))
        = (\cases (SomeSing c) (SomeSing c) -> SomeSing (SMkPair c c))
            (toSing b :: SomeSing a) (toSing b :: SomeSing b)
    instance (SingI n, SingI n) =>
             SingI ((:*:) (n :: a) (n :: b)) where
      sing = (:%*:) sing sing
    instance SingI n => SingI1 ((:*:) (n :: a)) where
      liftSing = (:%*:) sing
    instance SingI2 (:*:) where
      liftSing2 = (:%*:)
    instance SingI ((:*:@#@$) :: (~>) a ((~>) b ((:*:) a b))) where
      sing = singFun2 @(:*:@#@$) (:%*:)
    instance SingI d =>
             SingI ((:*:@#@$$) (d :: a) :: (~>) b ((:*:) a b)) where
      sing = singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) (sing @d))
    instance SingI1 ((:*:@#@$$) :: a -> (~>) b ((:*:) a b)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) s)
    instance (SingI n, SingI n) =>
             SingI (MkPair (n :: a) (n :: b)) where
      sing = SMkPair sing sing
    instance SingI n => SingI1 (MkPair (n :: a)) where
      liftSing = SMkPair sing
    instance SingI2 MkPair where
      liftSing2 = SMkPair
    instance SingI (MkPairSym0 :: (~>) a ((~>) b (Pair a b))) where
      sing = singFun2 @MkPairSym0 SMkPair
    instance SingI d =>
             SingI (MkPairSym1 (d :: a) :: (~>) b (Pair a b)) where
      sing = singFun1 @(MkPairSym1 (d :: a)) (SMkPair (sing @d))
    instance SingI1 (MkPairSym1 :: a -> (~>) b (Pair a b)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(MkPairSym1 (d :: a)) (SMkPair s)