decidable 0.1.3.0 → 0.1.3.1

raw patch · 4 files changed

+32/−25 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• decidable.cabal +2/−2
• src/Data/Type/Predicate.hs +14/−6
• src/Data/Type/Predicate/Auto.hs +6/−17

@@ -1,6 +1,15 @@ Changelog ========= +Version 0.1.3.1+---------------++*October 26, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.3.1>++*   *BUGFIX* Remove overlapping `Auto` instances for `IsNothing` and `IsLeft`.+ Version 0.1.3.0 --------------- @@ -13,6 +22,7 @@ *   Added `Universe` instances (and appropriate `Elem` and `Auto` instances)     for `Proxy` (the null universe) and `Identity`. *   `Auto` instances for `IsNothing` and `IsLeft`.+  Version 0.1.2.0 ---------------

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 5deeebc3dd1fcd483724e8469079eba0875cd3698198d81352d5b3bd6c2696ef+-- hash: 8f4356d2d59f7c72a3fb5358dda90a0b36b47bb7fd03398fb1ed2c4c631a5a77  name:           decidable-version:        0.1.3.0+version:        0.1.3.1 synopsis:       Combinators for manipulating dependently-typed predicates. description:    This library provides combinators and typeclasses for working and manipulating                 type-level predicates in Haskell, which are represented as matchable type-level

@@ -90,7 +90,7 @@ -- -- -- Then, write the 'Apply' instance, to specify the type of the -- -- witnesses of that predicate--- instance 'Apply' (Not p) a = (p '@@' a) -> Void+-- instance 'Apply' (Not p) a = (p '@@' a) -> 'Void' -- @ -- -- See the source of "Data.Type.Predicate" and "Data.Type.Predicate.Logic"@@ -98,8 +98,8 @@ -- always-true predicate 'Evident': -- -- @--- data Evident :: Predicate k--- instance Apply Evident a = Sing a+-- data Evident :: 'Predicate' k+-- instance Apply Evident a = 'Sing' a -- @ -- -- And the "and" predicate combinator:@@ -272,7 +272,7 @@ -- function: -- -- @--- decideTC :: Sing a -> 'Decision' (T a)+-- 'decideTC' :: 'Sing' a -> 'Decision' (T a) -- @ -- -- Is essentially 'Decidable', except with /type constructors/ @k ->@@ -287,6 +287,10 @@  -- | The canonical deciding function for @'DecidableTC' t@. --+-- Note that because @t@ must be an injective type constructor, you can use+-- this without explicit type applications; the instance of 'DecidableTC'+-- can be inferred from the result type.+-- -- @since 0.1.1.0 decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a) decideTC = decide @(TyPred t)@@ -296,7 +300,7 @@ -- function: -- -- @--- proveTC :: Sing a -> T a+-- 'proveTC' :: 'Sing' a -> T a -- @ -- -- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@@@ -310,6 +314,10 @@  -- | The canonical proving function for @'DecidableTC' t@. --+-- Note that because @t@ must be an injective type constructor, you can use+-- this without explicit type applications; the instance of 'ProvableTC'+-- can be inferred from the result type.+-- -- @since 0.1.1.0 proveTC :: forall t a. ProvableTC t => Sing a -> t a proveTC = prove @(TyPred t)@@ -355,7 +363,7 @@ instance Provable (Not Impossible) where     prove x v = absurd $ v x --- | Decide @Not p@ based on decisions of @p@.+-- | Decide @'Not' p@ based on decisions of @p@. decideNot     :: forall p a. ()     => Decision (p @@ a)

@@ -107,7 +107,7 @@ -- compile-time.  You can use: -- -- @--- 'auto' @_ @(AutoProvable P) @x+-- 'auto' \@_ \@('AutoProvable' P) \@x -- @ -- -- to obtain a @P \@\@ x@.@@ -130,14 +130,14 @@ -- Example usage: -- -- @--- autoElem :: Index '[1,6,2,3] 2+-- 'autoElem' :: 'Index' '[1,6,2,3] 2 -- -- IS (IS IZ)        -- third spot -- @ -- -- And when used with 'Auto': -- -- @--- auto @_ @(In [] '[1,6,2,3]) @2+-- 'auto' \@_ \@('In' [] '[1,6,2,3]) \@2 -- -- IS (IS IZ) -- @ class AutoElem f (as :: f k) (a :: k) where@@ -250,18 +250,10 @@ instance SingI a => Auto IsJust ('Just a) where     auto = WitAny IJust sing --- | @since 0.1.3.0-instance Auto IsNothing 'Nothing where-    auto = \case WitAny i _ -> case i of {}- -- | @since 0.1.2.0 instance SingI a => Auto IsRight ('Right a) where     auto = WitAny IRight sing --- | @since 0.1.3.0-instance Auto IsLeft ('Left a) where-    auto = \case WitAny i _ -> case i of {}- -- | @since 0.1.2.0 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where     auto = WitAny NEHead sing@@ -270,9 +262,6 @@ instance SingI a => Auto (NotNull ((,) j)) '(w, a) where     auto = WitAny ISnd sing -instance Auto (Null Proxy) 'Proxy where-    auto = \case WitAny i _ -> case i of {}- instance SingI a => Auto (NotNull Identity) ('Identity a) where     auto = WitAny IId sing @@ -282,8 +271,8 @@ instance Auto (NotNull g) bs => Auto (NotNull (f :+: g)) ('InR bs) where     auto = anySumR $ auto @_ @(NotNull g) @bs --- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to not be--- true at compiletime.+-- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to+-- not be true at compiletime. -- -- @since 0.1.2.0 type AutoNot (p :: Predicate k) = Auto (Not p)@@ -291,7 +280,7 @@ -- | Disprove @p \@\@ a@ at compiletime. -- -- @--- autoNot @_ @p @a :: Not p @@ a+-- 'autoNot' \@_ \@p \@a :: 'Not' p '@@' a -- @ -- -- @since 0.1.2.0