singletons-2.0: tests/compile-and-dump/Singletons/Nat.ghc710.template

Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| plus :: Nat -> Nat -> Nat
          plus Zero m = m
          plus (Succ n) m = Succ (plus n m)
          pred :: Nat -> Nat
          pred Zero = Zero
          pred (Succ n) = n
          
          data Nat
            where
              Zero :: Nat
              Succ :: Nat -> Nat
            deriving (Eq, Show, Read) |]
  ======>
    data Nat
      = Zero | Succ Nat
      deriving (Eq, Show, Read)
    plus :: Nat -> Nat -> Nat
    plus Zero m = m
    plus (Succ n) m = Succ (plus n m)
    pred :: Nat -> Nat
    pred Zero = Zero
    pred (Succ n) = n
    type family Equals_0123456789 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789 Zero Zero = TrueSym0
      Equals_0123456789 (Succ a) (Succ b) = (:==) a b
      Equals_0123456789 (a :: Nat) (b :: Nat) = FalseSym0
    instance PEq (KProxy :: KProxy Nat) where
      type (:==) (a :: Nat) (b :: Nat) = Equals_0123456789 a b
    type ZeroSym0 = Zero
    type SuccSym1 (t :: Nat) = Succ t
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) SuccSym0KindInference GHC.Tuple.())
    data SuccSym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply SuccSym0 arg) ~ KindOf (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = SuccSym1 l
    type PredSym1 (t :: Nat) = Pred t
    instance SuppressUnusedWarnings PredSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) PredSym0KindInference GHC.Tuple.())
    data PredSym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply PredSym0 arg) ~ KindOf (PredSym1 arg) =>
        PredSym0KindInference
    type instance Apply PredSym0 l = PredSym1 l
    type PlusSym2 (t :: Nat) (t :: Nat) = Plus t t
    instance SuppressUnusedWarnings PlusSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) PlusSym1KindInference GHC.Tuple.())
    data PlusSym1 (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (PlusSym1 l) arg) ~ KindOf (PlusSym2 l arg) =>
        PlusSym1KindInference
    type instance Apply (PlusSym1 l) l = PlusSym2 l l
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) PlusSym0KindInference GHC.Tuple.())
    data PlusSym0 (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. KindOf (Apply PlusSym0 arg) ~ KindOf (PlusSym1 arg) =>
        PlusSym0KindInference
    type instance Apply PlusSym0 l = PlusSym1 l
    type family Pred (a :: Nat) :: Nat where
      Pred Zero = ZeroSym0
      Pred (Succ n) = n
    type family Plus (a :: Nat) (a :: Nat) :: Nat where
      Plus Zero m = m
      Plus (Succ n) m = Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
    sPred ::
      forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t :: Nat)
    sPlus ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply PlusSym0 t) t :: Nat)
    sPred SZero
      = let
          lambda :: t ~ ZeroSym0 => Sing (Apply PredSym0 ZeroSym0 :: Nat)
          lambda = SZero
        in lambda
    sPred (SSucc sN)
      = let
          lambda ::
            forall n. t ~ Apply SuccSym0 n =>
            Sing n -> Sing (Apply PredSym0 (Apply SuccSym0 n) :: Nat)
          lambda n = n
        in lambda sN
    sPlus SZero sM
      = let
          lambda ::
            forall m. (t ~ ZeroSym0, t ~ m) =>
            Sing m -> Sing (Apply (Apply PlusSym0 ZeroSym0) m :: Nat)
          lambda m = m
        in lambda sM
    sPlus (SSucc sN) sM
      = let
          lambda ::
            forall n m. (t ~ Apply SuccSym0 n, t ~ m) =>
            Sing n
            -> Sing m
               -> Sing (Apply (Apply PlusSym0 (Apply SuccSym0 n)) m :: Nat)
          lambda n m
            = applySing
                (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                (applySing
                   (applySing (singFun2 (Proxy :: Proxy PlusSym0) sPlus) n) m)
        in lambda sN sM
    data instance Sing (z :: Nat)
      = z ~ Zero => SZero |
        forall (n :: Nat). z ~ Succ n => SSucc (Sing (n :: Nat))
    type SNat = (Sing :: Nat -> *)
    instance SingKind (KProxy :: KProxy Nat) where
      type DemoteRep (KProxy :: KProxy Nat) = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ b)
        = case toSing b :: SomeSing (KProxy :: KProxy Nat) of {
            SomeSing c -> SomeSing (SSucc c) }
    instance SEq (KProxy :: KProxy Nat) where
      (%:==) SZero SZero = STrue
      (%:==) SZero (SSucc _) = SFalse
      (%:==) (SSucc _) SZero = SFalse
      (%:==) (SSucc a) (SSucc b) = (%:==) a b
    instance SDecide (KProxy :: KProxy Nat) where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _)
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SSucc _) SZero
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SSucc a) (SSucc b)
        = case (%~) a b of {
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) }
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing