ReturnFunc.golden

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 IdFooSym0 :: (~>) c ((~>) a a)
    data IdFooSym0 :: (~>) c ((~>) a a)
      where
        IdFooSym0KindInference :: SameKind (Apply IdFooSym0 arg) (IdFooSym1 arg) =>
                                  IdFooSym0 a0123456789876543210
    type instance Apply @c @((~>) a a) IdFooSym0 a0123456789876543210 = IdFooSym1 a0123456789876543210
    instance SuppressUnusedWarnings IdFooSym0 where
      suppressUnusedWarnings = snd ((,) IdFooSym0KindInference ())
    type IdFooSym1 :: c -> (~>) a a
    data IdFooSym1 (a0123456789876543210 :: c) :: (~>) a a
      where
        IdFooSym1KindInference :: SameKind (Apply (IdFooSym1 a0123456789876543210) arg) (IdFooSym2 a0123456789876543210 arg) =>
                                  IdFooSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @a @a (IdFooSym1 a0123456789876543210) a0123456789876543210 = IdFoo a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (IdFooSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) IdFooSym1KindInference ())
    type IdFooSym2 :: c -> a -> a
    type family IdFooSym2 @c @a (a0123456789876543210 :: c) (a0123456789876543210 :: a) :: a where
      IdFooSym2 a0123456789876543210 a0123456789876543210 = IdFoo a0123456789876543210 a0123456789876543210
    type IdSym0 :: (~>) a a
    data IdSym0 :: (~>) a a
      where
        IdSym0KindInference :: SameKind (Apply IdSym0 arg) (IdSym1 arg) =>
                               IdSym0 a0123456789876543210
    type instance Apply @a @a IdSym0 a0123456789876543210 = Id a0123456789876543210
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings = snd ((,) IdSym0KindInference ())
    type IdSym1 :: a -> a
    type family IdSym1 @a (a0123456789876543210 :: a) :: a where
      IdSym1 a0123456789876543210 = Id a0123456789876543210
    type ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat)
    data ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat)
      where
        ReturnFuncSym0KindInference :: SameKind (Apply ReturnFuncSym0 arg) (ReturnFuncSym1 arg) =>
                                       ReturnFuncSym0 a0123456789876543210
    type instance Apply @Nat @((~>) Nat Nat) ReturnFuncSym0 a0123456789876543210 = ReturnFuncSym1 a0123456789876543210
    instance SuppressUnusedWarnings ReturnFuncSym0 where
      suppressUnusedWarnings = snd ((,) ReturnFuncSym0KindInference ())
    type ReturnFuncSym1 :: Nat -> (~>) Nat Nat
    data ReturnFuncSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        ReturnFuncSym1KindInference :: SameKind (Apply (ReturnFuncSym1 a0123456789876543210) arg) (ReturnFuncSym2 a0123456789876543210 arg) =>
                                       ReturnFuncSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @Nat @Nat (ReturnFuncSym1 a0123456789876543210) a0123456789876543210 = ReturnFunc a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ReturnFuncSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) ReturnFuncSym1KindInference ())
    type ReturnFuncSym2 :: Nat -> Nat -> Nat
    type family ReturnFuncSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      ReturnFuncSym2 a0123456789876543210 a0123456789876543210 = ReturnFunc a0123456789876543210 a0123456789876543210
    type IdFoo :: c -> a -> a
    type family IdFoo @c @a (a :: c) (a :: a) :: a where
      IdFoo _ a_0123456789876543210 = Apply IdSym0 a_0123456789876543210
    type Id :: a -> a
    type family Id @a (a :: a) :: a where
      Id x = x
    type ReturnFunc :: Nat -> Nat -> Nat
    type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where
      ReturnFunc _ a_0123456789876543210 = Apply SuccSym0 a_0123456789876543210
    sIdFoo ::
      (forall (t :: c) (t :: a).
       Sing t -> Sing t -> Sing (IdFoo t t :: a) :: Type)
    sId :: (forall (t :: a). Sing t -> Sing (Id t :: a) :: Type)
    sReturnFunc ::
      (forall (t :: Nat) (t :: Nat).
       Sing t -> Sing t -> Sing (ReturnFunc t t :: Nat) :: Type)
    sIdFoo _ (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = applySing (singFun1 @IdSym0 sId) sA_0123456789876543210
    sId (sX :: Sing x) = sX
    sReturnFunc
      _
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = applySing (singFun1 @SuccSym0 SSucc) sA_0123456789876543210
    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 SingI1 (IdFooSym1 :: c -> (~>) a a) where
      liftSing (s :: Sing (d :: c))
        = singFun1 @(IdFooSym1 (d :: c)) (sIdFoo s)
    instance SingI (IdSym0 :: (~>) a a) where
      sing = singFun1 @IdSym0 sId
    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))
    instance SingI1 (ReturnFuncSym1 :: Nat -> (~>) Nat Nat) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(ReturnFuncSym1 (d :: Nat)) (sReturnFunc s)