singletons-1.0: tests/compile-and-dump/Promote/Prelude.ghc78.template
Promote/Prelude.hs:0:0: Splicing declarations
promoteOnly
[d| odd :: Nat -> Bool
odd 0 = False
odd n = not . odd $ n - 1 |]
======>
Promote/Prelude.hs:(0,0)-(0,0)
type OddSym1 (t :: Nat) = Odd t
instance SuppressUnusedWarnings OddSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) OddSym0KindInference GHC.Tuple.())
data OddSym0 (l :: TyFun Nat Bool)
= forall arg. (GHC.Types.~) (Data.Singletons.KindOf (Apply OddSym0 arg)) (Data.Singletons.KindOf (OddSym1 arg)) =>
OddSym0KindInference
type instance Apply OddSym0 l = OddSym1 l
type family Odd (a :: Nat) :: Bool where
Odd 0 = FalseSym0
Odd n = Apply (Apply ($$) (Apply (Apply (:.$) NotSym0) OddSym0)) (Apply (Apply (:-$) n) 1)