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 (t :: a0123456789876543210) = FBox t instance SuppressUnusedWarnings FBoxSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) FBoxSym0KindInference) GHC.Tuple.()) data FBoxSym0 (l :: TyFun a0123456789876543210 (Box a0123456789876543210)) = forall arg. SameKind (Apply FBoxSym0 arg) (FBoxSym1 arg) => FBoxSym0KindInference type instance Apply FBoxSym0 l = FBox l type UnBoxSym1 (t :: Box a0123456789876543210) = UnBox t instance SuppressUnusedWarnings UnBoxSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) UnBoxSym0KindInference) GHC.Tuple.()) data UnBoxSym0 (l :: TyFun (Box a0123456789876543210) a0123456789876543210) = forall arg. SameKind (Apply UnBoxSym0 arg) (UnBoxSym1 arg) => UnBoxSym0KindInference type instance Apply UnBoxSym0 l = UnBox l type family UnBox (a :: Box a) :: a where UnBox (FBox a) = a sUnBox :: forall (t :: Box a). Sing t -> Sing (Apply UnBoxSym0 t :: a) sUnBox (SFBox (sA :: Sing a)) = sA data instance Sing (z :: Box a) = forall (n :: a). z ~ FBox n => SFBox (Sing (n :: a)) 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) = case toSing b :: SomeSing a of { SomeSing c -> SomeSing (SFBox c) } instance SingI n => SingI (FBox (n :: a)) where sing = SFBox sing