forall_congr should be generalized from Prop to Sort

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

forall_congr currently has type

theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a)

but could (should?) have type

theorem forall_congr {α : Sort u} {p q : α → Sort v} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a)

in order to accept more proofs using conv mode, which uses this theorem.

Steps to Reproduce

axiom ID : Type → Type
axiom ID.eq {α} : ID α = α
example : ((x:Type) → ID x) = ((x : Type) → x) := by
  conv => lhs; ext; apply ID.eq

live.lean

Expected behavior: No error

Actual behavior: The following error, reported while hovering over example:

application type mismatch
  @forall_congr Type fun x => ID x
argument has type
  Type → Type
but function has type
  ∀ {p q : Type → Prop}, (∀ (a : Type), p a = q a) → (∀ (a : Type), p a) = ∀ (a : Type), q a

By comparison, the following works:

-- theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
theorem Better.forall_congr {α : Sort u} {p q : α → Sort v} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
  (funext h : p = q) ▸ rfl

example : ((x:Type) → ID x) = ((x : Type) → x) := by
  apply Better.forall_congr
  apply ID.eq

Versions

"4.19.0-nightly-2025-03-15"

Additional Information

Impact

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

Start by locating the definition of forall_congr and the implementation or tests for conv mode. Generalize the theorem from predicates returning Prop to families returning Sort, then run the provided ID reproduction and confirm that the conv example reports no error.