polysemy-check 0.3.0.0 → 0.4.0.0

raw patch · 10 files changed

+202/−86 lines, 10 filesdep ~kind-genericsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: kind-generics

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• polysemy-check.cabal +5/−3
• src/Generics/Kind/Unexported.hs +51/−0
• src/Polysemy/Check.hs +4/−1
• src/Polysemy/Check/Arbitrary.hs +2/−2
• src/Polysemy/Check/Arbitrary/AnyEff.hs +10/−9
• src/Polysemy/Check/Arbitrary/Generic.hs +54/−45
• src/Polysemy/Check/Arbitrary/Generic.hs-boot +4/−3
• test/LawSpec.hs +25/−23
• test/WeirdEffectsSpec.hs +41/−0

@@ -1,5 +1,11 @@ # Changelog for polysemy-check +## v0.4.0.0 (2021-10-12)++- `GArbitraryK` now supports actions that contain existential types.+- (Internal) Aggressively rewrote the `GArbitraryK` typeclass to make better use+    of `kind-generics`.+ ## v0.3.0.0 (2021-10-09)  - `prepropLaw` now synthesizes a monadic prelude and postlude to your laws, to

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           polysemy-check-version:        0.3.0.0+version:        0.4.0.0 synopsis:       QuickCheck for Polysemy description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme> category:       Polysemy@@ -27,6 +27,7 @@  library   exposed-modules:+      Generics.Kind.Unexported       Polysemy.Check       Polysemy.Check.Arbitrary       Polysemy.Check.Arbitrary.AnyEff@@ -60,7 +61,7 @@       QuickCheck     , base >=4.7 && <5     , containers-    , kind-generics+    , kind-generics <=0.4.1.0     , kind-generics-th     , polysemy   default-language: Haskell2010@@ -72,6 +73,7 @@       CommutativeSpec       EquivSpec       LawSpec+      WeirdEffectsSpec       Paths_polysemy_check   hs-source-dirs:       test@@ -101,7 +103,7 @@     , base >=4.7 && <5     , containers     , hspec-    , kind-generics+    , kind-generics <=0.4.1.0     , kind-generics-th     , polysemy     , polysemy-check

@@ -0,0 +1,51 @@+module Generics.Kind.Unexported where++import Generics.Kind hiding (SubstRep)+++class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where+  type family SubstRep f x :: LoT k -> *+  substRep   :: f (x ':&&: xs) -> SubstRep f x xs+  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)++instance SubstRep' U1 x xs where+  type SubstRep U1 x = U1+  substRep   U1 = U1+  unsubstRep U1 = U1++instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where+  type SubstRep (f :+: g)  x = (SubstRep f x) :+: (SubstRep g x)+  substRep   (L1 x) = L1 (substRep   x)+  substRep   (R1 x) = R1 (substRep   x)+  unsubstRep (L1 x) = L1 (unsubstRep x)+  unsubstRep (R1 x) = R1 (unsubstRep x)++instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where+  type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x)+  substRep   (x :*: y) = substRep   x :*: substRep   y+  unsubstRep (x :*: y) = unsubstRep x :*: unsubstRep y++instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where+  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)+  substRep   (M1 x) = M1 (substRep   x)+  unsubstRep (M1 x) = M1 (unsubstRep x)++instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)+         => SubstRep' (c :=>: f) x xs where+  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)+  substRep   (SuchThat x) = SuchThat (substRep   x)+  unsubstRep (SuchThat x) = SuchThat (unsubstRep x)++instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs))+         => SubstRep' (Field t) x xs where+  type SubstRep (Field t) x = Field (SubstAtom t x)+  substRep   (Field x) = Field x+  unsubstRep (Field x) = Field x++type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where+  SubstAtom ('Var 'VZ)     x = 'Kon x+  SubstAtom ('Var ('VS v)) x = 'Var v+  SubstAtom ('Kon t)       x = 'Kon t+  SubstAtom (t1 ':@: t2)   x = (SubstAtom t1 x) ':@: (SubstAtom t2 x)+  SubstAtom (t1 ':&: t2)   x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)+

@@ -16,6 +16,9 @@   , SomeEff (..)   , SomeEffOfType (..) +    -- * Support for Existential Types+  , ExistentialFor+     -- * Constraints for Generators of Effects   , GArbitraryK   , ArbitraryAction@@ -36,7 +39,7 @@ import Polysemy import Polysemy.Check.Arbitrary import Polysemy.Check.Arbitrary.AnyEff-import Polysemy.Check.Arbitrary.Generic (GArbitraryK)+import Polysemy.Check.Arbitrary.Generic (GArbitraryK, ExistentialFor) import Polysemy.Check.Orphans () import Polysemy.Internal import Polysemy.Internal.Union.Inject (Inject, inject)

@@ -21,10 +21,10 @@ -- | Generate any action for effect @e@ that produces type @a@. arbitraryActionOfType     :: forall e a r-     . (GenericK (e (Sem r) a), GArbitraryK a (RepK (e (Sem r) a)))+     . (GenericK e, GArbitraryK e (RepK e) r a)     => Gen (e (Sem r) a)        -- ^-arbitraryActionOfType = genEff @e @a @(Sem r)+arbitraryActionOfType = genEff @e @r @a   ------------------------------------------------------------------------------

@@ -39,9 +39,10 @@ ------------------------------------------------------------------------------ -- | A type family that expands to a 'GArbitraryK' constaint for every type in -- the first list.-type family ArbitraryForAll (as :: [Type]) (m :: Type -> Type) :: Constraint where-  ArbitraryForAll '[] f = ()-  ArbitraryForAll (a ': as) f = (Eq a, Show a, GArbitraryK a (RepK (f a)), ArbitraryForAll as f)+type family ArbitraryForAll (e :: Effect) (as :: [Type]) (r :: EffectRow) :: Constraint where+  ArbitraryForAll e '[] f = ()+  ArbitraryForAll e (a ': as) r =+    (Eq a, Show a, GArbitraryK e (RepK e) r a, ArbitraryForAll e as r)   ------------------------------------------------------------------------------@@ -112,15 +113,15 @@     , Show a     , Show (e (Sem r) a)     , ArbitraryEffOfType a es r-    , GenericK (e (Sem r) a)-    , GArbitraryK a (RepK (e (Sem r) a))+    , GenericK e+    , GArbitraryK e (RepK e) r a     , CoArbitrary a     , Member e r     )     => ArbitraryEffOfType a (e ': es) r     where   genSomeEffOfType-    = fmap SomeEffOfType (genEff @e @a @(Sem r))+    = fmap SomeEffOfType (genEff @e @r @a)     : genSomeEffOfType @a @es @r  @@ -139,11 +140,11 @@     , Show a     , Member e r     , Show (e (Sem r) a)-    , GenericK (e (Sem r) a)+    , GenericK e     , CoArbitrary a-    , GArbitraryK a (RepK (e (Sem r) a))+    , GArbitraryK e (RepK e) r a     )     => ArbitraryAction (a : as) e r     where-  genSomeAction = (fmap SomeAction $ genEff @e @a @(Sem r)) : genSomeAction @as @e @r+  genSomeAction = (fmap SomeAction $ genEff @e @r @a) : genSomeAction @as @e @r 

@@ -3,77 +3,87 @@ import Control.Applicative (liftA2) import Data.Kind (Type) import GHC.Exts (type (~~))-import Generics.Kind-import Test.QuickCheck+import Generics.Kind hiding (SubstRep)+import Generics.Kind.Unexported import Polysemy import Polysemy.Check.Arbitrary.AnyEff import Polysemy.Internal (send)+import Test.QuickCheck   --------------------------------------------------------------------------------type a :~~~: b = 'Kon (~~) ':@: a ':@: b+-- | Data family for the instantiation of existential variables. If you want to+-- check properties for an effect @e@ that contains an existential type, the+-- synthesized 'Arbitrary' instance will instantiate all of @e@'s existential+-- types at @'ExistentialFor' e@.+--+-- @'ExistentialFor' e@ must have instances for every dictionary required by+-- @e@, and will likely require an 'Arbitrary' instance.+data family ExistentialFor (e :: Effect)   --------------------------------------------------------------------------------- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes--- generators for every well-typed constructor of @e m a@. It is capable of--- building generators for GADTs.-class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where-  garbitraryk :: [Gen (f x)]+-- | Given @'GArbitraryK' a ('RepK' e) r a@, this typeclass computes+-- generators for every well-typed constructor of @e (Sem r) a@. It is capable+-- of building generators for GADTs.+class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type)  where+  garbitraryk :: [Gen (f (LoT2 (Sem r) a))] -instance GArbitraryK a U1 where+instance GArbitraryK e U1 r a where   garbitraryk = pure $ pure U1 -instance (GArbitraryK1 (f :*: g)) => GArbitraryK a (f :*: g) where-  garbitraryk = garbitraryk1+instance (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :*: g) r a where+  garbitraryk = liftA2 (liftA2 (:*:)) (garbitraryk @e) (garbitraryk @e) -instance (GArbitraryK1 (Field b)) => GArbitraryK a (Field b) where-  garbitraryk = garbitraryk1+instance GArbitraryKTerm (Interpret f (LoT2 (Sem r) a)) => GArbitraryK e (Field f) r a where+  garbitraryk = pure $ fmap Field $ garbitrarykterm @(Interpret f (LoT2 (Sem r) a)) -instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) where-  garbitraryk = fmap (fmap L1) (garbitraryk @a @f)-             <> fmap (fmap R1) (garbitraryk @a @g)+instance+    ( GArbitraryK e (SubstRep f (ExistentialFor e)) r a+    , SubstRep' f (ExistentialFor e) (LoT2 (Sem r) a)+    ) => GArbitraryK e (Exists Type f) r a where+  garbitraryk = fmap (Exists . unsubstRep @_ @_ @_ @(ExistentialFor e)) <$>+    garbitraryk @e @(SubstRep f (ExistentialFor e)) @r @a -instance GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where-  garbitraryk = fmap SuchThat <$> garbitraryk1+instance (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :+: g) r a where+  garbitraryk = fmap (fmap L1) (garbitraryk @e @f)+             <> fmap (fmap R1) (garbitraryk @e @g) -instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where-  garbitraryk = []+instance (Interpret c (LoT2 (Sem r) a), GArbitraryK e f r a) => GArbitraryK e (c :=>: f) r a where+  garbitraryk = fmap (fmap SuchThat) (garbitraryk @e @f) -instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where-  garbitraryk = []+instance {-# OVERLAPPING #-} GArbitraryK e (c1 :=>: (c2 :=>: f)) r a+    => GArbitraryK e ((c1 ':&: c2) :=>: f) r a where+  garbitraryk =+    fmap+      ((\(SuchThat (SuchThat x)) -> SuchThat x)+            :: (c1 :=>: (c2 :=>: f)) x -> ((c1 ':&: c2) :=>: f) x)+        <$> garbitraryk @e -instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where-  garbitraryk = fmap M1 <$> garbitraryk @a+instance {-# OVERLAPPING #-} GArbitraryK e f r a => GArbitraryK e ('Kon ((~~) a) ':@: Var1 :=>: f) r a where+  garbitraryk = fmap SuchThat <$> garbitraryk @e @f +instance {-# OVERLAPPING #-} GArbitraryK e f r a => GArbitraryK e ('Kon (~~) ':@: Var1 ':@: 'Kon a :=>: f) r a where+  garbitraryk = fmap SuchThat <$> garbitraryk @e @f ---------------------------------------------------------------------------------- | @genEff \@e \@a \@m@ gets a generator capable of producing every--- well-typed GADT constructor of @e m a@.-genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)-genEff = fmap toK $ oneof $ garbitraryk @a @(RepK (e m a))+instance {-# INCOHERENT #-} GArbitraryK e ('Kon ((~~) b) ':@: Var1 :=>: f) r a where+  garbitraryk = [] +instance {-# INCOHERENT #-} GArbitraryK e ('Kon (~~) ':@: Var1 ':@: 'Kon b :=>: f) r a where+  garbitraryk = [] ---------------------------------------------------------------------------------- | Like @GArbitraryK@, but gets run after we've already discharged the @a--- ~ T@ GADT constraint.-class GArbitraryK1 (f :: LoT Type -> Type) where-  garbitraryk1 :: [Gen (f x)]+instance (GArbitraryK e f r a) => GArbitraryK e (M1 _1 _2 f) r a where+  garbitraryk = fmap M1 <$> garbitraryk @e -instance (GArbitraryK1 f, GArbitraryK1 g) => GArbitraryK1 (f :*: g) where-  garbitraryk1 = liftA2 (liftA2 (:*:)) garbitraryk1 garbitraryk1 -instance GArbitraryKTerm t => GArbitraryK1 (Field ('Kon t)) where-  garbitraryk1 = pure $ fmap Field garbitrarykterm+------------------------------------------------------------------------------+-- | @genEff \@e \@r \@a@ gets a generator capable of producing every+-- well-typed GADT constructor of @e (Sem r) a@.+genEff :: forall e r a. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a)+genEff = fmap toK $ oneof $ garbitraryk @e @(RepK e) @r -instance (GArbitraryK1 f) => GArbitraryK1 (M1 _1 _2 f) where-  garbitraryk1 = fmap M1 <$> garbitraryk1 -instance GArbitraryK1 U1 where-  garbitraryk1 = pure $ pure U1 - class GArbitraryKTerm (t :: Type) where   garbitrarykterm :: Gen t @@ -87,5 +97,4 @@  instance Arbitrary a => GArbitraryKTerm a where   garbitrarykterm = arbitrary- 

@@ -3,17 +3,18 @@ import Data.Kind (Type) import Generics.Kind import Test.QuickCheck+import Polysemy   ------------------------------------------------------------------------------ -- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes -- generators for every well-typed constructor of @e m a@. It is capable of -- building generators for GADTs.-class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where-  garbitraryk :: [Gen (f x)]+class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type)  where+  garbitraryk :: [Gen (f (LoT2 (Sem r) a))]  ------------------------------------------------------------------------------ -- | @genEff \@e \@a \@m@ gets a generator capable of producing every -- well-typed GADT constructor of @e m a@.-genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)+genEff :: forall e r a. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a) 

@@ -36,17 +36,25 @@       pure $ putGetLaw $ runIOState s  -putPutLaw-    :: forall s r-     . ( Arbitrary s-       , Member (State s) r+type LawConstraints f effs s r =+       ( Arbitrary s+       , Members effs r        , Eq s        , Show s-       , ArbitraryEff '[State s] r+       , ArbitraryEff effs r+       , f ~ (,) s+       , effs ~ '[State s]        )-    => (forall a. Sem r ((), a) -> IO (s, ((), a)))+++putPutLaw+    :: forall s r res effs f+     . ( res ~ ()+       , LawConstraints f effs s r+       )+    => (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property-putPutLaw = prepropLaw @'[State s] $ do+putPutLaw = prepropLaw @effs $ do   s1 <- arbitrary   s2 <- arbitrary   pure@@ -59,16 +67,13 @@   getPutLaw-    :: forall s r-     . ( Arbitrary s-       , Member (State s) r-       , Eq s-       , Show s-       , ArbitraryEff '[State s] r+    :: forall s r res effs f+     . ( res ~ ()+       , LawConstraints f effs s r        )-    => (forall a. Sem r ((), a) -> IO (s, ((), a)))+    => (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property-getPutLaw = prepropLaw @'[State s] $ do+getPutLaw = prepropLaw @effs $ do   pure     ( get >>= put     , pure ()@@ -76,16 +81,13 @@   putGetLaw-    :: forall s r-     . ( Arbitrary s-       , Member (State s) r-       , Eq s-       , Show s-       , ArbitraryEff '[State s] r+    :: forall s r res effs f+     . ( res ~ s+       , LawConstraints f effs s r        )-    => (forall a. Sem r (s, a) -> IO (s, (s, a)))+    => (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property-putGetLaw = prepropLaw @'[State s] $ do+putGetLaw = prepropLaw @effs $ do   s <- arbitrary   pure     ( do

@@ -0,0 +1,41 @@+module WeirdEffectsSpec where++import Data.Typeable+import Polysemy+import Polysemy.Check+import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck+++data MyEffect m a where+  -- | Here, @e@ is existential!+  CanShow :: (Show e, Typeable e) => e -> MyEffect m ()++makeSem ''MyEffect++deriving instance Show (MyEffect m a)+deriveGenericK ''MyEffect+++------------------------------------------------------------------------------+-- | When we synthesize a @MyEffect@ action, we instantiate all existentials at+-- @'ExistentialFor' MyEffect@.+--+-- This type must satisfy all of the constraints required by @CanShow@.+data instance ExistentialFor MyEffect = Hello+  deriving (Eq, Show)++-- It also requires an 'Arbitrary' instance!+instance Arbitrary (ExistentialFor MyEffect) where+  arbitrary = pure Hello+++spec :: Spec+spec = do+  prop @(Gen Expectation) "Existentials get instantiated at 'ExistentialFor MyEffect'" $ do+    SomeAction e <- arbitraryAction @MyEffect @'[MyEffect]+    pure $ case e of+      CanShow t ->+        cast t `shouldBe` Just Hello+