BoxUnBox.ghc76.template

Singletons/BoxUnBox.hs:0:0: Splicing declarations
    singletons
      [d| unBox :: Box a -> a
          unBox (FBox a) = a
          
          data Box a = FBox a |]
  ======>
    Singletons/BoxUnBox.hs:(0,0)-(0,0)
    data Box a = FBox a
    unBox :: forall a. Box a -> a
    unBox (FBox a) = a
    type BoxTyCtor = Box
    data BoxTyCtorSym0 (k :: TyFun * *)
    type instance Apply BoxTyCtorSym0 a = BoxTyCtor a
    data FBoxSym0 (k :: TyFun a (Box a))
    type instance Apply FBoxSym0 a = FBox a
    type family UnBox (a :: Box a) :: a
    type instance UnBox (FBox a) = a
    data UnBoxSym0 (k :: TyFun (Box a) a)
    type instance Apply UnBoxSym0 a = UnBox a
    data instance Sing (z :: Box a)
      = forall (n :: a). z ~ FBox n => SFBox (Sing n)
    type SBox (z :: Box a) = Sing z
    instance SingKind (KProxy :: KProxy a) =>
             SingKind (KProxy :: KProxy (Box a)) where
      type instance DemoteRep (KProxy :: KProxy (Box a)) =
          Box (DemoteRep (KProxy :: KProxy a))
      fromSing (SFBox b) = FBox (fromSing b)
      toSing (FBox b)
        = case toSing b :: SomeSing (KProxy :: KProxy a) of {
            SomeSing c -> SomeSing (SFBox c) }
    instance SingI n => SingI (FBox (n :: a)) where
      sing = SFBox sing
    sUnBox :: forall (t :: Box a). Sing t -> Sing (UnBox t)
    sUnBox (SFBox a) = a