Hovering over applications of non-constants with implicit parameters only doesn't show the implicit parameters

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

When hovering over applications of expressions that are not constants (e.g. free variables, lambda expressions) that don't have any explicit parameters, Lean only shows information for the unapplied constant instead of for the full expression

Context

Came up while debugging something else.

Steps to Reproduce

example (hide : {p : Prop} → Prop) (x : @hide True) : True := by

1. Go to the end of the line. The infoview should include a line x : hide
2. Hover/click on the hide in the line x : hide

Expected behavior: Lean shows @hide True : Prop, i.e. the expression with all parameters visible.

Actual behavior: Lean only shows @hide : {p : Prop} → Prop, making the implicit parameters unavailable to the user.

Versions

Lean 4.24.0-nightly-2025-08-27

Impact

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

Start with the minimal reproducer in the issue and inspect Lean's editor hover or infoview behavior for the hide application. Compare the displayed type for hide with the expected @hide True : Prop; done means hovering the non-constant application shows the full expression with its implicit parameter.