Singletons/HigherOrder.hs:0:0: Splicing declarations singletons [d| map :: (a -> b) -> [a] -> [b] map _ [] = [] map f (h : t) = (f h) : (map f t) liftMaybe :: (a -> b) -> Maybe a -> Maybe b liftMaybe f (Just x) = Just (f x) liftMaybe _ Nothing = Nothing |] ======> Singletons/HigherOrder.hs:(0,0)-(0,0) map :: forall a b. (a -> b) -> [a] -> [b] map _ GHC.Types.[] = [] map f (h GHC.Types.: t) = ((f h) GHC.Types.: (map f t)) liftMaybe :: forall a b. (a -> b) -> Maybe a -> Maybe b liftMaybe f (Just x) = Just (f x) liftMaybe _ Nothing = Nothing type family Map (a :: a -> b) (a :: [a]) :: [b] where Map z GHC.Types.[] = '[] Map f ((GHC.Types.:) h t) = (GHC.Types.:) (f h) (Map f t) type family LiftMaybe (a :: a -> b) (a :: Maybe a) :: Maybe b where LiftMaybe f (Just x) = Just (f x) LiftMaybe z Nothing = Nothing sMap :: forall (t :: a -> b) (t :: [a]). (forall (t :: a). Sing t -> Sing (t t)) -> Sing t -> Sing (Map t t) sMap _ SNil = SNil sMap f (SCons h t) = SCons (f h) (sMap f t) sLiftMaybe :: forall (t :: a -> b) (t :: Maybe a). (forall (t :: a). Sing t -> Sing (t t)) -> Sing t -> Sing (LiftMaybe t t) sLiftMaybe f (SJust x) = SJust (f x) sLiftMaybe _ SNothing = SNothing