refactor: pattern elaboration

We don't use the following hack anymore: - /- HACK: `fvarId` is not in the scope of `mvarId` - If this generates problems in the future, we should update the metavariable declarations. -/ - assignExprMVar mvarId (mkFVar fvarId) This hack was corrupting the `InfoTree`.
2022-03-09 18:19:14 -08:00 · 2022-03-09 18:19:14 -08:00 · ca253c43e1
commit ca253c43e1
parent b0246172fa
11 changed files with 355 additions and 338 deletions
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 import Lean.Util.CollectFVars
 import Lean.Meta.Match.MatchPatternAttr
 import Lean.Meta.Match.Match
-import Lean.Meta.SortLocalDecls
 import Lean.Meta.GeneralizeVars
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Arg
@ -192,8 +191,8 @@ open Lean.Elab.Term.Quotation in
  | _ => throwUnsupportedSyntax

 /- We convert the collected `PatternVar`s intro `PatternVarDecl` -/
-inductive PatternVarDecl where
-  | localVar     (fvarId : FVarId)
+structure PatternVarDecl where
+  fvarId : FVarId

 private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array PatternVarDecl → TermElabM α) : TermElabM α :=
  let rec loop (i : Nat) (decls : Array PatternVarDecl) (userNames : Array Name) := do
@ -202,7 +201,7 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P
      | PatternVar.localVar userName   =>
        let type ← mkFreshTypeMVar
        withLocalDecl userName BinderInfo.default type fun x =>
-          loop (i+1) (decls.push (PatternVarDecl.localVar x.fvarId!)) (userNames.push Name.anonymous)
+          loop (i+1) (decls.push { fvarId := x.fvarId! }) (userNames.push Name.anonymous)
    else
      k decls
  loop 0 #[] #[]
@ -381,17 +380,6 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
      | _ => throwError "unexpected match type"
    return (patterns, matchType)

-private def patternDeclsToLocalDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (Array LocalDecl) := do
-  let mut decls := #[]
-  for pdecl in patternVarDecls do
-    match pdecl with
-    | PatternVarDecl.localVar fvarId =>
-      let decl ← getLocalDecl fvarId
-      let decl ← instantiateLocalDeclMVars decl
-      decls := decls.push decl
-  /- We perform a topological sort (dependecies) on `decls` because the pattern elaboration process may produce a sequence where a declaration d₁ may occur after d₂ when d₂ depends on d₁. -/
-  sortLocalDecls decls
-
 open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.as Pattern.val Pattern.arrayLit AltLHS MatcherResult)

 private def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
@ -403,55 +391,31 @@ private def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=

 namespace ToDepElimPattern

+private def throwInvalidPattern (e : Expr) : MetaM α :=
+  throwError "invalid pattern {indentExpr e}"
+
 structure State where
-  found      : FVarIdSet := {}
-  localDecls : Array LocalDecl
-  newLocals  : FVarIdSet := {}
+  patternVars : Array Expr := #[]

 structure Context where
  /--
    When visiting an assigned metavariable, if it has an user-name. We save it here.
    We want to preserve these user-names when generating new pattern variables. -/
  userName : Name := Name.anonymous
+  /--
+    Pattern variables that were explicitly provided by the user.
+    Recall that implicit parameters and `_` are elaborated as metavariables, and then converted into pattern variables
+    by the `normalize` procedure.
+  -/
+  explicitPatternVars : Array FVarId := #[]

 abbrev M := ReaderT Context $ StateRefT State TermElabM

-private def alreadyVisited (fvarId : FVarId) : M Bool := do
-  let s ← get
-  return s.found.contains fvarId
-
-private def markAsVisited (fvarId : FVarId) : M Unit :=
-  modify fun s => { s with found := s.found.insert fvarId }
-
-private def throwInvalidPattern {α} (e : Expr) : M α :=
-  throwError "invalid pattern {indentExpr e}"
-
-/- Create a new LocalDecl `x` for the metavariable `mvar`, and return `Pattern.var x` -/
-private partial def mkLocalDeclFor (mvar : Expr) : M Pattern := do
-  let mvarId := mvar.mvarId!
-  assert! !(← isExprMVarAssigned mvarId)
-  let s ← get
-  let fvarId ← mkFreshFVarId
-  let mvarDecl ← getMVarDecl mvarId
-  let type ← eraseInaccessibleAnnotations (← instantiateMVars mvarDecl.type)
-  /- HACK: `fvarId` is not in the scope of `mvarId`
-     If this generates problems in the future, we should update the metavariable declarations. -/
-  assignExprMVar mvarId (mkFVar fvarId)
-  let mut userName := mvarDecl.userName
-  if userName.isAnonymous then
-    userName := (← read).userName
-  if userName.isAnonymous then
-    userName ← mkFreshBinderName
-  let newDecl := LocalDecl.cdecl default fvarId userName type BinderInfo.default
-  modify fun s =>
-    { s with
-      newLocals  := s.newLocals.insert fvarId,
-      localDecls :=
-      match s.localDecls.findIdx? fun decl => mvar.occurs decl.type with
-      | none   => s.localDecls.push newDecl -- None of the existing declarations depend on `mvar`
-      | some i => s.localDecls.insertAt i newDecl }
-  trace[Elab.match] "mkLocalDeclFor {mvar} => {mkFVar fvarId}"
-  return Pattern.var fvarId
+def isExplicitPatternVar (e : Expr) : M Bool := do
+  if e.isFVar then
+    return (← read).explicitPatternVars.any (. == e.fvarId!)
+  else
+    return false

 private def withMVar (mvarId : MVarId) (x : M α) : M α := do
  let localDecl ← getMVarDecl mvarId
@ -460,65 +424,41 @@ private def withMVar (mvarId : MVarId) (x : M α) : M α := do
  else
    x

-private def isMatchValue' (e : Expr) : M Bool := do
-  -- TODO: optimize if it is a bottleneck. Simple trick: check head symbol before invoking `instantiateMVars`
-  return isMatchValue (← instantiateMVars e)
-
-partial def main (e : Expr) : M Pattern := do
-  trace[Elab.match] "ToDepElimPattern.main: {e}"
-  let isLocalDecl (fvarId : FVarId) : M Bool := do
-    return (← get).localDecls.any fun d => d.fvarId == fvarId
-  let mkPatternVar (fvarId : FVarId) (e : Expr) : M Pattern := do
-    if (← alreadyVisited fvarId) then
-      return Pattern.inaccessible e
-    else
-      markAsVisited fvarId
-      return Pattern.var e.fvarId!
-  let rec mkInaccessible (e : Expr) : M Pattern := do
-    match e with
-    | Expr.fvar fvarId _ =>
-      if (← isLocalDecl fvarId) then
-        mkPatternVar fvarId e
-      else
-        return Pattern.inaccessible e
-    | _ =>
-      if e.getAppFn.isMVar then
-        let eNew ← instantiateMVars e
-        if eNew != e then
-          withMVar e.getAppFn.mvarId! <| mkInaccessible eNew
-        else
-          mkLocalDeclFor e.getAppFn
-      else
-        return Pattern.inaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e))
+partial def normalize (e : Expr) : M Expr := do
  match inaccessible? e with
-  | some t => mkInaccessible t
+  | some e => processInaccessible e
  | none =>
    match e.arrayLit? with
-    | some (α, lits) =>
-      return Pattern.arrayLit α (← lits.mapM main)
+    | some (α, lits) => mkArrayLit α (← lits.mapM normalize)
    | none =>
      if e.isAppOfArity ``_root_.namedPattern 4 then
-        let p ← main <| e.getArg! 2
-        match e.getArg! 1, e.getArg! 3 with
-        | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
-        | _,             _             => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue' e) then
-        return Pattern.val (← instantiateMVars e)
+        let x := e.getArg! 1
+        let p := e.getArg! 2
+        let h := e.getArg! 3
+        unless x.isFVar && h.isFVar do
+          throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
+        addVar x
+        let p ← normalize p
+        addVar h
+        return mkApp4 e.getAppFn (e.getArg! 0) x p h
+      else if isMatchValue e then
+        return e
      else if e.isFVar then
-        let fvarId := e.fvarId!
-        unless (← isLocalDecl fvarId) do
+        unless (← isExplicitPatternVar e) do
          throwInvalidPattern e
-        mkPatternVar fvarId e
+        processVar e
      else if e.getAppFn.isMVar then
        let eNew ← instantiateMVars e
        if eNew != e then
-          withMVar e.getAppFn.mvarId! <| main eNew
+          withMVar e.getAppFn.mvarId! <| normalize eNew
+        else if e.isMVar then
+          withMVar e.mvarId! <| processVar e
        else
-          mkLocalDeclFor e.getAppFn
+          throwInvalidPattern e
      else
        let eNew ← whnf e
        if eNew != e then
-          main eNew
+          normalize eNew
        else
          matchConstCtor e.getAppFn
            (fun _ => do
@ -531,7 +471,7 @@ partial def main (e : Expr) : M Pattern := do
                      | 1 => 45
                   ```
                -/
-                return Pattern.inaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e))
+                return mkInaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e))
              else
                throwInvalidPattern e)
            (fun v us => do
@ -541,32 +481,144 @@ partial def main (e : Expr) : M Pattern := do
              let params := args.extract 0 v.numParams
              let params ← params.mapM fun p => instantiateMVars p
              let fields := args.extract v.numParams args.size
-              let fields ← fields.mapM main
-              return Pattern.ctor v.name us params.toList fields.toList)
+              let fields ← fields.mapM normalize
+              return mkAppN e.getAppFn (params ++ fields))
+where
+  addVar (e : Expr) : M Unit := do
+    unless (← get).patternVars.contains e do
+      modify fun s => { s with patternVars := s.patternVars.push e }
+
+  processVar (e : Expr) : M Expr := do
+    if e.isMVar then
+      setMVarTag e.mvarId! (← read).userName
+    if (← get).patternVars.contains e then
+      return mkInaccessible e
+    else
+      modify fun s => { s with patternVars := s.patternVars.push e }
+      return e
+
+  processInaccessible (e : Expr) : M Expr := do
+    match e with
+    | Expr.fvar fvarId _ =>
+      if (← isExplicitPatternVar e) then
+        processVar e
+      else
+        return mkInaccessible e
+    | _ =>
+      if e.getAppFn.isMVar then
+        let eNew ← instantiateMVars e
+        if eNew != e then
+          withMVar e.getAppFn.mvarId! <| processInaccessible eNew
+        else if e.isMVar then
+          withMVar e.mvarId! <| processVar e
+        else
+          throwInvalidPattern e
+      else
+        return mkInaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e))
+
+private partial def packMatchTypePatterns (matchType : Expr) (ps : Array Expr) : MetaM Expr :=
+  ps.foldlM (init := matchType) fun result p => mkAppM ``PProd.mk #[result, p]
+
+private partial def unpackMatchTypePatterns (p : Expr) : Expr × Array Expr :=
+  if p.isAppOf ``PProd.mk then
+    let (matchType, ps) := unpackMatchTypePatterns (p.getArg! 2)
+    (matchType, ps.push (p.getArg! 3))
+  else
+    (p, #[])
+
+private partial def toPattern (e : Expr) : MetaM Pattern := do
+  match inaccessible? e with
+  | some e => return Pattern.inaccessible e
+  | none =>
+    match e.arrayLit? with
+    | some (α, lits) => return Pattern.arrayLit α (← lits.mapM toPattern)
+    | none =>
+      if e.isAppOfArity ``_root_.namedPattern 4 then
+        let p ← toPattern <| e.getArg! 2
+        match e.getArg! 1, e.getArg! 3 with
+        | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
+        | _,             _             => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
+      else if isMatchValue e then
+        return Pattern.val e
+      else if e.isFVar then
+        return Pattern.var e.fvarId!
+      else
+        matchConstCtor e.getAppFn (fun _ => unreachable!) fun v us => do
+          let args := e.getAppArgs
+          let params := args.extract 0 v.numParams
+          let params ← params.mapM fun p => instantiateMVars p
+          let fields := args.extract v.numParams args.size
+          let fields ← fields.mapM toPattern
+          return Pattern.ctor v.name us params.toList fields.toList
+
+structure TopSort.State where
+  visitedFVars : FVarIdSet := {}
+  visitedMVars : MVarIdSet := {}
+  result       : Array Expr := #[]
+
+abbrev TopSortM := StateRefT TopSort.State TermElabM
+
+private partial def topSort (patternVars : Array Expr) : TermElabM (Array Expr) := do
+  let (_, s) ← patternVars.mapM visit |>.run {}
+  return s.result
+where
+  visit (e : Expr) : TopSortM Unit := do
+    match e with
+    | Expr.proj _ _ e _    => visit e
+    | Expr.forallE _ d b _ => visit d; visit b
+    | Expr.lam _ d b _     => visit d; visit b
+    | Expr.letE _ t v b _  => visit t; visit v; visit b
+    | Expr.app f a _       => visit f; visit a
+    | Expr.mdata _ b _     => visit b
+    | Expr.mvar mvarId _   =>
+      let v ← instantiateMVars e
+      if !v.isMVar then
+        visit v
+      else if patternVars.contains e then
+        unless (← get).visitedMVars.contains mvarId do
+          modify fun s => { s with visitedMVars := s.visitedMVars.insert mvarId }
+          let mvarDecl ← getMVarDecl mvarId
+          visit mvarDecl.type
+          modify fun s => { s with result := s.result.push e }
+    | Expr.fvar fvarId _   =>
+      if patternVars.contains e then
+        unless (← get).visitedFVars.contains fvarId do
+          modify fun s => { s with visitedFVars := s.visitedFVars.insert fvarId }
+          let localDecl ← getLocalDecl fvarId
+          visit localDecl.type
+          modify fun s => { s with result := s.result.push e }
+    | _ => return ()
+
+def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
+  trace[Meta.debug] "patternVarDecls: {patternVarDecls.map fun d => mkFVar d.fvarId}"
+  trace[Meta.debug] "ps: {ps}"
+  let explicitPatternVars := patternVarDecls.map fun decl => decl.fvarId
+  let (ps, s) ← ps.mapM normalize |>.run { explicitPatternVars } |>.run {}
+  trace[Meta.debug] "s.patternVars: {s.patternVars}"
+  let patternVars ← topSort s.patternVars
+  let packed ← mkLambdaFVars patternVars (← packMatchTypePatterns matchType ps) (binderInfoForMVars := BinderInfo.default)
+  trace[Meta.debug] "packed: {packed}"
+  let lctx := explicitPatternVars.foldl (init := (← getLCtx)) fun lctx d => lctx.erase d
+  withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
+    trace[Meta.debug] "before check packed"
+    check packed
+    lambdaTelescope packed fun patternVars packed => do
+      let localDecls ← patternVars.mapM fun x => getLocalDecl x.fvarId!
+      let (matchType, patterns) := unpackMatchTypePatterns packed
+      trace[Meta.debug] "patterns: {patterns}"
+      k localDecls (← patterns.mapM fun p => toPattern p) matchType

 end ToDepElimPattern

-def withDepElimPatterns {α} (patternVarDecls : Array PatternVarDecl) (localDecls : Array LocalDecl) (ps : Array Expr) (k : Array LocalDecl → Array Pattern → TermElabM α) : TermElabM α := do
-  let (patterns, s) ← (ps.mapM ToDepElimPattern.main).run {} |>.run { localDecls := localDecls }
-  let localDecls ← s.localDecls.mapM fun d => instantiateLocalDeclMVars d
-  trace[Elab.match] "localDecls: {localDecls.map (·.userName)}"
-  /- toDepElimPatterns may have added new localDecls. Thus, we must update the local context before we execute `k` -/
-  let lctx ← getLCtx
-  let lctx := patternVarDecls.foldl (init := lctx) fun (lctx : LocalContext) d =>
-    match d with
-    | PatternVarDecl.localVar fvarId => lctx.erase fvarId
-  let lctx := localDecls.foldl (fun (lctx : LocalContext) d => lctx.addDecl d) lctx
-  withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
-    k localDecls patterns
+def withDepElimPatterns (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
+  ToDepElimPattern.main patternVarDecls ps matchType k

 private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (matchType : Expr)
    (k : AltLHS → Expr → TermElabM α) : ExceptT PatternElabException TermElabM α := do
  let (patterns, matchType) ← withSynthesize <| elabPatterns patternStxs matchType
  id (α := TermElabM α) do
-    -- let patterns ← patterns.mapM (instantiateMVars ·)
    trace[Elab.match] "patterns: {patterns}"
-    let localDecls ← patternDeclsToLocalDecls patternVarDecls
-    withDepElimPatterns patternVarDecls localDecls patterns fun localDecls patterns => do
+    withDepElimPatterns patternVarDecls patterns matchType fun localDecls patterns matchType => do
      k { ref := ref, fvarDecls := localDecls.toList, patterns := patterns.toList } matchType

 private def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : ExceptT PatternElabException TermElabM (AltLHS × Expr) := withRef alt.ref do
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@ -32,7 +32,6 @@ import Lean.Meta.Inductive
 import Lean.Meta.SizeOf
 import Lean.Meta.IndPredBelow
 import Lean.Meta.Coe
-import Lean.Meta.SortLocalDecls
 import Lean.Meta.CollectFVars
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.Injective
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@ -465,14 +465,14 @@ def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
    return LocalDecl.ldecl idx id n (← instantiateMVars type) (← instantiateMVars val) nonDep

@[inline] 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;
+  match x { lctx := (← getLCtx), mainModule := (← getEnv).mainModule } { mctx := (← getMCtx), ngen := (← getNGen), nextMacroScope := (← getThe Core.State).nextMacroScope } with
+  | EStateM.Result.ok e sNew => do
+    setMCtx sNew.mctx
+    modifyThe Core.State fun s => { s with ngen := sNew.ngen, nextMacroScope := sNew.nextMacroScope }
    pure e
-  | EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) newS => do
-    setMCtx newS.mctx;
-    setNGen newS.ngen;
+  | EStateM.Result.error (MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) sNew => do
+    setMCtx sNew.mctx
+    modifyThe Core.State fun s => { s with ngen := sNew.ngen, nextMacroScope := sNew.nextMacroScope }
    throwError "failed to create binder due to failure when reverting variable dependencies"

 def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
--- a/src/Lean/Meta/SortLocalDecls.lean
+++ b/src/Lean/Meta/SortLocalDecls.lean
@ -1,50 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
-/
-import Lean.Meta.Basic
-
-namespace Lean.Meta
-
-namespace SortLocalDecls
-
-structure Context where
-  localDecls : NameMap LocalDecl := {}
-
-structure State where
-  visited : NameSet := {}
-  result  : Array LocalDecl := #[]
-
-abbrev M := ReaderT Context $ StateRefT State MetaM
-
-mutual
-  partial def visitExpr (e : Expr) : M Unit := do
-    match e with
-    | Expr.proj _ _ e _    => visitExpr e
-    | Expr.forallE _ d b _ => visitExpr d; visitExpr b
-    | Expr.lam _ d b _     => visitExpr d; visitExpr b
-    | Expr.letE _ t v b _  => visitExpr t; visitExpr v; visitExpr b
-    | Expr.app f a _       => visitExpr f; visitExpr a
-    | Expr.mdata _ b _     => visitExpr b
-    | Expr.mvar _ _        => let v ← instantiateMVars e; unless v.isMVar do visitExpr v
-    | Expr.fvar fvarId _   => if let some localDecl := (← read).localDecls.find? fvarId.name then visitLocalDecl localDecl
-    | _                    => return ()
-
-  partial def visitLocalDecl (localDecl : LocalDecl) : M Unit := do
-    unless (← get).visited.contains localDecl.fvarId.name do
-      modify fun s => { s with visited := s.visited.insert localDecl.fvarId.name }
-      visitExpr localDecl.type
-      if let some val := localDecl.value? then
-        visitExpr val
-      modify fun s => { s with result := s.result.push localDecl }
-end
-
-end SortLocalDecls
-
-open SortLocalDecls in
-def sortLocalDecls (localDecls : Array LocalDecl) : MetaM (Array LocalDecl) :=
-  let aux : M (Array LocalDecl) := do localDecls.forM visitLocalDecl; return (← get).result
-  aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId.name d } |>.run' {}
-
-end Lean.Meta
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@ -736,11 +736,13 @@ instance : ToString Exception where

  We have a `NameGenerator` because we need to generate fresh auxiliary metavariables. -/
 structure State where
-  mctx  : MetavarContext
-  ngen  : NameGenerator
-  cache : HashMap ExprStructEq Expr := {}
+  mctx           : MetavarContext
+  nextMacroScope : MacroScope
+  ngen           : NameGenerator
+  cache          : HashMap ExprStructEq Expr := {}

 structure Context where
+  mainModule         : Name
  preserveOrder      : Bool
  /-- When creating binders for abstracted metavariables, we use the following `BinderInfo`. -/
  binderInfoForMVars : BinderInfo := BinderInfo.implicit
@ -750,6 +752,10 @@ structure Context where
 abbrev MCore := EStateM Exception State
 abbrev M     := ReaderT Context MCore

+private def mkFreshBinderName (n : Name := `x) : M Name := do
+  let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
+  return addMacroScope (← read).mainModule n fresh
+
 def preserveOrder : M Bool :=
  return (← read).preserveOrder

@ -907,7 +913,7 @@ mutual
        let mvarDecl := (← get).mctx.getDecl x.mvarId!
        let type := mvarDecl.type.headBeta
        let type ← abstractRangeAux xs i type
-        let id := if mvarDecl.userName.isAnonymous then x.mvarId!.name else mvarDecl.userName
+        let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName
        return Lean.mkForall id (← read).binderInfoForMVars type e
  where
    abstractRangeAux (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do
@ -1048,7 +1054,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
        let mvarDecl := (← get).mctx.getDecl x.mvarId!
        let type := mvarDecl.type.headBeta
        let type ← abstractRange xs i type
-        let id := if mvarDecl.userName.isAnonymous then x.mvarId!.name else mvarDecl.userName
+        let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName
        if isLambda then
          return (Lean.mkLambda id (← read).binderInfoForMVars type e, num + 1)
        else
@ -1056,17 +1062,21 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)

 end MkBinding

-abbrev MkBindingM := ReaderT LocalContext MkBinding.MCore
+structure MkBindingM.Context where
+  mainModule : Name
+  lctx       : LocalContext

-def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBindingM Expr := fun _ =>
-  MkBinding.elimMVarDeps xs e { preserveOrder }
+abbrev MkBindingM := ReaderT MkBindingM.Context MkBinding.MCore

-def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun _ =>
-  MkBinding.revert xs mvarId { preserveOrder }
+def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBindingM Expr := fun ctx =>
+  MkBinding.elimMVarDeps xs e { preserveOrder, mainModule := ctx.mainModule }

-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM (Expr × Nat) := fun lctx =>
+def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun ctx =>
+  MkBinding.revert xs mvarId { preserveOrder, mainModule := ctx.mainModule }
+
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM (Expr × Nat) := fun ctx =>
  let mvarIdsToAbstract := xs.foldl (init := {}) fun s x => if x.isMVar then s.insert x.mvarId! else s
-  MkBinding.mkBinding isLambda lctx xs e usedOnly usedLetOnly { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract }
+  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }

@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
  return (← mkBinding (isLambda := true) xs e usedOnly usedLetOnly binderInfoForMVars).1
@ -1074,8 +1084,8 @@ def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool :=
@[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
  return (← mkBinding (isLambda := false) xs e usedOnly usedLetOnly binderInfoForMVars).1

-@[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun _ =>
-  MkBinding.abstractRange xs n e { preserveOrder := false }
+@[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
+  MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }

 /--
  `isWellFormed mctx lctx e` return true if
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@ -1,11 +1,11 @@
 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
 context:
-α✝ β : Type
-a✝ : α✝
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
+α β✝ : Type
+a✝ : α
+x : Fam2 α β✝
+β : Type
+a : β
+⊢ β
 [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
  α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
    α : Type @ ⟨7, 13⟩-⟨7, 14⟩
@ -25,7 +25,7 @@ a : α
    β : Type @ ⟨7, 33⟩-⟨7, 34⟩
  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
  x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  _example.match_1 (fun α β x a => β) α β x a (fun α_1 a_1 => ?m a x α_1 a_1) fun n a =>
+  _example.match_1 (fun α β x a => β) α β x a (fun β_1 a_1 => ?m a x β_1 a_1) fun n a =>
    n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
    x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
@ -40,23 +40,28 @@ a : α
    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
    @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
    a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    α : Type @ ⟨1, 0⟩†-⟨1, 0⟩† @ Lean.Elab.Term.elabMVarWithIdKind
-    α : Type @ ⟨1, 0⟩†-⟨1, 0⟩† @ Lean.Elab.Term.elabMVarWithIdKind
-    Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩ @ Lean.Elab.Term.elabApp
-      [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.622]) ([mdata _inaccessible:1 ?_uniq.623]) @ ⟨9, 4⟩-⟨9, 12⟩
+    ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
+    ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
+    Fam2.any : Fam2 ?β ?β @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
+      [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.618]) ([mdata _inaccessible:1 ?_uniq.619]) @ ⟨9, 4⟩-⟨9, 12⟩
      @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-      α : Type @ ⟨1, 0⟩†-⟨1, 0⟩† @ Lean.Elab.Term.elabMVarWithIdKind
-    a : α @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
-      a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    ?m a✝ x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+      ?β : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
+        ?β : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
+    a : ?β @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
+      a : ?β @ ⟨8, 2⟩†-⟨10, 19⟩†
+    ?m a✝ x β a : β @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
    [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
    Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
    [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
    a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨1, 0⟩†-⟨1, 0⟩† @ Lean.Elab.Term.elabMVarWithIdKind
-    Nat : Type @ ⟨1, 0⟩†-⟨1, 0⟩† @ Lean.Elab.Term.elabMVarWithIdKind
+    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
+    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
    Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp
-      [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.640]) ([mdata _inaccessible:1 ?_uniq.641]) @ ⟨10, 4⟩-⟨10, 12⟩
+      [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.650]) ([mdata _inaccessible:1 ?_uniq.651]) @ ⟨10, 4⟩-⟨10, 12⟩
      Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
      n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent
        n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@ -1,22 +1,22 @@
 hidingInaccessibleNames.lean:4:15-4:16: error: don't know how to synthesize placeholder
 context:
 ⊢ Nat
-hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
-context:
- : [] ≠ []
-⊢ Nat
 hidingInaccessibleNames.lean:3:19-3:20: error: don't know how to synthesize placeholder
 context:
 a b : Nat
 : [a, b] ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
+context:
+ : [] ≠ []
+⊢ Nat
+hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
 x✝⁴ : List Nat
 x✝³ : Nat
 x✝² : x✝⁴ ≠ []
-a b x✝¹ : Nat
-x✝ : [a, b] ≠ []
+x✝¹ : Nat
+x✝ : [] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder
 context:
@ -27,13 +27,13 @@ x✝² : List Nat
 x✝¹ : Nat
 x✝ : x✝² ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
 context:
 x✝⁴ : List Nat
 x✝³ : Nat
 x✝² : x✝⁴ ≠ []
-x✝¹ : Nat
-x✝ : [] ≠ []
+a b x✝¹ : Nat
+x✝ : [a, b] ≠ []
 ⊢ Nat
 case inl
 p q : Prop
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@ -238,10 +238,10 @@
      Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
        Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
        Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
-          [.] `Nat : some Type.{?_uniq.787} @ ⟨27, 12⟩-⟨27, 15⟩
+          [.] `Nat : some Type.{?_uniq.795} @ ⟨27, 12⟩-⟨27, 15⟩
          Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
        Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
-          [.] `Array : some Type.{?_uniq.786} @ ⟨27, 18⟩-⟨27, 23⟩
+          [.] `Array : some Type.{?_uniq.794} @ ⟨27, 18⟩-⟨27, 23⟩
          Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
          Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
            Macro expansion
@ -249,17 +249,17 @@
            ===>
            Array Nat
              Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
-                [.] `Array : some Type.{?_uniq.788} @ ⟨27, 25⟩-⟨27, 30⟩
+                [.] `Array : some Type.{?_uniq.796} @ ⟨27, 25⟩-⟨27, 30⟩
                Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
                Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
-                  [.] `Nat : some Type.{?_uniq.789} @ ⟨27, 31⟩-⟨27, 34⟩
+                  [.] `Nat : some Type.{?_uniq.797} @ ⟨27, 31⟩-⟨27, 34⟩
                  Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
  s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
  Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
-    [.] `Array : some Sort.{?_uniq.791} @ ⟨27, 39⟩-⟨27, 44⟩
+    [.] `Array : some Sort.{?_uniq.799} @ ⟨27, 39⟩-⟨27, 44⟩
    Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
    Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Type.{?_uniq.792} @ ⟨27, 45⟩-⟨27, 48⟩
+      [.] `Nat : some Type.{?_uniq.800} @ ⟨27, 45⟩-⟨27, 48⟩
      Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
  s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
  Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
@ -275,11 +275,11 @@
  f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
 [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
  B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.834} @ ⟨30, 14⟩-⟨30, 15⟩
+    [.] `B : some Sort.{?_uniq.842} @ ⟨30, 14⟩-⟨30, 15⟩
    B : Type @ ⟨30, 14⟩-⟨30, 15⟩
  arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
  Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.836} @ ⟨30, 19⟩-⟨30, 22⟩
+    [.] `Nat : some Sort.{?_uniq.844} @ ⟨30, 19⟩-⟨30, 22⟩
    Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
  arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
  A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
@ -294,11 +294,11 @@
  f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩
 [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
  Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.857} @ ⟨33, 12⟩-⟨33, 15⟩
+    [.] `Nat : some Sort.{?_uniq.865} @ ⟨33, 12⟩-⟨33, 15⟩
    Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
  x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
  B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.859} @ ⟨33, 19⟩-⟨33, 20⟩
+    [.] `B : some Sort.{?_uniq.867} @ ⟨33, 19⟩-⟨33, 20⟩
    B : Type @ ⟨33, 19⟩-⟨33, 20⟩
  x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
  { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
@ -338,73 +338,73 @@ infoTree.lean:44:0: error: expected stx
  [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
 [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
  Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.881} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.889} @ ⟨45, 14⟩-⟨45, 17⟩
    Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.882 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.890 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
  Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.883} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.891} @ ⟨45, 14⟩-⟨45, 17⟩
    Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.884 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  Eq.{1} Nat _uniq.882 _uniq.882 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+  _uniq.892 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  Eq.{1} Nat _uniq.890 _uniq.890 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
    Macro expansion
    («term_=_» `x "=" `x)
    ===>
    (Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x)
-      Eq.{1} Nat _uniq.882 _uniq.882 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
-        _uniq.882 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
-          _uniq.882 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
-        _uniq.882 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
-          _uniq.882 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
-  _uniq.891 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
-  _uniq.892 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.891 _uniq.892]) f6.f7 : Eq.{1} Nat _uniq.891 _uniq.891 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
+      Eq.{1} Nat _uniq.890 _uniq.890 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
+        _uniq.890 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
+          _uniq.890 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
+        _uniq.890 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
+          _uniq.890 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
+  _uniq.899 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.900 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.899 _uniq.900]) f6.f7 : Eq.{1} Nat _uniq.899 _uniq.899 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
    Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.893} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.901} @ ⟨46, 20⟩-⟨46, 23⟩
      Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.894 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.902 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
    Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.895} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.903} @ ⟨46, 20⟩-⟨46, 23⟩
      Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.896 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.{1} Nat _uniq.894 _uniq.894 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+    _uniq.904 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.{1} Nat _uniq.902 _uniq.902 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
      Macro expansion
      («term_=_» `x "=" `x)
      ===>
      (Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x)
-        Eq.{1} Nat _uniq.894 _uniq.894 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
-          _uniq.894 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
-            _uniq.894 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
-          _uniq.894 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
-            _uniq.894 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
-    _uniq.901 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
-    _uniq.904 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
-    _uniq.905 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.refl.{1} Nat _uniq.904 : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
-      [.] `Eq.refl : some Eq.{?_uniq.898} Nat _uniq.904 _uniq.904 @ ⟨46, 36⟩-⟨46, 43⟩
+        Eq.{1} Nat _uniq.902 _uniq.902 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
+          _uniq.902 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
+            _uniq.902 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
+          _uniq.902 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
+            _uniq.902 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
+    _uniq.909 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
+    _uniq.912 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.913 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.refl.{1} Nat _uniq.912 : Eq.{1} Nat _uniq.912 _uniq.912 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
+      [.] `Eq.refl : some Eq.{?_uniq.906} Nat _uniq.912 _uniq.912 @ ⟨46, 36⟩-⟨46, 43⟩
      Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
-      _uniq.904 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.904 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
-    [mdata _recApp: _uniq.901 _uniq.891 _uniq.892] : Eq.{1} Nat _uniq.891 _uniq.891 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
-      _uniq.901 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
-      _uniq.891 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.891 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
-      _uniq.892 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.892 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
+      _uniq.912 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.912 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
+    [mdata _recApp: _uniq.909 _uniq.899 _uniq.900] : Eq.{1} Nat _uniq.899 _uniq.899 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
+      _uniq.909 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
+      _uniq.899 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.899 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
+      _uniq.900 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.900 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
  f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
  f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
 [Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
  B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.929} @ ⟨50, 12⟩-⟨50, 13⟩
+    [.] `B : some Sort.{?_uniq.937} @ ⟨50, 12⟩-⟨50, 13⟩
    B : Type @ ⟨50, 12⟩-⟨50, 13⟩
-  _uniq.930 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  _uniq.938 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
  B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.931} @ ⟨50, 17⟩-⟨50, 18⟩
+    [.] `B : some Sort.{?_uniq.939} @ ⟨50, 17⟩-⟨50, 18⟩
    B : Type @ ⟨50, 17⟩-⟨50, 18⟩
-  _uniq.934 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
-  B.mk (B.pair _uniq.934) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
-    B.pair _uniq.934 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
-      _uniq.934 : B @ ⟨50, 24⟩-⟨50, 25⟩
-      [.] _uniq.934 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
+  _uniq.942 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  B.mk (B.pair _uniq.942) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
+    B.pair _uniq.942 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
+      _uniq.942 : B @ ⟨50, 24⟩-⟨50, 25⟩
+      [.] _uniq.942 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
      B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
-    pair : Prod.{0 0} A A := B.pair _uniq.934 @ ⟨50, 22⟩†-⟨50, 32⟩
+    pair : Prod.{0 0} A A := B.pair _uniq.942 @ ⟨50, 22⟩†-⟨50, 32⟩
  f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@ -1,3 +1,18 @@
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
 jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
@ -28,6 +43,41 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
+jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.arrow G T EG getCtx
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx
+        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx
+        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
 jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
  @EGrfl
    (getCtx
@ -81,53 +131,3 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.arrow G T EG getCtx
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx
-        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx
-        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@ -4,7 +4,7 @@ open Lean

 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
    : Except MetavarContext.MkBinding.Exception (MetavarContext × NameGenerator × Expr) :=
-match MetavarContext.mkLambda xs e false true BinderInfo.default lctx { mctx := mctx, ngen := ngen } with
+match MetavarContext.mkLambda xs e false true BinderInfo.default { lctx, mainModule := `main } { mctx := mctx, ngen := ngen, nextMacroScope := firstFrontendMacroScope + 1 } with
 | EStateM.Result.ok e s    => Except.ok (s.mctx, s.ngen, e)
 | EStateM.Result.error e s => Except.error e

--- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out
+++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@ -1,26 +1,27 @@
-syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
-context:
-α✝ β : Type
-a✝ : α✝
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
 syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
 context:
 α β : Type
 a✝ : α
 x : Fam2 α β
-n a : Nat
+a : Nat
+n : Nat
 ⊢ Nat
+syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
+context:
+α β✝ : Type
+a✝ : α
+x : Fam2 α β✝
+β : Type
+a : β
+⊢ β
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
-α✝ β : Type
-a✝ : α✝
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
+α β✝ : Type
+a✝ : α
+x : Fam2 α β✝
+β : Type
+a : β
+⊢ β
 syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
 context:
 α β : Type