Singletons/T172.hs:(0,0)-(0,0): Splicing declarations singletonsOnly [d| ($>) :: Natural -> Natural -> Natural ($>) = (+) |] ======> type ($>@#@$) :: (~>) Natural ((~>) Natural Natural) data ($>@#@$) :: (~>) Natural ((~>) Natural Natural) where (:$>@#@$###) :: SameKind (Apply ($>@#@$) arg) (($>@#@$$) arg) => ($>@#@$) a0123456789876543210 type instance Apply ($>@#@$) a0123456789876543210 = ($>@#@$$) a0123456789876543210 instance SuppressUnusedWarnings ($>@#@$) where suppressUnusedWarnings = snd ((,) (:$>@#@$###) ()) type ($>@#@$$) :: Natural -> (~>) Natural Natural data ($>@#@$$) (a0123456789876543210 :: Natural) :: (~>) Natural Natural where (:$>@#@$$###) :: SameKind (Apply (($>@#@$$) a0123456789876543210) arg) (($>@#@$$$) a0123456789876543210 arg) => ($>@#@$$) a0123456789876543210 a0123456789876543210 type instance Apply (($>@#@$$) a0123456789876543210) a0123456789876543210 = ($>) a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (($>@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:$>@#@$$###) ()) type ($>@#@$$$) :: Natural -> Natural -> Natural type family ($>@#@$$$) (a0123456789876543210 :: Natural) (a0123456789876543210 :: Natural) :: Natural where ($>@#@$$$) a0123456789876543210 a0123456789876543210 = ($>) a0123456789876543210 a0123456789876543210 type ($>) :: Natural -> Natural -> Natural type family ($>) (a :: Natural) (a :: Natural) :: Natural where ($>) a_0123456789876543210 a_0123456789876543210 = Apply (Apply (+@#@$) a_0123456789876543210) a_0123456789876543210 (%$>) :: (forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply ($>@#@$) t) t :: Natural) :: Type) (%$>) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (applySing (singFun2 @(+@#@$) (%+)) sA_0123456789876543210) sA_0123456789876543210 instance SingI (($>@#@$) :: (~>) Natural ((~>) Natural Natural)) where sing = singFun2 @($>@#@$) (%$>) instance SingI d => SingI (($>@#@$$) (d :: Natural) :: (~>) Natural Natural) where sing = singFun1 @(($>@#@$$) (d :: Natural)) ((%$>) (sing @d)) instance SingI1 (($>@#@$$) :: Natural -> (~>) Natural Natural) where liftSing (s :: Sing (d :: Natural)) = singFun1 @(($>@#@$$) (d :: Natural)) ((%$>) s)