From 0036111db9d6ef99842e728ff91b030a9a14fa4e Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Mon, 2 Aug 2021 17:13:16 -0700
Subject: [PATCH] feat: pp.analyze original mvars are not unknown

---
 src/Init/NotationExtra.lean                   | 24 +++---
 .../Delaborator/TopDownAnalyze.lean           | 81 ++++++++++++++++---
 tests/lean/255.lean.expected.out              |  4 +-
 tests/lean/283.lean.expected.out              |  4 +-
 tests/lean/343.lean.expected.out              |  2 +-
 tests/lean/389.lean.expected.out              |  2 +-
 tests/lean/439.lean.expected.out              |  6 +-
 tests/lean/StxQuot.lean.expected.out          |  2 +-
 .../lean/autoBoundErrorMsg.lean.expected.out  |  2 +-
 .../autoBoundImplicits1.lean.expected.out     |  2 +-
 .../autoBoundImplicits2.lean.expected.out     |  2 +-
 tests/lean/autoPPExplicit.lean.expected.out   |  2 +-
 tests/lean/binderCacheIssue.lean.expected.out | 10 +--
 .../lean/binderCacheIssue2.lean.expected.out  |  2 +-
 tests/lean/evalWithMVar.lean.expected.out     |  8 +-
 tests/lean/funExpected.lean.expected.out      |  2 +-
 tests/lean/holes.lean.expected.out            |  6 +-
 tests/lean/macroPrio.lean.expected.out        |  4 +-
 tests/lean/macroResolveName.lean.expected.out |  4 +-
 tests/lean/match1.lean.expected.out           |  7 +-
 .../mulcommErrorMessage.lean.expected.out     |  8 +-
 tests/lean/parserPrio.lean.expected.out       |  4 +-
 tests/lean/precissues.lean.expected.out       |  8 +-
 tests/lean/rewrite.lean.expected.out          |  2 +-
 tests/lean/scopedunifhint.lean.expected.out   | 10 +--
 .../simpArgTypeMismatch.lean.expected.out     |  2 +-
 26 files changed, 131 insertions(+), 79 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 7c15a08b9a..03c160eb1d 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -95,7 +95,7 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi
 
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
-  | _            => throw ()
+  | _       => throw ()
 
 @[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `([])
@@ -104,39 +104,39 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi
 @[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
   | `($(_) $x [])      => `([$x])
   | `($(_) $x [$xs,*]) => `([$x, $xs,*])
-  | _                       => throw ()
+  | _                  => throw ()
 
 @[appUnexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
   | `($(_) [$xs,*]) => `(#[$xs,*])
-  | _                       => throw ()
+  | _               => throw ()
 
 @[appUnexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
   | `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
   | `($(_) $x $y)          => `(($x, $y))
-  | _                         => throw ()
+  | _                      => throw ()
 
 @[appUnexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
   | `($(_) $c $t $e) => `(if $c then $t else $e)
-  | _               => throw ()
+  | _                => throw ()
 
 @[appUnexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) _)    => `(sorry)
-  | `($(_) _ $b) => `(sorry)
-  | _               => throw ()
+  | `($(_) _)   => `(sorry)
+  | `($(_) _ _) => `(sorry)
+  | _           => throw ()
 
 @[appUnexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
-  | _                 => throw ()
+  | _             => throw ()
 
 @[appUnexpander Eq.rec] def unexpandEqRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
-  | _               => throw ()
+  | _             => throw ()
 
 @[appUnexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
   | `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
   | `($(_) fun $x:ident => $b)                     => `(∃ $x:ident, $b)
   | `($(_) fun ($x:ident : $t) => $b)              => `(∃ ($x:ident : $t), $b)
-  | _                                                => throw ()
+  | _                                              => throw ()
 
 @[appUnexpander Sigma] def unexpandSigma : Lean.PrettyPrinter.Unexpander
   | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
@@ -144,7 +144,7 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi
 
 @[appUnexpander PSigma] def unexpandPSigma : Lean.PrettyPrinter.Unexpander
   | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
-  | _                                   => throw ()
+  | _                                 => throw ()
 
 syntax "funext " (colGt term:max)+ : tactic
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 4c6d7e1341..54d0bb94f2 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -155,11 +155,64 @@ def isStructureInstance (e : Expr) : MetaM Bool := do
 
 namespace TopDownAnalyze
 
+partial def hasMVarAtCurrDepth (e : Expr) : MetaM Bool := do
+  let mctx ← getMCtx
+  Option.isSome $ e.findMVar? fun mvarId =>
+    match mctx.findDecl? mvarId with
+    | some mdecl => mdecl.depth == mctx.depth
+    | _ => false
+
+namespace FindLevelMVar
+
+abbrev Visitor := Option MVarId → Option MVarId
+
+mutual
+
+partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
+  if s.isSome || !e.hasLevelMVar then s else main p e s
+
+partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
+  if s.isSome || !l.hasMVar then s else mainLevel p l s
+
+@[specialize]
+partial def mainLevel (p : MVarId → Bool) : Level → Visitor
+  | Level.zero _        => id
+  | Level.succ l _      => visitLevel p l
+  | Level.max l₁ l₂ _   => visitLevel p l₁ ∘ visitLevel p l₂
+  | Level.imax l₁ l₂ _  => visitLevel p l₁ ∘ visitLevel p l₂
+  | Level.param n _     => id
+  | Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
+
+@[specialize]
+partial def main (p : MVarId → Bool) : Expr → Visitor
+  | Expr.proj _ _ e _    => visit p e
+  | Expr.forallE _ d b _ => visit p b ∘ visit p d
+  | Expr.lam _ d b _     => visit p b ∘ visit p d
+  | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
+  | Expr.app f a _       => visit p a ∘ visit p f
+  | Expr.mdata _ b _     => visit p b
+  | Expr.sort l _        => visitLevel p l
+  | Expr.const _ ls ..   => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
+  | Expr.mvar mvarId _   => id
+  | _                    => id
+
+end
+
+end FindLevelMVar
+
+@[inline] def findLevelMVar? (e : Expr) (p : MVarId → Bool) : Option MVarId :=
+  FindLevelMVar.main p e none
+
+partial def hasLevelMVarAtCurrDepth (e : Expr) : MetaM Bool := do
+  let mctx ← getMCtx
+  Option.isSome $ findLevelMVar? e fun mvarId =>
+    mctx.findLevelDepth? mvarId == some mctx.depth
+
 private def valUnknown (e : Expr) : MetaM Bool := do
-  (← instantiateMVars e).hasMVar
+  hasMVarAtCurrDepth (← instantiateMVars e)
 
 private def typeUnknown (e : Expr) : MetaM Bool := do
-  (← instantiateMVars (← inferType e)).hasMVar
+  valUnknown (← inferType e)
 
 def isHBinOp (e : Expr) : Bool := do
   -- TODO: instead of tracking these explicitly,
@@ -285,8 +338,10 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
         if ← canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i]
     if ← (isHBinOp e <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
     if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
-    let resultType ← instantiateMVars resultType
-    return !resultType.hasMVar
+    return !(← valUnknown resultType)
+
+partial def trivialBottomUp (e : Expr) : AnalyzeM Bool := do
+  e.isFVar || e.isMVar || e.isConst
 
 def withKnowing (knowsType knowsLevel : Bool) (x : AnalyzeM α) : AnalyzeM α := do
   withReader (fun ctx => { ctx with knowsType := knowsType, knowsLevel := knowsLevel }) x
@@ -435,6 +490,7 @@ mutual
     checkOutParams
     collectHigherOrders
     hBinOpHeuristic
+    collectTrivialBottomUps
     discard <| processPostponed (mayPostpone := true)
     analyzeFn
     for i in [:(← read).args.size] do analyzeArg i
@@ -473,10 +529,20 @@ mutual
       if ← (isHBinOp (← getExpr) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
         tryUnify mvars[0] mvars[1]
 
+    collectTrivialBottomUps := do
+      -- motivation: prevent levels from printing in
+      -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β
+      let ⟨_, _, args, mvars, bInfos, _⟩ ← read
+      for i in [:args.size] do
+        if bInfos[i] == BinderInfo.default then
+          if ← valUnknown mvars[i] <&&> trivialBottomUp args[i] then
+            tryUnify args[i] mvars[i]
+            modify fun s => { s with bottomUps := s.bottomUps.set! i true }
+
     analyzeFn := do
       -- Now, if this is the first staging, analyze the n-ary function without expected type
       let ⟨f, fType, _, _, _, forceRegularApp⟩ ← read
-      if !f.isApp then withKnowing false (forceRegularApp || !(← instantiateMVars fType).hasLevelMVar) $ withNaryFn (analyze (parentIsApp := true))
+      if !f.isApp then withKnowing false (forceRegularApp || !(← hasLevelMVarAtCurrDepth (← instantiateMVars fType))) $ withNaryFn (analyze (parentIsApp := true))
 
     annotateNamedArg (n : Name) : AnalyzeAppM Unit := do
       annotateBool `pp.analysis.namedArg
@@ -538,12 +604,9 @@ open TopDownAnalyze SubExpr
 
 def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   let s₀ ← get
-  let uResult := (← getMCtx).levelMVarToParam e (alreadyUsedPred := fun _ => false) (paramNamePrefix := `_pp_analyze)
-  setMCtx uResult.mctx
-  let e := uResult.expr
   traceCtx `pp.analyze do
     withReader (fun ctx => { ctx with config := Lean.Elab.Term.setElabConfig ctx.config }) do
-      let ϕ : AnalyzeM OptionsPerPos := do analyze; (← get).annotations
+      let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; (← get).annotations
       try
         let knowsType := getPPAnalyzeKnowsType (← getOptions)
         ϕ { knowsType := knowsType, knowsLevel := knowsType } (mkRoot e) |>.run' {}
diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out
index 1aa9bc4b5f..a854e5268a 100644
--- a/tests/lean/255.lean.expected.out
+++ b/tests/lean/255.lean.expected.out
@@ -1,6 +1,6 @@
 id x : α
 id x✝ : α
 255.lean:16:7-16:8: error: unknown constant 'x✝'
-id (α := ?m) (sorryAx ?m : ?m) : ?m
+id sorry : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (α := ?m) (sorryAx ?m : ?m) : ?m
+id sorry : ?m
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index fb37509315..62e37a2369 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -1,7 +1,7 @@
 283.lean:1:22-1:25: error: application type mismatch
-  f (f (t := ?m) ?m : ?m)
+  f (f ?m)
 argument
-  f (t := ?m) ?m
+  f ?m
 has type
   ?m : Sort ?u
 but is expected to have type
diff --git a/tests/lean/343.lean.expected.out b/tests/lean/343.lean.expected.out
index 8832f741ef..620d3337ad 100644
--- a/tests/lean/343.lean.expected.out
+++ b/tests/lean/343.lean.expected.out
@@ -2,6 +2,6 @@
 343.lean:30:24-30:54: error: stuck at solving universe constraint
   max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
 while trying to unify
-  (Catish.Obj : Type (max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1))) Catish.Obj
+  Catish.Obj Catish.Obj
 with
   CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}
diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out
index 86a6068e7a..ce7f012f50 100644
--- a/tests/lean/389.lean.expected.out
+++ b/tests/lean/389.lean.expected.out
@@ -1,5 +1,5 @@
 389.lean:7:7-7:17: error: application type mismatch
-  getFoo (A := ?m) bar
+  getFoo bar
 argument
   bar
 has type
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
index 06b637ba00..af5f5d52f3 100644
--- a/tests/lean/439.lean.expected.out
+++ b/tests/lean/439.lean.expected.out
@@ -1,16 +1,16 @@
 fn : {p : P} → Bar.fn p
 439.lean:20:7-20:12: error: function expected at
-  Fn.imp.{imax u ?u} fn (p := ?m)
+  Fn.imp.{imax u ?u} fn
 term has type
   Bar.fn ?m
 439.lean:31:7-31:11: error: function expected at
-  Fn.imp.{imax u ?u} fn (p := ?m)
+  Fn.imp.{imax u ?u} fn
 term has type
   Bar.fn ?m
 Fn.imp.{imax u u_1} fn : Bar.fn p
 Fn.imp.{imax u u_1} fn' Bp : Bar.fn p
 439.lean:41:7-41:12: error: application type mismatch
-  Fn.imp.{imax u ?u} fn' (p := ?m) p
+  Fn.imp.{imax u ?u} fn' p
 argument
   p
 has type
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index c85bad5038..1745b0e995 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -44,7 +44,7 @@ StxQuot.lean:18:15: error: expected term
 "#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]"
 "#[(numLit \"2\")]"
 StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice
-fun a => sorryAx (?m a) : (a : ?m) → ?m a
+fun a => sorry : (a : ?m) → ?m a
 "#[(some 1), (some 2)]"
 StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"
diff --git a/tests/lean/autoBoundErrorMsg.lean.expected.out b/tests/lean/autoBoundErrorMsg.lean.expected.out
index e9dd505072..0c1325136b 100644
--- a/tests/lean/autoBoundErrorMsg.lean.expected.out
+++ b/tests/lean/autoBoundErrorMsg.lean.expected.out
@@ -1,5 +1,5 @@
 autoBoundErrorMsg.lean:1:34-1:39: error: don't know how to synthesize implicit argument
-  @Eq.{?u} (?m (α := α) : Sort ?u) a b
+  @Eq (?m (α := α)) a b
 context:
 α : Sort ?u
 a b : ?m (α := α)
diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out
index 2c984af1a6..6892ceb092 100644
--- a/tests/lean/autoBoundImplicits1.lean.expected.out
+++ b/tests/lean/autoBoundImplicits1.lean.expected.out
@@ -11,5 +11,5 @@ autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
 autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry'
 f : {α : Type} → {n : Nat} → Vec α n → Vec α n
-f (α := ?m) (mkVec (α := ?m) : Vec ?m 0) : Vec ?m 0
+f mkVec : Vec ?m 0
 f mkVec : Vec Nat 0
diff --git a/tests/lean/autoBoundImplicits2.lean.expected.out b/tests/lean/autoBoundImplicits2.lean.expected.out
index 0733ef5d71..09869920fa 100644
--- a/tests/lean/autoBoundImplicits2.lean.expected.out
+++ b/tests/lean/autoBoundImplicits2.lean.expected.out
@@ -1,4 +1,4 @@
-g1 (α := ?m) : ?m → ?m
+g1 : ?m → ?m
 autoBoundImplicits2.lean:30:17-30:18: error: unknown universe level 'u'
 autoBoundImplicits2.lean:33:17-33:18: error: unknown universe level 'β'
 def h1.{u} : {m : Type u → Type u} → {α : Type u} → m α → m α :=
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 2cc5bfcdf1..858b52c943 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -1,5 +1,5 @@
 autoPPExplicit.lean:2:2-2:32: error: application type mismatch
-  @Eq.trans.{?u} α a (b = c)
+  @Eq.trans α a (b = c)
 argument
   b = c
 has type
diff --git a/tests/lean/binderCacheIssue.lean.expected.out b/tests/lean/binderCacheIssue.lean.expected.out
index 85cb0cd0ec..e8d0bf3670 100644
--- a/tests/lean/binderCacheIssue.lean.expected.out
+++ b/tests/lean/binderCacheIssue.lean.expected.out
@@ -1,6 +1,4 @@
-LNot.unpackFun (P := ?m) (L := ?m) : LNot (P := ?m) ?m → ∀ (p : ?m), ¬?m p
-Funtype.unpack (N := LNot (P := ?m) ?m) (O := ∀ (p : ?m), ¬?m p) (T :=
-  ∀ {p : ?m}, ¬?m p) : LNot (P := ?m) ?m → ∀ (p : ?m), ¬?m p
-LNot.applyFun (P := ?m) (L := ?m) : LNot (P := ?m) ?m → ∀ {p : ?m}, ¬?m p
-Funtype.apply (N := LNot (P := ?m) ?m) (O := ∀ (p : ?m), ¬?m p) (T :=
-  ∀ {p : ?m}, ¬?m p) : LNot (P := ?m) ?m → ∀ {p : ?m}, ¬?m p
+LNot.unpackFun (L := ?m) : LNot ?m → ∀ (p : ?m), ¬?m p
+Funtype.unpack : LNot ?m → ∀ (p : ?m), ¬?m p
+LNot.applyFun (L := ?m) : LNot ?m → ∀ {p : ?m}, ¬?m p
+Funtype.apply : LNot ?m → ∀ {p : ?m}, ¬?m p
diff --git a/tests/lean/binderCacheIssue2.lean.expected.out b/tests/lean/binderCacheIssue2.lean.expected.out
index 8275227ddc..5ecf6f9822 100644
--- a/tests/lean/binderCacheIssue2.lean.expected.out
+++ b/tests/lean/binderCacheIssue2.lean.expected.out
@@ -1,2 +1,2 @@
 def foo.{u, u_1} : {P : Sort u} → Bar.{u, u_1} P → Type :=
-fun {P} B => Foo.{imax u u_1} ((p : P) → (Bar.fn p : Sort u_1)) ({p : P} → (Bar.fn p : Sort u_1))
+fun {P} B => Foo.{imax u u_1} ((p : P) → Bar.fn p) ({p : P} → Bar.fn p)
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index c998ca227e..3b4b01b31a 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -1,11 +1,11 @@
-Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat
+Sum.someRight.{u_1, 0} (α := ?m) c : Option Nat
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
-  @Sum.someRight.{?u, 0} ?m Nat (c (α := ?m) : Sum ?m Nat)
+  @Sum.someRight ?m Nat c
 context:
 ⊢ Type ?u
 evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
   @c ?m
 context:
 ⊢ Type ?u
-Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat
-Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat
+Sum.someRight.{u_1, 0} (α := ?m) c : Option Nat
+Sum.someRight.{u_1, 0} (α := ?m) c : Option Nat
diff --git a/tests/lean/funExpected.lean.expected.out b/tests/lean/funExpected.lean.expected.out
index dc030ac87d..e2166fb207 100644
--- a/tests/lean/funExpected.lean.expected.out
+++ b/tests/lean/funExpected.lean.expected.out
@@ -1,4 +1,4 @@
 funExpected.lean:4:2-4:29: error: function expected at
-  List.map (β := ?m) (fun (x : Nat) => (HAdd.hAdd (β := ?m x) (γ := ?m) x 1 : ?m)) xs
+  List.map (fun x => x + 1) xs
 term has type
   List ?m
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 520bd3d0e3..136db189e8 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -23,11 +23,7 @@ x : Nat
 holes.lean:13:8-13:11: error: failed to infer binder type
 holes.lean:15:16-15:17: error: failed to infer binder type
 holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
-  @f Nat
-    (?m _ :
-    let f : {α : Sort ?u} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a;
-    ?m a (α := Nat))
-    a
+  @f Nat (?m _) a
 context:
 a : Nat
 f : {α : Type} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a
diff --git a/tests/lean/macroPrio.lean.expected.out b/tests/lean/macroPrio.lean.expected.out
index e040e7cfb9..3df230ae6d 100644
--- a/tests/lean/macroPrio.lean.expected.out
+++ b/tests/lean/macroPrio.lean.expected.out
@@ -1,6 +1,6 @@
 0 + 1 : Nat
 macroPrio.lean:12:7-12:13: error: ambiguous, possible interpretations 
-  HMul.hMul (α := ?m) (β := ?m) (γ := ?m) 1 2
+  1 * 2
   
-  HAdd.hAdd (α := ?m) (β := ?m) (γ := ?m) 1 1
+  1 + 1
 2 - 2 : Nat
diff --git a/tests/lean/macroResolveName.lean.expected.out b/tests/lean/macroResolveName.lean.expected.out
index f403c23623..93ebbc4d12 100644
--- a/tests/lean/macroResolveName.lean.expected.out
+++ b/tests/lean/macroResolveName.lean.expected.out
@@ -1,4 +1,2 @@
 some `Lean.Macro : Option Name
-List.cons (α := Lean.Name × List ?m)
-  (Prod.mk (β := List ?m) `Nat.succ (List.nil (α := ?m) : List ?m) : Lean.Name × List ?m)
-  (List.nil (α := Lean.Name × List ?m) : List (Lean.Name × List ?m)) : List (Lean.Name × List ?m)
+[(`Nat.succ, [])] : List (Lean.Name × List ?m)
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 3fed5c7811..09a5024c17 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -46,9 +46,6 @@ fun x =>
   | #[] => 0
   | #[3, 4, 5] => 3
   | x => 4 : Array Nat → Nat
-g.match_1 (α :=
-  ?m) : (motive : List ?m → Sort u_2) →
-  (x : List ?m) →
-    ((a : ?m) → motive (List.cons (α := ?m) a (List.nil (α := ?m) : List ?m) : List ?m)) →
-      ((x : List ?m) → motive x) → motive x
+g.match_1 : (motive : List ?m → Sort u_2) →
+  (x : List ?m) → ((a : ?m) → motive [a]) → ((x : List ?m) → motive x) → motive x
 fun e => nomatch e : Empty → False
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index 80a8cbc442..7d3be9f5f7 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -1,7 +1,7 @@
 mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
-  fun a b => ?m a b
+  fun a b => ?m _ _
 has type
-  (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
+  (a : ?m) → (b : ?m a) → ?m _ b : Sort (imax ?u ?u ?u)
 but is expected to have type
   a✝ * b✝ = b✝ * a✝ : Prop
 the following variables have been introduced by the implicit lamda feature
@@ -15,7 +15,7 @@ has type
 but is expected to have type
   true = false : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
-  fun a b => Bool.casesOn (motive := ?m a b) _ (?m _ _ : ?m a b false) (?m _ _ : ?m a b true)
+  fun a b => Bool.casesOn (motive := ?m a b) _ (?m _ _) (?m _ _)
 has type
   (a b : Bool) → ?m a b a : Sort (imax 1 1 ?u)
 but is expected to have type
@@ -25,7 +25,7 @@ the following variables have been introduced by the implicit lamda feature
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
 mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch
-  Bool.casesOn (motive := ?m a b) _ ?m (Bool.casesOn (motive := ?m a b) _ ?m ?m : ?m a b b)
+  Bool.casesOn (motive := ?m a b) _ ?m (Bool.casesOn (motive := ?m a b) _ ?m ?m)
 argument
   Bool.casesOn (motive := ?m a b) _ ?m ?m
 has type
diff --git a/tests/lean/parserPrio.lean.expected.out b/tests/lean/parserPrio.lean.expected.out
index e0784fd6b1..1c329a8c68 100644
--- a/tests/lean/parserPrio.lean.expected.out
+++ b/tests/lean/parserPrio.lean.expected.out
@@ -1,7 +1,7 @@
 [1, 2]
 6
 parserPrio.lean:28:7-28:10: error: ambiguous, possible interpretations 
-  HMul.hMul (α := ?m) (β := ?m) (γ := ?m) 2 1
+  2 * 1
   
-  List.cons (α := ?m) 1 (List.nil (α := ?m) : List ?m)
+  [1]
 [1, 2, 3]
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index eaed8e3a7f..4ea6b5e87a 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -1,11 +1,11 @@
-id (α := ?m → ?m) fun (x : ?m) => x : ?m → ?m
+id fun x => x : ?m → ?m
 0 : Nat
 f 1 fun x => x : Nat
 0 : Nat
 f 1 fun x => x : Nat
-id (α := ?m) : ?m → ?m
+id : ?m → ?m
 precissues.lean:15:10: error: expected command
-id (α := ?m) : ?m → ?m
+id : ?m → ?m
 precissues.lean:17:10: error: expected command
 1 : Nat
 id ((fun (this : True) => this) True.intro) : True
@@ -22,5 +22,5 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 id ¬p : Prop
 ∀ (a a : Nat), a = a : Prop
-id (α := ?m) : ?m → ?m
+id : ?m → ?m
 precissues.lean:41:10: error: expected command
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index 47a04c58e0..c619e3c911 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -2,7 +2,7 @@
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
 rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-  List.reverse (α := ?m) (List.reverse (α := ?m) ?as : List ?m)
+  List.reverse (List.reverse ?as)
 α : Type u_1
 as bs : List α
 ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out
index 11c8a9e959..5b73b5eb90 100644
--- a/tests/lean/scopedunifhint.lean.expected.out
+++ b/tests/lean/scopedunifhint.lean.expected.out
@@ -1,5 +1,5 @@
 scopedunifhint.lean:28:7-28:14: error: application type mismatch
-  mul (s := ?m) ?m x
+  mul ?m x
 argument
   x
 has type
@@ -7,7 +7,7 @@ has type
 but is expected to have type
   ?m.α : Type ?u
 scopedunifhint.lean:29:7-29:24: error: application type mismatch
-  mul (s := ?m) ?m (x, x)
+  mul ?m (x, x)
 argument
   (x, x)
 has type
@@ -15,7 +15,7 @@ has type
 but is expected to have type
   ?m.α : Type ?u
 scopedunifhint.lean:33:7-33:10: error: application type mismatch
-  mul (s := ?m) ?m x
+  ?m*x
 argument
   x
 has type
@@ -25,7 +25,7 @@ but is expected to have type
 x*x : Nat.Magma.α
 x*x : Nat.Magma.α
 scopedunifhint.lean:39:7-39:24: error: application type mismatch
-  mul (s := ?m) ?m (x, x)
+  ?m*(x, x)
 argument
   (x, x)
 has type
@@ -34,7 +34,7 @@ but is expected to have type
   ?m.α : Type ?u
 (x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
 scopedunifhint.lean:56:7-56:22: error: application type mismatch
-  mul (s := ?m) ?m (x, x)
+  ?m*(x, x)
 argument
   (x, x)
 has type
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index c60ad25f29..dab7b20ba4 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/tests/lean/simpArgTypeMismatch.lean.expected.out
@@ -1,5 +1,5 @@
 simpArgTypeMismatch.lean:3:13-3:31: error: application type mismatch
-  decideEqFalse (p := ?m) Unit
+  decideEqFalse Unit
 argument
   Unit
 has type