feat: elaborate do notation even when expected type is not available

see issue #1256

RELEASES.md

@@ -1,6 +1,17 @@
 Unreleased
 ---------
 
+* Try to elaborate `do` notation even if the expected type is not available. We still delay elaboration when the expected type
+  is not available. This change is particularly useful when writing examples such as
+  ```lean
+  #eval do
+    IO.println "hello"
+    IO.println "world"
+  ```
+  That is, we don't have to use the idiom `#eval show IO _ from do ...` anymore.
+  Note that auto monadic lifting is less effective when the expected type is not available.
+  Monadic polymorphic functions (e.g., `ST.Ref.get`) also require the expected type.
+
 * On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable `LEAN_BACKTRACE` to `0`.
   Other platforms are TBD.
 

src/Lean/Elab/Do.lean

@@ -90,36 +90,39 @@ structure ExtractMonadResult where
   α            : Expr
   expectedType : Expr
 
+private def mkUnknownMonadResult : MetaM ExtractMonadResult := do
+  let u ← mkFreshLevelMVar
+  let v ← mkFreshLevelMVar
+  let m ← mkFreshExprMVar (← mkArrow (mkSort (mkLevelSucc u)) (mkSort (mkLevelSucc v)))
+  let α ← mkFreshExprMVar (mkSort (mkLevelSucc u))
+  return { m, α, expectedType := mkApp m α }
+
 private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
-  match expectedType? with
-  | none => throwError "invalid 'do' notation, expected type is not available"
-  | some expectedType =>
-    let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
-      match type with
-      | Expr.app m α _ =>
-        try
-          let bindInstType ← mkAppM ``Bind #[m]
-          let _  ← Meta.synthInstance bindInstType
-          return some { m := m, α := α, expectedType := expectedType }
-        catch _ =>
-          return none
-      | _ =>
-        return none
-    let rec extract? (type : Expr) : MetaM (Option ExtractMonadResult) := do
-      match (← extractStep? type) with
-      | some r => return r
-      | none =>
-        let typeNew ← whnfCore type
-        if typeNew != type then
-          extract? typeNew
-        else
-          if typeNew.getAppFn.isMVar then throwError "invalid 'do' notation, expected type is not available"
-          match (← unfoldDefinition? typeNew) with
+  let some expectedType := expectedType? | mkUnknownMonadResult
+  let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
+    let .app m α _ := type | return none
+    try
+      let bindInstType ← mkAppM ``Bind #[m]
+      discard <| Meta.synthInstance bindInstType
+      return some { m, α, expectedType }
+    catch _ =>
+      return none
+  let rec extract? (type : Expr) : MetaM (Option ExtractMonadResult) := do
+    match (← extractStep? type) with
+    | some r => return r
+    | none =>
+      let typeNew ← whnfCore type
+      if typeNew != type then
+        extract? typeNew
+      else
+        if typeNew.getAppFn.isMVar then
+          mkUnknownMonadResult
+        else match (← unfoldDefinition? typeNew) with
           | some typeNew => extract? typeNew
           | none => return none
-    match (← extract? expectedType) with
-    | some r => return r
-    | none   => throwError "invalid 'do' notation, expected type is not a monad application{indentExpr expectedType}\nYou can use the `do` notation in pure code by writing `Id.run do` instead of `do`, where `Id` is the identity monad."
+  match (← extract? expectedType) with
+  | some r => return r
+  | none   => throwError "invalid 'do' notation, expected type is not a monad application{indentExpr expectedType}\nYou can use the `do` notation in pure code by writing `Id.run do` instead of `do`, where `Id` is the identity monad."
 
 namespace Do
 

tests/lean/474.lean

@@ -1,7 +1,7 @@
 import Lean
 open Lean Meta
 
-#eval show MetaM Unit from do
+#eval do
   let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat)
     assignExprMVar m.mvarId! y
@@ -14,7 +14,7 @@ open Lean Meta
       mkLambda `y BinderInfo.default (mkConst ``Nat) (e.abstract #[y])
   dbg_trace (← ppExpr e)
 
-#eval show MetaM Unit from
+#eval
   withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat)
     assignExprMVar m.mvarId! y
@@ -23,8 +23,8 @@ open Lean Meta
      dbg_trace (← instantiateMVars <| -- doesn't work: contains free variable
       mkLambda `y BinderInfo.default (mkConst ``Nat) (← abstract e #[y]))
 
-#eval show MetaM Unit from do
-  let (e, m) ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
+#eval do
+  let (e, _) ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat) (kind := MetavarKind.syntheticOpaque)
     let e := mkApp2 (mkConst ``Nat.add) m y
     dbg_trace (← ppExpr e)

tests/lean/625.lean

@@ -6,11 +6,11 @@ def px   : PUnit := ()
 
 @[appUnexpander foo] def unexpandFoo : Unexpander := fun _ => `(sorry)
 
-#eval show MetaM Format from do
+#eval do
   let e : Expr := mkApp (mkMData {} $ mkConst `foo [levelOne]) (mkConst `x)
   formatTerm (← delab e)
 
-#eval show MetaM Format from do
+#eval do
   let opts := ({}: Options).setBool `pp.universes true
   -- the MData annotation should make it not a regular application,
   -- so the unexpander should not be called.

tests/lean/doIfLet.lean

@@ -1,10 +1,10 @@
-#eval show Id Nat from do
+#eval Id.run do
   let mut x := 2
   if let n + 1 := x then
     x := n
   return x
 
-#eval show Id Nat from do
+#eval Id.run do
   let mut x := 2
   if let 0 := x then
     x := 0

tests/lean/forallMetaBounded.lean

@@ -5,12 +5,12 @@ def Set (α : Type) : Type :=
   α → Prop
 
 def Set.empty {α : Type} : Set α :=
-  fun a => False
+  fun _ => False
 
 def Set.insert (s : Set α) (a : α) : Set α :=
   fun x => x = a ∨ s a
 
-#eval show MetaM Unit from do
+#eval do
   let insertType ← inferType (mkConst `Set.insert)
-  let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope insertType 3
+  let ⟨_, _, resultType⟩ ← forallMetaBoundedTelescope insertType 3
   println! "{resultType}"

tests/lean/run/evalDo.lean

@@ -0,0 +1,3 @@
+#eval do
+  IO.println "hello"
+  IO.println "world"

tests/lean/sepByIndentQuot.lean

@@ -1,14 +1,14 @@
 import Lean
 open Lean Elab
 
-#eval show TermElabM _ from do
+#eval do
   let x := mkIdent `x
   let xs := #[x,x,x,x]
   let ys := xs
   PrettyPrinter.ppTerm <|<-
     `(frobnicate { $[$xs:ident := $ys:term],* })
 
-#eval show TermElabM _ from do
+#eval do
   let x := mkIdent `x
   let xs := #[x,x,x,x]
   let ys := xs