`coq.extraction`: Adding a nested module to `extracted_modules` raises an internal error

[toku-sa-n]

Expected Behavior

No internal error occurs.

Actual Behavior

Internal error, please report upstream including the contents of _build/log.
Description:
  ("Rule has targets in different directories.",
  { targets =
      { files =
          set
            { "default/Extraction.glob"
            ; "default/Extraction.vo"
            ; "default/Foo/Bar.ml"
            ; "default/Foo/Bar.mli"
            }
      ; dirs = set {}
      }
  })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from Dune_engine__Rule.make in file "src/dune_engine/rule.ml", line
  91, characters 6-121
Called from Dune_rules__Super_context.add_rule in file
  "src/dune_rules/super_context.ml" (inlined), line 168, characters 13-46
Called from Dune_rules__Coq_rules.setup_coqc_rule in file
  "src/dune_rules/coq/coq_rules.ml", line 737, characters 2-401
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("load-dir", In_build_dir "default")
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases. 
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.

Reproduction

git clone https://github.com/toku-sa-n/dune-coq-ie && \
cd dune-coq-ie && \
git checkout minimum && \
dune build

Minimum reproduction repo: https://github.com/toku-sa-n/dune-coq-ie/tree/minimum Practical example (something I was trying to achieve): https://github.com/toku-sa-n/dune-coq-ie/tree/practical

Specifications

• Version of dune (output of dune --version): 3.16.0
• Version of ocaml (output of ocamlc --version) 5.1.1
• Version of coq (output of coqc --version) The Coq Proof Assistant, version 8.19.0 compiled with OCaml 5.1.1
• Operating system (distribution and version): uname -r: 6.6.30-gentoo

Additional information

dune build --verbose

Shared cache: disabled
Shared cache location: /home/hiroki/.cache/dune/db
Workspace root: /home/hiroki/git_repositories/dune-coq-ie
Auto-detected concurrency: 16
Dune context:
 { name = "default"
 ; kind = "default"
 ; profile = Dev
 ; merlin = true
 ; fdo_target_exe = None
 ; build_dir = In_build_dir "default"
 ; instrument_with = []
 }
Actual targets:
- alias @@default
Internal error, please report upstream including the contents of _build/log.
Description:
  ("Rule has targets in different directories.",
  { targets =
      { files =
          set
            { "default/Extraction.glob"
            ; "default/Extraction.vo"
            ; "default/Foo/Bar.ml"
            ; "default/Foo/Bar.mli"
            }
      ; dirs = set {}
      }
  })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from Dune_engine__Rule.make in file "src/dune_engine/rule.ml", line
  91, characters 6-121
Called from Dune_rules__Super_context.add_rule in file
  "src/dune_rules/super_context.ml" (inlined), line 168, characters 13-46
Called from Dune_rules__Coq_rules.setup_coqc_rule in file
  "src/dune_rules/coq/coq_rules.ml", line 737, characters 2-401
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("load-dir", In_build_dir "default")
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases. 
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.

_build/log

# dune build --verbose
# OCAMLPARAM: unset
# Shared cache: disabled
# Shared cache location: /home/hiroki/.cache/dune/db
# Workspace root: /home/hiroki/git_repositories/dune-coq-ie
# Auto-detected concurrency: 16
# Dune context:
#  { name = "default"
#  ; kind = "default"
#  ; profile = Dev
#  ; merlin = true
#  ; fdo_target_exe = None
#  ; build_dir = In_build_dir "default"
#  ; instrument_with = []
#  }
# Actual targets:
# - alias @@default
$ /home/hiroki/.opam/default/bin/ocamlc.opt -config > /tmp/dune_455f2f_output
$ /home/hiroki/.opam/default/bin/coqc --print-version -boot > /tmp/dune_16647b_output
$ /home/hiroki/.opam/default/bin/coqc --config > /tmp/dune_4c6144_output