`unknown free variable` error when inferring a forall argument

Prerequisites

• 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

unknown free variable error when trying to infer a forall argument.

Context

I encountered the error when playing around with continuous functions in Mathlib.

Steps to Reproduce

structure IsFoo {X Y : Type} (f : X → Y) : Prop where

structure FooFun (X Y : Type) where
  toFun : X → Y
  isFoo_toFun : IsFoo toFun

theorem isFoo_subtype_mk {X Y : Type} {p : Y → Prop} {f : X → Y} (_ : IsFoo f) (hp : ∀ x, p (f x)) :
    IsFoo (Y := Subtype p) fun x ↦ ⟨f x, hp x⟩ where

theorem isFoo_comp {X Y Z : Type} {f : X → Y} {g : Y → Z} : IsFoo (g ∘ f) where

variable (α : Type)

/-- error: unknown free variable `_fvar.752` -/
#guard_msgs in
def fooFun (x : α) : FooFun α { x : α × α // True } where
  toFun t := ⟨⟨x, t⟩, by trivial⟩
  isFoo_toFun := isFoo_subtype_mk isFoo_comp _

Expected behavior: The coolFun definition should work

Actual behavior: There's an error on def coolFun: unknown free variable `_fvar.794​

Versions

Lean 4.28.0-nightly-2025-12-15
Target: x86_64-unknown-linux-gnu

Additional Information

Doing any of these changes to the repro fixes it:

• Delete the by before the trivial
• Add by exact after cool_toFun :=
• Change the x in toFun to be t (this creates a type mismatch instead, probably because using t twice breaks the function composition inference)

Replacing cool_comp with sorry still errors, which is why I believe the error is related to inferring the last argument of cool_subtype_mk.

btw I'd love to know how to root-cause Lean bugs to get to the offending Lean/C++ code if it's not too much trouble to explain.

Impact

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

Start by running the self-contained reproducer against the Lean nightly release, using the linked live.lean-lang.org setup if useful. Trace the forall-argument inference involved in isFoo_subtype_mk and confirm that the FooFun definition elaborates without an unknown free variable error while preserving the reported working and failing variations.