singletons-base-3.0: tests/compile-and-dump/Singletons/Maybe.golden
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.Types.Nat
-> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (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.Types.Nat ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) (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.Types.Nat
-> (~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: (~>) (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.Types.Nat
-> Maybe a -> (~>) GHC.Types.Symbol GHC.Types.Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (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.Types.Nat
-> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (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 -> GHC.Types.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)
-> GHC.Types.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.Types.Nat)
(t2 :: Maybe a)
(t3 :: GHC.Types.Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
-> GHC.Types.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
-> GHC.Types.Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance SDecide a =>
Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a
-> GHC.Types.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 SingI (JustSym0 :: (~>) a (Maybe a)) where
sing = (singFun1 @JustSym0) SJust