In short, depending on a coq.theory should also make its dependencies available. This issue is known to experts (at least Emilio and Rodolphe) but I didn't find a bug-tracker entry, and at Bluerock we are interested in a solution, so I figured I would make one.

Desired Behavior

Assume we have (coq.theory (name foo.logical.prefix) (theories direct_deps)) and a client client. Let us write deps for direct_deps plus any theories they depend on.
When client's bar.v tries to Require foo.logical.prefix.some_module., any used module from deps must be in scope — so clients of theory foo.logical.prefix need to depend on theories in deps, and shouldn't have to list deps explicitly among their dependencies — that can even change when foo.logical.prefix evolves.

Dune usually supports this, except if foo.logical.prefix is installed and clients are using dune-coq >= 0.8: in that case:

1. deps are also installed, but
2. installed theories are not available implicitly (https://dune.readthedocs.io/en/stable/coq.html#coq-language-version), and
3. installing foo.logical.prefix doesn't even record that it depends on direct_deps.

Hence, we should

4. change 3 and record the dependencies direct_deps of theories when installing them
5. and make those dependencies deps (so, direct_deps and their dependencies) available to client.

Possible future extension:

If client requires on some modules from dep in deps explicitly, arguably client should depend on dep explicitly — to be more robust if foo.logical.prefix drops the dependency on dep. Emilio has mentioned this a few times. However, nowadays dependencies are either available or not, and supporting this extension would require distinguishing direct and indirect uses — either in Coq, or in separate linters. Thankfully, that does not affect point 4: all (transitive) dependencies deps of foo.logical.prefix would be available as indirect dependencies for client, and none as direct dependencies. Hence, I propose to leave discussion of this to future work.

Implementation ideas

IIRC, Rodolphe proposed to reuse findlib for this:
https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/.5Blaodpath.5D.20Coqdep.20vs.2E.20Coqmod/near/285853410

Other threads about this

https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Dune-Coq.200.2E3.20dependency.20model
https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Adding.20transitive.20deps.20into.20theories

Example