Avoid non-exhaustive pattern match when using para recursion-scheme

Below is some code which I wrote as an exercise for using para from recursion-schemes (I know that this reduced example could also be solved using just cata, but let's ignore this for this question).

While doing this, I noticed that I have to do a non-exhaustive pattern match when I'm using para if I want to access the expression tree of any of the arguments to the Depth constructor.

I found an alternative implementation of gcata' and para' that don't have this issue, and also don't require a Comonad, but just a Functor instance on w. This makes me wonder: Why wasn't this version used in the implementation of recursion-schemes? Is there anything wrong with it, or are there just better ways to achieve what I'm looking for?

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Test where

import Data.Functor
import Data.Functor.Foldable

data ExprF a = Depth a a -- ^ Counts the maximum depth of the tree
             | Unit
  deriving Functor
type Expr = Fix ExprF

unit :: Expr
unit = Fix Unit

depth :: Expr -> Expr -> Expr
depth a b = Fix $ Depth a b

evalDepth :: Expr -> Int
evalDepth = cata phi where
  phi Unit = 0
  phi (Depth a b) = max a b + 1

eval :: Expr -> Int
eval = para phi where
  phi Unit = 0
  phi (Depth (Fix (Depth a b), _) _) = evalDepth a + evalDepth b
--            ^^^^^^^^^^^^^^^
-- at this point is the whole *current* expression tree, not just
-- the subtree that was given as first argument to `depth`

--------------------------------------------------------------------------------
-- Is this possible without definining gcata' / para' myself with the current API?

eval' :: Expr -> Int
eval' = para' phi where
  phi Unit = 0
  phi (Depth (a,_) (b,_)) = evalDepth a + evalDepth b
--            ^     ^
-- a and b are just the first and second argument to `depth`. No need
-- to do a pattern match which might go wrong.

gcata' :: forall t w a. (Foldable t, Functor w)
       => (forall b. Base t (w b) -> w (Base t b))
       -> (Base t (w a) -> a)
       -> t -> a
gcata' k g = fst . c where
  c :: t -> (a, w a)
  c y = (g x, g x <$ k x) where
    x :: Base t (w a)
    x = fmap (snd . c) . project $ y

para' :: (Foldable t, Unfoldable t) => (Base t (t,a) -> a) -> t -> a
para' = gcata' distPara

And here is an example how to use it:

eval' (depth (depth unit unit) (depth (depth unit unit) unit)
-- 3
eval (depth (depth unit unit) (depth (depth unit unit) unit))
-- 3

As you can see, both functions do the same, calculating the maximum depth of the tree (without counting the most outer depth call itself)

Solution

para is a very very special case.

Notably it uses (,) (Mu f) as its choice of Comonad.

This Comonad has a lot more structure than most.

Notably, it is left adjoint as (,) e -| (->) e.

Why does this matter? Well (,) e preserves colimits, and thus it only has one a inside of it.

So you can get away with g x <$ k x -- because you're only replacing one thing!

For any more interesting Comonad your gcata' should fail.

When you have more than one a to replace in w a, you're throwing away information, so this won't be a universal recursion scheme.