liftTermElabM uses a non-default meta context

[digama0]

In leanprover-community/batteries#671, there was an issue in the simpNF linter which was reduced to the setting of foApprox from the MetaM state. The problem is that not all methods for lifting a MetaM into IO to run it set the config in the same way:

import Lean.Meta.Tactic.Simp.Main
import Std.Tactic.OpenPrivate
import Std.Tactic.RunCmd

def MyPred (_ : Nat → Nat) : Prop := True
@[simp] theorem bad1 (f : Unit → Nat → Nat) : MyPred (f ()) = True := sorry

open Lean Elab Meta Tactic Term 

def test : MetaM Unit := withReducible do
  let (t, _) ← Elab.Term.TermElabM.run do
    Elab.Term.elabTerm (← `(fun f : Unit → Nat → Nat => MyPred (f ()))) none
  let ctx := { ← Simp.Context.mkDefault with config.decide := false }
  lambdaLetTelescope t fun _ lhs => do
    let ({ expr := lhs', .. }, _) ← simp lhs ctx
    if lhs == lhs' then throwError "did not simplify"

run_cmd Command.runTermElabM fun _ => test                             -- ok
run_cmd Command.liftTermElabM test                                     -- ok
run_elab test                                                          -- ok
run_meta test                                                          -- ok
#eval show TermElabM _ from test                                       -- ok
#eval show MetaM _ from test                                           -- fail
#eval show CoreM _ from MetaM.run' test {} {}                          -- fail
#eval show CoreM _ from MetaM.run' test { config.foApprox := true } {} -- ok
open private mkMetaContext from Lean.Elab.Command in
#eval show CoreM _ from MetaM.run' test mkMetaContext {}               -- ok

The fact that the default MetaM context constructed by {} is not the same as the MetaM context used by liftTermElabM (and transitively, most regular metaprogramming code) is error-prone since it means that you get different results depending on whether you use MetaM.run' or liftTermElabM, resulting in the above-demonstrated inconsistency. My recommendation is to have the current mkMetaContext be the default (i.e. make {} do the same thing as mkMetaContext).

cc: @leodemoura