doc: document problems with the variable and variables commands

tests/elabissues/vars.lean

@@ -0,0 +1,25 @@
+def f1 {α} [HasToString α] (a : α) : String := -- works
+">> " ++ toString a
+
+-- Moving `{α} [HasToString α]` to a `variables` break the example
+variables {α} [HasToString α]
+def f2 (a : α) : String :=
+">> " ++ toString a
+
+class Dummy (α : Type) := (val : α)
+
+/- The following fails because `variables {α : Type _} [Dummy α]` is processed as `variable {α : Type _} variable [Dummy α]`
+   The first command elaborates `α` as `variable {α : Type u_1}` where `u_1` is a fresh metavariable.
+   That is, in Lean3, metavariables are resolved before the end of the command. -/
+variables {α : Type _} [Dummy α]
+
+def f3 {α : Type _} [Dummy α] : α := -- works
+Dummy.val α
+
+/-
+In Lean4, we should use a different approach. We keep a metavariable context in the command elaborator.
+Before, a declaration `D` is sent to the kernel we resolve the metavariables occuring in `D`.
+We must implement a MetavarContext GC to make sure the metavariable context does not keep increasing.
+That is, after a declaration is sent to the kernel, we visit all variables in the elaborator context and
+instantiate assigned metavariables. Then, we delete all assigned metavariables.
+-/