Examining the binding structure in a free monad AST

Take this simple base functor and other machinery for a free monad with binding terms:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad.Free

data ProgF r =
    FooF (Double -> r)
  | BarF Double (Int -> r)
  | EndF
  deriving Functor

type Program = Free ProgF

foo   = liftF (FooF id)
bar a = liftF (BarF a id)

And here's a simple program

prog :: Program Int
prog = do
  a <- foo
  bar a

It has the following (hand-crafted) AST:

prog =
  Free (FooF (\p0 ->
    Free (BarF p0 (\p1 ->
      Pure p1))

What I'd like to be able to do is reason about bound terms in the following way:

look at the Pure term in the AST
note the bound variables that occur there
annotate the corresponding binding nodes in the AST

Annotating a free monad AST directly via a cofree comonad seems to be impossible without doing some kind of pairing, but you could imagine getting to something like the following annotated AST (via, say, Fix) in which nodes binding variables that appear in Pure are annotated with Just True:

annotatedProg =
  Just False :< FooF (\p0 ->
    Just True :< BarF p0 (\p1 ->
      Nothing  :< EndF))

So: is there a way to inspect the bindings in a program like this in such an ad-hoc way? I.e., without introducing a distinct variable type à la this question, for example.

I suspect that this might be impossible to do. Options like data-reify are attractive but it seems to be extremely difficult or impossible to make ProgF an instance of the requisite typeclasses (Foldable, Traversable, MuRef).

Is that intuition correct, or is there some means to do this that I haven't considered? Note that I'm happy to entertain any gruesomely unsafe or dynamic means.

Solution

I'm satisfied that this is not possible to do by any 'sane' ad-hoc method, for much the same reason that it's not possible to examine the binding structure of e.g. \a -> \b -> \c -> b + a.