diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs --- a/Data/Type/Natural/Class/Arithmetic.hs +++ b/Data/Type/Natural/Class/Arithmetic.hs @@ -294,7 +294,7 @@ multZeroR sn0 = multZeroRProof $ induction base step sn0 where base :: MultZeroR (Zero nat) - base = MultZeroR (multZeroR sZero) + base = MultZeroR (multZeroL sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k) step sk (MultZeroR ih) = MultZeroR $ diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs --- a/Data/Type/Natural/Class/Order.hs +++ b/Data/Type/Natural/Class/Order.hs @@ -2,6 +2,10 @@ {-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-} +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 +{-# LANGUAGE StandaloneKindSignatures #-} +#endif + module Data.Type.Natural.Class.Order (PeanoOrder(..), DiffNat(..), LeqView(..), FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR, @@ -62,12 +66,28 @@ => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m) succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m -coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l - -> IsTrue (n <= l) -> IsTrue (m <= l) +-- | Since 0.9.0.0 (type changed) +coerceLeqL +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 + :: forall nat (n :: nat) m l. +#else + :: forall (n :: nat) m l . +#endif + IsPeano nat + => n :~: m -> Sing l + -> IsTrue (n <= l) -> IsTrue (m <= l) coerceLeqL Refl _ Witness = Witness -coerceLeqR :: forall (n :: nat) m l . IsPeano nat => Sing l -> n :~: m - -> IsTrue (l <= n) -> IsTrue (l <= m) +-- | Since 0.9.0.0 (type changed) +coerceLeqR +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 + :: forall nat (n :: nat) m l . +#else + :: forall (n :: nat) m l . +#endif + IsPeano nat + => Sing l -> n :~: m + -> IsTrue (l <= n) -> IsTrue (l <= m) coerceLeqR _ Refl Witness = Witness singletonsOnly [d| diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs --- a/Data/Type/Natural/Definitions.hs +++ b/Data/Type/Natural/Definitions.hs @@ -3,6 +3,10 @@ {-# LANGUAGE KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-} {-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 +{-# LANGUAGE StandaloneKindSignatures #-} +#endif + module Data.Type.Natural.Definitions (module Data.Type.Natural.Definitions, module Data.Singletons.Prelude, diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -122,7 +122,8 @@ enumFrom = enumFromOrd enumFromTo = enumFromToOrd -enumFromToOrd :: forall (n :: nat). +-- | Since 0.9.0.0 (type changed) +enumFromToOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI n) => Ordinal n -> Ordinal n -> [Ordinal n] enumFromToOrd ok ol = @@ -130,7 +131,8 @@ l = ordToInt ol in genericTake (l - k + 1) $ enumFromOrd ok -enumFromOrd :: forall (n :: nat). +-- | Since 0.9.0.0 (type changed) +enumFromOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI n) => Ordinal n -> [Ordinal n] enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) @@ -139,7 +141,8 @@ enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n] enumOrdinal sn = withSingI sn $ map (reallyUnsafeNaturalToOrd Proxy) [0..toNatural sn - 1] -succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) +-- | Since 0.9.0.0 (type changed) +succOrd :: forall nat (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) succOrd (OLt n) = withRefl (succLneqSucc n (sing :: Sing n)) $ OLt (sSucc n) @@ -163,8 +166,8 @@ {-# INLINE maxBound #-} {-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-} --- | Since 0.8.0.0 -unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) +-- | Since 0.9.0.0 (type changed) +unsafeFromInt :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Int -> Ordinal n unsafeFromInt = unsafeNaturalToOrd . fromIntegral @@ -172,7 +175,7 @@ -- If the given natural is greater or equal to @n@, raises exception. -- -- Since 0.8.0.0 -unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) +unsafeNaturalToOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Natural -> Ordinal n unsafeNaturalToOrd k = fromMaybe (error "unsafeNaturalToOrd Out of bound") $ @@ -180,12 +183,12 @@ {-# DEPRECATED unsafeFromInt' "Use unsafeNaturalToOrd' instead" #-} -- | Since 0.8.0.0 -unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) +unsafeFromInt' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Int -> Ordinal n unsafeFromInt' p = unsafeNaturalToOrd' p . fromIntegral -- | Since 0.8.0.0 -unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) +unsafeNaturalToOrd' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Natural -> Ordinal n unsafeNaturalToOrd' _ n = case fromNatural n of @@ -269,7 +272,9 @@ -- | Ordinal addition. -(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m) +-- +-- Since 0.9.0.0 (type changed) +(@+) :: forall nat (n :: nat) m. (PeanoOrder nat, SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m) OLt k @+ OLt l = let (n, m) = (n :: Sing n, m :: Sing m) diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural -version: 0.8.3.1 +version: 0.9.0.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. . @@ -18,7 +18,8 @@ category: Math build-type: Simple cabal-version: >= 1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.3, GHC == 8.8.2 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, + GHC == 8.6.3, GHC == 8.8.3, GHC == 8.10.1 source-repository head Type: git @@ -47,7 +48,7 @@ , template-haskell >= 2.8 , constraints >= 0.3 , ghc-typelits-natnormalise >= 0.4 - , singletons >= 2.2 && < 2.6 + , singletons >= 2.2 && < 2.8 default-language: Haskell2010 default-extensions: DataKinds