newtype Codensity (m::TYPE rep -> Type) a = Codensity
  { runCodensity :: forall b. (a -> m b) -> m b
  }

Codensity :: (TYPE rep -> TYPE rep') -> (TYPE rep'' -> Type)

class GTraversable t where
  gtraverse :: (a -> f b) -> t a -> Curried (Yoneda f) (Yoneda f) a

Eq1 f => Eq1 (Coyoneda f)

ibind :: (a -> Ran k j b) -> (Ran j i a -> Ran k i b)
ibind k (Ran m) = Ran (\c -> m (\a -> runRan (k a) c))

iextend :: (Lan k j a -> b) -> (Lan k i a -> Lan j i b)
iextend f (Lan h ws) = Lan (f . Lan h) ws

class IxApplicative m => IxMonad m where
  ibind :: (a -> m j k b) -> (m i j a -> m i k b)

class IxCopointed w => IxComonad w where
  iextend :: (w j k a -> b) -> (w i k a -> w i j b)

Yoneda m >>= k = Yoneda (\f -> m id >>= \a -> runYoneda (k a) f)

Yoneda m >>= k = Yoneda (\f -> join . m $ \a -> runYoneda (k a) f)

-- Codensity (Const r) ~ Cont r
instance MonadCont (Codensity (Const r)) where
  callCC f = Codensity (\k -> mapConst $ runCodensity (f (\x -> Codensity (\_ -> mapConst $ k x))) k)
    where
      mapConst :: Const r a -> Const r b
      mapConst = Const . runConst

-- using callCC of m
instance MonadCont m => MonadCont (Codensity m) where
  callCC f = join . lift $ callCC (\k -> return $ f (lift . k . return))

newtype IOSim s a = IOSim { unIOSim :: forall r. (a -> SimA s r) -> SimA s r }

instance Functor (IOSim s) where
    {-# INLINE fmap #-}
    fmap f = \d -> IOSim $ oneShot $ \k -> unIOSim d (k . f)

instance Applicative (IOSim s) where
    {-# INLINE pure #-}
    {-# INLINE (<*>) #-}
    {-# INLINE (*>) #-}
    pure = \x -> IOSim $ oneShot $ \k -> k x
    (<*>) = \df dx -> IOSim $ oneShot $ \k -> unIOSim df (\f -> unIOSim dx (\x -> k (f x)))
    (*>) = \dm dn -> IOSim $ oneShot $ \k -> unIOSim dm (\_ -> unIOSim dn k)

instance Monad (IOSim s) where
    {-# INLINE (>>=) #-}
    {-# INLINE (>>) #-}
    return = pure
    (>>=) = \dm f -> IOSim $ oneShot $ \k -> unIOSim dm (\m -> unIOSim (f m) k)
    (>>) = (*>)

Codensity :: (k -> Type) -> (Type -> Type)

fold :: (forall xx. (f xx -> a) -> (g x -> lan)) -> (Lan f g a -> lan)
fold a (Lan b c) = a b c
-- as in paper, or
fold' :: Lan f g a -> (forall lan. (forall xx. (f xx -> a) -> (g xx -> lan)) -> lan)
fold' (Lan a b) c = c a b

hoistLan :: (g ~> g') -> (Lan f g ~> Lan f g')
hoistLan tau = fold (\g -> Lan g . tau)

data Comp :: (k -> Type) -> (k -> Type) -> (k' -> Type) -> (k' -> Type) where
  Comp :: (j xx -> g a) -> (f xx -> Comp j f g a)

foldComp :: (forall xx. (j xx -> g a) -> (f xx -> r)) -> (Comp j f g a -> r)
foldComp f (Comp a b) = f a b

intro2 :: m ~> Comp rel m rel
intro2 = Comp id

elim1 :: Comp rel rel m ~> m
elim1 = foldComp id

disassoc :: Comp rel (Comp rel f g) h ~> Comp rel f (Comp rel g h)
disassoc = foldComp $ \g -> foldComp $ \f -> Comp (Comp g . f) 

class RelMonad m rel where
  royalReturn :: rel ~> m
  relativeBind :: (rel a -> m b) -> (m a -> m b)

unit :: RelMonad m rel => rel ~> m
unit = royalReturn

mult :: RelMonad m rel => Comp rel m m ~> m
mult = foldComp relativeBind 

instance (Functor f, Representable g) => Distributive (Lan f g) where
  distribute :: Functor h => h (Lan f g a) -> Lan f g (h a)
  distribute = distributeRep

instance (Functor f, Representable g) => Representable (Lan f g) where
  type Rep (Lan f g) = f (Rep g)

  index :: Lan f g a -> (f (Rep g) -> a)
  index (Lan f g) = f . fmap (index g)

  tabulate :: (f (Rep g) -> a) -> Lan f g a
  tabulate = (`Lan` tabulate id)

data Day2__ :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
  Day2__ :: f xx -> g (xx -> a) -> (Day2__ f g) a

data Day3__ :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
  Day3__ :: f (xx -> a) -> g xx -> (Day3__ f g) a

day2 :: forall f g a. Functor g => Day f g a -> Day2__ f g a
day2 (Day fa gb f) = Day2__ fa (flip f gb)

day3 :: Functor f => Day f g a -> Day3__ f g a
day3 (Day fa gb f) = Day3__ (fmap f fa) gb 

pattern Day2 :: forall f g a. Functor g => forall xx. f xx -> g (xx -> a) -> Day f g a
pattern Day2 fa gb <- (day2 -> Day2__ fa gb)
  where Day2 fa gb = Day fa gb (&)

pattern Day3 :: forall f g a. Functor f => forall xx. f (xx -> a) -> g xx -> Day f g a
pattern Day3 fa gb <- (day3 -> Day3__ fa gb)
  where Day3 fa gb = Day fa gb id

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 #-}

-- 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 #-}

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

instance MonadTrans Codensity where
  lift = frob
frob :: forall m a . Monad m => m a -> Codensity m a
frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a)
newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b)
newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b)
blah :: Mag m a -> m a -> Mag2 m a
blah (Mag p) q = Mag2 (p q)

instance Semigroup a => Semigroup (Codensity m a) where
  (<>) = liftA2 (<>)

instance Monoid a => Monoid (Codensity m a) where
  mempty = pure mempty

#if !(MIN_VERSION_base(5,0,0))
  mappend = liftA2 (<>)
#endif

improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
improve m = lowerCodensity m

lowerCodensity :: Monad f => Codensity f a -> f a

improve' :: (Functor f, MonadFree f m') =>
            (forall m . MonadFree f m => m a) -> m' a
improve' m = lowerCodensity m

lowerCodensity :: Monad m => Codensity m a -> m a
lowerCodensity a = runCodensity a return

lowerCodensity :: Applicative f => Codensity f a -> f a
lowerCodensity a = runCodensity a pure

  foldr c n (Coyoneda k a) = foldr (c . k) n a 
  foldl f b (Coyoneda k a) = foldl (\acc -> f acc . k) go b a
  -- foldl', foldr', foldl1, foldr1 similarly
  toList (Coyoneda k a) = map k (toList a) -- but this is arguably worse than the default!
  length (Coyoneda _ a) = length a
  null (Coyoneda _ a) = null a

  forall r. w (a -> r) -> r
~ forall r x. (x -> a -> r) -> w x -> r
~ forall r x. ((x, a) -> r) -> w x -> r
~ forall x. w x -> (x, a)

newtype CovT w m a = CovT { runCovT :: forall x. w x -> m (x, a) }

instance Functor m => Functor (CovT w m) where
  fmap f cov = CovT $ \w -> (fmap . fmap) f (runCovT cov w)

instance (Comonad w, Monad m) => Applicative (CovT w m) where
  pure a = CovT $ \w -> pure (extract w, a)
  (<*>) = ap

instance (Comonad w, Monad m) => Monad (CovT w m) where
  m >>= f = CovT $ \w -> do
    (w', a) <- runCovT m (duplicate w)
    runCovT (f a) w'

instance f₁ ~ f₂ => Applicative (Ran f₁ f₂) where
  pure x = Ran (\k -> k x)
  Ran f <*> Ran g = Ran (\bfr -> f (\ab -> g (bfr . ab)))

instance f₁ ~ f₂ => Monad (Ran f₁ f₂) where
  return = pure
  m >>= k = Ran (\c -> runRan m (\a -> runRan (k a) c))
-- etc.

instance f₁ ~ f₂ => Comonad (Lan f₁ f₂) where
  duplicate (Lan f ws) = Lan (Lan f) ws
  extract (Lan f a) = f a
-- etc.

instance (Identity ~ id, Applicative f) => Applicative (Ran id f) where
  pure a = Ran (\f -> pure (runIdentity (f a)))

-- ... 
instance Identity ~ id => Foldable (Codensity id) where
  foldMap f = foldMap f . lowerYoneda . ranToYoneda . codensityToRan

data Lan :: (k -> Type) -> (k -> Type) -> (Type -> Type) where
  Lan :: (g b -> a) -> (h b) -> Lan g h a

newtype Ran :: (k -> Type) -> (k -> Type) -> (Type -> Type) where
  Ran :: { runRan :: forall b. (a -> g b) -> h b } -> Ran g h a

data VE w r = Val w | E (r (VE w r))

newtype Eff r a = Eff{runEff :: ∀ w. (a → VE w r) → VE w r}

send :: (∀ w. (a → VE w r) → r (VE w r)) → Eff r a
send f = Eff $ \k → E (f k)

admin :: Eff r w → VE w r
admin (Eff m) = m Val

send :: (forall x. (a -> Free f x) -> f (Free f x)) -> Codensity (Free f) a
send eff = Codensity \next -> Free (eff next)

-- still need to prove that MonadFix laws hold
instance MonadFix m => MonadFix (Codensity m) where
    mfix :: (a -> Codensity m a) -> Codensity m a
    mfix f = lift (mfix (lowerCodensity . f))

composeRan' :: forall compose f g a. Composition compose => Ran f (Codensity g) a -> Ran (compose f g) g a
composeRan' = coerce (composeRan @compose @f @g @g @a)

decomposeRan' :: forall compose f g a. (Composition compose, Functor f) => Ran (compose f g) g a -> Ran f (Codensity g) a
decomposeRan' = coerce (decomposeRan @compose @f @g @g @a)