Incorrect path constraint in with Module construct

[ppedrot]

Description of the problem

The path check in Mod_typing is incorrect in the submodule case, it uses the wrong modpath. This doesn't seem to lead to a proof of False, but is instead a source of incompleteness.

Small Rocq / Coq file to reproduce the bug

Module Type Inner.
  Parameter t : Type.
End Inner.

Module ConcreteInner : Inner.
  Definition t := True.
End ConcreteInner.

Module Wrapper.
  Module Sub := ConcreteInner.
End Wrapper.

Module Type MT.
  Module A := Wrapper.
End MT.

Module Type Good := MT with Module A.Sub := ConcreteInner.
(* No field named A in MT. *)

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response