Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations singletons [d| data Maybe a = Nothing | Just a deriving (Eq, Show) |] ======> data Maybe a = Nothing | Just a deriving (Eq, Show) type NothingSym0 :: forall a. Maybe a type family NothingSym0 :: Maybe a where NothingSym0 = Nothing type JustSym0 :: forall a. (~>) a (Maybe a) data JustSym0 :: (~>) a (Maybe a) where JustSym0KindInference :: SameKind (Apply JustSym0 arg) (JustSym1 arg) => JustSym0 a0123456789876543210 type instance Apply JustSym0 a0123456789876543210 = Just a0123456789876543210 instance SuppressUnusedWarnings JustSym0 where suppressUnusedWarnings = snd ((,) JustSym0KindInference ()) type JustSym1 :: forall a. a -> Maybe a type family JustSym1 (a0123456789876543210 :: a) :: Maybe a where JustSym1 a0123456789876543210 = Just a0123456789876543210 type TFHelper_0123456789876543210 :: Maybe a -> Maybe a -> Bool type family TFHelper_0123456789876543210 (a :: Maybe a) (a :: Maybe a) :: Bool where TFHelper_0123456789876543210 Nothing Nothing = TrueSym0 TFHelper_0123456789876543210 Nothing (Just _) = FalseSym0 TFHelper_0123456789876543210 (Just _) Nothing = FalseSym0 TFHelper_0123456789876543210 (Just a_0123456789876543210) (Just b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) (Maybe a) ((~>) (Maybe a) Bool) data TFHelper_0123456789876543210Sym0 :: (~>) (Maybe a) ((~>) (Maybe a) Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym0KindInference ()) type TFHelper_0123456789876543210Sym1 :: Maybe a -> (~>) (Maybe a) Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Maybe a) :: (~>) (Maybe a) Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Maybe a -> Maybe a -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe a) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Maybe a) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Maybe a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210 _ Nothing a_0123456789876543210 = Apply (Apply ShowStringSym0 "Nothing") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (Just arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Just ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) where ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) => ShowsPrec_0123456789876543210Sym0 a0123456789876543210 type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ()) type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural -> (~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol) data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol) where ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ()) type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural -> Maybe a -> (~>) GHC.Types.Symbol GHC.Types.Symbol data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Maybe a) :: (~>) GHC.Types.Symbol GHC.Types.Symbol where ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Maybe a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a data SMaybe :: forall a. Maybe a -> Type where SNothing :: forall a. SMaybe (Nothing :: Maybe a) SJust :: forall a (n :: a). (Sing n) -> SMaybe (Just n :: Maybe a) type instance Sing @(Maybe a) = SMaybe instance SingKind a => SingKind (Maybe a) where type Demote (Maybe a) = Maybe (Demote a) fromSing SNothing = Nothing fromSing (SJust b) = Just (fromSing b) toSing Nothing = SomeSing SNothing toSing (Just (b :: Demote a)) = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SJust c) instance SEq a => SEq (Maybe a) where (%==) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Maybe a) ((~>) (Maybe a) Bool) -> Type) t1) t2) (%==) SNothing SNothing = STrue (%==) SNothing (SJust _) = SFalse (%==) (SJust _) SNothing = SFalse (%==) (SJust (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SJust (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SShow a => SShow (Maybe a) where sShowsPrec :: forall (t1 :: GHC.Num.Natural.Natural) (t2 :: Maybe a) (t3 :: GHC.Types.Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) -> Type) t1) t2) t3) sShowsPrec _ SNothing (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (applySing (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Nothing")) sA_0123456789876543210 sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SJust (sArg_0123456789876543210 :: Sing arg_0123456789876543210)) (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (applySing (applySing (singFun3 @ShowParenSym0 sShowParen) (applySing (applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210) (sFromInteger (sing :: Sing 10)))) (applySing (applySing (singFun3 @(.@#@$) (%.)) (applySing (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Just "))) (applySing (applySing (singFun3 @ShowsPrecSym0 sShowsPrec) (sFromInteger (sing :: Sing 11))) sArg_0123456789876543210))) sA_0123456789876543210 instance SDecide a => SDecide (Maybe a) where (%~) SNothing SNothing = Proved Refl (%~) SNothing (SJust _) = Disproved (\ x -> case x of {}) (%~) (SJust _) SNothing = Disproved (\ x -> case x of {}) (%~) (SJust a) (SJust b) = case (%~) a b of Proved Refl -> Proved Refl Disproved contra -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance SDecide a => Data.Type.Equality.TestEquality (SMaybe :: Maybe a -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing a => Show (SMaybe (z :: Maybe a)) instance SingI Nothing where sing = SNothing instance SingI n => SingI (Just (n :: a)) where sing = SJust sing instance SingI1 Just where liftSing = SJust instance SingI (JustSym0 :: (~>) a (Maybe a)) where sing = singFun1 @JustSym0 SJust