infer the generalized monad rather than specifying it

HBind/ElabHdo.lean

@@ -99,7 +99,6 @@ private def mkUnknownMonadResult : MetaM ExtractMonadResult := do
   let returnType ← mkFreshExprMVar (mkSort (mkLevelSucc u))
   return { m, returnType, expectedType := mkApp m returnType }
 
--- TODO: Understand and update extractBind
 private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
   let some expectedType := expectedType? | mkUnknownMonadResult
   let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
@@ -127,6 +126,18 @@ private partial def extractBind (expectedType? : Option Expr) : TermElabM Extrac
   | 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."
 
+-- TODO: Update generalizeBindUniverse to support monads applied to arguments
+private def generalizeBindUniverse (bindInfo: ExtractMonadResult): TermElabM ExtractMonadResult := do
+  match bindInfo.m with
+  | .const name levels => do
+    trace[Elab.do] s!"Found monad constant {name} with levels {levels}"
+    let gm ← mkConstWithLevelParams name
+    trace[Elab.do] s!"Generalizing into {gm}"
+    return { bindInfo with m := gm }
+  | _ =>
+    trace[Elab.do] s!"Failed to generalize levels for monad: {bindInfo.m}"
+    return bindInfo
+
 namespace HDo
 
 abbrev Var := Syntax  -- TODO: should be `Ident`
@@ -1615,7 +1626,6 @@ private def mkMonadAlias (m : Expr) : TermElabM Syntax := do
       safety := DefinitionSafety.safe
   }
   ensureNoUnassignedMVars decl
-  dbg_trace m
   addAndCompile decl
   Term.applyAttributes name #[{ name := `inline }, { name := `reducible }]
   return mkIdent name
@@ -1624,6 +1634,7 @@ private def mkMonadAlias (m : Expr) : TermElabM Syntax := do
 @[termElab «hdo»] def elabHDo : TermElab := fun stx expectedType? => do
   tryPostponeIfNoneOrMVar expectedType?
   let bindInfo ← extractBind expectedType?
+  let bindInfo ← generalizeBindUniverse bindInfo
   let m ← mkMonadAlias bindInfo.m
   let returnType ← Term.exprToSyntax bindInfo.returnType
   let codeBlock ← ToCodeBlock.run stx m returnType
@@ -1637,12 +1648,8 @@ private def mkMonadAlias (m : Expr) : TermElabM Syntax := do
   | `(hdo (monad := $stx_monad:term) $stx_seq) =>
       let stx ← `(hdo $stx_seq)
 
-      -- We get an expression for the universe polymorphic monad as parameter
       let monad ← elabTerm stx_monad none
-      dbg_trace "Monad:"
-      dbg_trace monad
-      dbg_trace "Inferred monad type:"
-      dbg_trace (← inferType monad)
+      trace[Elab.do] s!"Manually-specified monad: {monad}: {← inferType monad}"
 
       tryPostponeIfNoneOrMVar expectedType?
       let bindInfo ← extractBind expectedType?

Main.lean

@@ -50,11 +50,9 @@ example: Id Unit :=
   pure default
 
 -- The `hdo` notation automatically sets `(m := Id)` and `(n := Id)`, where
--- `Id` is an identifier with level parameters.
--- TODO: We should write `(monad := Id)` and then look at level metavars to
--- find params, rather than naming them externally.
-universe u in
-example: Id Unit := hdo (monad := Id.{u})
+-- `Id` is an identifier with level parameters, inferred from the block's
+-- expected type with universes generalized.
+example: Id Unit := hdo
   let _ ← getD0
   let _ ← getD1
   let _ ← getDx.{2}