T172.golden

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