/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Data.LOption
import Lean.Environment
import Lean.Class
import Lean.ReducibilityAttrs
import Lean.Util.Trace
import Lean.Util.RecDepth
import Lean.Util.PPExt
import Lean.Compiler.InlineAttrs
import Lean.Meta.TransparencyMode
import Lean.Meta.DiscrTreeTypes
import Lean.Eval
import Lean.CoreM

/-
This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks.
1- Weak head normal form computation with support for metavariables and transparency modes.
2- Definitionally equality checking with support for metavariables (aka unification modulo definitional equality).
3- Type inference.
4- Type class resolution.

They are packed into the MetaM monad.
-/

namespace Lean.Meta

builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck

structure Config where
  foApprox           : Bool := false
  ctxApprox          : Bool := false
  quasiPatternApprox : Bool := false
  /- When `constApprox` is set to true,
     we solve `?m t =?= c` using
     `?m := fun _ => c`
     when `?m t` is not a higher-order pattern and `c` is not an application as -/
  constApprox        : Bool := false
  /-
    When the following flag is set,
    `isDefEq` throws the exeption `Exeption.isDefEqStuck`
    whenever it encounters a constraint `?m ... =?= t` where
    `?m` is read only.
    This feature is useful for type class resolution where
    we may want to notify the caller that the TC problem may be solveable
    later after it assigns `?m`. -/
  isDefEqStuckEx     : Bool := false
  transparency       : TransparencyMode := TransparencyMode.default
  /- If zetaNonDep == false, then non dependent let-decls are not zeta expanded. -/
  zetaNonDep         : Bool := true
  /- When `trackZeta == true`, we store zetaFVarIds all free variables that have been zeta-expanded. -/
  trackZeta          : Bool := false
  unificationHints   : Bool := true

structure ParamInfo where
  implicit     : Bool      := false
  instImplicit : Bool      := false
  hasFwdDeps   : Bool      := false
  backDeps     : Array Nat := #[]

instance : Inhabited ParamInfo := ⟨{}⟩

def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
  !p.implicit && p.instImplicit

structure FunInfo where
  paramInfo  : Array ParamInfo := #[]
  resultDeps : Array Nat       := #[]

structure InfoCacheKey where
  transparency : TransparencyMode
  expr         : Expr
  nargs?       : Option Nat

namespace InfoCacheKey
instance : Inhabited InfoCacheKey := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩
instance : Hashable InfoCacheKey :=
  ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩
instance : BEq InfoCacheKey :=
  ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩
end InfoCacheKey

open Std (PersistentArray PersistentHashMap)

abbrev SynthInstanceCache := PersistentHashMap Expr (Option Expr)

structure Cache where
  inferType     : PersistentExprStructMap Expr := {}
  funInfo       : PersistentHashMap InfoCacheKey FunInfo := {}
  synthInstance : SynthInstanceCache := {}
  whnfDefault   : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.default`
  whnfAll       : PersistentExprStructMap Expr := {} -- cache for closed terms and `TransparencyMode.all`

structure PostponedEntry where
  lhs       : Level
  rhs       : Level

structure State where
  mctx        : MetavarContext := {}
  cache       : Cache := {}
  /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
  zetaFVarIds : NameSet := {}
  postponed   : PersistentArray PostponedEntry := {}

instance : Inhabited State := ⟨{}⟩

structure Context where
  config         : Config         := {}
  lctx           : LocalContext   := {}
  localInstances : LocalInstances := #[]

abbrev MetaM  := ReaderT Context $ StateRefT State CoreM

instance : Inhabited (MetaM α) := {
  default := fun _ _ => arbitrary
}

instance : MonadLCtx MetaM := {
  getLCtx := do pure (← read).lctx
}

instance : MonadMCtx MetaM := {
  getMCtx    := do pure (← get).mctx,
  modifyMCtx := fun f => modify fun s => { s with mctx := f s.mctx }
}

instance : AddMessageContext MetaM := {
  addMessageContext := addMessageContextFull
}

@[inline] def MetaM.run (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
  x ctx |>.run s

@[inline] def MetaM.run' (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM α :=
  Prod.fst <$> x.run ctx s

@[inline] def MetaM.toIO (x : MetaM α) (ctxCore : Core.Context) (sCore : Core.State) (ctx : Context := {}) (s : State := {}) : IO (α × Core.State × State) := do
  let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore
  pure (a, sCore, s)

instance [MetaEval α] : MetaEval (MetaM α) :=
  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩

protected def throwIsDefEqStuck {α} : MetaM α :=
  throw $ Exception.internal isDefEqStuckExceptionId

builtin_initialize
  registerTraceClass `Meta
  registerTraceClass `Meta.debug

@[inline] def liftMetaM [MonadLiftT MetaM m] (x : MetaM α) : m α :=
  liftM x

@[inline] def mapMetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, MetaM α → MetaM α) {α} (x : m α) : m α :=
  controlAt MetaM fun runInBase => f $ runInBase x

@[inline] def map1MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → MetaM α) → MetaM α) {α} (k : β → m α) : m α :=
  controlAt MetaM fun runInBase => f fun b => runInBase $ k b

@[inline] def map2MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → γ → MetaM α) → MetaM α) {α} (k : β → γ → m α) : m α :=
  controlAt MetaM fun runInBase => f fun b c => runInBase $ k b c

section Methods
variables {m : Type → Type} [MonadLiftT MetaM m]
variables {n : Type → Type} [MonadControlT MetaM n] [Monad n]

def getLocalInstances : m LocalInstances := liftMetaM do pure (← read).localInstances
def getConfig : m Config := liftMetaM do pure (← read).config
def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
def resetZetaFVarIds : m Unit := liftMetaM $ modify fun s => { s with zetaFVarIds := {} }
def getZetaFVarIds : m NameSet := liftMetaM do pure (← get).zetaFVarIds

def getPostponed : m (PersistentArray PostponedEntry) := liftMetaM do
  pure (← get).postponed

def setPostponed (postponed : PersistentArray PostponedEntry) : m Unit := liftMetaM $
  modify fun s => { s with postponed := postponed }

@[inline] def modifyPostponed (f : PersistentArray PostponedEntry → PersistentArray PostponedEntry) : m Unit := liftMetaM $
  modify fun s => { s with postponed := f s.postponed }

builtin_initialize whnfRef : IO.Ref (Expr → MetaM Expr) ← IO.mkRef fun _ => throwError "whnf implementation was not set"
builtin_initialize inferTypeRef : IO.Ref (Expr → MetaM Expr) ← IO.mkRef fun _ => throwError "inferType implementation was not set"
builtin_initialize isExprDefEqAuxRef : IO.Ref (Expr → Expr → MetaM Bool) ← IO.mkRef fun _ _ => throwError "isDefEq implementation was not set"
builtin_initialize synthPendingRef : IO.Ref (MVarId → MetaM Bool) ← IO.mkRef fun _ => pure false

def whnf (e : Expr) : m Expr :=
  liftMetaM $ withIncRecDepth do (← whnfRef.get) e

def whnfForall [Monad m] (e : Expr) : m Expr := do
  let e' ← whnf e
  if e'.isForall then pure e' else pure e

def inferType (e : Expr) : m Expr :=
  liftMetaM $ withIncRecDepth do (← inferTypeRef.get) e

protected def isExprDefEqAux (t s : Expr) : MetaM Bool :=
  withIncRecDepth do (← isExprDefEqAuxRef.get) t s

protected def synthPending (mvarId : MVarId) : MetaM Bool :=
  withIncRecDepth do (← synthPendingRef.get) mvarId

-- withIncRecDepth for a monad `n` such that `[MonadControlT MetaM n]`
protected def withIncRecDepth {α} (x : n α) : n α :=
  mapMetaM (withIncRecDepth (m := MetaM)) x

private def mkFreshExprMVarAtCore
    (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind) (userName : Name) (numScopeArgs : Nat) : MetaM Expr := do
  modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId userName lctx localInsts type kind numScopeArgs;
  pure $ mkMVar mvarId

def mkFreshExprMVarAt
    (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr)
    (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0)
    : m Expr := liftMetaM do
  let mvarId ← mkFreshId
  mkFreshExprMVarAtCore mvarId lctx localInsts type kind userName numScopeArgs

def mkFreshLevelMVar : m Level := liftMetaM do
  let mvarId ← mkFreshId
  modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId;
  pure $ mkLevelMVar mvarId

private def mkFreshExprMVarCore (type : Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr := do
  let lctx ← getLCtx
  let localInsts ← getLocalInstances
  mkFreshExprMVarAt lctx localInsts type kind userName

private def mkFreshExprMVarImpl (type? : Option Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr :=
  match type? with
  | some type => mkFreshExprMVarCore type kind userName
  | none      => do
    let u ← mkFreshLevelMVar
    let type ← mkFreshExprMVarCore (mkSort u) MetavarKind.natural Name.anonymous
    mkFreshExprMVarCore type kind userName

def mkFreshExprMVar (type? : Option Expr) (kind := MetavarKind.natural) (userName := Name.anonymous) : m Expr :=
  liftMetaM $ mkFreshExprMVarImpl type? kind userName

def mkFreshTypeMVar (kind := MetavarKind.natural) (userName := Name.anonymous) : m Expr := liftMetaM do
  let u ← mkFreshLevelMVar
  mkFreshExprMVar (mkSort u) kind userName

/- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
   the metavar using this method. -/
private def mkFreshExprMVarWithIdCore (mvarId : MVarId) (type : Expr)
    (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0)
    : m Expr := liftMetaM do
  let lctx ← getLCtx
  let localInsts ← getLocalInstances
  mkFreshExprMVarAtCore mvarId lctx localInsts type kind userName numScopeArgs

def mkFreshExprMVarWithIdImpl (mvarId : MVarId) (type? : Option Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr :=
  match type? with
  | some type => mkFreshExprMVarWithIdCore mvarId type kind userName
  | none      => do
    let u ← mkFreshLevelMVar
    let type ← mkFreshExprMVar (mkSort u)
    mkFreshExprMVarWithIdCore mvarId type kind userName

def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName := Name.anonymous) : m Expr :=
  liftMetaM $ mkFreshExprMVarWithIdImpl mvarId type? kind userName

def shouldReduceAll : MetaM Bool := liftMetaM do
  return (← read).config.transparency == TransparencyMode.all

def shouldReduceReducibleOnly : m Bool := liftMetaM do
  return (← read).config.transparency == TransparencyMode.reducible

def getTransparency : m TransparencyMode := liftMetaM do
  return (← read).config.transparency

def getMVarDecl (mvarId : MVarId) : m MetavarDecl := liftMetaM do
  let mctx ← getMCtx
  match mctx.findDecl? mvarId with
  | some d => pure d
  | none   => throwError! "unknown metavariable '{mkMVar mvarId}'"

def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit := liftMetaM do
  modifyMCtx fun mctx => mctx.setMVarKind mvarId kind

/- Update the type of the given metavariable. This function assumes the new type is
   definitionally equal to the current one -/
def setMVarType (mvarId : MVarId) (type : Expr) : m Unit := liftMetaM do
  modifyMCtx fun mctx => mctx.setMVarType mvarId type

def isReadOnlyExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
  let mvarDecl ← getMVarDecl mvarId
  let mctx     ← getMCtx
  pure $ mvarDecl.depth != mctx.depth

def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
  let mvarDecl ← getMVarDecl mvarId
  match mvarDecl.kind with
  | MetavarKind.syntheticOpaque => pure true
  | _ => do
    let mctx ← getMCtx
    pure $ mvarDecl.depth != mctx.depth

def isReadOnlyLevelMVar (mvarId : MVarId) : m Bool := liftMetaM do
  let mctx ← getMCtx
  match mctx.findLevelDepth? mvarId with
  | some depth => pure $ depth != mctx.depth
  | _          => throwError! "unknown universe metavariable '{mkLevelMVar mvarId}'"

def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit := liftMetaM do
  modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName

def isExprMVarAssigned (mvarId : MVarId) : m Bool := liftMetaM do
  let mctx ← getMCtx
  pure $ mctx.isExprAssigned mvarId

def getExprMVarAssignment? (mvarId : MVarId) : m (Option Expr) := liftMetaM do
  let mctx ← getMCtx
  pure (mctx.getExprAssignment? mvarId)

def assignExprMVar (mvarId : MVarId) (val : Expr) : m Unit := liftMetaM do
  modifyMCtx fun mctx => mctx.assignExpr mvarId val

def isDelayedAssigned (mvarId : MVarId) : m Bool := liftMetaM do
  return (← getMCtx).isDelayedAssigned mvarId

def getDelayedAssignment? (mvarId : MVarId) : m (Option DelayedMetavarAssignment) := liftMetaM do
  return (← getMCtx).getDelayedAssignment? mvarId

def hasAssignableMVar (e : Expr) : m Bool := liftMetaM do
  return (← getMCtx).hasAssignableMVar e

def throwUnknownFVar {α} (fvarId : FVarId) : MetaM α :=
  throwError! "unknown free variable '{mkFVar fvarId}'"

def findLocalDecl? (fvarId : FVarId) : m (Option LocalDecl) := liftMetaM do
  return (← getLCtx).find? fvarId

def getLocalDecl (fvarId : FVarId) : m LocalDecl := liftMetaM do
  match (← getLCtx).find? fvarId with
  | some d => pure d
  | none   => throwUnknownFVar fvarId

def getFVarLocalDecl (fvar : Expr) : m LocalDecl := liftMetaM do
  getLocalDecl fvar.fvarId!

def getLocalDeclFromUserName (userName : Name) : m LocalDecl := liftMetaM do
  match (← getLCtx).findFromUserName? userName with
  | some d => pure d
  | none   => throwError! "unknown local declaration '{userName}'"

def instantiateLevelMVarsImp (u : Level) : MetaM Level :=
  MetavarContext.instantiateLevelMVars u

def instantiateLevelMVars (u : Level) : m Level := liftMetaM do
  instantiateLevelMVarsImp u

def instantiateMVarsImp (e : Expr) : MetaM Expr :=
  (MetavarContext.instantiateExprMVars e).run

def instantiateMVars (e : Expr) : m Expr := liftMetaM do
  instantiateMVarsImp e

def instantiateLocalDeclMVars (localDecl : LocalDecl) : m LocalDecl := liftMetaM do
  match localDecl with
  | LocalDecl.cdecl idx id n type bi  =>
    let type ← instantiateMVars type
    pure $ LocalDecl.cdecl idx id n type bi
  | LocalDecl.ldecl idx id n type val nonDep =>
    let type ← instantiateMVars type
    let val ← instantiateMVars val
    pure $ LocalDecl.ldecl idx id n type val nonDep

@[inline] private def liftMkBindingM {α} (x : MetavarContext.MkBindingM α) : MetaM α := do
  match x (← getLCtx) { mctx := (← getMCtx), ngen := (← getNGen) } with
  | EStateM.Result.ok e newS => do
    setNGen newS.ngen;
    setMCtx newS.mctx;
    pure e
  | EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) newS => do
    setMCtx newS.mctx;
    setNGen newS.ngen;
    throwError "failed to create binder due to failure when reverting variable dependencies"

def mkForallFVarsImp (xs : Array Expr) (e : Expr) : MetaM Expr :=
  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkForall xs e

def mkForallFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
  mkForallFVarsImp xs e

def mkLambdaFVarsImp (xs : Array Expr) (e : Expr) : MetaM Expr :=
  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkLambda xs e

def mkLambdaFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
  mkLambdaFVarsImp xs e

def mkLetFVars (xs : Array Expr) (e : Expr) : m Expr :=
  mkLambdaFVars xs e

def mkArrow (d b : Expr) : m Expr := liftMetaM do
  let n ← mkFreshUserName `x
  return Lean.mkForall n BinderInfo.default d b

def mkForallUsedOnlyImp (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) := do
  if xs.isEmpty then pure (e, 0) else liftMkBindingM <| MetavarContext.mkForallUsedOnly xs e

def mkForallUsedOnly (xs : Array Expr) (e : Expr) : m (Expr × Nat) := liftMetaM do
  mkForallUsedOnlyImp xs e

def elimMVarDepsImp (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr :=
  if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.elimMVarDeps xs e preserveOrder

def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : m Expr := liftMetaM do
  elimMVarDepsImp xs e preserveOrder

@[inline] def withConfig {α} (f : Config → Config) : n α → n α :=
  mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })

@[inline] def withTrackingZeta {α} (x : n α) : n α :=
  withConfig (fun cfg => { cfg with trackZeta := true }) x

@[inline] def withTransparency {α} (mode : TransparencyMode) : n α → n α :=
  mapMetaM <| withConfig (fun config => { config with transparency := mode })

@[inline] def withReducible {α} (x : n α) : n α :=
  withTransparency TransparencyMode.reducible x

@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : n α) : n α :=
  withConfig
    (fun config =>
      let oldMode := config.transparency
      let mode    := if oldMode.lt mode then mode else oldMode
      { config with transparency := mode })
    x

def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
  let env ← getEnv
  match env.find? constName with
  | some (info@(ConstantInfo.thmInfo _)) =>
    if (← shouldReduceAll) then
      pure (some info)
    else
      pure none
  | some (info@(ConstantInfo.defnInfo _)) =>
    if (← shouldReduceReducibleOnly) then
      if (← isReducible constName) then
        pure (some info)
      else
        pure none
    else
      pure (some info)
  | some info => pure (some info)
  | none      => throwUnknownConstant constName

def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
  let env ← getEnv
  match env.find? constName with
  | some (info@(ConstantInfo.thmInfo _)) =>
    if (← shouldReduceAll) then
      pure (some info)
    else
      pure none
  | some (info@(ConstantInfo.defnInfo _)) =>
    if (← shouldReduceReducibleOnly) then
      if (← isReducible constName) then
        pure (some info)
      else
        pure none
    else
      pure (some info)
  | some info => pure (some info)
  | none      => pure none

/-- Save cache, execute `x`, restore cache -/
@[inline] private def savingCacheImpl {α} (x : MetaM α) : MetaM α := do
  let s ← get
  let savedCache := s.cache
  try x finally modify fun s => { s with cache := savedCache }

@[inline] def savingCache {α} : n α → n α :=
  mapMetaM savingCacheImpl

private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
  let env ← getEnv
  if isClass env constName then
    pure (LOption.some constName)
  else
    match (← getConst? constName) with
    | some _ => pure LOption.undef
    | none   => pure LOption.none

private partial def isClassQuick? : Expr → MetaM (LOption Name)
  | Expr.bvar ..         => pure LOption.none
  | Expr.lit ..          => pure LOption.none
  | Expr.fvar ..         => pure LOption.none
  | Expr.sort ..         => pure LOption.none
  | Expr.lam ..          => pure LOption.none
  | Expr.letE ..         => pure LOption.undef
  | Expr.proj ..         => pure LOption.undef
  | Expr.forallE _ _ b _ => isClassQuick? b
  | Expr.mdata _ e _     => isClassQuick? e
  | Expr.const n _ _     => isClassQuickConst? n
  | Expr.mvar mvarId _   => do
    match (← getExprMVarAssignment? mvarId) with
    | some val => isClassQuick? val
    | none     => pure LOption.none
  | Expr.app f _ _       =>
    match f.getAppFn with
    | Expr.const n .. => isClassQuickConst? n
    | Expr.lam ..     => pure LOption.undef
    | _              => pure LOption.none

def saveAndResetSynthInstanceCache : MetaM SynthInstanceCache := do
  let s ← get
  let savedSythInstance := s.cache.synthInstance
  modify fun s => { s with cache := { s.cache with synthInstance := {} } }
  pure savedSythInstance

def restoreSynthInstanceCache (cache : SynthInstanceCache) : MetaM Unit :=
  modify fun s => { s with cache := { s.cache with synthInstance := cache } }

@[inline] private def resettingSynthInstanceCacheImpl {α} (x : MetaM α) : MetaM α := do
  let savedSythInstance ← saveAndResetSynthInstanceCache
  try x finally restoreSynthInstanceCache savedSythInstance

/-- Reset `synthInstance` cache, execute `x`, and restore cache -/
@[inline] def resettingSynthInstanceCache {α} : n α → n α :=
  mapMetaM resettingSynthInstanceCacheImpl

@[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : n α) : n α :=
  if b then resettingSynthInstanceCache x else x

private def withNewLocalInstanceImp {α} (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α := do
  let localDecl ← getFVarLocalDecl fvar
  /- Recall that we use `auxDecl` binderInfo when compiling recursive declarations. -/
  match localDecl.binderInfo with
  | BinderInfo.auxDecl => k
  | _ =>
    resettingSynthInstanceCache $
      withReader
        (fun ctx => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
        k

/-- Add entry `{ className := className, fvar := fvar }` to localInstances,
    and then execute continuation `k`.
    It resets the type class cache using `resettingSynthInstanceCache`. -/
def withNewLocalInstance {α} (className : Name) (fvar : Expr) : n α → n α :=
  mapMetaM $ withNewLocalInstanceImp className fvar

private def fvarsSizeLtMaxFVars (fvars : Array Expr) (maxFVars? : Option Nat) : Bool :=
  match maxFVars? with
  | some maxFVars => fvars.size < maxFVars
  | none          => true

mutual
  /--
    `withNewLocalInstances isClassExpensive fvars j k` updates the vector or local instances
    using free variables `fvars[j] ... fvars.back`, and execute `k`.

    - `isClassExpensive` is defined later.
    - The type class chache is reset whenever a new local instance is found.
    - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.
      Thus, each new local instance requires a new `resettingSynthInstanceCache`. -/
  private partial def withNewLocalInstancesImp {α}
      (fvars : Array Expr) (i : Nat) (k : MetaM α) : MetaM α := do
    if h : i < fvars.size then
      let fvar := fvars.get ⟨i, h⟩
      let decl ← getFVarLocalDecl fvar
      match (← isClassQuick? decl.type) with
      | LOption.none   => withNewLocalInstancesImp fvars (i+1) k
      | LOption.undef  =>
        match (← isClassExpensive? decl.type) with
        | none   => withNewLocalInstancesImp fvars (i+1) k
        | some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp fvars (i+1) k
      | LOption.some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp fvars (i+1) k
    else
      k

  /--
    `forallTelescopeAuxAux lctx fvars j type`
    Remarks:
    - `lctx` is the `MetaM` local context extended with declarations for `fvars`.
    - `type` is the type we are computing the telescope for. It contains only
      dangling bound variables in the range `[j, fvars.size)`
    - if `reducing? == true` and `type` is not `forallE`, we use `whnf`.
    - when `type` is not a `forallE` nor it can't be reduced to one, we
      excute the continuation `k`.

    Here is an example that demonstrates the `reducing?`.
    Suppose we have
    ```
    abbrev StateM s a := s -> Prod a s
    ```
    Now, assume we are trying to build the telescope for
    ```
    forall (x : Nat), StateM Int Bool
    ```
    if `reducing == true`, the function executes `k #[(x : Nat) (s : Int)] Bool`.
    if `reducing == false`, the function executes `k #[(x : Nat)] (StateM Int Bool)`

    if `maxFVars?` is `some max`, then we interrupt the telescope construction
    when `fvars.size == max`
  -/
  private partial def forallTelescopeReducingAuxAux {α}
      (reducing          : Bool) (maxFVars? : Option Nat)
      (type              : Expr)
      (k                 : Array Expr → Expr → MetaM α) : MetaM α := do
    let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do
      match type with
      | Expr.forallE n d b c =>
        if fvarsSizeLtMaxFVars fvars maxFVars? then
          let d     := d.instantiateRevRange j fvars.size fvars
          let fvarId ← mkFreshId
          let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo
          let fvar  := mkFVar fvarId
          let fvars := fvars.push fvar
          process lctx fvars j b
        else
          let type := type.instantiateRevRange j fvars.size fvars;
          withReader (fun ctx => { ctx with lctx := lctx }) do
            withNewLocalInstancesImp fvars j do
              k fvars type
      | _ =>
        let type := type.instantiateRevRange j fvars.size fvars;
        withReader (fun ctx => { ctx with lctx := lctx }) do
          withNewLocalInstancesImp fvars j do
            if reducing && fvarsSizeLtMaxFVars fvars maxFVars? then
              let newType ← whnf type
              if newType.isForall then
                process lctx fvars fvars.size newType
              else
                k fvars type
            else
              k fvars type
    process (← getLCtx) #[] 0 type

  private partial def forallTelescopeReducingAux {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α := do
    match maxFVars? with
    | some 0 => k #[] type
    | _ => do
      let newType ← whnf type
      if newType.isForall then
        forallTelescopeReducingAuxAux true maxFVars? newType k
      else
        k #[] type

  private partial def isClassExpensive? : Expr → MetaM (Option Name)
    | type => withReducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
      forallTelescopeReducingAux type none fun xs type => do
        match type.getAppFn with
        | Expr.const c _ _ => do
          let env ← getEnv
          pure $ if isClass env c then some c else none
        | _ => pure none

  private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
    match (← isClassQuick? type) with
    | LOption.none   => pure none
    | LOption.some c => pure (some c)
    | LOption.undef  => isClassExpensive? type

end

private def withNewLocalInstancesImpAux {α} (fvars : Array Expr) (j : Nat) : n α → n α :=
  mapMetaM $ withNewLocalInstancesImp fvars j

partial def withNewLocalInstances {α} (fvars : Array Expr) (j : Nat) : n α → n α :=
  mapMetaM $ withNewLocalInstancesImpAux fvars j

def isClass? (type : Expr) : m (Option Name) :=
  liftMetaM do try isClassImp? type catch _ => pure none

@[inline] private def forallTelescopeImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
  forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := none) type k

/--
  Given `type` of the form `forall xs, A`, execute `k xs A`.
  This combinator will declare local declarations, create free variables for them,
  execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
  map2MetaM (fun k => forallTelescopeImp type k) k

private def forallTelescopeReducingImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
  forallTelescopeReducingAux type (maxFVars? := none) k

/--
  Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
  it reduces `A` and continues bulding the telescope if it is a `forall`. -/
def forallTelescopeReducing {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
  map2MetaM (fun k => forallTelescopeReducingImp type k) k

private def forallBoundedTelescopeImp {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
  forallTelescopeReducingAux type maxFVars? k

/--
  Similar to `forallTelescopeReducing`, stops constructing the telescope when
  it reaches size `maxFVars`. -/
def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
  map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k) k

/-- Similar to `forallTelescopeAuxAux` but for lambda and let expressions. -/
private partial def lambdaTelescopeAux {α}
    (k : Array Expr → Expr → MetaM α)
    : Bool → LocalContext → Array Expr → Nat → Expr → MetaM α
  | consumeLet, lctx, fvars, j, Expr.lam n d b c => do
    let d := d.instantiateRevRange j fvars.size fvars
    let fvarId ← mkFreshId
    let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
    let fvar := mkFVar fvarId
    lambdaTelescopeAux k consumeLet lctx (fvars.push fvar) j b
  | true, lctx, fvars, j, Expr.letE n t v b _ => do
    let t := t.instantiateRevRange j fvars.size fvars
    let v := v.instantiateRevRange j fvars.size fvars
    let fvarId ← mkFreshId
    let lctx := lctx.mkLetDecl fvarId n t v
    let fvar := mkFVar fvarId
    lambdaTelescopeAux k true lctx (fvars.push fvar) j b
  | _, lctx, fvars, j, e =>
    let e := e.instantiateRevRange j fvars.size fvars;
    withReader (fun ctx => { ctx with lctx := lctx }) do
      withNewLocalInstancesImp fvars j do
        k fvars e

private partial def lambdaTelescopeImp {α} (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) : MetaM α := do
  let rec process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
    match consumeLet, e with
    | _, Expr.lam n d b c =>
      let d := d.instantiateRevRange j fvars.size fvars
      let fvarId ← mkFreshId
      let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
      let fvar := mkFVar fvarId
      process consumeLet lctx (fvars.push fvar) j b
    | true, Expr.letE n t v b _ => do
      let t := t.instantiateRevRange j fvars.size fvars
      let v := v.instantiateRevRange j fvars.size fvars
      let fvarId ← mkFreshId
      let lctx := lctx.mkLetDecl fvarId n t v
      let fvar := mkFVar fvarId
      process true lctx (fvars.push fvar) j b
    | _, e =>
      let e := e.instantiateRevRange j fvars.size fvars
      withReader (fun ctx => { ctx with lctx := lctx }) do
        withNewLocalInstancesImp fvars j do
          k fvars e
  process consumeLet (← getLCtx) #[] 0 e

/-- Similar to `forallTelescope` but for lambda and let expressions. -/
def lambdaLetTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
  map2MetaM (fun k => lambdaTelescopeImp type true k) k

/-- Similar to `forallTelescope` but for lambda expressions. -/
def lambdaTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
  map2MetaM (fun k => lambdaTelescopeImp type false k) k

def getParamNamesImp (declName : Name) : MetaM (Array Name) := do
  let cinfo ← getConstInfo declName
  forallTelescopeReducing cinfo.type fun xs _ => do
    xs.mapM fun x => do
      let localDecl ← getLocalDecl x.fvarId!
      pure localDecl.userName

/-- Return the parameter names for the givel global declaration. -/
def getParamNames (declName : Name) : m (Array Name) :=
  liftMetaM $ getParamNamesImp declName

-- `kind` specifies the metavariable kind for metavariables not corresponding to instance implicit `[ ... ]` arguments.
private partial def forallMetaTelescopeReducingAux
    (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) : MetaM (Array Expr × Array BinderInfo × Expr) :=
  let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
    match type with
    | Expr.forallE n d b c =>
      let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
        let d  := d.instantiateRevRange j mvars.size mvars
        let k  := if c.binderInfo.isInstImplicit then  MetavarKind.synthetic else kind
        let mvar ← mkFreshExprMVar d k n
        let mvars := mvars.push mvar
        let bis   := bis.push c.binderInfo
        process mvars bis j b
      match maxMVars? with
      | none          => cont ()
      | some maxMVars =>
        if mvars.size < maxMVars then
          cont ()
        else
          let type := type.instantiateRevRange j mvars.size mvars;
          pure (mvars, bis, type)
    | _ =>
      let type := type.instantiateRevRange j mvars.size mvars;
      if reducing then do
        let newType ← whnf type;
        if newType.isForall then
          process mvars bis mvars.size newType
        else
          pure (mvars, bis, type)
      else
        pure (mvars, bis, type)
  process #[] #[] 0 e

/-- Similar to `forallTelescope`, but creates metavariables instead of free variables. -/
def forallMetaTelescope (e : Expr) (kind := MetavarKind.natural) : m (Array Expr × Array BinderInfo × Expr) :=
  liftMetaM $ forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) kind

/-- Similar to `forallTelescopeReducing`, but creates metavariables instead of free variables. -/
def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind := MetavarKind.natural) : m (Array Expr × Array BinderInfo × Expr) :=
  liftMetaM $ forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind

/-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
private partial def lambdaMetaTelescopeImp (e : Expr) (maxMVars? : Option Nat) : MetaM (Array Expr × Array BinderInfo × Expr) :=
  let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
    let finalize : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
      let type := type.instantiateRevRange j mvars.size mvars
      pure (mvars, bis, type)
    let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
      match type with
      | Expr.lam n d b c =>
        let d     := d.instantiateRevRange j mvars.size mvars
        let mvar ← mkFreshExprMVar d
        let mvars := mvars.push mvar
        let bis   := bis.push c.binderInfo
        process mvars bis j b
      | _ => finalize ()
    match maxMVars? with
    | none          => cont ()
    | some maxMVars =>
      if mvars.size < maxMVars then
        cont ()
      else
        finalize ()
  process #[] #[] 0 e

/-- Similar to `forallMetaTelescope` but for lambda expressions. -/
partial def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : m (Array Expr × Array BinderInfo × Expr) :=
  liftMetaM $ lambdaMetaTelescopeImp e maxMVars?

private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
  match (← isClass? fvarType) with
  | none   => k fvar
  | some c => withNewLocalInstance c fvar $ k fvar

private def withLocalDeclImp {α} (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α := do
  let fvarId ← mkFreshId
  let ctx ← read
  let lctx := ctx.lctx.mkLocalDecl fvarId n type bi
  let fvar := mkFVar fvarId
  withReader (fun ctx => { ctx with lctx := lctx }) do
    withNewFVar fvar type k

def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) : n α :=
  map1MetaM (fun k => withLocalDeclImp name bi type k) k

def withLocalDeclD {α} (name : Name) (type : Expr) (k : Expr → n α) : n α :=
  withLocalDecl name BinderInfo.default type k

private def withLetDeclImp {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α := do
  let fvarId ← mkFreshId
  let ctx ← read
  let lctx := ctx.lctx.mkLetDecl fvarId n type val
  let fvar := mkFVar fvarId
  withReader (fun ctx => { ctx with lctx := lctx }) do
    withNewFVar fvar type k

def withLetDecl {α} (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) : n α :=
  map1MetaM (fun k => withLetDeclImp name type val k) k

private def withExistingLocalDeclsImp {α} (decls : List LocalDecl) (k : MetaM α) : MetaM α := do
  let ctx ← read
  let numLocalInstances := ctx.localInstances.size
  let lctx := decls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) ctx.lctx
  withReader (fun ctx => { ctx with lctx := lctx }) do
    let newLocalInsts ← decls.foldlM
      (fun (newlocalInsts : Array LocalInstance) (decl : LocalDecl) => (do {
        match (← isClass? decl.type) with
        | none   => pure newlocalInsts
        | some c => pure $ newlocalInsts.push { className := c, fvar := decl.toExpr } } : MetaM _))
      ctx.localInstances;
    if newLocalInsts.size == numLocalInstances then
      k
    else
      resettingSynthInstanceCache $ withReader (fun ctx => { ctx with localInstances := newLocalInsts }) k

def withExistingLocalDecls {α} (decls : List LocalDecl) : n α → n α :=
  mapMetaM $ withExistingLocalDeclsImp decls

private def withNewMCtxDepthImp {α} (x : MetaM α) : MetaM α := do
  let s ← get
  let savedMCtx  := s.mctx
  modifyMCtx fun mctx => mctx.incDepth
  try x finally setMCtx savedMCtx

/--
  Save cache and `MetavarContext`, bump the `MetavarContext` depth, execute `x`,
  and restore saved data. -/
def withNewMCtxDepth {α} : n α → n α :=
  mapMetaM withNewMCtxDepthImp

private def withLocalContextImp {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
  let localInstsCurr ← getLocalInstances
  withReader (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) do
    if localInsts == localInstsCurr then
      x
    else
      resettingSynthInstanceCache x

def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α :=
  mapMetaM $ withLocalContextImp lctx localInsts

private def withMVarContextImp {α} (mvarId : MVarId) (x : MetaM α) : MetaM α := do
  let mvarDecl ← getMVarDecl mvarId
  withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x

/--
  Execute `x` using the given metavariable `LocalContext` and `LocalInstances`.
  The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
  different from the current ones. -/
def withMVarContext {α} (mvarId : MVarId) : n α → n α :=
  mapMetaM $ withMVarContextImp mvarId

private def withMCtxImp {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
  let mctx' ← getMCtx
  setMCtx mctx
  try x finally setMCtx mctx'

def withMCtx {α} (mctx : MetavarContext) : n α → n α :=
  mapMetaM $ withMCtxImp mctx

@[inline] private def approxDefEqImp {α} (x : MetaM α) : MetaM α :=
  withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true}) x

/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`.  -/
@[inline] def approxDefEq {α} : n α → n α :=
  mapMetaM approxDefEqImp

@[inline] private def fullApproxDefEqImp {α} (x : MetaM α) : MetaM α :=
  withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true }) x

/--
  Similar to `approxDefEq`, but uses all available approximations.
  We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
  For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[Pure ?m]`.
  Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
  as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
  solve `[Pure (fun _ => IO Bool)]` -/
@[inline] def fullApproxDefEq {α} : n α → n α :=
  mapMetaM fullApproxDefEqImp

def normalizeLevel (u : Level) : m Level :=
  liftMetaM do let u ← instantiateLevelMVars u; pure u.normalize

def assignLevelMVar (mvarId : MVarId) (u : Level) : m Unit := liftMetaM do
  modifyMCtx fun mctx => mctx.assignLevel mvarId u

def whnfD [MonadLiftT MetaM n] (e : Expr) : n Expr :=
  withTransparency TransparencyMode.default $ whnf e

def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): m Unit := liftMetaM do
  let env ← getEnv
  match Compiler.setInlineAttribute env declName kind with
  | Except.ok env    => setEnv env
  | Except.error msg => throwError msg

private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
  if h : i < ps.size then
    let p := ps.get ⟨i, h⟩
    let e ← whnf e
    match e with
    | Expr.forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p)
    | _                    => throwError "invalid instantiateForall, too many parameters"
  else
    pure e

/- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`. -/
def instantiateForall (e : Expr) (ps : Array Expr) : m Expr :=
  liftMetaM $ instantiateForallAux ps 0 e

private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
  if h : i < ps.size then
    let p := ps.get ⟨i, h⟩
    let e ← whnf e
    match e with
    | Expr.lam _ _ b _ => instantiateLambdaAux ps (i+1) (b.instantiate1 p)
    | _                => throwError "invalid instantiateLambda, too many parameters"
  else
    pure e

/- Given `e` of the form `fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `t[p_1, ..., p_n]`.
   It uses `whnf` to reduce `e` if it is not a lambda -/
def instantiateLambda (e : Expr) (ps : Array Expr) : m Expr :=
  liftMetaM $ instantiateLambdaAux ps 0 e

/-- Return true iff `e` depends on the free variable `fvarId` -/
def dependsOn (e : Expr) (fvarId : FVarId) : m Bool := liftMetaM do
  let mctx ← getMCtx
  pure $ mctx.exprDependsOn e fvarId

def ppExprImp (e : Expr) : MetaM Format := do
  let env  ← getEnv
  let mctx ← getMCtx
  let lctx ← getLCtx
  let opts ← getOptions
  let ctxCore  ← readThe Core.Context
  Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := ctxCore.currNamespace, openDecls := ctxCore.openDecls  } e

def ppExpr (e : Expr) : m Format :=
  liftMetaM $ ppExprImp e

@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do
  let env  ← getEnv
  let mctx ← getMCtx
  try x catch _ => setEnv env; setMCtx mctx; y

instance {α} : OrElse (MetaM α) := ⟨Meta.orelse⟩

@[inline] private def orelseMergeErrorsImp {α} (x y : MetaM α)
    (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)
    (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ m₂) : MetaM α := do
  let env  ← getEnv
  let mctx ← getMCtx
  try
    x
  catch ex =>
    setEnv env
    setMCtx mctx
    match ex with
    | Exception.error ref₁ m₁ =>
      try
        y
      catch
        | Exception.error ref₂ m₂ => throw $ Exception.error (mergeRef ref₁ ref₂) (mergeMsg m₁ m₂)
        | ex => throw ex
    | ex => throw ex

/--
  Similar to `orelse`, but merge errors. Note that internal errors are not caught.
  The default `mergeRef` uses the `ref` (position information) for the first message.
  The default `mergeMsg` combines error messages using `Format.line ++ Format.line` as a separator. -/
@[inline] def orelseMergeErrors {α m} [MonadControlT MetaM m] [Monad m] (x y : m α)
    (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)
    (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ Format.line ++ m₂) : m α := do
  controlAt MetaM fun runInBase => orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg

/-- Execute `x`, and apply `f` to the produced error message -/
def mapErrorImp {α} (x : MetaM α) (f : MessageData → MessageData) : MetaM α := do
  try
    x
  catch
    | Exception.error ref msg => throw $ Exception.error ref $ f msg
    | ex => throw ex

@[inline] def mapError {α m} [MonadControlT MetaM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α :=
  controlAt MetaM fun runInBase => mapErrorImp (runInBase x) f

/-- `commitWhenSome? x` executes `x` and keep modifications when it returns `some a`. -/
@[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do
  let env  ← getEnv
  let mctx ← getMCtx
  try
    match (← x?) with
    | some a => pure (some a)
    | none   =>
      setEnv env
      setMCtx mctx
      pure none
  catch ex =>
    setEnv env
    setMCtx mctx
    throw ex

end Methods
end Meta

export Meta (MetaM)

end Lean