ReturnFunc.ghc84.template

Singletons/ReturnFunc.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| returnFunc :: Nat -> Nat -> Nat
          returnFunc _ = Succ
          id :: a -> a
          id x = x
          idFoo :: c -> a -> a
          idFoo _ = id |]
  ======>
    returnFunc :: Nat -> Nat -> Nat
    returnFunc _ = Succ
    id :: a -> a
    id x = x
    idFoo :: c -> a -> a
    idFoo _ = id
    type IdSym1 (t :: a0123456789876543210) = Id t
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) IdSym0KindInference) GHC.Tuple.())
    data IdSym0 (l :: TyFun a0123456789876543210 a0123456789876543210)
      = forall arg. SameKind (Apply IdSym0 arg) (IdSym1 arg) =>
        IdSym0KindInference
    type instance Apply IdSym0 l = Id l
    type IdFooSym2 (t :: c0123456789876543210) (t :: a0123456789876543210) =
        IdFoo t t
    instance SuppressUnusedWarnings IdFooSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) IdFooSym1KindInference) GHC.Tuple.())
    data IdFooSym1 (l :: c0123456789876543210) (l :: TyFun a0123456789876543210 a0123456789876543210)
      = forall arg. SameKind (Apply (IdFooSym1 l) arg) (IdFooSym2 l arg) =>
        IdFooSym1KindInference
    type instance Apply (IdFooSym1 l) l = IdFoo l l
    instance SuppressUnusedWarnings IdFooSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) IdFooSym0KindInference) GHC.Tuple.())
    data IdFooSym0 (l :: TyFun c0123456789876543210 (TyFun a0123456789876543210 a0123456789876543210
                                                     -> GHC.Types.Type))
      = forall arg. SameKind (Apply IdFooSym0 arg) (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. SameKind (Apply (ReturnFuncSym1 l) arg) (ReturnFuncSym2 l arg) =>
        ReturnFuncSym1KindInference
    type instance Apply (ReturnFuncSym1 l) l = ReturnFunc l l
    instance SuppressUnusedWarnings ReturnFuncSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) ReturnFuncSym0KindInference) GHC.Tuple.())
    data ReturnFuncSym0 (l :: TyFun Nat (TyFun Nat Nat
                                         -> GHC.Types.Type))
      = forall arg. SameKind (Apply ReturnFuncSym0 arg) (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 _ a_0123456789876543210 = Apply IdSym0 a_0123456789876543210
    type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where
      ReturnFunc _ a_0123456789876543210 = Apply SuccSym0 a_0123456789876543210
    sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a)
    sIdFoo ::
      forall (t :: c) (t :: a).
      Sing t -> Sing t -> Sing (Apply (Apply IdFooSym0 t) t :: a)
    sReturnFunc ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply ReturnFuncSym0 t) t :: Nat)
    sId (sX :: Sing x) = sX
    sIdFoo _ (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = (applySing ((singFun1 @IdSym0) sId)) sA_0123456789876543210
    sReturnFunc
      _
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = (applySing ((singFun1 @SuccSym0) SSucc)) sA_0123456789876543210