Singletons/T412.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| infixr 5 `D1`, `MkD1`, `d1A`, `d1B`
          infixl 5 `T1a`, `T1b`
          infix 5 `C1`
          
          class C1 a b where
            infix 6 `m1`
            m1 :: a -> b -> Bool
          type T1a a b = Either a b
          type family T1b a b where
            T1b a b = Either a b
          data D1 a b = MkD1 {d1A :: a, d1B :: b} |]
  ======>
    infix 5 `C1`
    class C1 a b where
      infix 6 `m1`
      m1 :: a -> b -> Bool
    infixl 5 `T1a`
    infixl 5 `T1b`
    type T1a a b = Either a b
    type family T1b a b where
      T1b a b = Either a b
    infixr 5 `D1`
    infixr 5 `MkD1`
    infixr 5 `d1A`
    infixr 5 `d1B`
    data D1 a b = MkD1 {d1A :: a, d1B :: b}
    data T1aSym0 a0123456789876543210
      where
        T1aSym0KindInference :: SameKind (Apply T1aSym0 arg) (T1aSym1 arg) =>
                                T1aSym0 a0123456789876543210
    type instance Apply T1aSym0 a0123456789876543210 = T1aSym1 a0123456789876543210
    instance SuppressUnusedWarnings T1aSym0 where
      suppressUnusedWarnings = snd ((,) T1aSym0KindInference ())
    infixl 5 `T1aSym0`
    data T1aSym1 a0123456789876543210 b0123456789876543210
      where
        T1aSym1KindInference :: SameKind (Apply (T1aSym1 a0123456789876543210) arg) (T1aSym2 a0123456789876543210 arg) =>
                                T1aSym1 a0123456789876543210 b0123456789876543210
    type instance Apply (T1aSym1 a0123456789876543210) b0123456789876543210 = T1a a0123456789876543210 b0123456789876543210
    instance SuppressUnusedWarnings (T1aSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) T1aSym1KindInference ())
    infixl 5 `T1aSym1`
    type family T1aSym2 a0123456789876543210 b0123456789876543210 where
      T1aSym2 a0123456789876543210 b0123456789876543210 = T1a a0123456789876543210 b0123456789876543210
    infixl 5 `T1aSym2`
    data T1bSym0 a0123456789876543210
      where
        T1bSym0KindInference :: SameKind (Apply T1bSym0 arg) (T1bSym1 arg) =>
                                T1bSym0 a0123456789876543210
    type instance Apply T1bSym0 a0123456789876543210 = T1bSym1 a0123456789876543210
    instance SuppressUnusedWarnings T1bSym0 where
      suppressUnusedWarnings = snd ((,) T1bSym0KindInference ())
    infixl 5 `T1bSym0`
    data T1bSym1 a0123456789876543210 b0123456789876543210
      where
        T1bSym1KindInference :: SameKind (Apply (T1bSym1 a0123456789876543210) arg) (T1bSym2 a0123456789876543210 arg) =>
                                T1bSym1 a0123456789876543210 b0123456789876543210
    type instance Apply (T1bSym1 a0123456789876543210) b0123456789876543210 = T1b a0123456789876543210 b0123456789876543210
    instance SuppressUnusedWarnings (T1bSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) T1bSym1KindInference ())
    infixl 5 `T1bSym1`
    type family T1bSym2 a0123456789876543210 b0123456789876543210 where
      T1bSym2 a0123456789876543210 b0123456789876543210 = T1b a0123456789876543210 b0123456789876543210
    infixl 5 `T1bSym2`
    type MkD1Sym0 :: forall a b. (~>) a ((~>) b (D1 a b))
    data MkD1Sym0 :: (~>) a ((~>) b (D1 a b))
      where
        MkD1Sym0KindInference :: SameKind (Apply MkD1Sym0 arg) (MkD1Sym1 arg) =>
                                 MkD1Sym0 a0123456789876543210
    type instance Apply MkD1Sym0 a0123456789876543210 = MkD1Sym1 a0123456789876543210
    instance SuppressUnusedWarnings MkD1Sym0 where
      suppressUnusedWarnings = snd ((,) MkD1Sym0KindInference ())
    infixr 5 `MkD1Sym0`
    type MkD1Sym1 :: forall a b. a -> (~>) b (D1 a b)
    data MkD1Sym1 (a0123456789876543210 :: a) :: (~>) b (D1 a b)
      where
        MkD1Sym1KindInference :: SameKind (Apply (MkD1Sym1 a0123456789876543210) arg) (MkD1Sym2 a0123456789876543210 arg) =>
                                 MkD1Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (MkD1Sym1 a0123456789876543210) a0123456789876543210 = MkD1 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MkD1Sym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MkD1Sym1KindInference ())
    infixr 5 `MkD1Sym1`
    type MkD1Sym2 :: forall a b. a -> b -> D1 a b
    type family MkD1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D1 a b where
      MkD1Sym2 a0123456789876543210 a0123456789876543210 = MkD1 a0123456789876543210 a0123456789876543210
    infixr 5 `MkD1Sym2`
    type D1BSym0 :: forall a b. (~>) (D1 a b) b
    data D1BSym0 :: (~>) (D1 a b) b
      where
        D1BSym0KindInference :: SameKind (Apply D1BSym0 arg) (D1BSym1 arg) =>
                                D1BSym0 a0123456789876543210
    type instance Apply D1BSym0 a0123456789876543210 = D1B a0123456789876543210
    instance SuppressUnusedWarnings D1BSym0 where
      suppressUnusedWarnings = snd ((,) D1BSym0KindInference ())
    infixr 5 `D1BSym0`
    type D1BSym1 :: forall a b. D1 a b -> b
    type family D1BSym1 (a0123456789876543210 :: D1 a b) :: b where
      D1BSym1 a0123456789876543210 = D1B a0123456789876543210
    infixr 5 `D1BSym1`
    type D1ASym0 :: forall a b. (~>) (D1 a b) a
    data D1ASym0 :: (~>) (D1 a b) a
      where
        D1ASym0KindInference :: SameKind (Apply D1ASym0 arg) (D1ASym1 arg) =>
                                D1ASym0 a0123456789876543210
    type instance Apply D1ASym0 a0123456789876543210 = D1A a0123456789876543210
    instance SuppressUnusedWarnings D1ASym0 where
      suppressUnusedWarnings = snd ((,) D1ASym0KindInference ())
    infixr 5 `D1ASym0`
    type D1ASym1 :: forall a b. D1 a b -> a
    type family D1ASym1 (a0123456789876543210 :: D1 a b) :: a where
      D1ASym1 a0123456789876543210 = D1A a0123456789876543210
    infixr 5 `D1ASym1`
    type D1B :: forall a b. D1 a b -> b
    type family D1B (a :: D1 a b) :: b where
      D1B (MkD1 _ field) = field
    type D1A :: forall a b. D1 a b -> a
    type family D1A (a :: D1 a b) :: a where
      D1A (MkD1 field _) = field
    infixr 5 `D1B`
    infixr 5 `D1A`
    infix 5 `PC1`
    type M1Sym0 :: forall a b. (~>) a ((~>) b Bool)
    data M1Sym0 :: (~>) a ((~>) b Bool)
      where
        M1Sym0KindInference :: SameKind (Apply M1Sym0 arg) (M1Sym1 arg) =>
                               M1Sym0 a0123456789876543210
    type instance Apply M1Sym0 a0123456789876543210 = M1Sym1 a0123456789876543210
    instance SuppressUnusedWarnings M1Sym0 where
      suppressUnusedWarnings = snd ((,) M1Sym0KindInference ())
    infix 6 `M1Sym0`
    type M1Sym1 :: forall a b. a -> (~>) b Bool
    data M1Sym1 (a0123456789876543210 :: a) :: (~>) b Bool
      where
        M1Sym1KindInference :: SameKind (Apply (M1Sym1 a0123456789876543210) arg) (M1Sym2 a0123456789876543210 arg) =>
                               M1Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (M1Sym1 a0123456789876543210) a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (M1Sym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) M1Sym1KindInference ())
    infix 6 `M1Sym1`
    type M1Sym2 :: forall a b. a -> b -> Bool
    type family M1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where
      M1Sym2 a0123456789876543210 a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210
    infix 6 `M1Sym2`
    class PC1 a b where
      type family M1 (arg :: a) (arg :: b) :: Bool
      infix 6 `M1`
    infixr 5 `sD1B`
    infixr 5 `sD1A`
    infixr 5 `SMkD1`
    infix 5 `SC1`
    sD1B ::
      forall a b (t :: D1 a b). Sing t -> Sing (Apply D1BSym0 t :: b)
    sD1A ::
      forall a b (t :: D1 a b). Sing t -> Sing (Apply D1ASym0 t :: a)
    sD1B (SMkD1 _ (sField :: Sing field)) = sField
    sD1A (SMkD1 (sField :: Sing field) _) = sField
    instance SingI (D1BSym0 :: (~>) (D1 a b) b) where
      sing = singFun1 @D1BSym0 sD1B
    instance SingI (D1ASym0 :: (~>) (D1 a b) a) where
      sing = singFun1 @D1ASym0 sD1A
    data SD1 :: forall a b. D1 a b -> Type
      where
        SMkD1 :: forall a b (n :: a) (n :: b).
                 (Sing n) -> (Sing n) -> SD1 (MkD1 n n :: D1 a b)
    type instance Sing @(D1 a b) = SD1
    instance (SingKind a, SingKind b) => SingKind (D1 a b) where
      type Demote (D1 a b) = D1 (Demote a) (Demote b)
      fromSing (SMkD1 b b) = MkD1 (fromSing b) (fromSing b)
      toSing (MkD1 (b :: Demote a) (b :: Demote b))
        = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of
            (,) (SomeSing c) (SomeSing c) -> SomeSing (SMkD1 c c)
    class SC1 a b where
      sM1 ::
        (forall (t :: a) (t :: b).
         Sing t
         -> Sing t -> Sing (Apply (Apply M1Sym0 t) t :: Bool) :: Type)
      infix 6 `sM1`
    instance (SingI n, SingI n) => SingI (MkD1 (n :: a) (n :: b)) where
      sing = SMkD1 sing sing
    instance SingI n => SingI1 (MkD1 (n :: a)) where
      liftSing = SMkD1 sing
    instance SingI2 MkD1 where
      liftSing2 = SMkD1
    instance SingI (MkD1Sym0 :: (~>) a ((~>) b (D1 a b))) where
      sing = singFun2 @MkD1Sym0 SMkD1
    instance SingI d =>
             SingI (MkD1Sym1 (d :: a) :: (~>) b (D1 a b)) where
      sing = singFun1 @(MkD1Sym1 (d :: a)) (SMkD1 (sing @d))
    instance SingI1 (MkD1Sym1 :: a -> (~>) b (D1 a b)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(MkD1Sym1 (d :: a)) (SMkD1 s)
    instance SC1 a b => SingI (M1Sym0 :: (~>) a ((~>) b Bool)) where
      sing = singFun2 @M1Sym0 sM1
    instance (SC1 a b, SingI d) =>
             SingI (M1Sym1 (d :: a) :: (~>) b Bool) where
      sing = singFun1 @(M1Sym1 (d :: a)) (sM1 (sing @d))
    instance SC1 a b => SingI1 (M1Sym1 :: a -> (~>) b Bool) where
      liftSing (s :: Sing (d :: a)) = singFun1 @(M1Sym1 (d :: a)) (sM1 s)
Singletons/T412.hs:0:0:: Splicing declarations
    genSingletons [''C2, ''T2a, ''T2b, ''D2]
  ======>
    type M2Sym0 :: forall a b. (~>) a ((~>) b Bool)
    data M2Sym0 :: (~>) a ((~>) b Bool)
      where
        M2Sym0KindInference :: SameKind (Apply M2Sym0 arg) (M2Sym1 arg) =>
                               M2Sym0 a0123456789876543210
    type instance Apply M2Sym0 a0123456789876543210 = M2Sym1 a0123456789876543210
    instance SuppressUnusedWarnings M2Sym0 where
      suppressUnusedWarnings = snd ((,) M2Sym0KindInference ())
    infix 6 `M2Sym0`
    type M2Sym1 :: forall a b. a -> (~>) b Bool
    data M2Sym1 (a0123456789876543210 :: a) :: (~>) b Bool
      where
        M2Sym1KindInference :: SameKind (Apply (M2Sym1 a0123456789876543210) arg) (M2Sym2 a0123456789876543210 arg) =>
                               M2Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (M2Sym1 a0123456789876543210) a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (M2Sym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) M2Sym1KindInference ())
    infix 6 `M2Sym1`
    type M2Sym2 :: forall a b. a -> b -> Bool
    type family M2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where
      M2Sym2 a0123456789876543210 a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210
    infix 6 `M2Sym2`
    type PC2 :: Type -> Type -> Constraint
    class PC2 (a :: Type) (b :: Type) where
      type family M2 (arg :: a) (arg :: b) :: Bool
    infix 5 `PC2`
    infix 6 `M2`
    class SC2 (a :: Type) (b :: Type) where
      sM2 ::
        (forall (t :: a) (t :: b).
         Sing t
         -> Sing t -> Sing (Apply (Apply M2Sym0 t) t :: Bool) :: Type)
    type SC2 :: Type -> Type -> Constraint
    infix 5 `SC2`
    infix 6 `sM2`
    instance SC2 a b => SingI (M2Sym0 :: (~>) a ((~>) b Bool)) where
      sing = singFun2 @M2Sym0 sM2
    instance (SC2 a b, SingI d) =>
             SingI (M2Sym1 (d :: a) :: (~>) b Bool) where
      sing = singFun1 @(M2Sym1 (d :: a)) (sM2 (sing @d))
    instance SC2 a b => SingI1 (M2Sym1 :: a -> (~>) b Bool) where
      liftSing (s :: Sing (d :: a)) = singFun1 @(M2Sym1 (d :: a)) (sM2 s)
    type T2aSym0 :: (~>) Type ((~>) Type Type)
    data T2aSym0 :: (~>) Type ((~>) Type Type)
      where
        T2aSym0KindInference :: SameKind (Apply T2aSym0 arg) (T2aSym1 arg) =>
                                T2aSym0 a0123456789876543210
    type instance Apply T2aSym0 a0123456789876543210 = T2aSym1 a0123456789876543210
    instance SuppressUnusedWarnings T2aSym0 where
      suppressUnusedWarnings = snd ((,) T2aSym0KindInference ())
    infixl 5 `T2aSym0`
    type T2aSym1 :: Type -> (~>) Type Type
    data T2aSym1 (a0123456789876543210 :: Type) :: (~>) Type Type
      where
        T2aSym1KindInference :: SameKind (Apply (T2aSym1 a0123456789876543210) arg) (T2aSym2 a0123456789876543210 arg) =>
                                T2aSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (T2aSym1 a0123456789876543210) a0123456789876543210 = T2a a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (T2aSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) T2aSym1KindInference ())
    infixl 5 `T2aSym1`
    type T2aSym2 :: Type -> Type -> Type
    type family T2aSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Type where
      T2aSym2 a0123456789876543210 a0123456789876543210 = T2a a0123456789876543210 a0123456789876543210
    infixl 5 `T2aSym2`
    type T2bSym0 :: (~>) Type ((~>) Type Type)
    data T2bSym0 :: (~>) Type ((~>) Type Type)
      where
        T2bSym0KindInference :: SameKind (Apply T2bSym0 arg) (T2bSym1 arg) =>
                                T2bSym0 a0123456789876543210
    type instance Apply T2bSym0 a0123456789876543210 = T2bSym1 a0123456789876543210
    instance SuppressUnusedWarnings T2bSym0 where
      suppressUnusedWarnings = snd ((,) T2bSym0KindInference ())
    infixl 5 `T2bSym0`
    type T2bSym1 :: Type -> (~>) Type Type
    data T2bSym1 (a0123456789876543210 :: Type) :: (~>) Type Type
      where
        T2bSym1KindInference :: SameKind (Apply (T2bSym1 a0123456789876543210) arg) (T2bSym2 a0123456789876543210 arg) =>
                                T2bSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (T2bSym1 a0123456789876543210) a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (T2bSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) T2bSym1KindInference ())
    infixl 5 `T2bSym1`
    type T2bSym2 :: Type -> Type -> Type
    type family T2bSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Type where
      T2bSym2 a0123456789876543210 a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210
    infixl 5 `T2bSym2`
    type MkD2Sym0 :: forall (a :: Type)
                            (b :: Type). (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))
    data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))
      where
        MkD2Sym0KindInference :: SameKind (Apply MkD2Sym0 arg) (MkD2Sym1 arg) =>
                                 MkD2Sym0 a0123456789876543210
    type instance Apply MkD2Sym0 a0123456789876543210 = MkD2Sym1 a0123456789876543210
    instance SuppressUnusedWarnings MkD2Sym0 where
      suppressUnusedWarnings = snd ((,) MkD2Sym0KindInference ())
    infixr 5 `MkD2Sym0`
    type MkD2Sym1 :: forall (a :: Type) (b :: Type). a
                                                     -> (~>) b (D2 (a :: Type) (b :: Type))
    data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: Type) (b :: Type))
      where
        MkD2Sym1KindInference :: SameKind (Apply (MkD2Sym1 a0123456789876543210) arg) (MkD2Sym2 a0123456789876543210 arg) =>
                                 MkD2Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (MkD2Sym1 a0123456789876543210) a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MkD2Sym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MkD2Sym1KindInference ())
    infixr 5 `MkD2Sym1`
    type MkD2Sym2 :: forall (a :: Type) (b :: Type). a
                                                     -> b -> D2 (a :: Type) (b :: Type)
    type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 (a :: Type) (b :: Type) where
      MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210
    infixr 5 `MkD2Sym2`
    infixr 5 `D2A`
    infixr 5 `D2B`
    type D2BSym0 :: forall (a :: Type)
                           (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) b
    data D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b
      where
        D2BSym0KindInference :: SameKind (Apply D2BSym0 arg) (D2BSym1 arg) =>
                                D2BSym0 a0123456789876543210
    type instance Apply D2BSym0 a0123456789876543210 = D2B a0123456789876543210
    instance SuppressUnusedWarnings D2BSym0 where
      suppressUnusedWarnings = snd ((,) D2BSym0KindInference ())
    type D2BSym1 :: forall (a :: Type)
                           (b :: Type). D2 (a :: Type) (b :: Type) -> b
    type family D2BSym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: b where
      D2BSym1 a0123456789876543210 = D2B a0123456789876543210
    type D2ASym0 :: forall (a :: Type)
                           (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) a
    data D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a
      where
        D2ASym0KindInference :: SameKind (Apply D2ASym0 arg) (D2ASym1 arg) =>
                                D2ASym0 a0123456789876543210
    type instance Apply D2ASym0 a0123456789876543210 = D2A a0123456789876543210
    instance SuppressUnusedWarnings D2ASym0 where
      suppressUnusedWarnings = snd ((,) D2ASym0KindInference ())
    type D2ASym1 :: forall (a :: Type)
                           (b :: Type). D2 (a :: Type) (b :: Type) -> a
    type family D2ASym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: a where
      D2ASym1 a0123456789876543210 = D2A a0123456789876543210
    type D2B :: forall (a :: Type)
                       (b :: Type). D2 (a :: Type) (b :: Type) -> b
    type family D2B (a :: D2 (a :: Type) (b :: Type)) :: b where
      D2B ('MkD2 _ field) = field
    type D2A :: forall (a :: Type)
                       (b :: Type). D2 (a :: Type) (b :: Type) -> a
    type family D2A (a :: D2 (a :: Type) (b :: Type)) :: a where
      D2A ('MkD2 field _) = field
    sD2B ::
      forall (a :: Type)
             (b :: Type)
             (t :: D2 (a :: Type) (b :: Type)). Sing t
                                                -> Sing (Apply D2BSym0 t :: b)
    sD2A ::
      forall (a :: Type)
             (b :: Type)
             (t :: D2 (a :: Type) (b :: Type)). Sing t
                                                -> Sing (Apply D2ASym0 t :: a)
    sD2B (SMkD2 _ (sField :: Sing field)) = sField
    sD2A (SMkD2 (sField :: Sing field) _) = sField
    instance SingI (D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b) where
      sing = singFun1 @D2BSym0 sD2B
    instance SingI (D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a) where
      sing = singFun1 @D2ASym0 sD2A
    type SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type
    data SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type
      where
        SMkD2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b).
                 (Sing n) ->
                 (Sing n) ->
                 SD2 ('MkD2 n n :: D2 (a :: Type) (b :: Type))
    type instance Sing @(D2 a b) = SD2
    instance (SingKind a, SingKind b) => SingKind (D2 a b) where
      type Demote (D2 a b) = D2 (Demote a) (Demote b)
      fromSing (SMkD2 b b) = MkD2 (fromSing b) (fromSing b)
      toSing (MkD2 (b :: Demote a) (b :: Demote b))
        = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of
            (,) (SomeSing c) (SomeSing c) -> SomeSing (SMkD2 c c)
    infixr 5 `SMkD2`
    infixr 5 `sD2A`
    infixr 5 `sD2B`
    instance (SingI n, SingI n) =>
             SingI ('MkD2 (n :: a) (n :: b)) where
      sing = SMkD2 sing sing
    instance SingI n => SingI1 ('MkD2 (n :: a)) where
      liftSing = SMkD2 sing
    instance SingI2 'MkD2 where
      liftSing2 = SMkD2
    instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))) where
      sing = singFun2 @MkD2Sym0 SMkD2
    instance SingI d =>
             SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: Type) (b :: Type))) where
      sing = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 (sing @d))
    instance SingI1 (MkD2Sym1 :: a
                                 -> (~>) b (D2 (a :: Type) (b :: Type))) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 s)