fix variables in hints

server/GameServer/RpcHandlers.lean

@@ -114,25 +114,24 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
-  goal.withContext do
+  let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
+    | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
-      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+  let hints ← level.hints.filterMapM fun hint => do
-    let hints ← level.hints.filterMapM fun hint => do
+    openAbstractCtxResult hint.goal fun hintFVars hintGoal => goal.withContext do
-      openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
+      if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
-        if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
+      then
+        let lctx := (← goal.getDecl).lctx
+        if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
         then
-          let lctx := (← goal.getDecl).lctx
+          let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
-          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
-          then
+          let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
-            let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
+          let text ← (MessageData.withContext ctx text).toString
-            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
+          return some { text := text, hidden := hint.hidden }
-            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+        else return none
-            let text ← (MessageData.withContext ctx text).toString
+      else
-            return some { text := text, hidden := hint.hidden }
+        return none
-          else return none
+  return hints
-        else
-          return none
-    return hints
 
 open RequestM in
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do