import Control.Arrow (right, left)
import Data.Void
import Test.QuickCheck
import Test.QuickCheck.Function

class Functor f => StrongSum f where
    distRight :: Either a (f b) -> f (Either a b)

instance StrongSum (Either a) where
    distRight = either (pure . Left) (fmap Right)

data WithInt a = WithInt Int a deriving (Eq, Show)

fromPair = uncurry WithInt
toPair (WithInt a b) = (a, b)

instance Arbitrary a => Arbitrary (WithInt a) where
    arbitrary = fromPair <$> arbitrary
    shrink = fmap fromPair . shrink . toPair

instance Functor WithInt where
   fmap f (WithInt no x) = WithInt no (f x)

instance StrongSum WithInt where
    distRight (Left x) = WithInt 0 (Left x)
    distRight (Right (WithInt no x)) = WithInt (no + 1) (Right x)

instance Applicative WithInt where
    pure = fmap (either id absurd) . distRight . Left
    WithInt a f <*> WithInt b x = WithInt (a + b) (f x)

law2 :: Fun Int Int -> Either Int (WithInt Int) -> Property
law2 (Fun _ f) x = lhs === rhs
  where
    lhs = distRight . left f $ x
    rhs = fmap (left f) . distRight $ x

-- | Doesn't hold
--
-- Not valid StrongSum, yet induced pure is still valid for the applicative (Writer Int)
law3 :: WithInt Int -> Property
law3 x = lhs === rhs
  where
    y = Right x :: Either Void (WithInt Int)
    lhs = either absurd (fmap Right) $ y
    rhs = distRight $ y

main :: IO ()
main = undefined