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 :: forall (a :: Type). MyProxy (a :: Type) type family MyProxySym0 :: MyProxy (a :: Type) where MyProxySym0 = MyProxy type Let0123456789876543210ZSym0 :: MyProxy a type family Let0123456789876543210ZSym0 :: MyProxy a where Let0123456789876543210ZSym0 = Let0123456789876543210Z type Let0123456789876543210Z :: MyProxy a type family Let0123456789876543210Z :: MyProxy a where Let0123456789876543210Z = MyProxySym0 type family Let0123456789876543210XSym0 where 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 = F a0123456789876543210 instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd ((,) FSym0KindInference ()) type family FSym1 a0123456789876543210 where 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 :: (Sing (Let0123456789876543210ZSym0 :: MyProxy a) :: Type) sZ = SMyProxy in sZ in sX instance SingI FSym0 where sing = singFun1 @FSym0 sF data SMyProxy :: forall (a :: Type). MyProxy a -> 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