singletons-base-3.2: 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 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)