Singletons/T376.hs:(0,0)-(0,0): Splicing declarations singletons [d| f :: (() -> ()) -> (() -> ()) f g = g :: () -> () |] ======> f :: (() -> ()) -> () -> () f g = g :: () -> () type FSym0 :: (~>) ((~>) () ()) ((~>) () ()) data FSym0 :: (~>) ((~>) () ()) ((~>) () ()) 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 :: (~>) () () -> (~>) () () data FSym1 (a0123456789876543210 :: (~>) () ()) :: (~>) () () where FSym1KindInference :: SameKind (Apply (FSym1 a0123456789876543210) arg) (FSym2 a0123456789876543210 arg) => FSym1 a0123456789876543210 a0123456789876543210 type instance Apply (FSym1 a0123456789876543210) a0123456789876543210 = F a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (FSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym1KindInference ()) type FSym2 :: (~>) () () -> () -> () type family FSym2 (a0123456789876543210 :: (~>) () ()) (a0123456789876543210 :: ()) :: () where FSym2 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210 type F :: (~>) () () -> () -> () type family F (a :: (~>) () ()) (a :: ()) :: () where F g a_0123456789876543210 = Apply (g :: (~>) () ()) a_0123456789876543210 sF :: (forall (t :: (~>) () ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply FSym0 t) t :: ()) :: Type) sF (sG :: Sing g) (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (sG :: Sing (g :: (~>) () ())) sA_0123456789876543210 instance SingI (FSym0 :: (~>) ((~>) () ()) ((~>) () ())) where sing = singFun2 @FSym0 sF instance SingI d => SingI (FSym1 (d :: (~>) () ()) :: (~>) () ()) where sing = singFun1 @(FSym1 (d :: (~>) () ())) (sF (sing @d)) instance SingI1 (FSym1 :: (~>) () () -> (~>) () ()) where liftSing (s :: Sing (d :: (~>) () ())) = singFun1 @(FSym1 (d :: (~>) () ())) (sF s)