{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Category.Objects where

import Algebra.Classes
import Algebra.Types
import Prelude (Int, Ord (..),otherwise,($),Show, Semigroup(..),show)
import Data.Kind
import Data.Constraint
import Test.QuickCheck
import Test.QuickCheck.Property
import Control.Applicative

type TimesCon con = forall a b. (con a, con b) => con (a⊗b) :: Constraint
type DualCon con = forall a. (con a) => con (Dual a) :: Constraint
type PlusCon con = forall a b. (con a, con b) => con (a⊕b) :: Constraint
type Con' x con = forall a b. (con a, con b) => con (a `x` b) :: Constraint
type UnCon o con = forall a. (con a) => con (o a) :: Constraint

type TimesCon1 con = forall x a b. (con (a (b x))) => con ((a⊗b) x) :: Constraint
type PlusCon1 con = forall {k} (x :: k) a b. (con (a x), con (b x)) => con ((a⊕b) x) :: Constraint
type OneCon1 (con :: Type -> Constraint) = forall x. con x => con (One x) :: Constraint
type ZeroCon1 con = forall x. con x => con (Zero x) :: Constraint
-- type LConTensor con = forall a b. con (a⊗b) => con a :: Constraint
-- type RConTensor con = forall a b. con (a⊗b) => con a :: Constraint

reprCon :: forall con a x i t o. (Con' x con, Con' t con, con i, con o) => Repr x i t o a -> Dict (con a)
reprCon :: forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon = \case
  RPlus Repr x i t o a1
a Repr x i t o b
b -> Dict (con a)
con a1 => Dict (con a)
forall (a :: Constraint). a => Dict a
Dict (con a1 => Dict (con a)) -> Dict (con a1) -> Dict (con a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon @con Repr x i t o a1
a (con b => Dict (con a)) -> Dict (con b) -> Dict (con a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon @con Repr x i t o b
b
  RTimes Repr x i t o a1
a Repr x i t o b
b -> Dict (con a)
con a1 => Dict (con a)
forall (a :: Constraint). a => Dict a
Dict (con a1 => Dict (con a)) -> Dict (con a1) -> Dict (con a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon @con Repr x i t o a1
a (con b => Dict (con a)) -> Dict (con b) -> Dict (con a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
forall (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon @con Repr x i t o b
b
  Repr x i t o a
RZero -> Dict (con a)
forall (a :: Constraint). a => Dict a
Dict
  Repr x i t o a
ROne -> Dict (con a)
forall (a :: Constraint). a => Dict a
Dict

reprCon1Comp :: forall (z :: Type) con (a :: Type -> Type) b. CompClosed con -> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))
reprCon1Comp :: forall z (con :: * -> Constraint) (a :: * -> *) (b :: * -> *).
CompClosed con
-> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))
reprCon1Comp c :: CompClosed con
c@CompClosed{} CRepr a
a CRepr b
b = Dict (con (a (b z)))
con (a (b z)) => Dict (con (a (b z)))
forall (a :: Constraint). a => Dict a
Dict (con (a (b z)) => Dict (con (a (b z))))
-> Dict (con (a (b z))) -> Dict (con (a (b z)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *).
con z =>
CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 @(b z) CompClosed con
c CRepr a
a (con (b z) => Dict (con (a (b z))))
-> Dict (con (b z)) -> Dict (con (a (b z)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *).
con z =>
CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 @z CompClosed con
c CRepr b
b

reprCon1 :: forall (z :: Type) (con :: Type -> Constraint) a. con z => CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 :: forall z (con :: * -> Constraint) (a :: * -> *).
con z =>
CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 c :: CompClosed con
c@CompClosed{forall x. Dict (con (One x))
forall x. con x => Dict (con (Id x))
forall (a :: * -> *) (b :: * -> *) x.
(con (a x), con (b x)) =>
Dict (con ((⊗) a b x))
forall (a :: * -> *) (b :: * -> *) x.
con (a (b x)) =>
Dict (con ((∘) a b x))
zero1Closed :: forall x. Dict (con (One x))
plus1Closed :: forall (a :: * -> *) (b :: * -> *) x.
(con (a x), con (b x)) =>
Dict (con ((⊗) a b x))
one1Closed :: forall x. con x => Dict (con (Id x))
times1Closed :: forall (a :: * -> *) (b :: * -> *) x.
con (a (b x)) =>
Dict (con ((∘) a b x))
zero1Closed :: forall (con :: * -> Constraint).
CompClosed con -> forall x. Dict (con (One x))
plus1Closed :: forall (con :: * -> Constraint).
CompClosed con
-> forall (a :: * -> *) (b :: * -> *) x.
   (con (a x), con (b x)) =>
   Dict (con ((⊗) a b x))
one1Closed :: forall (con :: * -> Constraint).
CompClosed con -> forall x. con x => Dict (con (Id x))
times1Closed :: forall (con :: * -> Constraint).
CompClosed con
-> forall (a :: * -> *) (b :: * -> *) x.
   con (a (b x)) =>
   Dict (con ((∘) a b x))
..} = \case
  RPlus Repr (∘) Id (⊗) One a1
a Repr (∘) Id (⊗) One b
b -> Dict (con (a z))
Dict (con ((⊗) a1 b z))
con (a1 z) => Dict (con (a z))
forall (a :: * -> *) (b :: * -> *) x.
(con (a x), con (b x)) =>
Dict (con ((⊗) a b x))
plus1Closed (con (a1 z) => Dict (con (a z)))
-> Dict (con (a1 z)) -> Dict (con (a z))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *).
con z =>
CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 @z CompClosed con
c Repr (∘) Id (⊗) One a1
a (con (b z) => Dict (con (a z)))
-> Dict (con (b z)) -> Dict (con (a z))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *).
con z =>
CompClosed con -> CRepr a -> Dict (con (a z))
reprCon1 @z CompClosed con
c Repr (∘) Id (⊗) One b
b
  RTimes Repr (∘) Id (⊗) One a1
a Repr (∘) Id (⊗) One b
b -> Dict (con (a z))
Dict (con ((∘) a1 b z))
con (a1 (b z)) => Dict (con (a z))
forall (a :: * -> *) (b :: * -> *) x.
con (a (b x)) =>
Dict (con ((∘) a b x))
times1Closed (con (a1 (b z)) => Dict (con (a z)))
-> Dict (con (a1 (b z))) -> Dict (con (a z))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall z (con :: * -> Constraint) (a :: * -> *) (b :: * -> *).
CompClosed con
-> con z => CRepr a -> CRepr b -> Dict (con (a (b z)))
reprCon1Comp @z CompClosed con
c Repr (∘) Id (⊗) One a1
a Repr (∘) Id (⊗) One b
b
  CRepr a
RZero -> Dict (con (a z))
Dict (con (One z))
forall x. Dict (con (One x))
zero1Closed
  CRepr a
ROne -> Dict (con (a z))
Dict (con (Id z))
forall x. con x => Dict (con (Id x))
one1Closed


type ProdObj :: forall {k}. (k -> Constraint) -> Constraint
class ProdObj (con :: k -> Constraint) where
  objprod :: (con a, con b) => Dict (con (a⊗b))
  objfstsnd :: forall z a b. (z ~ (a⊗b), con z) => Dict (con a, con b)
  objone :: Dict (con One)

type DualObj :: forall {k}. (k -> Constraint) -> Constraint
class ProdObj con => DualObj (con :: k -> Constraint) where
  objdual :: con a => Dict (con (Dual a))
  objdual' :: forall z a. (z ~ Dual a, con z) => Dict (con a)


objFstSnd :: forall con a b. ProdObj con => Dict (con (a ⊗ b)) -> Dict (con a, con b)
objFstSnd :: forall {k} (con :: k -> Constraint) (a :: k) (b :: k).
ProdObj con =>
Dict (con (a ⊗ b)) -> Dict (con a, con b)
objFstSnd Dict (con (a ⊗ b))
Dict = forall {k} (con :: k -> Constraint) (z :: k) (a :: k) (b :: k).
(ProdObj con, z ~ (a ⊗ b), con z) =>
Dict (con a, con b)
forall (con :: k -> Constraint) (z :: k) (a :: k) (b :: k).
(ProdObj con, z ~ (a ⊗ b), con z) =>
Dict (con a, con b)
objfstsnd @con @(a ⊗ b)

{-

type SumObj :: forall {k}. (k -> Constraint) -> Constraint
class SumObj (con :: k -> Constraint) where -- TensorClosed constraint causes problems in the Free module. (probably GHC bug)
  objsum :: (con a, con b) => Dict (con (a⊕b))
  objleftright :: forall z a b. (z ~ (a⊕b), con z) => Dict (con a, con b)
  objzero :: Dict (con Zero)


objSumProxy :: (SumObj con, con a, con b) => proxy1 a -> proxy2 b -> Dict (con (a⊕b))
objSumProxy _ _  = objsum

objProdProxy :: (ProdObj con, con a, con b) => proxy1 a -> proxy2 b -> Dict (con (a⊗b))
objProdProxy _ _  = objprod

instance ProdObj Trivial where
  objprod = Dict
  objfstsnd = Dict
  objone = Dict

instance SumObj Trivial where
  objsum = Dict
  objleftright = Dict
  objzero = Dict

instance ProdObj Finite where
  objprod = Dict
  objfstsnd = finiteFstsnd
  objone = Dict

instance SumObj Finite where
  objsum = Dict
  objleftright = finiteLeftRight
  objzero = Dict

-}

type Trivial :: k -> Constraint
class Trivial x
instance Trivial x



data Some1  f where
  Some1 :: f x -> Some1 f

sizedArbRepr :: Int -> Gen (Some1 (Repr x i t o))
sizedArbRepr :: forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbRepr Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = [(Int, Gen (Some1 (Repr x i t o)))] -> Gen (Some1 (Repr x i t o))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1,Some1 (Repr x i t o) -> Gen (Some1 (Repr x i t o))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure(Repr x i t o o -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 Repr x i t o o
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o o
RZero)), (Int
3,Some1 (Repr x i t o) -> Gen (Some1 (Repr x i t o))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure(Repr x i t o i -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 Repr x i t o i
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o i
ROne))]
  | Bool
otherwise = do
      Some1 Repr x i t o x
l <- Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbRepr  (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
      Some1 Repr x i t o x
r <- Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbRepr  (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
      [Some1 (Repr x i t o)] -> Gen (Some1 (Repr x i t o))
forall a. HasCallStack => [a] -> Gen a
elements [Repr x i t o (t x x) -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 (Repr x i t o x -> Repr x i t o x -> Repr x i t o (t x x)
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k)
       (a1 :: k) (b :: k).
Repr x i t o a1 -> Repr x i t o b -> Repr x i t o (t a1 b)
RPlus Repr x i t o x
l Repr x i t o x
r),Repr x i t o (x x x) -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 (Repr x i t o x -> Repr x i t o x -> Repr x i t o (x x x)
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k)
       (a1 :: k) (b :: k).
Repr x i t o a1 -> Repr x i t o b -> Repr x i t o (x a1 b)
RTimes Repr x i t o x
l Repr x i t o x
r)]

sizedArbSum :: Int -> Gen (Some1 (Repr x i t o))
sizedArbSum :: forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbSum Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = [(Int, Gen (Some1 (Repr x i t o)))] -> Gen (Some1 (Repr x i t o))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1,Some1 (Repr x i t o) -> Gen (Some1 (Repr x i t o))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure(Repr x i t o o -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 Repr x i t o o
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o o
RZero)), (Int
3,Some1 (Repr x i t o) -> Gen (Some1 (Repr x i t o))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure(Repr x i t o i -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 Repr x i t o i
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Repr x i t o i
ROne))]
  | Bool
otherwise = do
      Some1 Repr x i t o x
l <- Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbSum  (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
      Some1 Repr x i t o x
r <- Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbSum  (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
      [Some1 (Repr x i t o)] -> Gen (Some1 (Repr x i t o))
forall a. HasCallStack => [a] -> Gen a
elements [Repr x i t o (t x x) -> Some1 (Repr x i t o)
forall {k} (f :: k -> *) (x :: k). f x -> Some1 f
Some1 (Repr x i t o x -> Repr x i t o x -> Repr x i t o (t x x)
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k)
       (a1 :: k) (b :: k).
Repr x i t o a1 -> Repr x i t o b -> Repr x i t o (t a1 b)
RPlus Repr x i t o x
l Repr x i t o x
r)]


isArbitrary1 :: CRepr x -> Dict (Arbitrary1 x)
isArbitrary1 :: forall (x :: * -> *). CRepr x -> Dict (Arbitrary1 x)
isArbitrary1 = Repr (∘) Id (⊗) One x -> Dict (Arbitrary1 x)
forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon

isCoArbitrary :: MRepr x -> Dict (CoArbitrary x)
isCoArbitrary :: forall x. MRepr x -> Dict (CoArbitrary x)
isCoArbitrary = Repr (⊗) One (⊕) Zero x -> Dict (CoArbitrary x)
forall {k} (con :: k -> Constraint) (a :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Con' x con, Con' t con, con i, con o) =>
Repr x i t o a -> Dict (con a)
reprCon

instance Arbitrary (Some1 (Repr x i t o)) where
  arbitrary :: Gen (Some1 (Repr x i t o))
arbitrary = (Int -> Gen (Some1 (Repr x i t o))) -> Gen (Some1 (Repr x i t o))
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbRepr

forallSumType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property
forallSumType :: forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
(forall (a :: k). Repr x i t o a -> Property) -> Property
forallSumType forall (a :: k). Repr x i t o a -> Property
gen = Gen Prop -> Property
MkProperty (Gen Prop -> Property) -> Gen Prop -> Property
forall a b. (a -> b) -> a -> b
$ do
  Some1 Repr x i t o x
t <- ((Int -> Gen (Some1 (Repr x i t o))) -> Gen (Some1 (Repr x i t o))
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (Some1 (Repr x i t o))
forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
Int -> Gen (Some1 (Repr x i t o))
sizedArbSum :: Gen (Some1 (Repr x i t o)))
  Property -> Gen Prop
unProperty (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"obj: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Repr x i t o x -> String
forall a. Show a => a -> String
show Repr x i t o x
t) (Property -> Property
forall prop. Testable prop => prop -> Property
property (Repr x i t o x -> Property
forall (a :: k). Repr x i t o a -> Property
gen Repr x i t o x
t)))

forallType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property
forallType :: forall {k} (x :: k -> k -> k) (i :: k) (t :: k -> k -> k) (o :: k).
(forall (a :: k). Repr x i t o a -> Property) -> Property
forallType forall (a :: k). Repr x i t o a -> Property
gen = Gen Prop -> Property
MkProperty (Gen Prop -> Property) -> Gen Prop -> Property
forall a b. (a -> b) -> a -> b
$ do
  Some1 Repr x i t o x
t <- (Gen (Some1 (Repr x i t o))
forall a. Arbitrary a => Gen a
arbitrary :: Gen (Some1 (Repr x i t o)))
  Property -> Gen Prop
unProperty (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"obj: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Repr x i t o x -> String
forall a. Show a => a -> String
show Repr x i t o x
t) (Property -> Property
forall prop. Testable prop => prop -> Property
property (Repr x i t o x -> Property
forall (a :: k). Repr x i t o a -> Property
gen Repr x i t o x
t)))



arbitrary2' :: forall f a b proxy. Arbitrary (f a b) => proxy a -> proxy b -> Gen (f a b)
arbitrary2' :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k) (proxy :: k -> *).
Arbitrary (f a b) =>
proxy a -> proxy b -> Gen (f a b)
arbitrary2' proxy a
_ proxy b
_ = Gen (f a b)
forall a. Arbitrary a => Gen a
arbitrary

forallMorphism :: forall f a b x i t o. (Show (f a b), Arbitrary (f a b))
               => Repr x i t o a -> Repr x i t o b -> (f a b -> Property) -> Property
forallMorphism :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k) (x :: k -> k -> k)
       (i :: k) (t :: k -> k -> k) (o :: k).
(Show (f a b), Arbitrary (f a b)) =>
Repr x i t o a -> Repr x i t o b -> (f a b -> Property) -> Property
forallMorphism Repr x i t o a
t1 Repr x i t o b
t2 = Gen (f a b) -> (f a b -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Repr x i t o a -> Repr x i t o b -> Gen (f a b)
forall {k} (f :: k -> k -> *) (a :: k) (b :: k) (proxy :: k -> *).
Arbitrary (f a b) =>
proxy a -> proxy b -> Gen (f a b)
arbitrary2' Repr x i t o a
t1 Repr x i t o b
t2)