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 `SPair` infixr 9 `SMkPair` data instance Sing :: (:*:) a b -> GHC.Types.Type where (:%*:) :: forall a b (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 ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b) of { (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%*:) c) c) } data instance Sing :: Pair a b -> GHC.Types.Type where SMkPair :: forall a b (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 ((,) (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 (TyCon2 (:*:) :: (~>) a ((~>) b ((:*:) a b))) where sing = (singFun2 @(TyCon2 (:*:))) (:%*:) instance SingI d => SingI ((:*:@#@$$) (d :: a) :: (~>) b ((:*:) a b)) where sing = (singFun1 @((:*:@#@$$) (d :: a))) ((:%*:) (sing @d)) instance SingI d => SingI (TyCon1 ((:*:) (d :: a)) :: (~>) b ((:*:) a b)) where sing = (singFun1 @(TyCon1 ((:*:) (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 (TyCon2 MkPair :: (~>) a ((~>) b (Pair a b))) where sing = (singFun2 @(TyCon2 MkPair)) SMkPair instance SingI d => SingI (MkPairSym1 (d :: a) :: (~>) b (Pair a b)) where sing = (singFun1 @(MkPairSym1 (d :: a))) (SMkPair (sing @d)) instance SingI d => SingI (TyCon1 (MkPair (d :: a)) :: (~>) b (Pair a b)) where sing = (singFun1 @(TyCon1 (MkPair (d :: a)))) (SMkPair (sing @d))