T172.golden

Singletons/T172.hs:(0,0)-(0,0): Splicing declarations
    singletonsOnly
      [d| ($>) :: Nat -> Nat -> Nat
          ($>) = (+) |]
  ======>
    type ($>@#@$) :: (~>) Nat ((~>) Nat Nat)
    data ($>@#@$) :: (~>) Nat ((~>) Nat Nat)
      where
        (:$>@#@$###) :: SameKind (Apply ($>@#@$) arg) (($>@#@$$) arg) =>
                        ($>@#@$) a0123456789876543210
    type instance Apply ($>@#@$) a0123456789876543210 = ($>@#@$$) a0123456789876543210
    instance SuppressUnusedWarnings ($>@#@$) where
      suppressUnusedWarnings = snd (((,) (:$>@#@$###)) ())
    type ($>@#@$$) :: Nat -> (~>) Nat Nat
    data ($>@#@$$) (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        (:$>@#@$$###) :: SameKind (Apply (($>@#@$$) a0123456789876543210) arg) (($>@#@$$$) a0123456789876543210 arg) =>
                         ($>@#@$$) a0123456789876543210 a0123456789876543210
    type instance Apply (($>@#@$$) a0123456789876543210) a0123456789876543210 = ($>) a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (($>@#@$$) a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) (:$>@#@$$###)) ())
    type ($>@#@$$$) :: Nat -> Nat -> Nat
    type family ($>@#@$$$) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      ($>@#@$$$) a0123456789876543210 a0123456789876543210 = ($>) a0123456789876543210 a0123456789876543210
    type ($>) :: Nat -> Nat -> Nat
    type family ($>) (a :: Nat) (a :: Nat) :: Nat where
      ($>) a_0123456789876543210 a_0123456789876543210 = Apply (Apply (+@#@$) a_0123456789876543210) a_0123456789876543210
    (%$>) ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply ($>@#@$) t) t :: Nat)
    (%$>)
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = (applySing
           ((applySing ((singFun2 @(+@#@$)) (%+))) sA_0123456789876543210))
          sA_0123456789876543210
    instance SingI (($>@#@$) :: (~>) Nat ((~>) Nat Nat)) where
      sing = (singFun2 @($>@#@$)) (%$>)
    instance SingI d =>
             SingI (($>@#@$$) (d :: Nat) :: (~>) Nat Nat) where
      sing = (singFun1 @(($>@#@$$) (d :: Nat))) ((%$>) (sing @d))