Should `--dep` really emit `.krml` targets for files explicitly excluded by `--extract` ?

Currently, when generating a dependency file with `--dep`, F* produces rules for `.krml` files for all modules in the dependency cone of the files provided on the command line argument, even for modules explicitly excluded by `--extract`. In
project-everest/everparse#62, @nikswamy expresses the need for F* `--dep` to not produce rules for `.krml` files corresponding to such excluded modules, because some functions in such modules are using exceptions, which F* chokes on at extraction to `.krml`.

But then (in https://github.com/project-everest/everparse/pull/62#issuecomment-956317740), @msprotz warns against skipping such modules:
> This will break a large number of applications (e.g. Noise*, HACL*, and soon MLS*) that rely on this behavior.
>
> In those applications, we do --extract Spec.* -Impl.*, meaning "extract specs to OCaml and ditch low-level code" -- this allows us to then test the specs via OCaml compilation. Low-level compilation is controlled by kremlin's bundle flags.
>
> Note that changing this behavior might be dangerous, too, since for Low* code you may inadvertently remove a definition that would be needed by another file, resulting in Warning 2 errors and potentially invalid C code if, for instance, B.foo needs A.bar but you forgot that and passed --extract -A.

Similarly to Nik, I also need to skip producing .krml for some modules, namely `Steel.Effect.*`, `FStar.NMST` and the like containing things like effect definitions, which F* chokes on at extraction, in the context of the C model examples of #2349. More precisely, I simply exclude some files from the call to KReMLin in the Makefile: https://github.com/FStarLang/FStar/blob/49b166a96bdf2f0d4a6242c8f590ee876054acd5/examples/steel/arraystructs/Makefile#L63-L67
This is enough because, in the dependency file generated by `--dep`, no rule depends on building a `.krml` file, so omitting some of them will not break the dependency tree per se.

In practice for those Steel examples, this works because I manage to avoid the last point mentioned by Jonathan above, by maintaining a clear discipline that any `Steel.*` function used in those examples shall either have an extraction rule in `src/extraction/FStar.Extraction.Kremlin.fs` or be marked `inline_for_extraction`.

What should we do here?

Start with the --dep and --extract usage in examples/steel/arraystructs/Makefile, then read src/extraction/FStar.Extraction.Kremlin.fs to understand the excluded modules and extraction rules involved. Compare the generated dependency file with the modules omitted from the KReMLin call; done requires a decided behavior that preserves needed definitions while avoiding invalid .krml targets.

Written by the indexing model from the issue text.