type-natural 0.3.0.0 → 0.4.0.0

raw patch · 7 files changed

+511/−239 lines, 7 filesdep +ghc-typelits-natnormalisedep +ghc-typelits-presburgerdep ~constraintsdep ~equational-reasoningdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-typelits-natnormalise, ghc-typelits-presburger

Dependency ranges changed: constraints, equational-reasoning, singletons, template-haskell

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +68/−88
• Data/Type/Natural/Builtin.hs +328/−0
• Data/Type/Natural/Compat.hs +8/−0
• Data/Type/Natural/Core.hs +29/−67
• Data/Type/Natural/Definitions.hs +7/−15
• Data/Type/Ordinal.hs +37/−50
• type-natural.cabal +34/−19

@@ -1,48 +1,32 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}-{-# LANGUAGE UndecidableInstances                                           #-}+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                 #-}+{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies          #-}+{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-} -- | Type level peano natural number, some arithmetic functions and their singletons. module Data.Type.Natural (-- * Re-exported modules.                           module Data.Singletons,                           -- * Natural Numbers                           -- | Peano natural numbers. It will be promoted to the type-level natural number.                           Nat(..),-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           SSym0, SSym1, ZSym0,-#endif                           -- | Singleton type for 'Nat'.                           SNat, Sing (SZ, SS),-                          -- ** Smart constructors-                          -- | WARNING: Smart constructors are deprecated as of singletons 0.10,-                          -- so these are provided only for backward compatibility.-                          sZ, sS,                           -- ** Arithmetic functions and their singletons.                           min, Min, sMin, max, Max, sMax,-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           MinSym0, MinSym1, MinSym2,                           MaxSym0, MaxSym1, MaxSym2,-#endif                           (:+:), (:+),-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           (:+$), (:+$$), (:+$$$),-#endif                           (%+), (%:+), (:*), (:*:),-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           (:*$), (:*$$), (:*$$$),-#endif                           (%:*), (%*), (:-:), (:-),                           (:**:), (:**), (%:**), (%**),-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           (:-$), (:-$$), (:-$$$),-#endif                           (%:-), (%-),                           -- ** Type-level predicate & judgements                           Leq(..), (:<=), (:<<=),-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           (:<<=$),(:<<=$$),(:<<=$$$),-#endif                           (%:<<=), LeqInstance,                           boolToPropLeq, boolToClassLeq, propToClassLeq,                           LeqTrueInstance, propToBoolLeq,@@ -52,13 +36,13 @@                           nat, snat,                           -- * Properties of natural numbers                           succCongEq, plusCongR, plusCongL, succPlusL, succPlusR,-                          plusZR, plusZL, eqPreservesS, plusAssociative,+                          pluSZR, pluSZL, eqPreserveSS, plusAssociative,                           multAssociative, multComm, multZL, multZR, multOneL,                           multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR,                           plusMultDistr, multPlusDistr, multCongL, multCongR,                           sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent,                           eqSuccMinus, plusMinusEqL, plusMinusEqR,-                          zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,+                          zAbsorbsMinR, zAbsorbsMinL, pluSSR, plusNeutralR, plusNeutralL,                           leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,                           -- * Properties of ordering 'Leq'                           leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,@@ -69,49 +53,34 @@                           twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,                           Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten,                           Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty,-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                           ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0,                           SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0,                           ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0,                           EighteenSym0, NineteenSym0, TwentySym0,-#endif                           sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven,                           sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty,                           n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,                           N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20,-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708                            N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0,-#endif                           sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,                           sN15, sN16, sN17, sN18, sN19, sN20                          ) where-import Data.Singletons-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,-                                Min, MinSym0, MinSym1, MinSym2, SOrd (..))-import Data.Singletons.TH      (singletons)-#endif+import Data.Type.Natural.Compat+import Data.Type.Natural.Core+import Data.Type.Natural.Definitions hiding ((:<=))+ import           Data.Constraint           hiding ((:-))+import           Data.Singletons import           Data.Type.Monomorphic import           Language.Haskell.TH import           Language.Haskell.TH.Quote import           Prelude                   (Bool (..), Eq (..), Int,-                                            Integral (..), Ord ((<)), Show (..),-                                            error, id, otherwise, undefined,-                                            ($), (.))+                                            Integral (..), Ord ((<)), error,+                                            otherwise, ($), (.))+import           Prelude                   (Ord (..)) import qualified Prelude                   as P import           Proof.Equational-import           Unsafe.Coerce-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710-import Data.Type.Natural.Definitions hiding ((:<=))--- import Data.Type.Natural.Proofs.GHC710-import Prelude (Num (..), Ord (..))-#else-import Data.Type.Natural.Definitions--- import Data.Type.Natural.Proofs.GHC708-#endif-import Data.Type.Natural.Core  -------------------------------------------------- -- * Conversion functions.@@ -139,37 +108,32 @@   demote  (Monomorphic sn) = sNatToInt sn   promote n       | n < 0     = error "negative integer!"-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 708-      | n == 0    = Monomorphic sZ-      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn-#else       | n == 0    = Monomorphic SZ       | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn-#endif  -------------------------------------------------- -- * Properties ---------------------------------------------------plusZR :: SNat n -> n :+: Z :=: n-plusZR SZ     = Refl-plusZR (SS n) =+pluSZR :: SNat n -> n :+: 'Z :=: n+pluSZR SZ     = Refl+pluSZR (SS n) =  start (SS n %+ SZ)    =~= SS (n %+ SZ)-   === SS n          `because` cong' SS (plusZR n)+   === SS n          `because` cong' SS (pluSZR n) -eqPreservesS :: n :=: m -> S n :=: S m-eqPreservesS Refl = Refl+eqPreserveSS :: n :=: m -> 'S n :=: 'S m+eqPreserveSS Refl = Refl -plusZL :: SNat n -> Z :+: n :=: n-plusZL _ = Refl+pluSZL :: SNat n -> 'Z :+: n :=: n+pluSZL _ = Refl -succCongEq :: n :=: m -> S n :=: S m+succCongEq :: n :=: m -> 'S n :=: 'S m succCongEq Refl = Refl -snEqZAbsurd :: S n :=: Z -> a-snEqZAbsurd _ = bugInGHC "impossible!"+snEqZAbsurd :: 'S n :=: 'Z -> a+snEqZAbsurd _ = bugInGHC -succInjective :: S n :=: S m -> n :=: m+succInjective :: 'S n :=: 'S m -> n :=: m succInjective Refl = Refl  plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l@@ -183,7 +147,7 @@     === m %:+ l   `because` eq     === l %:+ m   `because` plusCommutative m l -sAndPlusOne :: SNat n -> S n :=: n :+: One+sAndPlusOne :: SNat n -> 'S n :=: n :+: One sAndPlusOne SZ = Refl sAndPlusOne (SS n) =   start (SS (SS n))@@ -200,8 +164,8 @@     =~= SS (n %+ m) %+ l     =~= (SS n %+ m) %+ l -plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m-plusSR n m =+pluSSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m+pluSSR n m =   start (SS (n %+ m))     === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)     === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)@@ -213,10 +177,10 @@ plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n plusCongR _ Refl = Refl -succPlusL :: SNat n -> SNat m -> S n :+ m :=: S (n :+ m)+succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m) succPlusL _ _ = Refl -succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m)+succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m) succPlusR SZ     _ = Refl succPlusR (SS n) m =   start (SS n %+ SS m)@@ -249,32 +213,35 @@     === m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)     === m %+ SS n        `because` plusCongL m (symmetry $ sAndPlusOne n) -eqSuccMinus :: ((m :<<= n) ~ True)-            => SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m))+eqSuccMinus :: ((m :<<= n) ~ 'True)+            => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m)) eqSuccMinus _      SZ     = Refl eqSuccMinus (SS n) (SS m) =   start (SS (SS n) %:- SS m)     =~= SS n %:- m     === SS (n %:- m)       `because` eqSuccMinus n m     =~= SS (SS n %:- SS m)+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 eqSuccMinus _ _ = bugInGHC+#endif + plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n plusMinusEqL SZ     m = minusNilpotent m plusMinusEqL (SS n) m =   case propToBoolLeq (plusLeqR n m) of-    Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)+    Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreserveSS $ plusMinusEqL n m)  plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m) -zAbsorbsMinR :: SNat n -> Min n Z :=: Z+zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z zAbsorbsMinR SZ     = Refl zAbsorbsMinR (SS n) =   case zAbsorbsMinR n of     Refl -> Refl -zAbsorbsMinL :: SNat n -> Min Z n :=: Z+zAbsorbsMinL :: SNat n -> Min 'Z n :=: 'Z zAbsorbsMinL SZ     = Refl zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl @@ -284,7 +251,7 @@ minComm (SS _) SZ = Refl minComm (SS n) (SS m) = case minComm n m of Refl -> Refl -maxZL :: SNat n -> Max Z n :=: n+maxZL :: SNat n -> Max 'Z n :=: n maxZL SZ = Refl maxZL (SS _) = Refl @@ -294,7 +261,7 @@ maxComm (SS _) SZ = Refl maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl -maxZR :: SNat n -> Max n Z :=: n+maxZR :: SNat n -> Max n 'Z :=: n maxZR n = transitivity (maxComm n SZ) (maxZL n)  multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l)@@ -380,14 +347,14 @@     === m %* (n %+ sOne)     `because` symmetry (multPlusDistr m n sOne)     === m %* SS n            `because` multCongL m (symmetry $ sAndPlusOne n) -plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: Z+plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: 'Z plusNeutralR SZ m eq =   start m     =~= SZ %:+ m     === SZ       `because` eq plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq -plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z+plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: 'Z plusNeutralL n m eq = plusNeutralR m n $   start (m %:+ n)     === n %:+ m   `because` plusCommutative m n@@ -401,14 +368,16 @@ leqRefl SZ = ZeroLeq SZ leqRefl (SS n) = SuccLeqSucc $ leqRefl n -leqSucc :: SNat n -> Leq n (S n)+leqSucc :: SNat n -> Leq n ('S n) leqSucc SZ = ZeroLeq sOne leqSucc (SS n) = SuccLeqSucc $ leqSucc n  leqTrans :: Leq n m -> Leq m l -> Leq n l leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 leqTrans _ _ = error "impossible!"+#endif  instance Preorder Leq where   reflexivity = leqRefl@@ -417,12 +386,12 @@ plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k) plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k) plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =-  case plusSR m (leqRhs leq) of+  case pluSSR m (leqRhs leq) of     Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'  plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)-plusLeqL SZ     m = ZeroLeq $ coerce (symmetry $ plusZL m) m+plusLeqL SZ     m = ZeroLeq $ coerce (symmetry $ pluSZL m) m plusLeqL (SS n) m =   start (SS n)     =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)@@ -443,8 +412,10 @@  leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl-leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2-leqAnitsymmetric _ _ = bugInGHC+leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreserveSS $ leqAnitsymmetric leq1 leq2+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+leqAnitsymmetric _ _ = error "impossible!"+#endif  maxLeqL :: SNat n -> SNat m -> Leq n (Max n m) maxLeqL SZ m = ZeroLeq (sMax SZ m)@@ -456,28 +427,37 @@ maxLeqR n m = case maxComm n m of                 Refl -> maxLeqL m n -leqSnZAbsurd :: Leq (S n) Z -> a-leqSnZAbsurd _ = error "cannot be occured"+leqSnZAbsurd :: Leq ('S n) 'Z -> a+leqSnZAbsurd = \case {} -leqnZElim :: Leq n Z -> n :=: Z+leqnZElim :: Leq n 'Z -> n :=: 'Z leqnZElim (ZeroLeq SZ) = Refl -leqSnLeq :: Leq (S n) m -> Leq n m+leqSnLeq :: Leq ('S n) m -> Leq n m leqSnLeq (SuccLeqSucc leq) =   let n = leqLhs leq       m = SS $ leqRhs leq   in start n        =<= SS n   `because` leqSucc n        =<= m      `because` SuccLeqSucc leq+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+leqSnLeq _ = bugInGHC+#endif -leqPred :: Leq (S n) (S m) -> Leq n m+leqPred :: Leq ('S n) ('S m) -> Leq n m leqPred (SuccLeqSucc leq) = leq+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+leqPred _ = bugInGHC+#endif -leqSnnAbsurd :: Leq (S n) n -> a+leqSnnAbsurd :: Leq ('S n) n -> a leqSnnAbsurd (SuccLeqSucc leq) =   case leqLhs leq of     SS _ -> leqSnnAbsurd leq+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800     _    -> bugInGHC "cannot be occured"+leqSnnAbsurd _ = bugInGHC+#endif  -------------------------------------------------- -- * Quasi Quoter

@@ -0,0 +1,328 @@+{-# LANGUAGE ConstraintKinds, CPP, DataKinds, GADTs, PolyKinds, RankNTypes #-}+{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances             #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+-- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@+module Data.Type.Natural.Builtin+       ( -- * Sysnonym to avoid confusion+         Peano,+         -- * Coercion between builtin type-level natural and peano numerals+         FromPeano, ToPeano, sFromPeano, sToPeano,+         -- * Properties of @'FromPeano'@ and @'ToPeano'@.+         fromPeanoInjective, toPeanoInjective,+         -- ** Bijection+         fromToPeano, toFromPeano,+         -- ** Algebraic isomorphisms+         fromPeanoZeroCong, toPeanoZeroCong,+         fromPeanoOneCong,  toPeanoOneCong,+         fromPeanoSuccCong, toPeanoSuccCong,+         fromPeanoPlusCong, toPeanoPlusCong,+         fromPeanoMultCong, toPeanoMultCong,+         fromPeanoMonotone, toPeanoMonotone,+         -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@+         plusZR, plusZL, plusSuccR, plusSuccL,+         multZR, multZL, multSuccR, multSuccL,+         inductionNat,+         plusComm, multComm, plusAssoc, multAssoc,+         plusMultDistr, multPlusDistr+       )+       where+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+import Data.Type.Natural.Compat+#endif++import Data.Promotion.Prelude.Enum (Succ)+import           Data.Singletons              (Sing, SingI, sing)+import           Data.Singletons.Decide       (Decision (..), (%~))+import           Data.Singletons.Decide       (Void)+import           Data.Singletons.Prelude.Bool (Sing (..))+import           Data.Singletons.Prelude.Enum (Pred, sPred, sSucc)+import           Data.Singletons.Prelude.Num  (SNum (..))+import           Data.Type.Natural            (Nat (S, Z), Sing (SS, SZ))+import           Data.Type.Natural            (plusCongR, succCongEq)+import qualified Data.Type.Natural            as PN+import           Data.Void                    (absurd)+import qualified GHC.TypeLits                 as TL+import           Proof.Equational             ((:=:), (:~:) (Refl), coerce)+import           Proof.Equational             (start, sym, (===), (=~=))+import           Proof.Equational             (because)+import           Unsafe.Coerce                (unsafeCoerce)++-- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.+type Peano = PN.Nat++type family FromPeano (n :: PN.Nat) :: TL.Nat where+  FromPeano 'Z = 0+  FromPeano ('S n) = Succ (FromPeano n)++type family ToPeano (n :: TL.Nat) :: PN.Nat where+  ToPeano 0 = 'Z+  ToPeano n = 'S (ToPeano (Pred n))++data NatView (n :: TL.Nat) where+  IsZero :: NatView 0+  IsSucc :: Sing n -> NatView (Succ n)++viewNat :: Sing n -> NatView n+viewNat n =+  case n %~ (sing :: Sing 0) of+    Proved Refl -> IsZero+    Disproved _ -> IsSucc (sPred n)++sFromPeano :: Sing n -> Sing (FromPeano n)+sFromPeano SZ = sing+sFromPeano (SS sn) = sSucc (sFromPeano sn)++toPeanoInjective :: ToPeano n :=: ToPeano m -> n :=: m+toPeanoInjective Refl = Refl++-- trustMe :: a :=: b+-- trustMe = unsafeCoerce (Refl :: () :=: ())+-- {-# WARNING trustMe+--     "Used unproven type-equalities; This may cause disastrous result..." #-}++toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: 'S (ToPeano n)+toPeanoSuccCong _ = unsafeCoerce (Refl :: () :=: ())+  -- We cannot prove this lemma within Haskell, so we assume it a priori.++sToPeano :: Sing n -> Sing (ToPeano n)+sToPeano sn =+  case sn %~ (sing :: Sing 0) of+    Proved Refl  -> SZ+    Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn)))++-- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat).+--                     Succ n :=: Succ m -> n :=: m+-- litSuccInjective Refl = Refl++toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n+toFromPeano SZ = Refl+toFromPeano (SS sn) =+  start (sToPeano (sFromPeano (SS sn)))+    =~= sToPeano (sSucc (sFromPeano sn))+    === SS (sToPeano (sFromPeano sn)) `because` toPeanoSuccCong (sFromPeano sn)+    === SS sn                         `because` succCongEq (toFromPeano sn)++congFromPeano :: n :=: m -> FromPeano n :=: FromPeano m+congFromPeano Refl = Refl++congToPeano :: n :=: m -> ToPeano n :=: ToPeano m+congToPeano Refl = Refl++congSucc :: n :=: m -> Succ n :=: Succ m+congSucc Refl = Refl++fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n+fromToPeano sn  =+  case viewNat sn of+    IsZero    -> Refl+    IsSucc n1 ->+      start (sFromPeano (sToPeano sn))+        =~= sFromPeano (sToPeano (sSucc n1))+        === sFromPeano (SS (sToPeano n1))+              `because` congFromPeano (toPeanoSuccCong n1)+        =~= sSucc (sFromPeano (sToPeano n1))+        === sSucc n1 `because` congSucc (fromToPeano n1)++fromPeanoInjective :: forall n m. (SingI n, SingI m)+                   => FromPeano n :=: FromPeano m -> n :=: m+fromPeanoInjective frEq =+  let sn = sing :: Sing n+      sm = sing :: Sing m+  in start sn+       === sToPeano (sFromPeano sn) `because` sym (toFromPeano sn)+       === sToPeano (sFromPeano sm) `because` congToPeano frEq+       === sm                       `because` toFromPeano sm++fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :=: Succ (FromPeano n)+fromPeanoSuccCong _sn = Refl++fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :=: FromPeano n TL.+ FromPeano m+fromPeanoPlusCong SZ _ = Refl+fromPeanoPlusCong (SS sn) sm =+  start (sFromPeano (SS sn %:+ sm))+    =~= sFromPeano (SS (sn %:+ sm))+    === sSucc (sFromPeano (sn %:+ sm))           `because` fromPeanoSuccCong (sn %:+ sm)+    === sSucc (sFromPeano sn  %:+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm)+    =~= sSucc (sFromPeano sn) %:+ sFromPeano sm+    =~= sFromPeano (SS sn)    %:+ sFromPeano sm++toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :=: ToPeano n PN.:+ ToPeano m+toPeanoPlusCong sn sm =+  case viewNat sn of+    IsZero -> Refl+    IsSucc pn ->+      start (sToPeano (sSucc pn %:+ sm))+        =~= sToPeano (sSucc (pn %:+ sm))+        === SS (sToPeano (pn %:+ sm))+            `because` toPeanoSuccCong (pn %:+ sm)+        === SS (sToPeano pn %:+ sToPeano sm)+            `because` succCongEq (toPeanoPlusCong pn sm)+        =~= SS (sToPeano pn) %:+ sToPeano sm+        === (sToPeano (sSucc pn) %:+ sToPeano sm)+            `because` plusCongR (sToPeano sm) (sym (toPeanoSuccCong pn))+        =~= sToPeano sn %:+ sToPeano sm++fromPeanoZeroCong :: FromPeano 'Z :=: 0+fromPeanoZeroCong = Refl++toPeanoZeroCong :: ToPeano 0 :=: 'Z+toPeanoZeroCong = Refl++fromPeanoOneCong :: FromPeano PN.One :=: 1+fromPeanoOneCong = Refl++toPeanoOneCong :: ToPeano 1 :=: PN.One+toPeanoOneCong = Refl++natPlusCongR :: Sing r -> n :=: m -> n TL.+ r :=: m TL.+ r+natPlusCongR _ Refl = Refl++fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :=: FromPeano n TL.* FromPeano m+fromPeanoMultCong SZ _ = Refl+fromPeanoMultCong (SS psn) sm =+  start (sFromPeano (SS psn %:* sm))+    =~= sFromPeano (psn %:* sm %:+ sm)+    === sFromPeano (psn %:* sm) %:+ sFromPeano sm+        `because` fromPeanoPlusCong (psn %:* sm) sm+    === sFromPeano psn %:* sFromPeano sm %:+ sFromPeano sm+        `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm)+    =~= sSucc (sFromPeano psn) %:* sFromPeano sm+    =~= sFromPeano (SS psn)    %:* sFromPeano sm+++toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :=: ToPeano n PN.:* ToPeano m+toPeanoMultCong sn sm =+  case viewNat sn of+    IsZero -> Refl+    IsSucc psn ->+      start (sToPeano (sSucc psn %:* sm))+        =~= sToPeano (psn %:* sm %:+ sm)+        === sToPeano (psn %:* sm) %:+ sToPeano sm+            `because` toPeanoPlusCong (psn %:* sm) sm+        === sToPeano psn %:* sToPeano sm %:+ sToPeano sm+            `because` plusCongR (sToPeano sm) (toPeanoMultCong psn sm)+        =~= SS (sToPeano psn) %:* sToPeano sm+        === sToPeano (sSucc psn) %:* sToPeano sm+            `because` PN.multCongR (sToPeano sm) (sym (toPeanoSuccCong psn))++infix 4 %:<=?+(%:<=?) :: Sing n -> Sing m -> Sing (n TL.<=? m)+sn %:<=? sm =+  case viewNat sn of+    IsZero -> STrue+    IsSucc pn -> case viewNat sm of+      IsZero -> SFalse+      IsSucc pm ->+        case pn %:<=? pm of+          STrue  -> STrue+          SFalse -> SFalse++natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) TL.<=? (m TL.+ 1)) :~: (n TL.<=? m)+natLeqSuccEq _ _ = Refl++leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z)+leqqCong Refl Refl = Refl++leqCong :: n :=: m -> l :=: z -> (n PN.:<<= l) :~: (m PN.:<<= z)+leqCong Refl Refl = Refl++fromPeanoMonotone :: ((n PN.:<<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True+fromPeanoMonotone SZ _ = Refl+fromPeanoMonotone (SS n) (SS m) =+   start (sFromPeano (SS n) %:<=? sFromPeano (SS m))+     === (sSucc (sFromPeano n) %:<=? sSucc (sFromPeano m))+      `because` leqqCong  (fromPeanoSuccCong n) (fromPeanoSuccCong m)+     === (sFromPeano n %:<=? sFromPeano m)+      `because` natLeqSuccEq (sFromPeano n) (sFromPeano m)+     === STrue+      `because` fromPeanoMonotone n m+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+fromPeanoMonotone _ _ = bugInGHC+#endif++natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0+natLeqZero _ = Refl++-- | Currently, ghc-typelits-natnormalise reduces @(0 - 1) + 1@ to @0@,+--   which is contradictory to current GHC's behaviour.+--   So our assumption @((n :~: 0) -> Void)@ is simply disregarded.+natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n+natSuccPred _ = Refl++myLeqPred :: Sing n -> Sing m -> ('S n PN.:<<= 'S m) :=: (n PN.:<<= m)+myLeqPred SZ _ = Refl+myLeqPred (SS _) (SS _) = Refl+myLeqPred (SS _) SZ = Refl++toPeanoCong :: a :=: b -> ToPeano a :=: ToPeano b+toPeanoCong Refl = Refl++toPeanoMonotone :: (n TL.<= m)+                => Sing n -> Sing m -> ((ToPeano n) PN.:<<= (ToPeano m)) :~: 'True+toPeanoMonotone sn sm =+  case sn %~ (sing :: Sing 0) of+    Proved Refl -> Refl+    Disproved nPos -> case sm %~ (sing :: Sing 0) of+      Proved Refl -> absurd $ nPos $ natLeqZero sm+      Disproved mPos ->+        let pn = sPred sn+            pm = sPred sm+        in start (sToPeano sn PN.%:<<= sToPeano sm)+             === (sToPeano (sSucc pn) PN.%:<<= sToPeano (sSucc pm))+                 `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos)+                                   (toPeanoCong $ sym $ natSuccPred mPos)+             === (SS (sToPeano pn) PN.%:<<= SS (sToPeano pm))+                 `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm)+             === (sToPeano pn PN.%:<<= sToPeano pm)+                 `because` myLeqPred (sToPeano pn) (sToPeano pm)+             === STrue `because` toPeanoMonotone pn pm++-- | Induction scheme for built-in @'TL.Nat'@.+inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m TL.+ 1)) -> Sing n -> p n+inductionNat base step snat =+  case viewNat snat of+    IsZero -> base+    IsSucc sl -> step (inductionNat base step sl)++plusZR :: Sing n -> n TL.+ 0 :~: n+plusZR _ = Refl++plusZL :: Sing n -> 0 TL.+ n :~: n+plusZL _ = Refl++plusSuccL :: Sing n -> Sing m -> (Succ n) TL.+ m :~: Succ (n TL.+ m)+plusSuccL _ _ =  Refl++plusSuccR :: Sing n -> Sing m -> n TL.+ (Succ m) :~: Succ (n TL.+ m)+plusSuccR _ _ =  Refl++multZL :: Sing n -> 0 TL.* n :~: 0+multZL _ = Refl++multZR :: Sing n -> n TL.* 0 :~: 0+multZR _ = Refl++multSuccL :: Sing n -> Sing m -> Succ n TL.* m :~: (n TL.* m) TL.+ m+multSuccL _ _ = Refl++multSuccR :: Sing n -> Sing m -> n TL.* Succ m :~: (n TL.* m) TL.+ n+multSuccR _ _ = Refl++plusComm :: Sing n -> Sing m -> (n TL.+ m) :~: (m TL.+ n)+plusComm _ _ = Refl++multComm :: Sing n -> Sing m -> (n TL.* m) :~: (m TL.* n)+multComm _ _ = Refl++plusAssoc :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.+ l :~: n TL.+ (m TL.+ l)+plusAssoc _ _ _ = Refl++multAssoc :: Sing n -> Sing m -> Sing l -> (n TL.* m) TL.* l :~: n TL.* (m TL.* l)+multAssoc _ _ _ = Refl++plusMultDistr :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.* l :~: n TL.* l TL.+  m TL.* l+plusMultDistr _ _ _ = Refl++multPlusDistr :: Sing n -> Sing m -> Sing l -> n TL.* (m TL.+ l) :~: n TL.* m TL.+  n TL.* l+multPlusDistr _ _ _ = Refl

@@ -0,0 +1,8 @@+{-# LANGUAGE CPP #-}+module Data.Type.Natural.Compat (bugInGHC) where+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+import Data.Singletons.Prelude (bugInGHC)+#else+bugInGHC :: a+bugInGHC = error "GHC case-analysis error!"+#endif

@@ -1,75 +1,47 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}-{-# LANGUAGE UndecidableInstances                                           #-}+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                 #-}+{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies          #-}+{-# LANGUAGE TypeOperators, UndecidableInstances                        #-} module Data.Type.Natural.Core where-import Data.Singletons-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,-                                Min, MinSym0, MinSym1, MinSym2, SOrd (..))-import Data.Singletons.TH      (singletons)-#endif-import           Data.Constraint           hiding ((:-))-import           Data.Type.Monomorphic-import           Language.Haskell.TH-import           Language.Haskell.TH.Quote-import           Prelude                   (Bool (..), Eq (..), Int,-                                            Integral (..), Ord ((<)), Show (..),-                                            error, id, otherwise, undefined,-                                            ($), (.))-import qualified Prelude                   as P-import           Proof.Equational-import           Unsafe.Coerce-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710-import Data.Type.Natural.Definitions hiding ((:<=))-import Prelude                       (Num (..))-#else-import Data.Type.Natural.Definitions+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+import Data.Type.Natural.Compat #endif ------------------------------------------------------- ** Convenient synonyms-----------------------------------------------------#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-sZ :: SNat Z-sZ = SZ--sS :: SNat n -> SNat (S n)-sS = SS--{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}-#endif+import Data.Constraint               hiding ((:-))+import Data.Type.Natural.Definitions hiding ((:<=))+import Prelude                       (Bool (..), Eq (..), Show (..), ($))+import Unsafe.Coerce  -------------------------------------------------- -- ** Type-level predicate & judgements. -------------------------------------------------- -- | Comparison via type-class. class (n :: Nat) :<= (m :: Nat)-instance Z :<= n-instance (n :<= m) => S n :<= S m+instance 'Z :<= n+instance (n :<= m) => 'S n :<= 'S m  -- | Comparison via GADTs. data Leq (n :: Nat) (m :: Nat) where   ZeroLeq     :: SNat m -> Leq Zero m-  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)+  SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m) -type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)+type LeqTrueInstance a b = Dict ((a :<<= b) ~ 'True) -(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)+(%-) :: (m :<<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m) n   %- SZ    = n SS n %- SS m = n %- m-_    %- _    = error "impossible!"+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+_    %- _    = bugInGHC+#endif  infixl 6 %- deriving instance Show (SNat n) deriving instance Eq (SNat n)  data (a :: Nat) :<: (b :: Nat) where-  ZeroLtSucc :: Zero :<: S m-  SuccLtSucc :: n :<: m -> S n :<: S m+  ZeroLtSucc :: Zero :<: 'S m+  SuccLtSucc :: n :<: m -> 'S n :<: 'S m  deriving instance Show (a :<: b) @@ -80,7 +52,7 @@ propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE propToBoolLeq #-} -boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE boolToClassLeq #-} @@ -93,40 +65,30 @@ propToBoolLeq :: Leq n m -> LeqTrueInstance n m propToBoolLeq (ZeroLeq _) = Dict propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict-{-# RULES- "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .-  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)- #-}  boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq SZ     _      = Dict boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict boolToClassLeq _ _ = bugInGHC-{-# RULES- "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).-  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)- #-}  propToClassLeq :: Leq n m -> LeqInstance n m propToClassLeq (ZeroLeq _) = Dict propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict-{-# RULES- "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .-  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)- #-} -}  type LeqInstance n m = Dict (n :<= m) -boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m+boolToPropLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> Leq n m boolToPropLeq SZ     m      = ZeroLeq m boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m-boolToPropLeq _      _      = bugInGHC+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+boolToPropLeq _      _     = bugInGHC+#endif  leqRhs :: Leq n m -> SNat m leqRhs (ZeroLeq m) = m-leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq+leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq  leqLhs :: Leq n m -> SNat n-leqLhs (ZeroLeq _) = sZ-leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq+leqLhs (ZeroLeq _) = SZ+leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq

@@ -22,21 +22,13 @@ import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,                                 Min, MinSym0, MinSym1, MinSym2, SOrd (..)) #endif-import Data.Singletons.TH (singletons) #endif-import           Data.Constraint           hiding ((:-))-import           Data.Type.Monomorphic-import           Data.Typeable             (Typeable)-import           Language.Haskell.TH-import           Language.Haskell.TH.Quote-import           Prelude                   (Bool (..), Eq (..), Int,-                                            Integral (..), Ord ((<)), Show (..),-                                            error, id, otherwise, undefined,-                                            ($), (.))-import qualified Prelude                   as P-import           Proof.Equational-import           Unsafe.Coerce+import           Data.Typeable (Typeable)+import           Prelude       (Bool (..), Eq (..), Show (..))+import qualified Prelude       as P ++ -------------------------------------------------- -- * Natural numbers and its singleton type --------------------------------------------------@@ -113,7 +105,7 @@     abs n = n      signum Z = Z-    signum (S n) = S Z+    signum (S _) = S Z      fromInteger n = if n == 0 then Z else S (fromInteger (n-1))  |]@@ -159,7 +151,7 @@  singletons [d|  (**) :: Nat -> Nat -> Nat- n ** Z = S Z+ _ ** Z = S Z  n ** S m = (n ** m) * n  |] 

@@ -1,11 +1,7 @@-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts         #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds      #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}-{-# LANGUAGE TypeFamilies, TypeOperators                              #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-{-# LANGUAGE EmptyCase, LambdaCase #-}-#endif+{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls   #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures      #-}+{-# LANGUAGE LambdaCase, PolyKinds, ScopedTypeVariables, StandaloneDeriving  #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                    #-} -- | Set-theoretic ordinal arithmetic module Data.Type.Ordinal        ( -- * Data-types@@ -21,34 +17,33 @@          -- * Quasi Quoter          od        ) where+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800+import Data.Type.Natural.Compat+#endif++import Control.Monad             (liftM) import Data.Constraint+import Data.Singletons.Prelude import Data.Type.Monomorphic-import Data.Type.Natural         hiding (promote)+import Data.Type.Natural+import Data.Typeable             (Typeable) import Language.Haskell.TH import Language.Haskell.TH.Quote-import Proof.Equational          (coerce) import Unsafe.Coerce-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-import Data.Singletons.Prelude-import Data.Typeable (Typeable)-#endif-import Control.Monad (liftM)  -- | Set-theoretic (finite) ordinals: -- -- > n = {0, 1, ..., n-1} ----- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal Z@ is isomorphic to @Void@.+-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. data Ordinal n where-  OZ :: Ordinal (S n)-  OS :: Ordinal n -> Ordinal (S n)+  OZ :: Ordinal ('S n)+  OS :: Ordinal n -> Ordinal ('S n) -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707--- | Since 0.2.3.0  +-- | Since 0.2.3.0 deriving instance Typeable Ordinal-#endif -- | Parsing always fails, because there are no inhabitant.-instance Read (Ordinal Z) where+instance Read (Ordinal 'Z) where   readsPrec _ _ = []  instance SingI n => Num (Ordinal n) where@@ -63,7 +58,7 @@   signum = error "What does Ordinal sign mean?"   fromInteger = unsafeFromInt . fromInteger -deriving instance Read (Ordinal n) => Read (Ordinal (S n))+deriving instance Read (Ordinal n) => Read (Ordinal ('S n)) deriving instance Show (Ordinal n) deriving instance Eq (Ordinal n) deriving instance Ord (Ordinal n)@@ -87,7 +82,7 @@ enumOrdinal SZ = [] enumOrdinal (SS n) = OZ : map OS (enumOrdinal n) -instance SingI n => Bounded (Ordinal (S n)) where+instance SingI n => Bounded (Ordinal ('S n)) where   minBound = OZ   maxBound =     case propToBoolLeq $ leqRefl (sing :: SNat n) of@@ -97,38 +92,32 @@ unsafeFromInt n =     case (promote n :: Monomorphic (Sing :: Nat -> *)) of       Monomorphic sn ->-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707-        case singInstance sn of-          SingInstance ->-#endif            case SS sn %:<<= (sing :: SNat n) of              STrue -> sNatToOrd' (sing :: SNat n) sn              SFalse -> error "Bound over!"  -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.-sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n+sNatToOrd' :: ('S m :<<= n) ~ 'True => SNat n -> SNat m -> Ordinal n sNatToOrd' (SS _) SZ = OZ sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 sNatToOrd' _ _ = bugInGHC+#endif  -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal n+sNatToOrd :: (SingI n, ('S m :<<= n) ~ 'True) => SNat m -> Ordinal n sNatToOrd = sNatToOrd' sing  data CastedOrdinal n where-  CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n+  CastedOrdinal :: ('S m :<<= n) ~ 'True => SNat m -> CastedOrdinal n --- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@.+-- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@. ordToSNat' :: Ordinal n -> CastedOrdinal n ordToSNat' OZ = CastedOrdinal SZ ordToSNat' (OS on) =   case ordToSNat' on of     CastedOrdinal m ->-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707      -      case singInstance m of-        SingInstance ->-#endif-          CastedOrdinal (SS m)+      CastedOrdinal (SS m)  -- | Convert @Ordinal n@ into monomorphic @SNat@ ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)@@ -145,12 +134,12 @@ ordToInt (OS n) = 1 + ordToInt n  -- | Inclusion function for ordinals.-inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m+inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-} {- -- The "proof" of the correctness of the above-inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m+inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m inclusion' (SS SZ) OZ = OZ inclusion' (SS (SS _)) OZ = OZ inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m@@ -158,7 +147,7 @@ -}  -- | Inclusion function for ordinals with codomain inferred.-inclusion :: ((n :<<= m) ~ True) => Ordinal n -> Ordinal m+inclusion :: ((n :<<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-} @@ -172,30 +161,28 @@ OS n @+ m =   case sing :: SNat n of     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800     _ -> bugInGHC+#endif --- | Since @Ordinal Z@ is logically not inhabited, we can coerce it to any value.+-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. -- -- Since 0.2.3.0-absurdOrd :: Ordinal Z -> a-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707+absurdOrd :: Ordinal 'Z -> a absurdOrd cs = case cs of {}-#else-absurdOrd _ = error "Impossible!"-#endif  -- | 'absurdOrd' for the value in 'Functor'.--- +-- --   Since 0.2.3.0-vacuousOrd :: Functor f => f (Ordinal Z) -> f a+vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a vacuousOrd = fmap absurdOrd  -- | 'absurdOrd' for the value in 'Monad'. --   This function will become uneccesary once 'Applicative' (and hence 'Functor') --   become the superclass of 'Monad'.--- +-- --   Since 0.2.3.0-vacuousOrdM :: Monad m => m (Ordinal Z) -> m a+vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a vacuousOrdM = liftM absurdOrd  -- | Quasiquoter for ordinals

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.3.0.0+version:             0.4.0.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural@@ -13,9 +13,8 @@ copyright:           (C) Hiromi ISHII 2013-2014 category:            Math build-type:          Simple-cabal-version:       >=1.8-tested-with:         GHC == 7.8.3, GHC == 7.8.4,-                     GHC == 7.10.2+cabal-version:       >= 1.10+tested-with:         GHC == 7.10.3, GHC == 8.0.1  source-repository head   Type: git@@ -23,18 +22,34 @@   library-  exposed-modules:     Data.Type.Natural, Data.Type.Ordinal-  other-modules:       Data.Type.Natural.Definitions,-                       Data.Type.Natural.Core-  build-depends:       base                     >= 4       && < 5-               ,       equational-reasoning     == 0.2.*-               ,       monomorphic              >= 0.0.3-               ,       template-haskell         >= 2.8     && < 2.11-               ,       constraints              >= 0.3     && < 0.5-  if impl(ghc < 7.8)-    build-depends:     singletons               == 0.8.*-  else-    if impl(ghc < 7.10)-      build-depends:     singletons               == 1.*-    else -      build-depends:     singletons               == 2.0.*+  ghc-options:         -Wall -O2 -fno-warn-orphans+  if impl(ghc >= 8.0.0)+    ghc-options:       -Wno-redundant-constraints+  exposed-modules:     Data.Type.Natural+                     , Data.Type.Ordinal+                     , Data.Type.Natural.Builtin+  other-modules:       Data.Type.Natural.Definitions+                     , Data.Type.Natural.Core+                     , Data.Type.Natural.Compat+  build-depends:       base                      >= 4       && < 5+                     , equational-reasoning      == 0.4.*+                     , monomorphic               >= 0.0.3+                     , template-haskell          >= 2.8     && < 3+                     , constraints               >= 0.3     && < 0.9+                     , ghc-typelits-natnormalise == 0.4.*+                     , ghc-typelits-presburger   == 0.1.*+                     , singletons                >= 2.0 && < 2.3++  default-language:    Haskell2010+  default-extensions:  DataKinds+                       PolyKinds+                       ConstraintKinds+                       GADTs+                       ScopedTypeVariables+                       TemplateHaskell+                       TypeFamilies+                       TypeOperators+                       MultiParamTypeClasses+                       UndecidableInstances+                       FlexibleContexts+                       FlexibleInstances