Nat.ghc82.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
      where
        Zero :: Nat
        Succ :: Nat -> 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_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789876543210 Zero Zero = TrueSym0
      Equals_0123456789876543210 (Succ a) (Succ b) = (:==) a b
      Equals_0123456789876543210 (a :: Nat) (b :: Nat) = FalseSym0
    instance PEq Nat where
      type (:==) (a :: Nat) (b :: Nat) = Equals_0123456789876543210 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. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = Succ 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. SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
        PredSym0KindInference
    type instance Apply PredSym0 l = Pred 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. SameKind (Apply (PlusSym1 l) arg) (PlusSym2 l arg) =>
        PlusSym1KindInference
    type instance Apply (PlusSym1 l) l = Plus l l
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) PlusSym0KindInference) GHC.Tuple.())
    data PlusSym0 (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
      = forall arg. SameKind (Apply PlusSym0 arg) (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 = SZero
    sPred (SSucc (sN :: Sing n)) = sN
    sPlus SZero (sM :: Sing m) = sM
    sPlus (SSucc (sN :: Sing n)) (sM :: Sing m)
      = (applySing ((singFun1 @SuccSym0) SSucc))
          ((applySing ((applySing ((singFun2 @PlusSym0) sPlus)) sN)) sM)
    data instance Sing (z :: Nat)
      = z ~ Zero => SZero |
        forall (n :: Nat). z ~ Succ n => SSucc (Sing (n :: Nat))
    type SNat = (Sing :: Nat -> GHC.Types.Type)
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ b)
        = case toSing b :: SomeSing Nat of {
            SomeSing c -> SomeSing (SSucc c) }
    instance SEq Nat where
      (%:==) SZero SZero = STrue
      (%:==) SZero (SSucc _) = SFalse
      (%:==) (SSucc _) SZero = SFalse
      (%:==) (SSucc a) (SSucc b) = ((%:==) a) b
    instance SDecide 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