Misleading error message when deriving subterm for Prop-valued inductives

[kyoDralliam]

On Equations 1.2, Coq 8.10.0, the following code has a puzzling behaviour. Derive Subterm fail to solve all obligations when the indexed family has one constructor, but it works when the constructor is duplicated...

From Equations Require Import Equations.

Inductive t2 : unit -> Type :=
| base1 : t2 tt
| base2 :  t2 tt.

Derive Subterm for t2.
(** Solves all obligations  *)

Inductive t : unit -> Type :=
| base : t tt.

(* These 3 derive do not seem to help here... *)
Derive Signature for t.
Derive NoConfusion for t.
Derive NoConfusionHom for t.
Derive Subterm for t.
(** Fail to solve the well founded-ness obligation because of an anomaly
   "Uncaught exception Pretype_errors.PretypeError(_, _, _)." *)

[kyoDralliam]

The problem with t here is that it is "optimized" by Coq to land in Prop so it is expected that we cannot derive Subterm. For reference, it can be fixed either by replacing Type by Set or by adding an explicit universe annotation:

Inductive t@{u} : unit -> Type@{u} :=
| base : t tt.

Derive Subterm for t.

However it would be great if Equations could raise a more meaningful error when trying to derive the subterm relation of an inductive in Prop, for instance "Subterm relation cannot be derived for Prop-valued inductives".