fix(ClickSuggestions): instantiate all metavariables in the local context (#41001)

This PR fixes the panic in `#click_suggestions` that was reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23click_suggestions.20doesn.27t.20find.20lemma/near/606231763

There are two separate problems that this PR fixes:
1. The implementation of `#click_suggestion` assumes all metavariables have already been instantiated. This is valid because they are all instantiated at the very beginning. However, this was not done properly, causing the types of free variables to still be able to contain metavariables.
2. The function `viewKAbstractSubExpr` was able to reach its `unreachable!` block. The reason is that `kabstractPositions` calls `instantiateMVars` on the expression `e` but not on the pattern `p`, causing a discrepancy. This is fixed by removing the `instantiateMVars` call. This is fine, because in both of the use cases (`rw??` and `#click_suggestions`), the expressions already have instantiated metavariables at this point.

Author: JovanGerb

Mathlib/Lean/Meta/KAbstractPositions.lean

@@ -33,7 +33,6 @@ namespace Lean.Meta
 /-- Return the positions that `kabstract` would abstract for pattern `p` in expression `e`.
 i.e. the positions that unify with `p`. -/
 def kabstractPositions (p e : Expr) : MetaM (Array SubExpr.Pos) := do
-  let e ← instantiateMVars e
   let mctx ← getMCtx
   let pHeadIdx := p.toHeadIndex
   let pNumArgs := p.headNumArgs

Mathlib/Tactic/ClickSuggestions.lean

@@ -72,12 +72,13 @@ def viewKAbstractSubExpr' {m α}
 /-- Compute the suggestions. Use `token` for the output. -/
 public def generateSuggestions (loc : SubExpr.GoalsLocation) (parentDecl? : Option Name)
     (token : RefreshToken) : ClickSuggestionsM Unit := withReducible do
+  -- Instantiate all metavariables, so that we won't need to worry about this later on.
+  instantiateMVarDeclMVars loc.mvarId
+  loc.mvarId.withContext do
   -- TODO: instead of just putting `✝` after inaccessible names,
   -- we should figure out how to use `rename_i` to actually refer to shadowed local variables.
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
   Meta.withLCtx' lctx do
-  -- Instantiate all metavariables, so that we will not need to do this later on.
-  instantiateMVarDeclMVars loc.mvarId
   trackingComputation "click_suggestions" do
   let (fvarId?, pos) ← match loc.loc with
     | .hypType fvarId pos  => pure (some fvarId, pos)

MathlibTest/ClickSuggestions/Test.lean

@@ -184,3 +184,10 @@ example (a b c : Nat) : a + b + c = a + b := by
   click_test "/1" => "nth_rw 2 [Nat.add_comm a b]"
   click_test "/0/1/0/1" => "nth_rw 1 [Nat.add_comm a b]"
   exact test_sorry
+
+-- This example used to panic
+example : True := by
+  by_cases h : False
+  · click_test h "" => "rw [← true_eq_false_of_false h] at h"
+    trivial
+  · trivial