singletons-base-3.3: tests/compile-and-dump/Singletons/T353.golden
Singletons/T353.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| type family Symmetry (a :: Proxy t) (y :: Proxy t) (e :: (a :: Proxy (t :: k))
:~:
(y :: Proxy (t :: k))) :: Type where
Symmetry a y _ = y :~: a |]
======>
type family Symmetry (a :: Proxy t) (y :: Proxy t) (e :: (:~:) (a :: Proxy (t :: k)) (y :: Proxy (t :: k))) :: Type where
Symmetry a y _ = (:~:) y a
data SymmetrySym0 :: (~>) (Proxy t0123456789876543210) ((~>) (Proxy t0123456789876543210) ((~>) ((:~:) (a0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210)) (y0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210))) Type))
where
SymmetrySym0KindInference :: SameKind (Apply SymmetrySym0 arg) (SymmetrySym1 arg) =>
SymmetrySym0 a0123456789876543210
type instance Apply SymmetrySym0 a0123456789876543210 = SymmetrySym1 a0123456789876543210
instance SuppressUnusedWarnings SymmetrySym0 where
suppressUnusedWarnings = snd ((,) SymmetrySym0KindInference ())
data SymmetrySym1 (a0123456789876543210 :: Proxy t0123456789876543210) :: (~>) (Proxy t0123456789876543210) ((~>) ((:~:) (a0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210)) (y0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210))) Type)
where
SymmetrySym1KindInference :: SameKind (Apply (SymmetrySym1 a0123456789876543210) arg) (SymmetrySym2 a0123456789876543210 arg) =>
SymmetrySym1 a0123456789876543210 y0123456789876543210
type instance Apply (SymmetrySym1 a0123456789876543210) y0123456789876543210 = SymmetrySym2 a0123456789876543210 y0123456789876543210
instance SuppressUnusedWarnings (SymmetrySym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) SymmetrySym1KindInference ())
data SymmetrySym2 (a0123456789876543210 :: Proxy t0123456789876543210) (y0123456789876543210 :: Proxy t0123456789876543210) :: (~>) ((:~:) (a0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210)) (y0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210))) Type
where
SymmetrySym2KindInference :: SameKind (Apply (SymmetrySym2 a0123456789876543210 y0123456789876543210) arg) (SymmetrySym3 a0123456789876543210 y0123456789876543210 arg) =>
SymmetrySym2 a0123456789876543210 y0123456789876543210 e0123456789876543210
type instance Apply (SymmetrySym2 a0123456789876543210 y0123456789876543210) e0123456789876543210 = Symmetry a0123456789876543210 y0123456789876543210 e0123456789876543210
instance SuppressUnusedWarnings (SymmetrySym2 a0123456789876543210 y0123456789876543210) where
suppressUnusedWarnings = snd ((,) SymmetrySym2KindInference ())
type family SymmetrySym3 (a0123456789876543210 :: Proxy t0123456789876543210) (y0123456789876543210 :: Proxy t0123456789876543210) (e0123456789876543210 :: (:~:) (a0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210)) (y0123456789876543210 :: Proxy (t0123456789876543210 :: k0123456789876543210))) :: Type where
SymmetrySym3 a0123456789876543210 y0123456789876543210 e0123456789876543210 = Symmetry a0123456789876543210 y0123456789876543210 e0123456789876543210
Singletons/T353.hs:0:0:: Splicing declarations
genDefunSymbols [''Prod]
======>
type MkProdSym0 :: forall k
(f :: k -> Type)
(g :: k -> Type)
(p :: k). (~>) (f p) ((~>) (g p) (Prod f g p))
data MkProdSym0 :: (~>) (f p) ((~>) (g p) (Prod f g p))
where
MkProdSym0KindInference :: SameKind (Apply MkProdSym0 arg) (MkProdSym1 arg) =>
MkProdSym0 a0123456789876543210
type instance Apply MkProdSym0 a0123456789876543210 = MkProdSym1 a0123456789876543210
instance SuppressUnusedWarnings MkProdSym0 where
suppressUnusedWarnings = snd ((,) MkProdSym0KindInference ())
type MkProdSym1 :: forall k
(f :: k -> Type)
(g :: k -> Type)
(p :: k). f p -> (~>) (g p) (Prod f g p)
data MkProdSym1 (a0123456789876543210 :: f p) :: (~>) (g p) (Prod f g p)
where
MkProdSym1KindInference :: SameKind (Apply (MkProdSym1 a0123456789876543210) arg) (MkProdSym2 a0123456789876543210 arg) =>
MkProdSym1 a0123456789876543210 a0123456789876543210
type instance Apply (MkProdSym1 a0123456789876543210) a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MkProdSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MkProdSym1KindInference ())
type MkProdSym2 :: forall k
(f :: k -> Type)
(g :: k -> Type)
(p :: k). f p -> g p -> Prod f g p
type family MkProdSym2 (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where
MkProdSym2 a0123456789876543210 a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210
Singletons/T353.hs:0:0:: Splicing declarations
genDefunSymbols [''Foo]
======>
type MkFooSym0 :: forall k
k
(a :: k)
(b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
where
MkFooSym0KindInference :: SameKind (Apply MkFooSym0 arg) (MkFooSym1 arg) =>
MkFooSym0 a0123456789876543210
type instance Apply MkFooSym0 a0123456789876543210 = MkFooSym1 a0123456789876543210
instance SuppressUnusedWarnings MkFooSym0 where
suppressUnusedWarnings = snd ((,) MkFooSym0KindInference ())
type MkFooSym1 :: forall k k (a :: k) (b :: k). Proxy a
-> (~>) (Proxy b) (Foo a b)
data MkFooSym1 (a0123456789876543210 :: Proxy a) :: (~>) (Proxy b) (Foo a b)
where
MkFooSym1KindInference :: SameKind (Apply (MkFooSym1 a0123456789876543210) arg) (MkFooSym2 a0123456789876543210 arg) =>
MkFooSym1 a0123456789876543210 a0123456789876543210
type instance Apply (MkFooSym1 a0123456789876543210) a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MkFooSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MkFooSym1KindInference ())
type MkFooSym2 :: forall k k (a :: k) (b :: k). Proxy a
-> Proxy b -> Foo a b
type family MkFooSym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where
MkFooSym2 a0123456789876543210 a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210