singletons-2.7: tests/compile-and-dump/Singletons/T297.golden
Singletons/T297.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| f MyProxy
= let
x = let
z :: MyProxy a
z = MyProxy
in z
in x
data MyProxy (a :: Type) = MyProxy |]
======>
data MyProxy (a :: Type) = MyProxy
f MyProxy
= let
x = let
z :: MyProxy a
z = MyProxy
in z
in x
type MyProxySym0 = MyProxy :: MyProxy (a :: Type)
type Let0123456789876543210ZSym0 =
Let0123456789876543210Z :: MyProxy a
type Let0123456789876543210Z :: MyProxy a
type family Let0123456789876543210Z where
Let0123456789876543210Z = MyProxySym0
type Let0123456789876543210XSym0 = Let0123456789876543210X
type family Let0123456789876543210X where
Let0123456789876543210X = Let0123456789876543210ZSym0
data FSym0 a0123456789876543210
where
FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) =>
FSym0 a0123456789876543210
type instance Apply FSym0 a0123456789876543210 = FSym1 a0123456789876543210
instance SuppressUnusedWarnings FSym0 where
suppressUnusedWarnings = snd (((,) FSym0KindInference) ())
type FSym1 a0123456789876543210 = F a0123456789876543210
type family F a where
F MyProxy = Let0123456789876543210XSym0
sF :: forall arg. Sing arg -> Sing (Apply FSym0 arg)
sF SMyProxy
= let
sX :: Sing @_ Let0123456789876543210XSym0
sX
= let
sZ :: forall a. Sing (Let0123456789876543210ZSym0 :: MyProxy a)
sZ = SMyProxy
in sZ
in sX
instance SingI FSym0 where
sing = (singFun1 @FSym0) sF
data SMyProxy :: forall a. MyProxy (a :: Type) -> Type
where
SMyProxy :: forall (a :: Type).
SMyProxy (MyProxy :: MyProxy (a :: Type))
type instance Sing @(MyProxy a) = SMyProxy
instance SingKind a => SingKind (MyProxy a) where
type Demote (MyProxy a) = MyProxy (Demote a)
fromSing SMyProxy = MyProxy
toSing MyProxy = SomeSing SMyProxy
instance SingI MyProxy where
sing = SMyProxy