Instances for contravariant Coyoneda/Day

[thoughtpolice]

I stumbled across these while implementing Termination Combinators Forever. The termination combinator type Test described therein is the contravariant Coyoneda transformation of the Equivalence functor. Its combinators are characterized by these instances: given Test a ~ Coyoneda Equivalence a, then chosen and divided are exactly the combinators eitherT and pairT, and conquer is alwaysT. These can then be derived automatically, all thanks to -XDerivingVia. (Equivalence technically demands symmetry which WQOs violate, but for deriving instances we can ignore it since we don't derive any others that need it.)

instance Divisible f => Divisible (Coyoneda f) where
  conquer :: Coyoneda f a
  conquer = Coyoneda id conquer
  {-# INLINE conquer #-}

  divide :: (a -> (b, c)) -> Coyoneda f b -> Coyoneda f c -> Coyoneda f a
  divide cleave (Coyoneda fb b) (Coyoneda fc c)
    = Coyoneda (bimap fb fc . cleave) (divided b c)
  {-# INLINE divide #-}

instance Decidable f => Decidable (Coyoneda f) where
  lose :: (a -> Void) -> Coyoneda f a
  lose f = Coyoneda id (lose f)
  {-# INLINE lose #-}

  choose :: (a -> Either b c) -> Coyoneda f b -> Coyoneda f c -> Coyoneda f a
  choose fork (Coyoneda fb b) (Coyoneda fc c)
    = Coyoneda (bimap fb fc . fork) (chosen b c)
  {-# INLINE choose #-}

Proof of equality is left as a simple exercise:

-- Generalized implementation of 'Test' from "Termination Combinators Forever"
newtype Test (a :: Type) = Test (Coyoneda Equivalence a)
  -- DerivingVia is amazing.
  deriving Contravariant via (Coyoneda Equivalence)
  deriving Divisible     via (Coyoneda Equivalence)
  deriving Decidable     via (Coyoneda Equivalence)

-- 'WQO' constructor, backwards-compatible with the
-- termination-combinators package/paper.
pattern WQO :: forall a. forall b. (a -> b) -> (b -> b -> Bool) -> Test a
pattern WQO co eq = Test (Coyoneda co (Equivalence eq))
{-# COMPLETE WQO #-}

---

Also, while playing around more, I stumbled upon the following instance for contravariant Day:

contract :: Divisible f => Day f f a -> f a
contract (Day ca cb k) = divide k ca cb

instance Divisible f => Divisible (Day f f) where
  conquer :: Day f f a
  conquer = diag conquer

  divide :: (a -> (b, c)) -> Day f f b -> Day f f c -> Day f f a
  divide cleave fb fc = Day (contract fb) (contract fc) cleave

I feel there is something lurking within Divisible (Day f f) that can get us to Divisible (Coyoneda f), but I'm not sure.