packages feed

singletons-2.3: tests/compile-and-dump/Promote/GenDefunSymbols.ghc82.template

Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
    genDefunSymbols [''LiftMaybe, ''NatT, ''(:+)]
  ======>
    type LiftMaybeSym2 (t :: TyFun a0123456789876543210 b0123456789876543210
                             -> Type) (t :: Maybe a0123456789876543210) =
        LiftMaybe t t
    instance SuppressUnusedWarnings LiftMaybeSym1 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) LiftMaybeSym1KindInference) GHC.Tuple.())
    data LiftMaybeSym1 (l :: TyFun a0123456789876543210 b0123456789876543210
                             -> Type) (l :: TyFun (Maybe a0123456789876543210) (Maybe b0123456789876543210))
      = forall arg. Data.Singletons.SameKind (Apply (LiftMaybeSym1 l) arg) (LiftMaybeSym2 l arg) =>
        LiftMaybeSym1KindInference
    type instance Apply (LiftMaybeSym1 l) l = LiftMaybe l l
    instance SuppressUnusedWarnings LiftMaybeSym0 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) LiftMaybeSym0KindInference) GHC.Tuple.())
    data LiftMaybeSym0 (l :: TyFun (TyFun a0123456789876543210 b0123456789876543210
                                    -> Type) (TyFun (Maybe a0123456789876543210) (Maybe b0123456789876543210)
                                              -> Type))
      = forall arg. Data.Singletons.SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
        LiftMaybeSym0KindInference
    type instance Apply LiftMaybeSym0 l = LiftMaybeSym1 l
    type ZeroSym0 = Zero
    type SuccSym1 (t :: NatT) = Succ t
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
    data SuccSym0 (l :: TyFun NatT NatT)
      = forall arg. Data.Singletons.SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = Succ l
    type (:+$$$) (t :: Nat) (t :: Nat) = (:+) t t
    instance SuppressUnusedWarnings (:+$$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:+$$###)) GHC.Tuple.())
    data (:+$$) (l :: Nat) l
      = forall arg. Data.Singletons.SameKind (Apply ((:+$$) l) arg) ((:+$$$) l arg) =>
        (:+$$###)
    type instance Apply ((:+$$) l) l = (:+) l l
    instance SuppressUnusedWarnings (:+$) where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) (:+$###)) GHC.Tuple.())
    data (:+$) l
      = forall arg. Data.Singletons.SameKind (Apply (:+$) arg) ((:+$$) arg) =>
        (:+$###)
    type instance Apply (:+$) l = (:+$$) l