Failure to derive NoConfusionHom

[co-dan]

Sorry for a non-informative title. I stumbled upon this trying to add another constructor to the type o intristically-typed expressions in examples/definterp.v. I added the following constructor:

| Y {Γ} {t} : Expr Γ (t ⇒ t)

It made Derive NoConfusionHom for Expr fail (not completely fail, but leaving some goals unsolved).

Here is a minimized example showcasing the problem:

From Equations Require Import Equations.
Set Transparent Obligations.

Inductive ty :=
| tunit
| tarr (t1 t2 : ty)
.

Derive NoConfusion EqDec for ty.

Inductive tm : ty -> Type :=
| N : tm tunit
| T {t} : tm (tarr t t)
.

Derive Signature NoConfusion NoConfusionHom for tm.
(* Expectation : the previos vernacular solves all the goals *)

[mattam82]

I think you need UIP to derive this as you have a non-linear pattern (tarr t t) in your index.