genInjectivity failure

[arthur-adjedj]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In some cases, Lean fails to generate injectivity lemmas for inductive types

Context

The issue was first discovered in lean-reflection

Steps to Reproduce

MWE:

inductive Tyₛ : Type (u+1)
| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ

inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)

Expected behavior: No error

Actual behavior: Error:

application type mismatch
  Tyₛ.SPi T A
argument has type
  T✝ → Tyₛ
but function has type
  (T → Tyₛ) → Tyₛ

Versions

4.6.0-rc1
Web

Additional Information

The generated injectivity lemma looks like this:

theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
  Tmₛ.app a arg = Tmₛ.app a_1 arg →
    T = T_1 ∧ HEq a a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq 

The error happens because T is duplicated where it shouldn't be. In order for the injectivity lemma to be as general as possible, Lean duplicates any argument which doesn't occur in the end type of the constructor (here, in Tmₛ (A arg)). However, this is not precise enough, as some terms of that type may still depend on the variable: here, T doesn't appear in that type, but appears in the type of A. A solution would be to also check the occurence of variables inside the types of free variables appearing in the end type.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.