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