ReturnFunc.ghc78.template

Singletons/ReturnFunc.hs:0:0: Splicing declarations
    singletons
      [d| returnFunc :: Nat -> Nat -> Nat
          returnFunc _ = Succ
          id :: a -> a
          id x = x
          idFoo :: c -> a -> a
          idFoo _ = id |]
  ======>
    Singletons/ReturnFunc.hs:(0,0)-(0,0)
    returnFunc :: Nat -> Nat -> Nat
    returnFunc _ = Succ
    id :: forall a. a -> a
    id x = x
    idFoo :: forall c a. c -> a -> a
    idFoo _ = id
    type IdSym1 (t :: a) = Id t
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) IdSym0KindInference GHC.Tuple.())
    data IdSym0 (l :: TyFun a a)
      = forall arg. KindOf (Apply IdSym0 arg) ~ KindOf (IdSym1 arg) =>
        IdSym0KindInference
    type instance Apply IdSym0 l = IdSym1 l
    type IdFooSym2 (t :: c) (t :: a) = IdFoo t t
    instance SuppressUnusedWarnings IdFooSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) IdFooSym1KindInference GHC.Tuple.())
    data IdFooSym1 (l :: c) (l :: TyFun a a)
      = forall arg. KindOf (Apply (IdFooSym1 l) arg) ~ KindOf (IdFooSym2 l arg) =>
        IdFooSym1KindInference
    type instance Apply (IdFooSym1 l) l = IdFooSym2 l l
    instance SuppressUnusedWarnings IdFooSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) IdFooSym0KindInference GHC.Tuple.())
    data IdFooSym0 (l :: TyFun c (TyFun a a -> *))
      = forall arg. KindOf (Apply IdFooSym0 arg) ~ KindOf (IdFooSym1 arg) =>
        IdFooSym0KindInference
    type instance Apply IdFooSym0 l = IdFooSym1 l
    type ReturnFuncSym2 (t :: Nat) (t :: Nat) = ReturnFunc t t
    instance SuppressUnusedWarnings ReturnFuncSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ReturnFuncSym1KindInference GHC.Tuple.())
    data ReturnFuncSym1 (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (ReturnFuncSym1 l) arg) ~ KindOf (ReturnFuncSym2 l arg) =>
        ReturnFuncSym1KindInference
    type instance Apply (ReturnFuncSym1 l) l = ReturnFuncSym2 l l
    instance SuppressUnusedWarnings ReturnFuncSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ReturnFuncSym0KindInference GHC.Tuple.())
    data ReturnFuncSym0 (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. KindOf (Apply ReturnFuncSym0 arg) ~ KindOf (ReturnFuncSym1 arg) =>
        ReturnFuncSym0KindInference
    type instance Apply ReturnFuncSym0 l = ReturnFuncSym1 l
    type family Id (a :: a) :: a where
      Id x = x
    type family IdFoo (a :: c) (a :: a) :: a where
      IdFoo z a_0123456789 = Apply IdSym0 a_0123456789
    type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where
      ReturnFunc z a_0123456789 = Apply SuccSym0 a_0123456789
    sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t)
    sIdFoo ::
      forall (t :: c) (t :: a).
      Sing t -> Sing t -> Sing (Apply (Apply IdFooSym0 t) t)
    sReturnFunc ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply ReturnFuncSym0 t) t)
    sId sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply IdSym0 x)
          lambda x = x
        in lambda sX
    sIdFoo _ sA_0123456789
      = let
          lambda ::
            forall a_0123456789 wild. (t ~ wild, t ~ a_0123456789) =>
            Sing a_0123456789
            -> Sing (Apply (Apply IdFooSym0 wild) a_0123456789)
          lambda a_0123456789
            = applySing (singFun1 (Proxy :: Proxy IdSym0) sId) a_0123456789
        in lambda sA_0123456789
    sReturnFunc _ sA_0123456789
      = let
          lambda ::
            forall a_0123456789 wild. (t ~ wild, t ~ a_0123456789) =>
            Sing a_0123456789
            -> Sing (Apply (Apply ReturnFuncSym0 wild) a_0123456789)
          lambda a_0123456789
            = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) a_0123456789
        in lambda sA_0123456789