Merge branch 'ghc-8.8'

CHANGELOG.md

@@ -1,6 +1,20 @@
 Changelog
 =========
 
+Version 0.3.0.0
+---------------
+
+*Feburary 2, 2020*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.3.0.0>
+
+*   Update to work with *singletons-2.6*, the type family update
+*   Change `Evident` to now be a defunctionalization symbol for `Sing`, instead
+    of a type synonym with `TyPred`, to match with *singletons-2.6*.  Most code
+    in practice should be the same.
+*   Fix instances for `FProd`s: now can prove and decide any `FProd f (Wit p)`,
+    and can prove and decide and auto any `FProd f WrappedSing`.
+
 Version 0.2.1.0
 ---------------
 

package.yaml

@@ -1,5 +1,5 @@
 name:                decidable
-version:             0.2.1.0
+version:             0.3.0.0
 github:              "mstksg/decidable"
 license:             BSD3
 author:              "Justin Le"
@@ -29,11 +29,11 @@ ghc-options:
 - -Werror=incomplete-patterns
 
 dependencies:
-- base >= 4.11 && < 5
-- singletons >= 2.5
+- base >= 4.13 && < 5
+- singletons >= 2.6
 - vinyl
 - microlens
-- functor-products
+- functor-products >= 0.1.1
 
 library:
   source-dirs: src

src/Data/Type/Predicate.hs

@@ -134,7 +134,8 @@ type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
 -- @
 -- 'Evident' :: 'Predicate' k
 -- @
-type Evident = (TyPred Sing :: Predicate k)
+data Evident :: Predicate k
+type instance Apply Evident a = Sing a
 
 -- | The always-false predicate
 --
@@ -361,36 +362,118 @@ instance Decidable Evident
 instance Provable Evident where
     prove = id
 
--- | @since 2.0.0
-instance Provable (TyPred (Rec Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (Rec Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PMaybe Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PMaybe Sing))
--- | @since 2.0.0
-instance Provable (TyPred (NERec Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (NERec Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PIdentity Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PIdentity Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PEither Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PEither Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PTup Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PTup Sing))
+-- | @since 3.0.0
+instance Decidable (TyPred WrappedSing)
+-- | @since 3.0.0
+instance Provable (TyPred WrappedSing) where
+    prove = WrapSing
+
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (Rec (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
+    decide = \case
+      SNil         -> Proved RNil
+      x `SCons` xs -> case decide @p x of
+        Proved p -> case decideTC xs of
+          Proved ps -> Proved $ Wit p :& ps
+          Disproved vs -> Disproved $ \case
+            _ :& ps -> vs ps
+        Disproved v -> Disproved $ \case
+          Wit p :& _ -> v p
+
+-- | @since 3.0.0
+instance Provable (TyPred (Rec WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (Rec WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
+    decide = \case
+      SNothing -> Proved PNothing
+      SJust x  -> mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)
+                . decide @p
+                $ x
+
+-- | @since 3.0.0
+instance Provable (TyPred (PMaybe WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PMaybe WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (NERec (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (NERec (Wit p))) where
+    decide = \case
+      x NE.:%| xs -> case decide @p x of
+        Proved p -> case decideTC xs of
+          Proved ps -> Proved $ Wit p :&| ps
+          Disproved vs -> Disproved $ \case
+            _ :&| ps -> vs ps
+        Disproved v -> Disproved $ \case
+          Wit p :&| _ -> v p
+
+-- | @since 3.0.0
+instance Provable (TyPred (NERec WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (NERec WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
+    decide = \case
+      SIdentity x -> mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)
+                   . decide @p
+                   $ x
+
+-- | @since 3.0.0
+instance Provable (TyPred (PIdentity WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PIdentity WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PEither (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
+    decide = \case
+      SLeft  x -> Proved $ PLeft x
+      SRight y -> mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)
+                . decide @p
+                $ y
+
+-- | @since 3.0.0
+instance Provable (TyPred (PEither WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PEither WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PTup (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
+    decide (STuple2 x y) = mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)
+                         . decide @p
+                         $ y
+
+-- | @since 3.0.0
+instance Provable (TyPred (PTup WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PTup WrappedSing))
 
 instance (Decidable p, SingI f) => Decidable (PMap f p) where
     decide = decide @p . applySing (sing :: Sing f)

src/Data/Type/Predicate/Auto.hs

@@ -180,7 +180,7 @@ instance AutoElem Identity ('Identity a) a where
     autoElem = IId
 
 instance AutoElem f as a => Auto (In f as) a where
-    auto = autoElem @f @as @a
+    auto = autoElem @_ @f @as @a
 
 -- | Helper class for deriving 'Auto' instances for 'All' predicates; each
 -- 'Universe' instance is expected to implement these if possible, to get
@@ -200,7 +200,7 @@ instance AutoAll [] p '[] where
 instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
     autoAll = WitAll $ \case
         IZ   -> auto @_ @p @a
-        IS i -> runWitAll (autoAll @[] @p @as) i
+        IS i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance AutoAll Maybe p 'Nothing where
     autoAll = WitAll $ \case {}
@@ -217,7 +217,7 @@ instance Auto p a => AutoAll (Either j) p ('Right a) where
 instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
     autoAll = WitAll $ \case
         NEHead   -> auto @_ @p @a
-        NETail i -> runWitAll (autoAll @[] @p @as) i
+        NETail i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance Auto p a => AutoAll ((,) j) p '(w, a) where
     autoAll = WitAll $ \case ISnd -> auto @_ @p @a
@@ -227,7 +227,7 @@ instance Auto p a => AutoAll Identity p ('Identity a) where
 
 -- | @since 0.1.2.0
 instance AutoAll f p as => Auto (All f p) as where
-    auto = autoAll @f @p @as
+    auto = autoAll @_ @f @p @as
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull []) (a ': as) where
@@ -301,7 +301,7 @@ autoAny i = WitAny i (auto @_ @p @a)
 
 -- | @since 0.1.2.0
 instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
-    auto = allNotNone sing $ autoAll @f @(Not p) @as
+    auto = allNotNone sing $ autoAll @_ @f @(Not p) @as
 
 -- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out
 -- a specific @a@ in @as@ where the predicate is disprovable at compile-time.
@@ -321,21 +321,40 @@ instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch
     auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))
          $ auto @_ @(Not (Any f (Found p))) @as
 
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (Rec Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PMaybe Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (NERec Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PEither Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PTup Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PIdentity Sing)) as where
-    auto = singProd sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (Rec WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (NERec WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PEither WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PTup WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where
+    auto = proveTC sing
+
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where
+    auto = proveTC sing

src/Data/Type/Predicate/Logic.hs

@@ -42,7 +42,6 @@ module Data.Type.Predicate.Logic (
 
 import           Data.Singletons
 import           Data.Singletons.Decide
-import           Data.Singletons.Prelude.Bool (Sing(..))
 import           Data.Type.Predicate
 import           Data.Void
 

stack.yaml

@@ -18,7 +18,7 @@
 #
 # resolver: ./custom-snapshot.yaml
 # resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: nightly-2019-08-03
+resolver: nightly-2020-01-31
 
 # User packages to be built.
 # Various formats can be used as shown in the example below.
@@ -35,20 +35,14 @@ resolver: nightly-2019-08-03
 #  - wai
 packages:
 - .
-# - location:
-#     git: https://github.com/goldfirere/singletons.git
-#     commit: c776637d11055ac1c47ddf7e96c7ed9067687041
-#   extra-dep: true
-# - location:
-#     git: https://github.com/goldfirere/th-desugar.git
-#     commit: 6dfdb7aa076b79d2595e4338c5e8192b1782de87
-#   extra-dep: true
 
 # Dependency packages to be pulled from upstream that are not in the resolver
 # using the same syntax as the packages field.
 # (e.g., acme-missiles-0.3)
 extra-deps:
-- functor-products-0.1.0.0
+- functor-products-0.1.1.0
+- singletons-2.6
+- vinyl-0.12.0
 # - github: mstksg/functor-products
 #   commit: 476b961bb007d7ee9aa0e60500c1473bc4a34e73
 

stack.yaml.lock

@@ -5,15 +5,29 @@
 
 packages:
 - completed:
-    hackage: functor-products-0.1.0.0@sha256:cc5e526b5f3694d33a89044578e4fe74e4e05dd01d5d96bc57be06d6d98a1883,1455
+    hackage: functor-products-0.1.1.0@sha256:2bea36b6106b5756be6b81b3a5bfe7b41db1cf45fb63c19a1f04b572ba90fd0c,1456
     pantry-tree:
       size: 408
-      sha256: 33712b9ee5c4491bcf320dc53618dba0f765a1ece19e26336fa9ed2aa3809365
+      sha256: 6c7d58498a2c23338baa8275a51e9099739812b1bd36126f887e5cdf57cce45b
   original:
-    hackage: functor-products-0.1.0.0
+    hackage: functor-products-0.1.1.0
+- completed:
+    hackage: singletons-2.6@sha256:e8e9cea442e37f565fab8604fe54f78c776421e54ed67ac6b4c454e11991db0b,7167
+    pantry-tree:
+      size: 23889
+      sha256: 0b51b772102a36eca4522cbcf564e8966a8756ca2cd51cc377a9771dbc9f88c6
+  original:
+    hackage: singletons-2.6
+- completed:
+    hackage: vinyl-0.12.0@sha256:6136e2608c2c4be0c112944fb0f5a6a0df56b50adec12eb1b7240258abfcf9b1,3790
+    pantry-tree:
+      size: 1857
+      sha256: aeb9e0e1a3bbe2b1f048a096430d240964a31c6936a1da89f4b32e931eba9d69
+  original:
+    hackage: vinyl-0.12.0
 snapshots:
 - completed:
-    size: 523441
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2019/8/3.yaml
-    sha256: 096b436543020fde7f0dd0ceb029c4a324977e7e8feb64e6b2a90f7906db21d3
-  original: nightly-2019-08-03
+    size: 471739
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2020/1/31.yaml
+    sha256: 33d27fc35a58c51d7a8873c8538e64053560031210613cb218232f398c266f82
+  original: nightly-2020-01-31