BoxUnBox.ghc80.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 :: forall a. Box a -> a
    unBox (FBox a) = a
    type FBoxSym1 (t :: a0123456789) = FBox t
    instance SuppressUnusedWarnings FBoxSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) FBoxSym0KindInference GHC.Tuple.())
    data FBoxSym0 (l :: TyFun a0123456789 (Box a0123456789))
      = forall arg. KindOf (Apply FBoxSym0 arg) ~ KindOf (FBoxSym1 arg) =>
        FBoxSym0KindInference
    type instance Apply FBoxSym0 l = FBoxSym1 l
    type UnBoxSym1 (t :: Box a0123456789) = UnBox t
    instance SuppressUnusedWarnings UnBoxSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) UnBoxSym0KindInference GHC.Tuple.())
    data UnBoxSym0 (l :: TyFun (Box a0123456789) a0123456789)
      = forall arg. KindOf (Apply UnBoxSym0 arg) ~ KindOf (UnBoxSym1 arg) =>
        UnBoxSym0KindInference
    type instance Apply UnBoxSym0 l = UnBoxSym1 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)
      = let
          lambda ::
            forall a.
            t ~ Apply FBoxSym0 a => Sing a -> Sing (Apply UnBoxSym0 t :: a)
          lambda a = a
        in lambda 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 DemoteRep (Box a) = Box (DemoteRep 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