refactor: move isOutParam to Expr.lean, rename consumeAutoOptParam => consumeTypeAnnotations

src/Lean/Class.lean

@@ -50,10 +50,6 @@ def hasOutParams (env : Environment) (n : Name) : Bool :=
   | some b => b
   | none   => false
 
-@[export lean_is_out_param]
-def isOutParam (e : Expr) : Bool :=
-  e.isAppOfArity `outParam 1
-
 /--
   Auxiliary function for checking whether a class has `outParam`, and
   whether they are being correctly used.
@@ -68,7 +64,7 @@ def isOutParam (e : Expr) : Bool :=
 -/
 private partial def checkOutParam : Nat → Array FVarId → Expr → Except String Bool
   | i, outParams, Expr.forallE _ d b _ =>
-    if isOutParam d then
+    if d.isOutParam then
       let fvarId    := { name := Name.mkNum `_fvar outParams.size }
       let outParams := outParams.push fvarId
       let fvar      := mkFVar fvarId

src/Lean/Elab/App.lean

@@ -163,7 +163,7 @@ private def addNewArg (argName : Name) (arg : Expr) : M Unit := do
   Recall that, `Arg` may be wrapping an already elaborated `Expr`. -/
 private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do
   let s ← get
-  let expectedType := (← getArgExpectedType).consumeAutoOptParam
+  let expectedType := (← getArgExpectedType).consumeTypeAnnotations
   match arg with
   | Arg.expr val =>
     let arg ← ensureArgType s.f val expectedType

src/Lean/Elab/MutualDef.lean

@@ -675,7 +675,7 @@ private partial def mkInst? (className : Name) (type : Expr) : MetaM (Option MkI
     unless instTypeType.isForall do
       return none
     let d := instTypeType.bindingDomain!
-    if isOutParam d then
+    if d.isOutParam then
       let mvar ← mkFreshExprMVar d
       go? (mkApp instType mvar) (instTypeType.bindingBody!.instantiate1 mvar) (outParams.push mvar)
     else

src/Lean/Expr.lean

@@ -931,15 +931,21 @@ def getAutoParamTactic? (e : Expr) : Option Expr :=
   else
     none
 
+@[export lean_is_out_param]
+def isOutParam (e : Expr) : Bool :=
+  e.isAppOfArity `outParam 1
+
 def isOptParam (e : Expr) : Bool :=
   e.isAppOfArity `optParam 2
 
 def isAutoParam (e : Expr) : Bool :=
   e.isAppOfArity `autoParam 2
 
-partial def consumeAutoOptParam (e : Expr) : Expr :=
+partial def consumeTypeAnnotations (e : Expr) : Expr :=
   if e.isOptParam || e.isAutoParam then
-    consumeAutoOptParam e.appFn!.appArg!
+    consumeTypeAnnotations e.appFn!.appArg!
+  else if e.isOutParam then
+    consumeTypeAnnotations e.appArg!
   else
     e
 

src/Lean/Meta/CongrTheorems.lean

@@ -64,8 +64,8 @@ partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem :=
         let mut hs := #[]
         for x in xs, y in ys, eq in eqs do
           hs := hs.push x |>.push y |>.push eq
-        let xType := xType.consumeAutoOptParam
-        let yType := yType.consumeAutoOptParam
+        let xType := xType.consumeTypeAnnotations
+        let yType := yType.consumeTypeAnnotations
         let resultType ← if xType == yType then mkEq xType yType else mkHEq xType yType
         let congrType ← mkForallFVars hs resultType
         return {
@@ -79,8 +79,8 @@ where
       if  i < xs.size then
         let x := xs[i]
         let y := ys[i]
-        let xType := (← inferType x).consumeAutoOptParam
-        let yType := (← inferType y).consumeAutoOptParam
+        let xType := (← inferType x).consumeTypeAnnotations
+        let yType := (← inferType y).consumeTypeAnnotations
         if xType == yType then
           withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h =>
             loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq)

src/Lean/Meta/SynthInstance.lean

@@ -633,7 +633,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) :
     match type with
     | Expr.forallE _ d b _ => do
       let arg := args.get ⟨i, h⟩
-      let arg ← if isOutParam d then mkFreshExprMVar d else pure arg
+      let arg ← if d.isOutParam then mkFreshExprMVar d else pure arg
       let args := args.set ⟨i, h⟩ arg
       preprocessArgs (b.instantiate1 arg) (i+1) args
     | _ =>

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -295,7 +295,7 @@ where
     | Expr.forallE _ fd fb _, Expr.forallE _ md mb _ => do
       -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here?
       -- if so, I'll need to take a callback
-      if isOutParam fd then
+      if fd.isOutParam then
         tryUnify (args[i]) (mvars[i])
       inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars
     | _, _ => return ()