singletons-base-3.0: tests/compile-and-dump/Singletons/T412.golden
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 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 -> GHC.Types.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)
infix 6 `sM1`
instance (SingI n, SingI n) => SingI (MkD1 (n :: a) (n :: b)) where
sing = (SMkD1 sing) sing
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 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))
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 :: GHC.Types.Type -> GHC.Types.Type -> Constraint
class PC2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where
type M2 (arg :: a) (arg :: b) :: Bool
infix 5 `PC2`
infix 6 `M2`
class SC2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where
sM2 ::
forall (t :: a) (t :: b).
Sing t -> Sing t -> Sing (Apply (Apply M2Sym0 t) t :: Bool)
type SC2 :: GHC.Types.Type -> GHC.Types.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))
type T2aSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type)
data T2aSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.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 :: GHC.Types.Type
-> (~>) GHC.Types.Type GHC.Types.Type
data T2aSym1 (a0123456789876543210 :: GHC.Types.Type) :: (~>) GHC.Types.Type GHC.Types.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 :: GHC.Types.Type -> GHC.Types.Type -> GHC.Types.Type
type family T2aSym2 (a0123456789876543210 :: GHC.Types.Type) (a0123456789876543210 :: GHC.Types.Type) :: GHC.Types.Type where
T2aSym2 a0123456789876543210 a0123456789876543210 = T2a a0123456789876543210 a0123456789876543210
infixl 5 `T2aSym2`
type T2bSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type)
data T2bSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.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 :: GHC.Types.Type
-> (~>) GHC.Types.Type GHC.Types.Type
data T2bSym1 (a0123456789876543210 :: GHC.Types.Type) :: (~>) GHC.Types.Type GHC.Types.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 :: GHC.Types.Type -> GHC.Types.Type -> GHC.Types.Type
type family T2bSym2 (a0123456789876543210 :: GHC.Types.Type) (a0123456789876543210 :: GHC.Types.Type) :: GHC.Types.Type where
T2bSym2 a0123456789876543210 a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210
infixl 5 `T2bSym2`
type MkD2Sym0 :: forall (a :: GHC.Types.Type)
(b :: GHC.Types.Type).
(~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)))
data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 :: GHC.Types.Type)
(b :: GHC.Types.Type).
a -> (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))
data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 :: GHC.Types.Type)
(b :: GHC.Types.Type).
a -> b -> D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)
type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where
MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210
infixr 5 `MkD2Sym2`
infixr 5 `D2A`
infixr 5 `D2B`
type D2BSym0 :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
(~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) b
data D2BSym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) -> b
type family D2BSym1 (a0123456789876543210 :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: b where
D2BSym1 a0123456789876543210 = D2B a0123456789876543210
type D2ASym0 :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
(~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) a
data D2ASym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) -> a
type family D2ASym1 (a0123456789876543210 :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: a where
D2ASym1 a0123456789876543210 = D2A a0123456789876543210
type D2B :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) -> b
type family D2B (a :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: b where
D2B ('MkD2 _ field) = field
type D2A :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) -> a
type family D2A (a :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: a where
D2A ('MkD2 field _) = field
sD2B ::
forall (a :: GHC.Types.Type)
(b :: GHC.Types.Type)
(t :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)).
Sing t -> Sing (Apply D2BSym0 t :: b)
sD2A ::
forall (a :: GHC.Types.Type)
(b :: GHC.Types.Type)
(t :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 :: GHC.Types.Type) (b :: GHC.Types.Type)) b) where
sing = (singFun1 @D2BSym0) sD2B
instance SingI (D2ASym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) a) where
sing = (singFun1 @D2ASym0) sD2A
type SD2 :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 a b -> GHC.Types.Type
data SD2 :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type).
D2 a b -> GHC.Types.Type
where
SMkD2 :: forall (a :: GHC.Types.Type)
(b :: GHC.Types.Type)
(n :: a)
(n :: b).
(Sing n)
-> (Sing n)
-> SD2 ('MkD2 n n :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.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 (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)))) where
sing = (singFun2 @MkD2Sym0) SMkD2
instance SingI d =>
SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))) where
sing = (singFun1 @(MkD2Sym1 (d :: a))) (SMkD2 (sing @d))