Implicit homomorphism

One of the really nice features of macros and their mathematical first cousin notational definitions is that they leave their straightforward, recursive expansion implicit. When we write in math:

A ⇔ B = A ⇒ B ∧ B ⇒ A

what we really mean is that all occurrences of ⇔ should be recursively expanded within a term. But there's essentially an implicit structural recursion through all propositions in the logic (which is left open "until" all notational definitions have been provided) which expands any occurrences of notational definitions homomorphically through sub-propositions. We don't require anyone to go through the painstaking and virtually information-free process of explicitly marking all points of recursive expansion.

I would love a similar notational style for defining annotations. I often find myself defining an instrumentation function that inserts one or two kinds of extra pieces of information into a tree. Maybe term-rewriting would work pretty well for this. Say we're writing a function that annotates certain λ-expressions with their height. We could write

λ x . e → λ [ |e| ] x . e

and then leave the compatible, reflexive, and transitive closure of this rewriting rule implicit, since they're obvious.

Then I would really like some way to make this style of definition composable with other definitions, so for example I could define a type-checking-cum-instrumentation algorithm

Γ ⊢ e : τ → e'

where the instrumentation portion (→ e') is mostly left implicit.