T197b.ghc84.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 (:*:@#@$$$) (t :: a0123456789876543210) (t :: b0123456789876543210) =
        (:*:) t t
    instance SuppressUnusedWarnings (:*:@#@$$) where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) (::*:@#@$$###)) GHC.Tuple.())
    data (:*:@#@$$) (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 ((:*:) a0123456789876543210 b0123456789876543210))
      = forall arg. SameKind (Apply ((:*:@#@$$) l) arg) ((:*:@#@$$$) l arg) =>
        (::*:@#@$$###)
    type instance Apply ((:*:@#@$$) l) l = (:*:) l l
    instance SuppressUnusedWarnings (:*:@#@$) where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) (::*:@#@$###)) GHC.Tuple.())
    data (:*:@#@$) (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 ((:*:) a0123456789876543210 b0123456789876543210)
                                                     -> GHC.Types.Type))
      = forall arg. SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) =>
        (::*:@#@$###)
    type instance Apply (:*:@#@$) l = (:*:@#@$$) l
    type MkPairSym2 (t :: a0123456789876543210) (t :: b0123456789876543210) =
        MkPair t t
    instance SuppressUnusedWarnings MkPairSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) MkPairSym1KindInference) GHC.Tuple.())
    data MkPairSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210))
      = forall arg. SameKind (Apply (MkPairSym1 l) arg) (MkPairSym2 l arg) =>
        MkPairSym1KindInference
    type instance Apply (MkPairSym1 l) l = MkPair l l
    instance SuppressUnusedWarnings MkPairSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) MkPairSym0KindInference) GHC.Tuple.())
    data MkPairSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210)
                                                      -> GHC.Types.Type))
      = forall arg. SameKind (Apply MkPairSym0 arg) (MkPairSym1 arg) =>
        MkPairSym0KindInference
    type instance Apply MkPairSym0 l = MkPairSym1 l
    infixr 9 `SMkPair`
    infixr 9 `SPair`
    data instance Sing (z :: (:*:) a b)
      where
        (:%*:) :: forall (n :: a) (n :: b).
                  (Sing (n :: a)) -> (Sing (n :: b)) -> Sing ((:*:) n n)
    type %:*: = (Sing :: (:*:) a b -> GHC.Types.Type)
    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
              (GHC.Tuple.(,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b)
          of {
            GHC.Tuple.(,) (SomeSing c) (SomeSing c)
              -> SomeSing (((:%*:) c) c) }
    data instance Sing (z :: Pair a b)
      where
        SMkPair :: forall (n :: a) (n :: b).
                   (Sing (n :: a)) -> (Sing (n :: b)) -> Sing (MkPair n n)
    type SPair = (Sing :: Pair a b -> GHC.Types.Type)
    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
              (GHC.Tuple.(,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b)
          of {
            GHC.Tuple.(,) (SomeSing c) (SomeSing c)
              -> SomeSing ((SMkPair c) c) }
    instance (SingI n, SingI n) =>
             SingI ((:*:) (n :: a) (n :: b)) where
      sing = ((:%*:) sing) sing
    instance (SingI n, SingI n) =>
             SingI (MkPair (n :: a) (n :: b)) where
      sing = (SMkPair sing) sing