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 (a0123456789876543210 :: a0123456789876543210) =
        Id a0123456789876543210
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings = snd (((,) IdSym0KindInference) ())
    data IdSym0 :: forall a0123456789876543210.
                   (~>) a0123456789876543210 a0123456789876543210
      where
        IdSym0KindInference :: forall a0123456789876543210
                                      arg. SameKind (Apply IdSym0 arg) (IdSym1 arg) =>
                               IdSym0 a0123456789876543210
    type instance Apply IdSym0 a0123456789876543210 = Id a0123456789876543210
    type IdFooSym2 (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: a0123456789876543210) =
        IdFoo a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (IdFooSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) IdFooSym1KindInference) ())
    data IdFooSym1 (a0123456789876543210 :: c0123456789876543210) :: forall a0123456789876543210.
                                                                     (~>) a0123456789876543210 a0123456789876543210
      where
        IdFooSym1KindInference :: forall a0123456789876543210
                                         a0123456789876543210
                                         arg. SameKind (Apply (IdFooSym1 a0123456789876543210) arg) (IdFooSym2 a0123456789876543210 arg) =>
                                  IdFooSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (IdFooSym1 a0123456789876543210) a0123456789876543210 = IdFoo a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings IdFooSym0 where
      suppressUnusedWarnings = snd (((,) IdFooSym0KindInference) ())
    data IdFooSym0 :: forall a0123456789876543210 c0123456789876543210.
                      (~>) c0123456789876543210 ((~>) a0123456789876543210 a0123456789876543210)
      where
        IdFooSym0KindInference :: forall a0123456789876543210
                                         arg. SameKind (Apply IdFooSym0 arg) (IdFooSym1 arg) =>
                                  IdFooSym0 a0123456789876543210
    type instance Apply IdFooSym0 a0123456789876543210 = IdFooSym1 a0123456789876543210
    type ReturnFuncSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
        ReturnFunc a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ReturnFuncSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) ReturnFuncSym1KindInference) ())
    data ReturnFuncSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        ReturnFuncSym1KindInference :: forall a0123456789876543210
                                              a0123456789876543210
                                              arg. SameKind (Apply (ReturnFuncSym1 a0123456789876543210) arg) (ReturnFuncSym2 a0123456789876543210 arg) =>
                                       ReturnFuncSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ReturnFuncSym1 a0123456789876543210) a0123456789876543210 = ReturnFunc a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ReturnFuncSym0 where
      suppressUnusedWarnings = snd (((,) ReturnFuncSym0KindInference) ())
    data ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat)
      where
        ReturnFuncSym0KindInference :: forall a0123456789876543210
                                              arg. SameKind (Apply ReturnFuncSym0 arg) (ReturnFuncSym1 arg) =>
                                       ReturnFuncSym0 a0123456789876543210
    type instance Apply ReturnFuncSym0 a0123456789876543210 = ReturnFuncSym1 a0123456789876543210
    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 a (t :: a). Sing t -> Sing (Apply IdSym0 t :: a)
    sIdFoo ::
      forall c a (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
    instance SingI (IdSym0 :: (~>) a a) where
      sing = (singFun1 @IdSym0) sId
    instance SingI (IdFooSym0 :: (~>) c ((~>) a a)) where
      sing = (singFun2 @IdFooSym0) sIdFoo
    instance SingI d => SingI (IdFooSym1 (d :: c) :: (~>) a a) where
      sing = (singFun1 @(IdFooSym1 (d :: c))) (sIdFoo (sing @d))
    instance SingI (ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat)) where
      sing = (singFun2 @ReturnFuncSym0) sReturnFunc
    instance SingI d =>
             SingI (ReturnFuncSym1 (d :: Nat) :: (~>) Nat Nat) where
      sing
        = (singFun1 @(ReturnFuncSym1 (d :: Nat))) (sReturnFunc (sing @d))