constraints 0.10.1 → 0.11

raw patch · 5 files changed

+106/−25 lines, 5 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +16/−1
• constraints.cabal +6/−5
• src/Data/Constraint.hs +61/−10
• src/Data/Constraint/Forall.hs +7/−1
• src/Data/Constraint/Nat.hs +16/−8

@@ -1,3 +1,18 @@+0.11 [2019.05.10]+-----------------+* Introduce a `HasDict` type class for types that witness evidence of+  constraints, such as `Dict`, `(:-)`, `Coercion`, `(:~:)`, `(:~~:)`, and+  `TypeRep`.+* Generalize the types of `withDict` and `(\\)` to be polymorphic over+  any `HasDict` instance.+* Add `type (⊢) = (:-)`.+* Fix unsafe mistakes in the statements of `dividesDef` and `timesDiv` in+  `Data.Constraint.Nat`.+* Make the implementations of `Min` and `Max` reduce on more inputs in+  `Data.Constraint.Nat`.+* Add `minusNat` and `minusZero` functions to `Data.Constraint.Nat`.+* Support `hashable-1.3.*` and `semigroups-0.19.*`.+ 0.10.1 [2018.07.02] ------------------- * Allow building with GHC 8.6.@@ -41,7 +56,7 @@     when a type mismatch error is thrown   * Add `defer_` and `deferEither_`, counterparts to `defer` and `deferEither`     which do not require proxy arguments-  * Enable `PolyKinds`. This allows the `Deferrable (a ~ b` instance to be+  * Enable `PolyKinds`. This allows the `Deferrable (a ~ b)` instance to be     polykinded on all supported versions of GHC _except_ 7.10, where the kinds     must be `*` due to an old GHC bug   * Introduce a heterogeneous equality type `(:~~:)`, and use it to define a

@@ -1,6 +1,6 @@ name:          constraints category:      Constraints-version:       0.10.1+version:       0.11 license:       BSD2 cabal-version: >= 1.10 license-file:  LICENSE@@ -21,8 +21,9 @@              , GHC == 7.10.3              , GHC == 8.0.2              , GHC == 8.2.2-             , GHC == 8.4.3-             , GHC == 8.6.1+             , GHC == 8.4.4+             , GHC == 8.6.5+             , GHC == 8.8.1 extra-source-files: README.markdown                   , CHANGELOG.markdown @@ -51,9 +52,9 @@     binary >= 0.7.1 && < 0.9,     deepseq >= 1.3 && < 1.5,     ghc-prim,-    hashable >= 1.2 && < 1.3,+    hashable >= 1.2 && < 1.4,     mtl >= 2.1.2 && < 2.3,-    semigroups >= 0.17 && < 0.19,+    semigroups >= 0.17 && < 0.20,     transformers >= 0.3.0.0 && < 0.6,     transformers-compat >= 0.5 && < 1 

@@ -11,12 +11,17 @@ {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ >= 706+{-# LANGUAGE PolyKinds #-}+#endif #if __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableSuperClasses #-} #endif #if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710@@ -56,10 +61,12 @@     Constraint   -- * Dictionary   , Dict(Dict)+  , HasDict(..)   , withDict+  , (\\)   -- * Entailment   , (:-)(Sub)-  , (\\)+  , type (⊢)   , weaken1, weaken2, contract   , strengthen1, strengthen2   , (&&&), (***)@@ -78,11 +85,14 @@ import Control.DeepSeq import Control.Monad import Data.Complex+#if __GLASGOW_HASKELL__ >= 800 && __GLASGOW_HASKELL__ < 806+import Data.Kind+#endif import Data.Ratio #if !MIN_VERSION_base(4,11,0) import Data.Semigroup #endif-import Data.Data+import Data.Data hiding (TypeRep) import qualified GHC.Exts as Exts (Any) import GHC.Exts (Constraint) import Data.Bits (Bits)@@ -93,6 +103,12 @@ #if !MIN_VERSION_base(4,8,0) import Data.Word (Word) #endif+import Data.Coerce (Coercible)+import Data.Type.Coercion(Coercion(..))+#if MIN_VERSION_base(4,10,0)+import Data.Type.Equality (type (~~))+import Type.Reflection (TypeRep, typeRepKind, withTypeable)+#endif  -- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. --@@ -136,18 +152,59 @@ instance NFData (Dict c) where   rnf Dict = () +-- | Witnesses that a value of type @e@ contains evidence of the constraint @c@.+--+-- Mainly intended to allow ('\\') to be overloaded, since it's a useful operator.+class HasDict c e | e -> c where+  evidence :: e -> Dict c++instance HasDict a (Dict a) where+  evidence = Prelude.id++instance a => HasDict b (a :- b) where+  evidence (Sub x) = x++instance HasDict (Coercible a b) (Coercion a b) where+  evidence Coercion = Dict++instance HasDict (a ~ b) (a :~: b) where+  evidence Refl = Dict++#if MIN_VERSION_base(4,10,0)+instance HasDict (a ~~ b) (a :~~: b) where+  evidence HRefl = Dict++instance HasDict (Typeable k, Typeable a) (TypeRep (a :: k)) where+  evidence tr = withTypeable tr $ withTypeable (typeRepKind tr) Dict+#endif+ -- | From a 'Dict', takes a value in an environment where the instance -- witnessed by the 'Dict' is in scope, and evaluates it. -- -- Essentially a deconstruction of a 'Dict' into its continuation-style -- form. ---withDict :: Dict a -> (a => r) -> r-withDict d r = case d of+-- Can also be used to deconstruct an entailment, @a ':-' b@, using a context @a@.+--+-- @+-- withDict :: 'Dict' c -> (c => r) -> r+-- withDict :: a => (a ':-' c) -> (c => r) -> r+-- @+withDict :: HasDict c e => e -> (c => r) -> r+withDict d r = case evidence d of                  Dict -> r +infixl 1 \\ -- required comment++-- | Operator version of 'withDict', with the arguments flipped+(\\) :: HasDict c e => (c => r) -> e -> r+r \\ d = withDict d r+ infixr 9 :-+infixr 9 ⊢ +type (⊢) = (:-)+ -- | This is the type of entailment. -- -- @a ':-' b@ is read as @a@ \"entails\" @b@.@@ -244,12 +301,6 @@  instance a => NFData (a :- b) where   rnf (Sub Dict) = ()--infixl 1 \\ -- required comment---- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@-(\\) :: a => (b => r) -> (a :- b) -> r-r \\ Sub Dict = r  -------------------------------------------------------------------------------- -- Constraints form a Category

@@ -40,6 +40,12 @@ import Data.Constraint import Unsafe.Coerce (unsafeCoerce) +#if __GLASGOW_HASKELL__ >= 806+# define KVS(kvs) kvs+#else+# define KVS(kvs)+#endif+ {- The basic trick of this module is to use "skolem" types as test candidates  - for whether a class predicate holds, and if so assume that it holds for all  - types, unsafely coercing the typeclass dictionary.@@ -143,7 +149,7 @@ instance Forall (Q p t) => ForallT p t  -- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.-instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)+instT :: forall KVS(k1 k2 k3 k4) (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a) instT = Sub $   case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->   case inst :: Forall (R p t f) :- R p t f a of

@@ -10,6 +10,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE UndecidableInstances #-} #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif@@ -18,8 +19,8 @@ -- This module is only available on GHC 8.0 or later. module Data.Constraint.Nat   ( Min, Max, Lcm, Gcd, Divides, Div, Mod-  , plusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat-  , plusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne+  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat+  , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne   , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates   , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes   , plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm@@ -47,13 +48,14 @@  import Data.Constraint import Data.Proxy+import Data.Type.Bool import GHC.TypeLits import Unsafe.Coerce  type family Min (m::Nat) (n::Nat) :: Nat where-    Min m m = m+    Min m n = If (n <=? m) n m type family Max (m::Nat) (n::Nat) :: Nat where-    Max m m = m+    Max m n = If (n <=? m) m n #if !(MIN_VERSION_base(4,11,0)) type family Div (m::Nat) (n::Nat) :: Nat where     Div m 1 = m@@ -114,6 +116,9 @@ plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m) plusNat = magic (+) +minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)+minusNat = Sub $ case magic @n @m (-) of Sub r -> r+ minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m) minNat = magic min @@ -135,6 +140,9 @@ plusZero :: forall n. Dict ((n + 0) ~ n) plusZero = Dict +minusZero :: forall n. Dict ((n - 0) ~ n)+minusZero = Dict+ timesZero :: forall n. Dict ((n * 0) ~ 0) timesZero = Dict @@ -142,10 +150,10 @@ timesOne = Dict  minZero :: forall n. Dict (Min n 0 ~ 0)-minZero = axiom+minZero = Dict  maxZero :: forall n. Dict (Max n 0 ~ n)-maxZero = axiom+maxZero = Dict  powZero :: forall n. Dict ((n ^ 0) ~ 1) powZero = Dict@@ -324,13 +332,13 @@ dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c) dividesMax = Sub axiom -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ a)+dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b) dividesDef = Sub axiom  dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n) dividesPow = Sub axiom -timesDiv :: forall a b. Dict ((a * Div b a) <= a)+timesDiv :: forall a b. Dict ((a * Div b a) <= b) timesDiv = axiom  -- (<=) is an internal category in the category of constraints.