ReturnFunc.ghc80.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 :: forall a. a -> a
    id x = x
    idFoo :: forall c a. c -> a -> a
    idFoo _ = id
    type IdSym1 (t :: a0123456789) = Id t
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) IdSym0KindInference GHC.Tuple.())
    data IdSym0 (l :: TyFun a0123456789 a0123456789)
      = forall arg. KindOf (Apply IdSym0 arg) ~ KindOf (IdSym1 arg) =>
        IdSym0KindInference
    type instance Apply IdSym0 l = IdSym1 l
    type IdFooSym2 (t :: c0123456789) (t :: a0123456789) = IdFoo t t
    instance SuppressUnusedWarnings IdFooSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) IdFooSym1KindInference GHC.Tuple.())
    data IdFooSym1 (l :: c0123456789)
                   (l :: TyFun a0123456789 a0123456789)
      = 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 c0123456789 (TyFun a0123456789 a0123456789
                                            -> GHC.Types.Type))
      = 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
                                         -> GHC.Types.Type))
      = 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_0123456789 a_0123456789 = Apply IdSym0 a_0123456789
    type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where
      ReturnFunc _z_0123456789 a_0123456789 = Apply SuccSym0 a_0123456789
    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
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply IdSym0 t :: a)
          lambda x = x
        in lambda sX
    sIdFoo _s_z_0123456789 sA_0123456789
      = let
          lambda ::
            forall _z_0123456789 a_0123456789.
            (t ~ _z_0123456789, t ~ a_0123456789) =>
            Sing _z_0123456789
            -> Sing a_0123456789 -> Sing (Apply (Apply IdFooSym0 t) t :: a)
          lambda _z_0123456789 a_0123456789
            = applySing (singFun1 (Proxy :: Proxy IdSym0) sId) a_0123456789
        in lambda _s_z_0123456789 sA_0123456789
    sReturnFunc _s_z_0123456789 sA_0123456789
      = let
          lambda ::
            forall _z_0123456789 a_0123456789.
            (t ~ _z_0123456789, t ~ a_0123456789) =>
            Sing _z_0123456789
            -> Sing a_0123456789
               -> Sing (Apply (Apply ReturnFuncSym0 t) t :: Nat)
          lambda _z_0123456789 a_0123456789
            = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) a_0123456789
        in lambda _s_z_0123456789 sA_0123456789