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 type Let0123456789876543210ZSym0 = Let0123456789876543210Z type family Let0123456789876543210Z :: MyProxy a where Let0123456789876543210Z = MyProxySym0 type Let0123456789876543210XSym0 = Let0123456789876543210X type family Let0123456789876543210X where Let0123456789876543210X = Let0123456789876543210ZSym0 type FSym1 a0123456789876543210 = F a0123456789876543210 instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd (((,) FSym0KindInference) ()) data FSym0 a0123456789876543210 where FSym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply FSym0 arg) (FSym1 arg) => FSym0 a0123456789876543210 type instance Apply FSym0 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 instance Sing :: MyProxy a -> Type where SMyProxy :: Sing MyProxy type SMyProxy = (Sing :: MyProxy a -> Type) 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