T197b.ghc88.template

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 (:*:@#@$$$) (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) =
        (:*:) t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings ((:*:@#@$$) t0123456789876543210) where
      suppressUnusedWarnings = snd (((,) (::*:@#@$$###)) ())
    data (:*:@#@$$) (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210.
                                                                      (~>) b0123456789876543210 ((:*:) a0123456789876543210 b0123456789876543210)
      where
        (::*:@#@$$###) :: forall t0123456789876543210
                                 t0123456789876543210
                                 arg. SameKind (Apply ((:*:@#@$$) t0123456789876543210) arg) ((:*:@#@$$$) t0123456789876543210 arg) =>
                          (:*:@#@$$) t0123456789876543210 t0123456789876543210
    type instance Apply ((:*:@#@$$) t0123456789876543210) t0123456789876543210 = (:*:) t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (:*:@#@$) where
      suppressUnusedWarnings = snd (((,) (::*:@#@$###)) ())
    data (:*:@#@$) :: forall a0123456789876543210 b0123456789876543210.
                      (~>) a0123456789876543210 ((~>) b0123456789876543210 ((:*:) a0123456789876543210 b0123456789876543210))
      where
        (::*:@#@$###) :: forall t0123456789876543210
                                arg. SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) =>
                         (:*:@#@$) t0123456789876543210
    type instance Apply (:*:@#@$) t0123456789876543210 = (:*:@#@$$) t0123456789876543210
    type MkPairSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) =
        MkPair t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (MkPairSym1 t0123456789876543210) where
      suppressUnusedWarnings = snd (((,) MkPairSym1KindInference) ())
    data MkPairSym1 (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210.
                                                                      (~>) b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210)
      where
        MkPairSym1KindInference :: forall t0123456789876543210
                                          t0123456789876543210
                                          arg. SameKind (Apply (MkPairSym1 t0123456789876543210) arg) (MkPairSym2 t0123456789876543210 arg) =>
                                   MkPairSym1 t0123456789876543210 t0123456789876543210
    type instance Apply (MkPairSym1 t0123456789876543210) t0123456789876543210 = MkPair t0123456789876543210 t0123456789876543210
    infixr 9 `MkPairSym1`
    instance SuppressUnusedWarnings MkPairSym0 where
      suppressUnusedWarnings = snd (((,) MkPairSym0KindInference) ())
    data MkPairSym0 :: forall a0123456789876543210
                              b0123456789876543210.
                       (~>) a0123456789876543210 ((~>) b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210))
      where
        MkPairSym0KindInference :: forall t0123456789876543210
                                          arg. SameKind (Apply MkPairSym0 arg) (MkPairSym1 arg) =>
                                   MkPairSym0 t0123456789876543210
    type instance Apply MkPairSym0 t0123456789876543210 = MkPairSym1 t0123456789876543210
    infixr 9 `MkPairSym0`
    infixr 9 `SMkPair`
    infixr 9 `SPair`
    data (%:*:) :: forall a b. (:*:) a b -> GHC.Types.Type
      where
        (:%*:) :: forall a b (n :: a) (n :: b).
                  (Sing (n :: a)) -> (Sing (n :: b)) -> (%:*:) ((:*:) n n)
    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 :: a)) -> (Sing (n :: b)) -> SPair (MkPair n n)
    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))