{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RequiredTypeArguments #-}

-- | Generic property-testing infrastructure for categories: 'Testable' says how to generate and
-- enumerate the objects of a kind, 'TestableProfunctor' and 'TestableType' how to generate values
-- (using @falsify@ generators), and 'TestingEqShow' provides semantic equality and display for
-- values without useful structural 'Eq'\/'Show' (functions, opaque morphisms). Instances for your
-- own category plus the law checks in "Proarrow.Testing.Laws" give it a test suite.
module Proarrow.Testing where

import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (mapMaybe)
import Data.Typeable (Typeable, eqT, (:~:) (..))
import GHC.Exts qualified as GHC
import Test.Falsify.Generator (Fun, Function (..), Gen, applyFun, elem, fun, functionMap, minimalValue, oneof)
import Test.Tasty.Falsify (Property, discard, genWith)
import Prelude hiding (elem, fst, id, snd, (.), (>>))

import Control.Applicative (Alternative (..))
import Control.Monad (ap)
import Debug.Trace (traceM, traceShowM)
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product (Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CategoryOf (..), Hom, Is, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Functor (type (@))
import Proarrow.Functor qualified as Rep
import Proarrow.Object (Ob')
import Proarrow.Profunctor.Representable (Rep (..))
import Test.Falsify.Interactive (falsify)

data GenTotal a where
  GenEmpty :: ~(forall x. a -> x) -> GenTotal a
  GenNENonFun :: Gen a -> GenTotal a
  GenFun :: (TestableType a, TestableType b) => ((a -> b) -> p) -> Gen (Fun (ShowP a) (ShowP b)) -> GenTotal p

invmap :: (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
invmap :: forall a b. (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
invmap a -> b
_ b -> a
f' (GenEmpty forall x. a -> x
g) = (forall x. b -> x) -> GenTotal b
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty (a -> x
forall x. a -> x
g (a -> x) -> (b -> a) -> b -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b -> a
f')
invmap a -> b
f b -> a
_ (GenNENonFun Gen a
g) = Gen b -> GenTotal b
forall a. Gen a -> GenTotal a
GenNENonFun ((a -> b) -> Gen a -> Gen b
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Gen a
g)
invmap a -> b
f b -> a
_ (GenFun (a -> b) -> a
f' Gen (Fun (ShowP a) (ShowP b))
g) = ((a -> b) -> b) -> Gen (Fun (ShowP a) (ShowP b)) -> GenTotal b
forall a b p.
(TestableType a, TestableType b) =>
((a -> b) -> p) -> Gen (Fun (ShowP a) (ShowP b)) -> GenTotal p
GenFun (a -> b
f (a -> b) -> ((a -> b) -> a) -> (a -> b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a
f') Gen (Fun (ShowP a) (ShowP b))
g

flatten :: GenTotal a -> Gen a
flatten :: forall a. GenTotal a -> Gen a
flatten (GenNENonFun Gen a
g) = Gen a
g
flatten (GenFun (a -> b) -> a
f Gen (Fun (ShowP a) (ShowP b))
g) = (a -> b) -> a
f ((a -> b) -> a)
-> (Fun (ShowP a) (ShowP b) -> a -> b)
-> Fun (ShowP a) (ShowP b)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> a -> b
forall a b. Fun (ShowP a) (ShowP b) -> a -> b
applyFunP (Fun (ShowP a) (ShowP b) -> a)
-> Gen (Fun (ShowP a) (ShowP b)) -> Gen a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Fun (ShowP a) (ShowP b))
g
flatten (GenEmpty forall x. a -> x
_) = [Char] -> Gen a
forall a. HasCallStack => [Char] -> a
error [Char]
"flatten: Match on GenEmpty first"

pattern GenNonEmpty :: Gen a -> GenTotal a
pattern $mGenNonEmpty :: forall {r} {a}. GenTotal a -> (Gen a -> r) -> ((# #) -> r) -> r
$bGenNonEmpty :: forall a. Gen a -> GenTotal a
GenNonEmpty g <- (flatten -> g)
  where
    GenNonEmpty Gen a
g = Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNENonFun Gen a
g

{-# COMPLETE GenEmpty, GenNonEmpty #-}

instance Functor GenTotal where
  fmap :: forall a b. (a -> b) -> GenTotal a -> GenTotal b
fmap a -> b
f = (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
forall a b. (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
invmap a -> b
f ([Char] -> b -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"fmap GenTotal")

instance Applicative GenTotal where
  pure :: forall a. a -> GenTotal a
pure a
a = Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNENonFun (a -> Gen a
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a)
  <*> :: forall a b. GenTotal (a -> b) -> GenTotal a -> GenTotal b
(<*>) = GenTotal (a -> b) -> GenTotal a -> GenTotal b
forall (m :: Type -> Type) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Alternative GenTotal where
  empty :: forall a. GenTotal a
empty = (forall x. a -> x) -> GenTotal a
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty ([Char] -> a -> x
forall a. HasCallStack => [Char] -> a
error [Char]
"empty")
  GenEmpty forall x. a -> x
f <|> :: forall a. GenTotal a -> GenTotal a -> GenTotal a
<|> GenEmpty forall x. a -> x
_ = (forall x. a -> x) -> GenTotal a
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty a -> x
forall x. a -> x
f
  GenEmpty forall x. a -> x
_ <|> GenTotal a
g = GenTotal a
g
  GenTotal a
f <|> GenEmpty forall x. a -> x
_ = GenTotal a
f
  GenNonEmpty Gen a
g <|> GenNonEmpty Gen a
h = Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNonEmpty (NonEmpty (Gen a) -> Gen a
forall a. NonEmpty (Gen a) -> Gen a
oneof (Gen a
g Gen a -> [Gen a] -> NonEmpty (Gen a)
forall a. a -> [a] -> NonEmpty a
:| [Item [Gen a]
Gen a
h]))

-- | Uniformly choose among any number of alternatives, dropping the empty ones. Plain '<|>'
-- only combines two generators at 50\/50, so chaining it over more than two alternatives
-- associates pairwise and skews weight towards whichever branch ends up outermost in the
-- resulting tree instead of splitting evenly — use this instead whenever there are more than
-- two alternatives to pick fairly among.
oneOfTotal :: [GenTotal a] -> GenTotal a
oneOfTotal :: forall a. [GenTotal a] -> GenTotal a
oneOfTotal [GenTotal a]
gts = case (GenTotal a -> Maybe (Gen a)) -> [GenTotal a] -> [Gen a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe GenTotal a -> Maybe (Gen a)
forall {a}. GenTotal a -> Maybe (Gen a)
toGen [GenTotal a]
gts of
  [] -> GenTotal a
forall a. GenTotal a
forall (f :: Type -> Type) a. Alternative f => f a
empty
  Gen a
g : [Gen a]
gs -> Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNonEmpty (NonEmpty (Gen a) -> Gen a
forall a. NonEmpty (Gen a) -> Gen a
oneof (Gen a
g Gen a -> [Gen a] -> NonEmpty (Gen a)
forall a. a -> [a] -> NonEmpty a
:| [Gen a]
gs))
  where
    toGen :: GenTotal a -> Maybe (Gen a)
toGen (GenEmpty forall x. a -> x
_) = Maybe (Gen a)
forall a. Maybe a
Nothing
    toGen (GenNonEmpty Gen a
g) = Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just Gen a
g

instance Monad GenTotal where
  GenEmpty forall x. a -> x
_ >>= :: forall a b. GenTotal a -> (a -> GenTotal b) -> GenTotal b
>>= a -> GenTotal b
_ = (forall x. b -> x) -> GenTotal b
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty ([Char] -> b -> x
forall a. HasCallStack => [Char] -> a
error [Char]
">>= GenEmpty")
  GenNonEmpty Gen a
g >>= a -> GenTotal b
f = case a -> GenTotal b
f (Gen a -> a
forall a. Gen a -> a
minimalValue Gen a
g) of
    GenEmpty forall x. b -> x
x -> (forall x. b -> x) -> GenTotal b
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty b -> x
forall x. b -> x
x
    GenTotal b
_ -> Gen b -> GenTotal b
forall a. Gen a -> GenTotal a
GenNonEmpty do
      p <- (a -> GenTotal b) -> Gen a -> Gen (GenTotal b)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> GenTotal b
f Gen a
g
      case p of
        GenEmpty forall x. b -> x
_ -> [Char] -> Gen b
forall a. HasCallStack => [Char] -> a
error [Char]
">>= GenEmpty"
        GenNonEmpty Gen b
g' -> Gen b
g'

class TestingEqShow a where
  eqP :: a -> a -> Property Bool
  default eqP :: (Eq a) => a -> a -> Property Bool
  eqP a
l a
r = Bool -> Property Bool
forall a. a -> Property' [Char] a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
r)
  showP :: a -> String
  default showP :: (Show a) => a -> String
  showP = a -> [Char]
forall a. Show a => a -> [Char]
show

class (TestingEqShow a) => TestableType a where
  gen :: GenTotal a

-- | Supplies a 'Show' instance derived from 'showP'.
--
-- falsify's 'Show' instance for 'Fun' needs 'Show' on both parameters, and we
-- only ever have 'TestingEqShow'. Rather than reinterpret a @'Fun' a b@ at the
-- wrapped type after the fact, 'GenFun' generates at
-- @'Fun' ('ShowP' a) ('ShowP' b)@ from the start, so 'show' applies directly and
-- no coercion is involved. 'applyFunP' unwraps on the way back out.
newtype ShowP a = ShowP {forall a. ShowP a -> a
unShowP :: a}

instance (TestingEqShow a) => Show (ShowP a) where
  show :: ShowP a -> [Char]
show (ShowP a
a) = a -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP a
a

instance (Function a) => Function (ShowP a) where
  function :: forall b. Gen b -> Gen (ShowP a :-> b)
function = ((a :-> b) -> ShowP a :-> b)
-> Gen (a :-> b) -> Gen (ShowP a :-> b)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ShowP a -> a) -> (a -> ShowP a) -> (a :-> b) -> ShowP a :-> b
forall b a c. (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
functionMap ShowP a -> a
forall a. ShowP a -> a
unShowP a -> ShowP a
forall a. a -> ShowP a
ShowP) (Gen (a :-> b) -> Gen (ShowP a :-> b))
-> (Gen b -> Gen (a :-> b)) -> Gen b -> Gen (ShowP a :-> b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Gen b -> Gen (a :-> b)
forall b. Gen b -> Gen (a :-> b)
forall a b. Function a => Gen b -> Gen (a :-> b)
function

-- | Apply a generated function, wrapping and unwrapping the 'ShowP' it was
-- generated at. Both directions are ordinary newtype constructor applications.
applyFunP :: Fun (ShowP a) (ShowP b) -> a -> b
applyFunP :: forall a b. Fun (ShowP a) (ShowP b) -> a -> b
applyFunP Fun (ShowP a) (ShowP b)
f = ShowP b -> b
forall a. ShowP a -> a
unShowP (ShowP b -> b) -> (a -> ShowP b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> ShowP a -> ShowP b
forall a b. Fun a b -> a -> b
applyFun Fun (ShowP a) (ShowP b)
f (ShowP a -> ShowP b) -> (a -> ShowP a) -> a -> ShowP b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> ShowP a
forall a. a -> ShowP a
ShowP

genP :: (TestableType a) => Property a
genP :: forall a. TestableType a => Property a
genP = case GenTotal a
forall a. TestableType a => GenTotal a
gen of
  GenNENonFun Gen a
g -> (a -> Maybe [Char]) -> Gen a -> Property a
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> (a -> [Char]) -> a -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP) Gen a
g
  GenFun (a -> b) -> a
f Gen (Fun (ShowP a) (ShowP b))
g -> (a -> b) -> a
f ((a -> b) -> a)
-> (Fun (ShowP a) (ShowP b) -> a -> b)
-> Fun (ShowP a) (ShowP b)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> a -> b
forall a b. Fun (ShowP a) (ShowP b) -> a -> b
applyFunP (Fun (ShowP a) (ShowP b) -> a)
-> Property' [Char] (Fun (ShowP a) (ShowP b)) -> Property a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Fun (ShowP a) (ShowP b) -> Maybe [Char])
-> Gen (Fun (ShowP a) (ShowP b))
-> Property' [Char] (Fun (ShowP a) (ShowP b))
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char])
-> (Fun (ShowP a) (ShowP b) -> [Char])
-> Fun (ShowP a) (ShowP b)
-> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> [Char]
forall a. Show a => a -> [Char]
show) Gen (Fun (ShowP a) (ShowP b))
g
  GenEmpty forall x. a -> x
_ -> Property a
forall e a. Property' e a
discard

genNamed :: (TestableType a) => String -> Property a
genNamed :: forall a. TestableType a => [Char] -> Property a
genNamed [Char]
nm = case GenTotal a
forall a. TestableType a => GenTotal a
gen of
  GenNENonFun Gen a
g -> [Char] -> (a -> Maybe [Char]) -> Gen a -> Property a
forall a. [Char] -> (a -> Maybe [Char]) -> Gen a -> Property a
genWithNamed [Char]
nm ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> (a -> [Char]) -> a -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP) Gen a
g
  GenFun (a -> b) -> a
f Gen (Fun (ShowP a) (ShowP b))
g -> (a -> b) -> a
f ((a -> b) -> a)
-> (Fun (ShowP a) (ShowP b) -> a -> b)
-> Fun (ShowP a) (ShowP b)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> a -> b
forall a b. Fun (ShowP a) (ShowP b) -> a -> b
applyFunP (Fun (ShowP a) (ShowP b) -> a)
-> Property' [Char] (Fun (ShowP a) (ShowP b)) -> Property a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char]
-> (Fun (ShowP a) (ShowP b) -> Maybe [Char])
-> Gen (Fun (ShowP a) (ShowP b))
-> Property' [Char] (Fun (ShowP a) (ShowP b))
forall a. [Char] -> (a -> Maybe [Char]) -> Gen a -> Property a
genWithNamed [Char]
nm ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char])
-> (Fun (ShowP a) (ShowP b) -> [Char])
-> Fun (ShowP a) (ShowP b)
-> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fun (ShowP a) (ShowP b) -> [Char]
forall a. Show a => a -> [Char]
show) Gen (Fun (ShowP a) (ShowP b))
g
  GenEmpty forall x. a -> x
_ -> Property a
forall e a. Property' e a
discard

genWithNamed :: String -> (a -> Maybe String) -> Gen a -> Property a
genWithNamed :: forall a. [Char] -> (a -> Maybe [Char]) -> Gen a -> Property a
genWithNamed [Char]
nm a -> Maybe [Char]
f = (a -> Maybe [Char]) -> Gen a -> Property' [Char] a
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith (ShowS -> Maybe [Char] -> Maybe [Char]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ShowS
named (Maybe [Char] -> Maybe [Char])
-> (a -> Maybe [Char]) -> a -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> Maybe [Char]
f)
  where
    named :: ShowS
named [Char]
s = [Char]
"for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s

-- | 'True' if a type's generator is non-empty. A pure check on 'TestableType's 'gen' — it
-- doesn't sample anything, so it's safe (and cheap) to call as many times as convenient, e.g.
-- once in a 'genSuchThat' predicate and again via the real 'gen'\/'genNamed' call that
-- actually produces a value.
isGenNonEmpty :: forall a. (TestableType a) => Bool
isGenNonEmpty :: forall a. TestableType a => Bool
isGenNonEmpty = case forall a. TestableType a => GenTotal a
gen @a of
  GenEmpty forall x. a -> x
_ -> Bool
False
  GenTotal a
_ -> Bool
True

-- | Resample @genKey@ (cheaply, within 'Gen') up to 'maxTries' times until @isUsable@ accepts
-- the draw, before ever asking 'Property' to commit to a choice.
--
-- 'Property'-level 'discard' restarts the *whole* property from scratch (and can trip
-- falsify's per-slot discard-ratio limit, aborting the entire test run early) — so when a
-- later, dependent draw (e.g. \"a morphism out of this object\") is likely to be empty for a
-- \"bad\" choice made here, it's far cheaper to reject that choice immediately, inside 'Gen',
-- than to commit to it via 'Property' and let the dependent draw discover the problem. A
-- choice that's still unusable after 'maxTries' attempts is returned anyway, so a genuinely
-- unsatisfiable requirement still falls through to whatever ordinary 'discard' the caller's
-- own dependent generation triggers.
genSuchThat :: Gen key -> (key -> Bool) -> Gen key
genSuchThat :: forall key. Gen key -> (key -> Bool) -> Gen key
genSuchThat Gen key
genKey key -> Bool
isUsable = Int -> Gen key
go Int
maxTries
  where
    go :: Int -> Gen key
go Int
n = do
      k <- Gen key
genKey
      if isUsable k || n <= (0 :: Int) then pure k else go (n - 1)

-- | How many times 'genSuchThat' resamples before giving up. There's no principled formula
-- for this — it depends on how sparse the specific requirement being searched for is, which
-- 'genSuchThat' has no way to know in advance. 100 is a pragmatic default: comfortably more
-- than the number of candidates a small test object palette usually offers (so a single
-- unlucky pick is very unlikely to exhaust it), while still cheap, since each attempt is a
-- plain 'Gen' sample rather than a 'Property'-level 'discard'.
maxTries :: Int
maxTries :: Int
maxTries = Int
100

-- | 'genOb', but resampled (see 'genSuchThat') until @isUsable@ accepts the object.
genObSuchThat :: forall k. (Testable k) => (Some k -> Bool) -> Property (Some k)
genObSuchThat :: forall k. Testable k => (Some k -> Bool) -> Property (Some k)
genObSuchThat = (Some k -> Maybe [Char]) -> Gen (Some k) -> Property (Some k)
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char])
-> (Some k -> [Char]) -> Some k -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Some k -> [Char]
forall a. Show a => a -> [Char]
show) (Gen (Some k) -> Property (Some k))
-> ((Some k -> Bool) -> Gen (Some k))
-> (Some k -> Bool)
-> Property (Some k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Gen (Some k) -> (Some k -> Bool) -> Gen (Some k)
forall key. Gen key -> (key -> Bool) -> Gen key
genSuchThat (forall k. Testable k => Gen (Some k)
genSome @k)

type SomeProfunctorElt :: (j +-> k) -> Type
data SomeProfunctorElt p where
  SomeP :: (TestOb a, TestOb b) => p a b -> SomeProfunctorElt p

someP :: forall {k} {j} (p :: k +-> j) a b. (Profunctor p, TestObIsOb j, TestObIsOb k) => p a b -> SomeProfunctorElt p
someP :: forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
(Profunctor p, TestObIsOb j, TestObIsOb k) =>
p a b -> SomeProfunctorElt p
someP p a b
p = p a b -> SomeProfunctorElt p
forall {k} {j} (a :: k) (b :: j) (p :: j +-> k).
(TestOb a, TestOb b) =>
p a b -> SomeProfunctorElt p
SomeP p a b
p ((Ob a, Ob b) => SomeProfunctorElt p)
-> p a b -> SomeProfunctorElt p
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance
  (forall a b. (TestOb (a :: k), TestOb (b :: j)) => TestingEqShow (p a b), Testable k, Testable j)
  => Show (SomeProfunctorElt p)
  where
  show :: SomeProfunctorElt p -> [Char]
show (SomeP @a @b p a b
p) = p a b -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP p a b
p [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" @" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @k @a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" @" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @j @b

type TestableTypeP :: (j +-> k) -> Constraint
class (forall a b. (TestOb (a :: k), TestOb (b :: j)) => TestableType (p a b)) => TestableTypeP (p :: j +-> k)
instance (forall a b. (TestOb (a :: k), TestOb (b :: j)) => TestableType (p a b)) => TestableTypeP (p :: j +-> k)

type TestableProfunctor :: forall {j} {k}. j +-> k -> Constraint
class
  (Testable j, Testable k, Profunctor p, forall a b. (TestOb (a :: k), TestOb (b :: j)) => TestingEqShow (p a b)) =>
  TestableProfunctor (p :: j +-> k)
  where
  -- | The default implementation generates types @a@ and @b@ and then generates a value of type @p a b@.
  -- But that can cause too many discarded tests.
  genProfunctorElt :: String -> Property (SomeProfunctorElt p)
  default genProfunctorElt :: (TestableTypeP p) => String -> Property (SomeProfunctorElt p)
  genProfunctorElt [Char]
nm = do
    Some @a <- Property (Some k)
forall k. Testable k => Property (Some k)
genOb
    Some @b <- genOb
    p <- genNamed @(p a b) nm
    pure $ SomeP p

class (forall (a :: k). (TestOb a) => Ob' a, TestableProfunctor (Hom k), TestableTypeP (Hom k), CategoryOf k) => Testable k where
  type TestOb (a :: k) :: GHC.Constraint
  type TestOb a = Ob a
  showOb :: forall (a :: k). (TestOb a) => String
  eqOb :: (TestOb (a :: k), TestOb b) => Maybe (a :~: b)
  default eqOb :: forall a b. (TestOb (a :: k), TestOb b, Typeable a, Typeable b) => Maybe (a :~: b)
  eqOb = forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b
  genSome :: Gen (Some k)

genOb :: (Testable k) => Property (Some k)
genOb :: forall k. Testable k => Property (Some k)
genOb = (Some k -> Maybe [Char])
-> Gen (Some k) -> Property' [Char] (Some k)
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char])
-> (Some k -> [Char]) -> Some k -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Some k -> [Char]
forall a. Show a => a -> [Char]
show) Gen (Some k)
forall k. Testable k => Gen (Some k)
genSome

instance (TestableProfunctor p) => TestableProfunctor (Op p) where
  genProfunctorElt :: [Char] -> Property (SomeProfunctorElt (Op p))
genProfunctorElt [Char]
nm = do
    SomeP p <- forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
forall (p :: j +-> k).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
genProfunctorElt @p [Char]
nm
    pure $ SomeP (Op p)
instance (Testable k) => Testable (OPPOSITE k) where
  type TestOb a = (Is OP a, TestOb (UN OP a))
  showOb :: forall (a :: OPPOSITE k). TestOb a => [Char]
showOb @(OP a) = [Char]
"OP (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @k @a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  eqOb :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(TestOb a, TestOb b) =>
Maybe (a :~: b)
eqOb @(OP a) @(OP b) = ((UN 'OP a :~: UN 'OP b) -> a :~: b)
-> Maybe (UN 'OP a :~: UN 'OP b) -> Maybe (a :~: b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\UN 'OP a :~: UN 'OP b
Refl -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl) (Maybe (UN 'OP a :~: UN 'OP b) -> Maybe (a :~: b))
-> Maybe (UN 'OP a :~: UN 'OP b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b) =>
Maybe (a :~: b)
eqOb @k @a @b
  genSome :: Gen (Some (OPPOSITE k))
genSome = mapSome OP (Some k -> Some (OPPOSITE k))
-> Gen (Some k) -> Gen (Some (OPPOSITE k))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Some k)
forall k. Testable k => Gen (Some k)
genSome

instance TestableProfunctor Unit
instance Testable () where
  showOb :: forall (a :: ()). TestOb a => [Char]
showOb = [Char]
"()"
  genSome :: Gen (Some ())
genSome = Some () -> Gen (Some ())
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall {k} (a :: k). TestOb a => Some k
forall (a :: ()). TestOb a => Some ()
Some @'())

instance (TestableProfunctor p, TestableProfunctor q) => TestableProfunctor (p :**: q) where
  genProfunctorElt :: [Char] -> Property (SomeProfunctorElt (p :**: q))
genProfunctorElt [Char]
nm = do
    SomeP p <- forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
forall (p :: j1 +-> k1).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
genProfunctorElt @p ([Char]
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"_0")
    SomeP q <- genProfunctorElt @q (nm ++ "_1")
    pure $ SomeP (p :**: q)
instance (Testable j, Testable k) => Testable (j, k) where
  type TestOb a = (a ~ '(Fst @ a, Snd @ a), TestOb (Fst @ a), TestOb (Snd @ a))
  showOb :: forall (a :: (j, k)). TestOb a => [Char]
showOb @'(a, b) = [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @j @a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @k @b [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  eqOb :: forall (a :: (j, k)) (b :: (j, k)).
(TestOb a, TestOb b) =>
Maybe (a :~: b)
eqOb @'(a1, a2) @'(b1, b2) = case (forall k (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b) =>
Maybe (a :~: b)
eqOb @j @a1 @b1, forall k (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b) =>
Maybe (a :~: b)
eqOb @k @a2 @b2) of
    (Just (Fst @ a) :~: (Fst @ b)
Refl, Just (Snd @ a) :~: (Snd @ b)
Refl) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    (Maybe ((Fst @ a) :~: (Fst @ b)), Maybe ((Snd @ a) :~: (Snd @ b)))
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  genSome :: Gen (Some (j, k))
genSome = do
    Some @a <- forall k. Testable k => Gen (Some k)
genSome @j
    Some @b <- genSome @k
    pure $ Some @'(a, b)

class (TestOb a) => TestOb' a
instance (TestOb a) => TestOb' a

class (forall (a :: k). (Ob a) => TestOb' a) => TestObIsOb k
instance (forall (a :: k). (Ob a) => TestOb' a) => TestObIsOb k

-- | Recover @'Ob' a@ from @'TestOb' a@ (the 'Testable' superclass entailment), packaged as a
-- function so that call sites with other quantified givens in scope (e.g. the comonoid supply of a
-- 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard' category, whose head has @Ob@ as a
-- superclass) don't have to rely on GHC expanding superclasses of quantified-constraint heads.
-- Observed on GHC 9.10.3: with such a given in scope, @\\r -> r@ at this type fails with "Could not
-- deduce Ob a", while the same lambda compiles without it (cf. 'Proarrow.Testing.Laws.propSymMonoidal_'
-- versus 'Proarrow.Testing.Laws.propCopyDiscard_'). Likely a solver limitation; retry dropping this
-- helper after a GHC upgrade.
obFromTestOb :: forall {k} (a :: k) r. (Testable k, TestOb a) => ((Ob a) => r) -> r
obFromTestOb :: forall {k} (a :: k) r. (Testable k, TestOb a) => (Ob a => r) -> r
obFromTestOb Ob a => r
r = r
Ob a => r
r

data Some k where
  Some :: forall {k} a. (TestOb (a :: k)) => Some k

mapSome :: forall {j} {k}. forall (f :: j -> k) -> (forall a. (TestOb a) => TestOb' (f a)) => Some j -> Some k
mapSome :: forall {j} {k}.
forall (f :: j -> k) ->
(forall (a :: j). TestOb a => TestOb' (f a)) => Some j -> Some k
mapSome f (Some @a) = forall (a :: k). TestOb a => Some k
forall {k} (a :: k). TestOb a => Some k
Some @(f a)

class MkSomeList (as :: [k]) where
  mkSomeList :: [Some k]
instance MkSomeList '[] where
  mkSomeList :: [Some k]
mkSomeList = []
instance (TestOb (a :: k), MkSomeList as) => MkSomeList (a ': as) where
  mkSomeList :: [Some k]
mkSomeList = forall (a :: k). TestOb a => Some k
forall {k} (a :: k). TestOb a => Some k
Some @a Some k -> [Some k] -> [Some k]
forall a. a -> [a] -> [a]
: forall k (as :: [k]). MkSomeList as => [Some k]
mkSomeList @k @as
instance (Testable k) => Show (Some k) where
  show :: Some k -> [Char]
show (Some @a) = forall k (a :: k). (Testable k, TestOb a) => [Char]
showOb @k @a

someElem :: (Show a) => [a] -> Property a
someElem :: forall a. Show a => [a] -> Property a
someElem = (a -> [Char]) -> [a] -> Property a
forall a. (a -> [Char]) -> [a] -> Property a
someElemWith a -> [Char]
forall a. Show a => a -> [Char]
show

someElemNamed :: (Show a) => String -> [a] -> Property a
someElemNamed :: forall a. Show a => [Char] -> [a] -> Property a
someElemNamed [Char]
nm = (a -> [Char]) -> [a] -> Property a
forall a. (a -> [Char]) -> [a] -> Property a
someElemWith (\a
a -> [Char]
"for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
a)

someElemWith :: (a -> String) -> [a] -> Property a
someElemWith :: forall a. (a -> [Char]) -> [a] -> Property a
someElemWith a -> [Char]
_ [] = Property' [Char] a
forall e a. Property' e a
discard
someElemWith a -> [Char]
f (a
x : [a]
xs) = (a -> Maybe [Char]) -> Gen a -> Property' [Char] a
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> (a -> [Char]) -> a -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> [Char]
f) (NonEmpty a -> Gen a
forall a. NonEmpty a -> Gen a
elem (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs))

genSomeDef :: forall {k} (obs :: [k]). (Testable k, MkSomeList obs) => Gen (Some k)
genSomeDef :: forall {k} (obs :: [k]).
(Testable k, MkSomeList obs) =>
Gen (Some k)
genSomeDef = case forall k (as :: [k]). MkSomeList as => [Some k]
mkSomeList @k @obs of
  [] -> [Char] -> Gen (Some k)
forall a. HasCallStack => [Char] -> a
error [Char]
"genSomeDef: empty list"
  (Some k
x : [Some k]
xs) -> NonEmpty (Some k) -> Gen (Some k)
forall a. NonEmpty a -> Gen a
elem (Some k
x Some k -> [Some k] -> NonEmpty (Some k)
forall a. a -> [a] -> NonEmpty a
:| [Some k]
xs)

optGen :: [a] -> GenTotal a
optGen :: forall a. [a] -> GenTotal a
optGen [] = [Char] -> GenTotal a
forall a. HasCallStack => [Char] -> a
error [Char]
"optGen: empty list"
optGen (a
x : [a]
xs) = Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNonEmpty (NonEmpty a -> Gen a
forall a. NonEmpty a -> Gen a
elem (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs))

oneElem :: a -> GenTotal a
oneElem :: forall a. a -> GenTotal a
oneElem a
x = Gen a -> GenTotal a
forall a. Gen a -> GenTotal a
GenNonEmpty (a -> Gen a
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
x)

instance (TestableType a, TestingEqShow b) => TestingEqShow (a -> b) where
  eqP :: (a -> b) -> (a -> b) -> Property Bool
eqP = (a -> b) -> (a -> b) -> Property Bool
forall a b.
(TestableType a, TestingEqShow b) =>
(a -> b) -> (a -> b) -> Property Bool
eqHask
  showP :: (a -> b) -> [Char]
showP a -> b
_ = [Char]
"<function>"

instance (Function a, TestableType a, TestableType b) => TestableType (a -> b) where
  gen :: GenTotal (a -> b)
gen = case forall a. TestableType a => GenTotal a
gen @b of
    GenEmpty forall x. b -> x
absurd -> case forall a. TestableType a => GenTotal a
gen @a of
      GenEmpty forall x. a -> x
absurda -> (a -> b) -> GenTotal (a -> b)
forall a. a -> GenTotal a
oneElem a -> b
forall x. a -> x
absurda
      GenNonEmpty Gen a
g -> (forall x. (a -> b) -> x) -> GenTotal (a -> b)
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty \a -> b
ab -> b -> x
forall x. b -> x
absurd (a -> b
ab (Gen a -> a
forall a. Gen a -> a
minimalValue Gen a
g))
    GenNonEmpty Gen b
gb -> ((a -> b) -> a -> b)
-> Gen (Fun (ShowP a) (ShowP b)) -> GenTotal (a -> b)
forall a b p.
(TestableType a, TestableType b) =>
((a -> b) -> p) -> Gen (Fun (ShowP a) (ShowP b)) -> GenTotal p
GenFun (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (Gen (ShowP b) -> Gen (Fun (ShowP a) (ShowP b))
forall a b. Function a => Gen b -> Gen (Fun a b)
fun (b -> ShowP b
forall a. a -> ShowP a
ShowP (b -> ShowP b) -> Gen b -> Gen (ShowP b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen b
gb))

eqHask :: (TestableType a, TestingEqShow b) => (a -> b) -> (a -> b) -> Property Bool
eqHask :: forall a b.
(TestableType a, TestingEqShow b) =>
(a -> b) -> (a -> b) -> Property Bool
eqHask a -> b
l a -> b
r =
  case GenTotal a
forall a. TestableType a => GenTotal a
gen of
    GenEmpty forall x. a -> x
_ -> Bool -> Property Bool
forall a. a -> Property' [Char] a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True -- There can only be one function of a type with no values
    GenNonEmpty Gen a
ga -> do
      a <- (a -> Maybe [Char]) -> Gen a -> Property' [Char] a
forall a e.
HasCallStack =>
(a -> Maybe [Char]) -> Gen a -> Property' e a
genWith ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> (a -> [Char]) -> a -> Maybe [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP) Gen a
ga
      eqP (l a) (r a)

instance (TestableType (p b a)) => TestableType (Op p (OP a) (OP b)) where
  gen :: GenTotal (Op p ('OP a) ('OP b))
gen = (p b a -> Op p ('OP a) ('OP b))
-> (Op p ('OP a) ('OP b) -> p b a)
-> GenTotal (p b a)
-> GenTotal (Op p ('OP a) ('OP b))
forall a b. (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
invmap p b a -> Op p ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Op p ('OP a) ('OP b) -> p b a
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp GenTotal (p b a)
forall a. TestableType a => GenTotal a
gen
instance (TestingEqShow (p b a)) => TestingEqShow (Op p (OP a) (OP b)) where
  eqP :: Op p ('OP a) ('OP b) -> Op p ('OP a) ('OP b) -> Property Bool
eqP (Op p b1 a1
l) (Op p b1 a1
r) = p b1 a1 -> p b1 a1 -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP p b1 a1
l p b1 a1
p b1 a1
r
  showP :: Op p ('OP a) ('OP b) -> [Char]
showP (Op p b1 a1
p) = [Char]
"Op (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ p b1 a1 -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP p b1 a1
p [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance (TestableType (a ~> (f Rep.@ b)), Ob b) => TestableType (Rep f a b) where
  gen :: GenTotal (Rep f a b)
gen = ((a ~> (f @ b)) -> Rep f a b)
-> (Rep f a b -> a ~> (f @ b))
-> GenTotal (a ~> (f @ b))
-> GenTotal (Rep f a b)
forall a b. (a -> b) -> (b -> a) -> GenTotal a -> GenTotal b
invmap (a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep Rep f a b -> a ~> (f @ b)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Rep f a b -> a ~> (f @ b)
unRep (forall a. TestableType a => GenTotal a
gen @(a ~> f Rep.@ b))
instance (TestingEqShow (a ~> (f Rep.@ b)), Ob b) => TestingEqShow (Rep f a b) where
  eqP :: Rep f a b -> Rep f a b -> Property Bool
eqP (Rep a ~> (f @ b)
l) (Rep a ~> (f @ b)
r) = (a ~> (f @ b)) -> (a ~> (f @ b)) -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP a ~> (f @ b)
l a ~> (f @ b)
r
  showP :: Rep f a b -> [Char]
showP (Rep a ~> (f @ b)
p) = (a ~> (f @ b)) -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP a ~> (f @ b)
p

instance (TestingEqShow (catk a1 b1), TestingEqShow (catj a2 b2)) => TestingEqShow ((catk :**: catj) '(a1, a2) '(b1, b2)) where
  eqP :: (:**:) catk catj '(a1, a2) '(b1, b2)
-> (:**:) catk catj '(a1, a2) '(b1, b2) -> Property Bool
eqP (catk a1 b1
l1 :**: catj a2 b2
l2) (catk a1 b1
r1 :**: catj a2 b2
r2) = (Bool -> Bool -> Bool)
-> Property Bool -> Property Bool -> Property Bool
forall a b c.
(a -> b -> c)
-> Property' [Char] a -> Property' [Char] b -> Property' [Char] c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) (catk a1 b1 -> catk a1 b1 -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP catk a1 b1
l1 catk a1 b1
catk a1 b1
r1) (catj a2 b2 -> catj a2 b2 -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP catj a2 b2
l2 catj a2 b2
catj a2 b2
r2)
  showP :: (:**:) catk catj '(a1, a2) '(b1, b2) -> [Char]
showP (catk a1 b1
l1 :**: catj a2 b2
l2) = [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ catk a1 b1 -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP catk a1 b1
l1 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") :**: (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ catj a2 b2 -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP catj a2 b2
l2 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
instance (TestableType (catk a1 b1), TestableType (catj a2 b2)) => TestableType ((catk :**: catj) '(a1, a2) '(b1, b2)) where
  gen :: GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2))
gen = case (GenTotal (catk a1 b1)
forall a. TestableType a => GenTotal a
gen, GenTotal (catj a2 b2)
forall a. TestableType a => GenTotal a
gen) of
    (GenEmpty forall x. catk a1 b1 -> x
f, GenTotal (catj a2 b2)
_) -> (forall x. (:**:) catk catj '(a1, a2) '(b1, b2) -> x)
-> GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2))
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty \(catk a1 b1
l :**: catj a2 b2
_) -> catk a1 b1 -> x
forall x. catk a1 b1 -> x
f catk a1 b1
catk a1 b1
l
    (GenTotal (catk a1 b1)
_, GenEmpty forall x. catj a2 b2 -> x
f) -> (forall x. (:**:) catk catj '(a1, a2) '(b1, b2) -> x)
-> GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2))
forall a. (forall x. a -> x) -> GenTotal a
GenEmpty \(catk a1 b1
_ :**: catj a2 b2
r) -> catj a2 b2 -> x
forall x. catj a2 b2 -> x
f catj a2 b2
catj a2 b2
r
    (GenNonEmpty Gen (catk a1 b1)
ga, GenNonEmpty Gen (catj a2 b2)
gb) -> Gen ((:**:) catk catj '(a1, a2) '(b1, b2))
-> GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2))
forall a. Gen a -> GenTotal a
GenNonEmpty (Gen ((:**:) catk catj '(a1, a2) '(b1, b2))
 -> GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2)))
-> Gen ((:**:) catk catj '(a1, a2) '(b1, b2))
-> GenTotal ((:**:) catk catj '(a1, a2) '(b1, b2))
forall a b. (a -> b) -> a -> b
$ (catk a1 b1 -> catj a2 b2 -> (:**:) catk catj '(a1, a2) '(b1, b2))
-> Gen (catk a1 b1)
-> Gen (catj a2 b2)
-> Gen ((:**:) catk catj '(a1, a2) '(b1, b2))
forall a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 catk a1 b1 -> catj a2 b2 -> (:**:) catk catj '(a1, a2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
(:**:) Gen (catk a1 b1)
ga Gen (catj a2 b2)
gb

instance (Ob a, Ob b) => TestableType (Unit a b) where
  gen :: GenTotal (Unit a b)
gen = Unit a b -> GenTotal (Unit a b)
forall a. a -> GenTotal a
oneElem Unit a b
Unit '() '()
Unit
instance TestingEqShow (Unit a b) where
  showP :: Unit a b -> [Char]
showP Unit a b
_ = [Char]
"Unit"
  eqP :: Unit a b -> Unit a b -> Property Bool
eqP Unit a b
_ Unit a b
_ = Bool -> Property Bool
forall a. a -> Property' [Char] a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True

sampleT :: forall t. (TestableType t) => IO (Maybe String)
sampleT :: forall t. TestableType t => IO (Maybe [Char])
sampleT = Property' [Char] () -> IO (Maybe [Char])
forall e a. Property' e a -> IO (Maybe e)
falsify (Property' [Char] () -> IO (Maybe [Char]))
-> Property' [Char] () -> IO (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ do
  p <- forall a. TestableType a => Property a
genP @t
  traceM (showP p)

sampleP :: forall {j} {k} (p :: j +-> k). (Testable j, Testable k, TestableProfunctor p) => IO (Maybe String)
sampleP :: forall {j} {k} (p :: j +-> k).
(Testable j, Testable k, TestableProfunctor p) =>
IO (Maybe [Char])
sampleP = Property' [Char] () -> IO (Maybe [Char])
forall e a. Property' e a -> IO (Maybe e)
falsify (Property' [Char] () -> IO (Maybe [Char]))
-> Property' [Char] () -> IO (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ do
  p <- forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
forall (p :: j +-> k).
TestableProfunctor p =>
[Char] -> Property (SomeProfunctorElt p)
genProfunctorElt @p [Char]
"p"
  traceShowM p

sampleK :: forall k. (Testable k) => IO (Maybe String)
sampleK :: forall k. Testable k => IO (Maybe [Char])
sampleK = forall e a. Property' e a -> IO (Maybe e)
falsify @_ @() (Property' [Char] () -> IO (Maybe [Char]))
-> Property' [Char] () -> IO (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  traceM $ showOb @k @a