Failure when generating below lemma

[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

The code handling the generation of the below helper functions is too conservative with regards to reduction, and fails in certain cases

Steps to Reproduce

inductive Bar : Nat -> Prop :=
  | bar e : (α → Bar e) -> Bar e --works

def Foo (F : α -> Prop) : Prop :=
  ∀ x , F x
inductive Bad : Nat -> Prop :=
  | bar e : Foo (fun _ => Bad e) -> Bad e --fails

Expected behavior: Both types get accepted with no error

Actual behavior: Some errors occur in mkCtorType in Lean/Meta/IndPredBelow.lean

Versions

Lean v4.2.0

Impact

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