singletons-2.4: tests/compile-and-dump/Singletons/T172.ghc84.template
Singletons/T172.hs:(0,0)-(0,0): Splicing declarations
singletonsOnly
[d| ($>) :: Nat -> Nat -> Nat
($>) = (+) |]
======>
type ($>@#@$$$) (t :: Nat) (t :: Nat) = ($>) t t
instance SuppressUnusedWarnings ($>@#@$$) where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) (:$>@#@$$###)) GHC.Tuple.())
data ($>@#@$$) (l :: Nat) (l :: TyFun Nat Nat)
= forall arg. SameKind (Apply (($>@#@$$) l) arg) (($>@#@$$$) l arg) =>
(:$>@#@$$###)
type instance Apply (($>@#@$$) l) l = ($>) l l
instance SuppressUnusedWarnings ($>@#@$) where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) (:$>@#@$###)) GHC.Tuple.())
data ($>@#@$) (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
= forall arg. SameKind (Apply ($>@#@$) arg) (($>@#@$$) arg) =>
(:$>@#@$###)
type instance Apply ($>@#@$) l = ($>@#@$$) l
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