singletons-2.5: tests/compile-and-dump/Singletons/T249.ghc86.template
Singletons/T249.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| data Foo1 a = MkFoo1 a
data Foo2 a where MkFoo2 :: x -> Foo2 x
data Foo3 a where MkFoo3 :: forall x. x -> Foo3 x |]
======>
data Foo1 a = MkFoo1 a
data Foo2 a where MkFoo2 :: x -> Foo2 x
data Foo3 a where MkFoo3 :: forall x. x -> Foo3 x
type MkFoo1Sym1 (t0123456789876543210 :: a0123456789876543210) =
MkFoo1 t0123456789876543210
instance SuppressUnusedWarnings MkFoo1Sym0 where
suppressUnusedWarnings = snd (((,) MkFoo1Sym0KindInference) ())
data MkFoo1Sym0 :: forall a0123456789876543210.
(~>) a0123456789876543210 (Foo1 a0123456789876543210)
where
MkFoo1Sym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply MkFoo1Sym0 arg) (MkFoo1Sym1 arg) =>
MkFoo1Sym0 t0123456789876543210
type instance Apply MkFoo1Sym0 t0123456789876543210 = MkFoo1 t0123456789876543210
type MkFoo2Sym1 (t0123456789876543210 :: x0123456789876543210) =
MkFoo2 t0123456789876543210
instance SuppressUnusedWarnings MkFoo2Sym0 where
suppressUnusedWarnings = snd (((,) MkFoo2Sym0KindInference) ())
data MkFoo2Sym0 :: forall x0123456789876543210.
(~>) x0123456789876543210 (Foo2 x0123456789876543210)
where
MkFoo2Sym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply MkFoo2Sym0 arg) (MkFoo2Sym1 arg) =>
MkFoo2Sym0 t0123456789876543210
type instance Apply MkFoo2Sym0 t0123456789876543210 = MkFoo2 t0123456789876543210
type MkFoo3Sym1 (t0123456789876543210 :: x0123456789876543210) =
MkFoo3 t0123456789876543210
instance SuppressUnusedWarnings MkFoo3Sym0 where
suppressUnusedWarnings = snd (((,) MkFoo3Sym0KindInference) ())
data MkFoo3Sym0 :: forall x0123456789876543210.
(~>) x0123456789876543210 (Foo3 x0123456789876543210)
where
MkFoo3Sym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply MkFoo3Sym0 arg) (MkFoo3Sym1 arg) =>
MkFoo3Sym0 t0123456789876543210
type instance Apply MkFoo3Sym0 t0123456789876543210 = MkFoo3 t0123456789876543210
data instance Sing :: Foo1 a -> Type
where
SMkFoo1 :: forall a (n :: a). (Sing (n :: a)) -> Sing (MkFoo1 n)
type SFoo1 = (Sing :: Foo1 a -> Type)
instance SingKind a => SingKind (Foo1 a) where
type Demote (Foo1 a) = Foo1 (Demote a)
fromSing (SMkFoo1 b) = MkFoo1 (fromSing b)
toSing (MkFoo1 (b :: Demote a))
= case toSing b :: SomeSing a of {
SomeSing c -> SomeSing (SMkFoo1 c) }
data instance Sing :: Foo2 a -> Type
where
SMkFoo2 :: forall x (n :: x). (Sing (n :: x)) -> Sing (MkFoo2 n)
type SFoo2 = (Sing :: Foo2 a -> Type)
instance SingKind a => SingKind (Foo2 a) where
type Demote (Foo2 a) = Foo2 (Demote a)
fromSing (SMkFoo2 b) = MkFoo2 (fromSing b)
toSing (MkFoo2 (b :: Demote x))
= case toSing b :: SomeSing x of {
SomeSing c -> SomeSing (SMkFoo2 c) }
data instance Sing :: Foo3 a -> Type
where
SMkFoo3 :: forall x (n :: x). (Sing (n :: x)) -> Sing (MkFoo3 n)
type SFoo3 = (Sing :: Foo3 a -> Type)
instance SingKind a => SingKind (Foo3 a) where
type Demote (Foo3 a) = Foo3 (Demote a)
fromSing (SMkFoo3 b) = MkFoo3 (fromSing b)
toSing (MkFoo3 (b :: Demote x))
= case toSing b :: SomeSing x of {
SomeSing c -> SomeSing (SMkFoo3 c) }
instance SingI n => SingI (MkFoo1 (n :: a)) where
sing = SMkFoo1 sing
instance SingI (MkFoo1Sym0 :: (~>) a (Foo1 a)) where
sing = (singFun1 @MkFoo1Sym0) SMkFoo1
instance SingI (TyCon1 MkFoo1 :: (~>) a (Foo1 a)) where
sing = (singFun1 @(TyCon1 MkFoo1)) SMkFoo1
instance SingI n => SingI (MkFoo2 (n :: x)) where
sing = SMkFoo2 sing
instance SingI (MkFoo2Sym0 :: (~>) x (Foo2 x)) where
sing = (singFun1 @MkFoo2Sym0) SMkFoo2
instance SingI (TyCon1 MkFoo2 :: (~>) x (Foo2 x)) where
sing = (singFun1 @(TyCon1 MkFoo2)) SMkFoo2
instance SingI n => SingI (MkFoo3 (n :: x)) where
sing = SMkFoo3 sing
instance SingI (MkFoo3Sym0 :: (~>) x (Foo3 x)) where
sing = (singFun1 @MkFoo3Sym0) SMkFoo3
instance SingI (TyCon1 MkFoo3 :: (~>) x (Foo3 x)) where
sing = (singFun1 @(TyCon1 MkFoo3)) SMkFoo3