chore: update stage0

stage0/src/Lean/Elab/App.lean

@@ -925,37 +925,6 @@ private def elabAtom : TermElab := fun stx expectedType? =>
 @[builtinTermElab proj] def elabProj : TermElab := elabAtom
 @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
 
-@[builtinTermElab binrel] def elabBinRel : TermElab :=  fun stx expectedType? => do
-  match (← resolveId? stx[1]) with
-  | some f =>
-    let s ← saveAllState
-    let (lhs, rhs) ← withSynthesize (mayPostpone := true) do
-      let mut lhs ← elabTerm stx[2] none
-      let mut rhs ← elabTerm stx[3] none
-      if lhs.isAppOfArity `OfNat.ofNat 3 then
-        lhs ← ensureHasType (← inferType rhs) lhs
-      else if rhs.isAppOfArity `OfNat.ofNat 3 then
-        rhs ← ensureHasType (← inferType lhs) rhs
-      return (lhs, rhs)
-    let lhsType ← inferType lhs
-    let rhsType ← inferType rhs
-    let (lhs, rhs) ←
-      try
-        pure (lhs, ← withRef stx[3] do ensureHasType lhsType rhs)
-      catch _ =>
-        try
-          pure (← withRef stx[2] do ensureHasType rhsType lhs, rhs)
-        catch _ =>
-          s.restore
-          -- Use default approach
-          let lhs ← elabTerm stx[2] none
-          let rhs ← elabTerm stx[3] none
-          let lhsType ← inferType lhs
-          let rhsType ← inferType rhs
-          pure (lhs, ← withRef stx[3] do ensureHasType lhsType rhs)
-    elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false)
-  | none   => throwUnknownConstant stx[1].getId
-
 builtin_initialize
   registerTraceClass `Elab.app
 

stage0/src/Lean/Elab/Extra.lean

@@ -3,17 +3,84 @@ 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.Elab.Term
+import Lean.Elab.App
 
 /-
 Auxiliary elaboration functions: AKA custom elaborators
 -/
 
 namespace Lean.Elab.Term
+open Meta
+
+@[builtinTermElab binrel] def elabBinRel : TermElab :=  fun stx expectedType? => do
+  match (← resolveId? stx[1]) with
+  | some f =>
+    let s ← saveAllState
+    let (lhs, rhs) ← withSynthesize (mayPostpone := true) do
+      let mut lhs ← elabTerm stx[2] none
+      let mut rhs ← elabTerm stx[3] none
+      if lhs.isAppOfArity `OfNat.ofNat 3 then
+        lhs ← ensureHasType (← inferType rhs) lhs
+      else if rhs.isAppOfArity `OfNat.ofNat 3 then
+        rhs ← ensureHasType (← inferType lhs) rhs
+      return (lhs, rhs)
+    let lhsType ← inferType lhs
+    let rhsType ← inferType rhs
+    let (lhs, rhs) ←
+      try
+        pure (lhs, ← withRef stx[3] do ensureHasType lhsType rhs)
+      catch _ =>
+        try
+          pure (← withRef stx[2] do ensureHasType rhsType lhs, rhs)
+        catch _ =>
+          s.restore
+          -- Use default approach
+          let lhs ← elabTerm stx[2] none
+          let rhs ← elabTerm stx[3] none
+          let lhsType ← inferType lhs
+          let rhsType ← inferType rhs
+          pure (lhs, ← withRef stx[3] do ensureHasType lhsType rhs)
+    elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false)
+  | none   => throwUnknownConstant stx[1].getId
 
 @[builtinTermElab forInMacro] def elabForIn : TermElab :=  fun stx expectedType? => do
   match stx with
-  | `(forIn! $c $e $body) => elabTerm (← `(forIn $c $e $body)) expectedType?
+  | `(forIn! $col $init $body) =>
+      match (← isLocalIdent? col) with
+      | none   => elabTerm (← `(let col := $col; forIn! col $init $body)) expectedType?
+      | some colFVar =>
+        tryPostponeIfNoneOrMVar expectedType?
+        let m ← getMonad expectedType?
+        let colType ← inferType colFVar
+        let elemType ← mkFreshExprMVar (mkSort (mkLevelSucc (← mkFreshLevelMVar)))
+        let forInInstance ←
+          try
+            mkAppM `ForIn #[m, colType, elemType]
+          catch
+            ex => tryPostpone; throwError! "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+        match (← trySynthInstance forInInstance) with
+        | LOption.some val =>
+          let ref ← getRef
+          let forInFn ← mkConst ``forIn
+          let namedArgs : Array NamedArg := #[
+            { ref := ref, name := `m, val := Arg.expr m},
+            { ref := ref, name := `ρ, val := Arg.expr colType},
+            { ref := ref, name := `α, val := Arg.expr elemType},
+            { ref := ref, name := `self, val := Arg.expr forInInstance},
+            { ref := ref, name := `inst, val := Arg.expr val} ]
+          elabAppArgs forInFn #[] #[Arg.stx col, Arg.stx init, Arg.stx body] expectedType? (explicit := false) (ellipsis := false)
+        | LOption.undef    => tryPostpone; throwFailure forInInstance
+        | LOption.none     => throwFailure forInInstance
   | _ => throwUnsupportedSyntax
+where
+  getMonad (expectedType? : Option Expr) : TermElabM Expr := do
+    match expectedType? with
+    | none => throwError "invalid 'forIn!' notation, expected type is not available"
+    | some expectedType =>
+      match (← isTypeApp? expectedType) with
+      | some (m, _) => return m
+      | none => throwError! "invalid 'forIn!' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
+  throwFailure (forInInstance : Expr) : TermElabM Expr :=
+    throwError! "failed to synthesize instance for 'forIn!' notation{indentExpr forInInstance}"
 
 end Lean.Elab.Term

stage0/src/Lean/Elab/Term.lean

@@ -623,7 +623,7 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp
         | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
         | _                     => throwTypeMismatchError errorMsgHeader? expectedType eType e f?
 
-private def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do
+def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do
   let type ← withReducible $ whnf type
   match type with
   | Expr.app m α _ => pure (some ((← instantiateMVars m), (← instantiateMVars α)))

stage0/stdlib/Lean/Elab/Term.c

@@ -558,7 +558,6 @@ uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1(lean_object*);
 lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacro_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -766,7 +765,6 @@ lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_obj
 extern lean_object* l_Lean_Elab_throwAbortTerm___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabEnsureExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam_x27_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabQuotedName_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -958,7 +956,6 @@ extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_Context_declName_x3f___default;
 lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabHole___closed__1;
 lean_object* l_Lean_Elab_Term_SavedState_restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_toArray___rarg(lean_object*);
@@ -979,6 +976,7 @@ lean_object* l_Lean_Name_beq___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabStrLit_match__1(lean_object*);
 lean_object* l_Lean_mkApp5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Name_isAnonymous(lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore_match__1(lean_object*);
 lean_object* l_Lean_Elab_Term_resolveName_x27___closed__2;
@@ -999,6 +997,7 @@ lean_object* l_Lean_Elab_Term_State_syntheticMVars___default;
 lean_object* l_Lean_Elab_logAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instInhabitedSavedState___closed__1;
 lean_object* l_Lean_Elab_Term_registerMVarErrorCustomInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_mapM___at_Lean_Elab_Term_resolveName_x27___spec__6___closed__2;
 lean_object* l_Lean_Elab_Term_observing___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1035,6 +1034,7 @@ extern lean_object* l_Lean_Elab_pp_macroStack;
 lean_object* l_Lean_Elab_Term_resolveName_x27___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabProp___closed__1;
 lean_object* l_Lean_Elab_Term_mkConst___closed__1;
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_compileDecl___at_Lean_Elab_Term_evalExpr___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__1(lean_object*);
 lean_object* l_Lean_Elab_Term_ensureHasType_match__1(lean_object*);
@@ -1308,7 +1308,6 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_mkSimpleThunk(lean_object*);
 lean_object* l_Lean_Elab_Term_registerSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f_match__1(lean_object*);
 extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_ensureHasTypeAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_observing___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1322,6 +1321,7 @@ lean_object* l_Lean_Elab_Term_elabByTactic_match__1(lean_object*);
 lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit(lean_object*);
 lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___closed__1;
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f_match__1(lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam_x27_match__1(lean_object*);
 extern lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors;
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore_match__3___rarg(lean_object*);
@@ -13552,7 +13552,7 @@ lean_dec(x_7);
 return x_13;
 }
 }
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_1) == 5)
@@ -13578,15 +13578,15 @@ return x_9;
 }
 }
 }
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f_match__1(lean_object* x_1) {
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f_match__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f_match__1___rarg), 3, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_isTypeApp_x3f_match__1___rarg), 3, 0);
 return x_2;
 }
 }
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; 
@@ -13992,11 +13992,11 @@ return x_92;
 }
 }
 }
-lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+lean_object* l_Lean_Elab_Term_isTypeApp_x3f___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
 lean_object* x_9; 
-x_9 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+x_9 = l_Lean_Elab_Term_isTypeApp_x3f(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
 lean_dec(x_3);
 lean_dec(x_2);
 return x_9;
@@ -14306,7 +14306,7 @@ lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_9 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+x_9 = l_Lean_Elab_Term_isTypeApp_x3f(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
 if (lean_obj_tag(x_9) == 0)
 {
 lean_object* x_10; 
@@ -15217,7 +15217,7 @@ lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_14);
-x_19 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(x_14, x_6, x_7, x_8, x_9, x_10, x_11, x_18);
+x_19 = l_Lean_Elab_Term_isTypeApp_x3f(x_14, x_6, x_7, x_8, x_9, x_10, x_11, x_18);
 if (lean_obj_tag(x_19) == 0)
 {
 lean_object* x_20; 
@@ -15254,7 +15254,7 @@ lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_17);
-x_28 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_25);
+x_28 = l_Lean_Elab_Term_isTypeApp_x3f(x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_25);
 if (lean_obj_tag(x_28) == 0)
 {
 lean_object* x_29; 
@@ -17215,7 +17215,7 @@ lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_17);
-x_398 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTypeApp_x3f(x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_395);
+x_398 = l_Lean_Elab_Term_isTypeApp_x3f(x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_395);
 if (lean_obj_tag(x_398) == 0)
 {
 lean_object* x_399;