update for 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"

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