bug: `specialize` tactic is missing an occurs check

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The tactic specialize does not check to see if the main goal occurs in the value that to which it assigns the main goal. This causes a stack overflow:

open Lean Meta Elab Tactic in
/-- `rename_main_goal a` renames the main goal to `a`. -/
elab "rename_main_goal " n:ident : tactic => do
  let g ← getMainGoal
  g.setUserName n.getId

example (h : True → True) : True := by
  rename_main_goal a
  specialize h ?a -- stack overflow

Steps to Reproduce

1. Obtain a goal and a hypothesis in that goal's context which has an argument of the same type as the goal.
2. With that goal as the main goal, specialize the hypothesis applied to that goal.

Expected behavior: An error pointing out that the goal occurs in the specialized value.

Actual behavior: Stack overflow

Reproduces how often: Always

Versions

4.0.0-rc4; macOS Ventura 13.4.1 (Intel-based)

Start by running the self-contained reproducer in the issue and inspect the specialize tactic entry point and its goal-assignment path. Confirm that applying the main goal produces an error about the goal occurring in the specialized value rather than a stack overflow, then add or run a regression test for the example.