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. 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)