coqchk reports names from inner modules of opaque modules as axioms

[JasonGross]

Description of the problem

#5030 strikes again.

$ cat foo.v

Module Type A.
  Module B.
    Axiom t : Set.
  End B.
End A.

Module a : A.
  Module B.
    Definition t : Set := unit.
  End B.
End a.

Check a.B.t.

$ coqc -q -R . Top foo.v
a.B.t
     : Set
$ coqchk -silent -o -Q . Top foo.vo

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Top.foo.a.B.t

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

By contrast:

$ cat bar.v

Module Type A.
  Module B.
    Axiom t : Set.
  End B.
End A.

Module a <: A.
  Module B.
    Definition t : Set := unit.
  End B.
End a.

Check a.B.t.

$ coqc -q -R . Top bar.v
a.B.t
     : Set
$ coqchk -silent -o -Q . Top bar.vo

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms: <none>

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

cc @proux01 the author of #12076 and @ppedrot who seemed to be the main other person involved in the discussion

Coq Version

master / 8.13 / ef08abe

[ppedrot]

Well, the criterion was known to be neither sound nor complete, so ¯_(ツ)_/¯

[JasonGross]

Shouldn't it be possible to just have the code recurse over inner modules or something?

[JasonGross]

Like, would it be enough to have

coq/checker/mod_checking.ml

Lines 103 to 112 in aa92642

	let collect_constants_without_body sign mp =
	let collect_sf s lab = function
	| SFBconst cb ->
	let c = Constant.make2 mp lab in
	if Declareops.constant_has_body cb then s else Cset.add c s
	| SFBmind _ | SFBmodule _ | SFBmodtype _ -> s in
	match sign with
	| MoreFunctor _ -> Cset.empty (* currently ignored *)
	| NoFunctor struc ->
	List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) Cset.empty struc

call itself recursively when it hits SFBmodule?

[proux01]

Like, would it be enough to have [...] call itself recursively when it hits SFBmodule?

Quite probably yes (feel free to open a PR).

However, as noticed by Pierre Marie, this would remain incomplete (I wouldn't bet for unsound but he certainly knows better than me). Having something complete seems feasible but requires some work which I didn't found time for yet (unlikely to change in a near future unfortunately). So, if you want to dig into this, feel free to, but the best I can promise is a careful review (maybe could I trade it for a review of #12218 ;-) ).
Thanks for reporting anyway!