diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs --- a/Data/Type/Natural/Builtin.hs +++ b/Data/Type/Natural/Builtin.hs @@ -376,13 +376,16 @@ {-# SPECIALISE instance PeanoOrder TL.Nat #-} eqlCmpEQ _ _ Refl = Refl ltToLeq _ _ Refl = Witness - succLeqToLT m n Witness = - case sCompare (sSucc m) n of - SLT -> Refl - SEQ -> Refl -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 - _ -> bugInGHC -#endif + succLeqToLT n m w = case sCompare n m of + SEQ -> eliminate $ + start SLT === sCompare n m `because` sym (leqToLT n m w) + === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) + =~= SEQ + SGT -> eliminate $ + start SLT === sCompare n m `because` sym (leqToLT n m w) + =~= SGT + SLT -> Refl + cmpZero _ = Refl leqRefl _ = Witness eqToRefl _ _ Refl = Refl @@ -397,7 +400,7 @@ leqToMin _ _ Witness = Refl leqToMax _ _ Witness = Refl - geqToMax n m mLEQn = + geqToMax n m mLEQn@Witness = case leqToCmp m n mLEQn of Left eql -> withRefl eql Refl Right mLTn -> 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 @@ -1,8 +1,8 @@ -{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-} +{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-} -{-# LANGUAGE TypeInType, ViewPatterns , ExplicitNamespaces #-} +{-# LANGUAGE TypeInType, ViewPatterns #-} module Data.Type.Natural.Class.Arithmetic (Zero, One, S, sZero, sOne, ZeroOrSucc(..), plusCong, plusCongR, plusCongL, succCong, @@ -11,22 +11,25 @@ IsPeano(..), pattern Zero, pattern Succ, module Data.Type.Natural.Singleton.Compat ) where -import Data.Type.Natural.Singleton.Compat - (type (/=), type (==), type (+), type (*), type (-) - ,type (/=@#@$) ,type (/=@#@$$), type (/=@#@$$$) - ,type (==@#@$) ,type (==@#@$$), type (==@#@$$$) - ,type (+@#@$) ,type (+@#@$$), type (+@#@$$$) - ,type (*@#@$) ,type (*@#@$$), type (*@#@$$$) - ,type (-@#@$) ,type (-@#@$$), type (-@#@$$$) - ,(%==), (%/=), (%+), (%*), (%-) - , FromInteger, FromIntegerSym0, FromIntegerSym1 - ,SNum(..), PNum(..) - ) +import Data.Type.Natural.Singleton.Compat (type (*), type (*@#@$), + type (*@#@$$), type (*@#@$$$), + type (+), type (+@#@$), + type (+@#@$$), type (+@#@$$$), + type (-), type (-@#@$), + type (-@#@$$), type (-@#@$$$), + type (/=), type (/=@#@$), + type (/=@#@$$), type (/=@#@$$$), + type (==), type (==@#@$), + type (==@#@$$), type (==@#@$$$), + FromInteger, FromIntegerSym0, + FromIntegerSym1, PNum (..), + SNum (..), (%*), (%+), (%-), (%/=), + (%==)) import Data.Functor.Const (Const (..)) import Data.Singletons.Decide (SDecide (..)) -import Data.Singletons.Prelude (Apply, SingI (..), SingKind (..), - SomeSing (..), Sing) +import Data.Singletons.Prelude (Apply, Sing, SingI (..), SingKind (..), + SomeSing (..)) import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc) import Data.Type.Equality ((:~:) (..)) import Data.Void (Void, absurd) @@ -570,3 +573,4 @@ pattern Succ n <- (zeroOrSucc -> IsSucc n) where Succ n = sSucc n +{-# COMPLETE Zero, Succ #-} 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 @@ -10,7 +10,6 @@ ) where import Data.Type.Natural.Singleton.Compat -import Data.Promotion.Prelude.Enum import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum import Data.Singletons.TH diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -56,6 +56,8 @@ data Ordinal (n :: nat) where OLt :: (IsPeano nat, (n < m) ~ 'True) => Sing (n :: nat) -> Ordinal m +{-# COMPLETE OLt #-} + fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n < Succ m) ~ 'True, SingI m) => Sing (n :: nat) -> Ordinal m fromOLt n = diff --git a/Data/Type/Ordinal/Builtin.hs b/Data/Type/Ordinal/Builtin.hs --- a/Data/Type/Ordinal/Builtin.hs +++ b/Data/Type/Ordinal/Builtin.hs @@ -50,6 +50,7 @@ pattern OLt :: () => forall (n1 :: Nat). ((n1 SC.< t) ~ 'True) => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n +{-# COMPLETE OLt #-} -- | Pattern synonym representing the 0-th ordinal. -- diff --git a/Data/Type/Ordinal/Peano.hs b/Data/Type/Ordinal/Peano.hs --- a/Data/Type/Ordinal/Peano.hs +++ b/Data/Type/Ordinal/Peano.hs @@ -49,6 +49,7 @@ pattern OLt :: () => forall (n1 :: Nat). ((n1 < t) ~ 'True) => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n +{-# COMPLETE OLt #-} -- | Pattern synonym representing the 0-th ordinal. -- 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.2.0 +version: 0.8.3.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. . @@ -18,7 +18,7 @@ category: Math build-type: Simple cabal-version: >= 1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.3, GHC == 8.8.2 source-repository head Type: git @@ -29,6 +29,7 @@ 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.Ordinal.Builtin @@ -46,8 +47,7 @@ , template-haskell >= 2.8 , constraints >= 0.3 , ghc-typelits-natnormalise >= 0.4 - , ghc-typelits-presburger >= 0.2.0.0 - , singletons >= 2.2 && < 2.5 + , singletons >= 2.2 && < 2.6 default-language: Haskell2010 default-extensions: DataKinds @@ -62,3 +62,9 @@ UndecidableInstances FlexibleContexts FlexibleInstances + if impl(ghc >= 8.6) + default-extensions: NoStarIsType + if impl(ghc >= 8.4) + build-depends: ghc-typelits-presburger >= 0.3 && <0.4 + else + build-depends: ghc-typelits-presburger >= 0.2 && <0.3