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 (:*:@#@$) 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 ((:*:@#@$$) a0123456789876543210) a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((:*:@#@$$) a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) (::*:@#@$$###)) ())
    type (:*:@#@$$$) :: forall a b. a -> b -> (:*:) a b
    type family (:*:@#@$$$) (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 MkPairSym0 a0123456789876543210 = MkPairSym1 a0123456789876543210
    instance SuppressUnusedWarnings MkPairSym0 where
      suppressUnusedWarnings = snd (((,) MkPairSym0KindInference) ())
    infixr 9 `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 (MkPairSym1 a0123456789876543210) a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MkPairSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) MkPairSym1KindInference) ())
    infixr 9 `MkPairSym1`
    type MkPairSym2 :: forall a b. a -> b -> Pair a b
    type family MkPairSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where
      MkPairSym2 a0123456789876543210 a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210
    infixr 9 `MkPairSym2`
    infixr 9 `SMkPair`
    data (%:*:) :: forall a b. (:*:) a b -> GHC.Types.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))
        = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b) of {
            (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%*:) c) c) }
    data SPair :: forall a b. Pair a b -> GHC.Types.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))
        = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b) of {
            (,) (SomeSing c) (SomeSing c) -> SomeSing ((SMkPair c) c) }
    instance (SingI n, SingI n) =>
             SingI ((:*:) (n :: a) (n :: b)) where
      sing = ((:%*:) sing) sing
    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 (SingI n, SingI n) =>
             SingI (MkPair (n :: a) (n :: b)) where
      sing = (SMkPair sing) sing
    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))