How can you build a coinductive memoization table for recursive functions over binary trees? The StreamMemo library for Coq illustrates how to memoize a function f : nat -&gt; A over the natural numbers.  In particular when f (S n) = g (f n), the imemo_make shares the computation of recursive calls.

Suppose instead of natural numbers, we want to memoize recursive functions over binary trees:

Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -&gt; binTree -&gt; binTree.


Suppose we have a function f : binTree -&gt; A that is structurally recursive, meaning that there is a function g : A -&gt; A -&gt; A such that f (Branch x y) = g (f x) (f y).  How do we build a similar memo table for f in Coq such that the recursive computations are shared?

In Haskell, it is not too hard to build such a memo table (see MemoTrie for example) and tie-the-knot.  Clearly such memo tables are productive.  How can we arrange things to convince a dependently typed language to accept such knot tying is productive?

Although I've specified the problem in Coq, I wouldd be happy with an answer in Agda or any other dependently typed language as well.
It's easy enough to get the recursion pattern to work with sized types.
Hopefully the sharing is preserved through compilation![1]

module _ where

open import Size
open import Data.Nat

data BT (i : Size) : Set where
  Leaf : BT i
  Branch : ∀ {j : Size&lt; i} → BT j → BT j → BT i

record Memo (A : Set) (i : Size) : Set where
  coinductive
  field
    leaf : A
    branch : ∀ {j : Size&lt; i} → Memo (Memo A j) j

open Memo

trie : ∀ {i} {A} → (BT i → A) → Memo A i
trie f .leaf = f Leaf
trie f .branch = trie (\ l → trie \ r → f (Branch l r))

untrie : ∀ {i A} → Memo A i → BT i → A
untrie m Leaf         = m .leaf
untrie m (Branch l r) = untrie (untrie (m .branch) l) r

memo : ∀ {i A} → (BT i → A) → BT i → A
memo f = untrie (trie f)

memoFix : ∀ {A : Set} → A → (A → A → A) → ∀ {i} → BT i → A
memoFix {A} lf br = go
 where
  go h : ∀ {i} → BT i → A
  go = memo h
  h Leaf = lf
  h (Branch l r) = br (go l) (go r)


[1] https://github.com/agda/agda/issues/2918