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