packages feed

singletons-base-3.1: tests/compile-and-dump/Singletons/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)
    (%$>)
      (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)