Description of the problem

I defined a new type which has a private type as a parameter, and I tried to do a case analysis on the new type, it failed with the message "case analysis on a private type".

I guess this is a bug because I did a case analysis on the new type not the private type. Or is there any theory behind it that prevents from doing a case analysis on a type based on the private type?

The funny thing is that if I print the function new_type_ind, which is defined automatically as the new_type is defined, and try to define a new function with the same definition, it also fails with the same error.

If there is a reason to prevent the case analysis on the new type, this is definitely a bug since the function new_type_ind was defined normally.

This problem arises when I want to make new type to be also a private type. Doing HoTT stuffs, I want to impose the custom computation rule on the new type but there is no way to do that.

Small Rocq / Coq file to reproduce the bug

Module P.
Private Inductive private_type :=
|cons:private_type.
End P.
Import P.

Inductive new_type: private_type-> Type :=
|cons2: forall m:private_type, new_type m.

Fail Definition my_fun (x:private_type) (y:new_type x) :=
  match y with
  |cons2 _ =>True
  end.

Print new_type_ind.

(*The copy of the definition of new_type_ind *)
Fail Definition my_fun2:=fun
  (P : forall p : private_type, new_type p -> Prop)
  (f : forall m : private_type, P m (cons2 m))
  (p : private_type) (n : new_type p) =>
match
  n as n0 in (new_type p0) return (P p0 n0)
with
| cons2 m => f m
end.

Version of Rocq / Coq where this bug occurs

8.19.1

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

No response