singletons-2.5: tests/compile-and-dump/Singletons/BoxUnBox.ghc86.template
Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| unBox :: Box a -> a
unBox (FBox a) = a
data Box a = FBox a |]
======>
data Box a = FBox a
unBox :: Box a -> a
unBox (FBox a) = a
type FBoxSym1 (t0123456789876543210 :: a0123456789876543210) =
FBox t0123456789876543210
instance SuppressUnusedWarnings FBoxSym0 where
suppressUnusedWarnings = snd (((,) FBoxSym0KindInference) ())
data FBoxSym0 :: forall a0123456789876543210.
(~>) a0123456789876543210 (Box a0123456789876543210)
where
FBoxSym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply FBoxSym0 arg) (FBoxSym1 arg) =>
FBoxSym0 t0123456789876543210
type instance Apply FBoxSym0 t0123456789876543210 = FBox t0123456789876543210
type UnBoxSym1 (a0123456789876543210 :: Box a0123456789876543210) =
UnBox a0123456789876543210
instance SuppressUnusedWarnings UnBoxSym0 where
suppressUnusedWarnings = snd (((,) UnBoxSym0KindInference) ())
data UnBoxSym0 :: forall a0123456789876543210.
(~>) (Box a0123456789876543210) a0123456789876543210
where
UnBoxSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply UnBoxSym0 arg) (UnBoxSym1 arg) =>
UnBoxSym0 a0123456789876543210
type instance Apply UnBoxSym0 a0123456789876543210 = UnBox a0123456789876543210
type family UnBox (a :: Box a) :: a where
UnBox (FBox a) = a
sUnBox ::
forall a (t :: Box a). Sing t -> Sing (Apply UnBoxSym0 t :: a)
sUnBox (SFBox (sA :: Sing a)) = sA
instance SingI (UnBoxSym0 :: (~>) (Box a) a) where
sing = (singFun1 @UnBoxSym0) sUnBox
data instance Sing :: Box a -> GHC.Types.Type
where SFBox :: forall a (n :: a). (Sing (n :: a)) -> Sing (FBox n)
type SBox = (Sing :: Box a -> GHC.Types.Type)
instance SingKind a => SingKind (Box a) where
type Demote (Box a) = Box (Demote a)
fromSing (SFBox b) = FBox (fromSing b)
toSing (FBox (b :: Demote a))
= case toSing b :: SomeSing a of {
SomeSing c -> SomeSing (SFBox c) }
instance SingI n => SingI (FBox (n :: a)) where
sing = SFBox sing
instance SingI (FBoxSym0 :: (~>) a (Box a)) where
sing = (singFun1 @FBoxSym0) SFBox
instance SingI (TyCon1 FBox :: (~>) a (Box a)) where
sing = (singFun1 @(TyCon1 FBox)) SFBox