Error: Ill-formed constant ROrderedType.R_as_OT.t: expected canonical name Stdlib.Reals.ROrderedType.R_as_DT.t but found Stdlib.Reals.ROrderedType.R_as_OT.t

[JasonGross]

Description of the problem

I'm not 100% sure this is not the fault of some patch I have on top of Rocq, but should be pretty easy to check

Small Rocq / Coq file to reproduce the bug

Require Stdlib.Reals.ROrderedType. Check ROrderedType.R_as_OT.t.

Version of Rocq / Coq where this bug occurs

9.2

Interface of Rocq / Coq where this bug occurs

No response

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

9.1

[ppedrot]

Can reproduce on master (f5272de). A proof of False in the pipes?

[ppedrot]

Self-contained:

Axiom R : Set.

Module Type Typ.
  Parameter Inline(10) t : Type.
End Typ.

Module UsualIsEq (E:Typ).
End UsualIsEq.

Module Make_UDTF (M:Typ) := M <+ UsualIsEq.

Module R_as_UBE.
 Definition t := R.
End R_as_UBE.

Module R_as_DT := Make_UDTF R_as_UBE.

Module R_as_OT.
 Include R_as_DT.
End R_as_OT.

Definition foo := R_as_OT.t.

[SkySkimmer]

further reduced

Axiom R : Set.

Module Type Typ.
  Parameter Inline(10) t : Type.
End Typ.

Module Make_UDTF (M:Typ).
  Include M.
End Make_UDTF.

Module R_as_UBE.
 Definition t := R.
End R_as_UBE.

Module R_as_DT := Make_UDTF R_as_UBE.

Module R_as_OT.
 Include R_as_DT.
End R_as_OT.

Definition foo := R_as_OT.t.

[ppedrot]

The kernel seems to have the right data, it's the nametab which is fed a broken name.

[ppedrot]

Correction: we store inlining hints in the safe env resolver, which is wrong. I don't know if there is a way to exploit this into a broken substitution but it's definitely foul-smelling.