fix: make Std.Do's post macro universe polymorphic (#12159)

This PR makes Std.Do's `post` macro universe polymorphic by expanding to
`PUnit.unit` instead of `()`.

src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean

@@ -209,8 +209,8 @@ def SuccessPoint.clause (p : SuccessPoint) : Expr :=
 
 /-- The last syntactic element of a `FailureCond`. -/
 inductive ExceptCondsDefault where
-  /-- `()`. This means we can suggest `post⟨...⟩`. -/
-  | unit
+  /-- `PUnit.unit`. This means we can suggest `post⟨...⟩`. -/
+  | punit
   /-- `ExceptConds.false`. This means we can suggest `⇓ _ => _`. -/
   | false
   /-- `ExceptConds.true`. This means we can suggest `⇓? _ => _`. -/
@@ -229,7 +229,7 @@ When the default is not defeq to `ExceptConds.false`, we use it as the default.
 -/
 structure FailureCondHints where
   points : Array Expr := #[]
-  default : ExceptCondsDefault := .unit
+  default : ExceptCondsDefault := .punit
 
 /-- Look at how `inv` is used in the `vcs` and collect hints about how `inv` should be instantiated.
 In case it succeeds, there will be
@@ -293,8 +293,8 @@ def collectInvariantHints (vcs : Array MVarId) (inv : MVarId) (xs : Expr) (letMu
         -- Just overwrite the existing entry. Computing a join here is overkill for the few cases
         -- where this is going to be used.
         failureConds := { failureConds with points := points }
-        if conds.isConstOf ``Unit.unit then
-          failureConds := { failureConds with default := .unit }
+        if conds.isConstOf ``PUnit.unit then
+          failureConds := { failureConds with default := .punit }
         else if conds.isAppOfArity ``ExceptConds.false 1 then
           failureConds := { failureConds with default := .false }
         else if conds.isAppOfArity ``ExceptConds.true 1 then
@@ -402,8 +402,8 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
   -- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturn`.
   -- 3. When there are non-`False` failure conditions, we cannot suggest `⇓ ⟨xs, letMuts⟩ => ...`.
   --    We might be able to suggest `⇓? ⟨xs, letMuts⟩ => ...` (`True` failure condition),
-  --    or `post⟨...⟩` (more than 0 failure handlers, but ending in `()`), and fall back to
-  --    `by exact ⟨...⟩` (not ending in `()`).
+  --    or `post⟨...⟩` (more than 0 failure handlers, but ending in `PUnit.unit`), and fall back to
+  --    `by exact ⟨...⟩` (not ending in `PUnit.unit`).
   -- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturn`.
   -- Hence the spaghetti code.
   --
@@ -429,7 +429,7 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
       -- Now the configuration mess.
       if failureConds.points.isEmpty then
         match failureConds.default with
-        | .false | .unit =>
+        | .false | .punit =>
           `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue))
         -- we handle the following two cases here rather than through
         -- `postCondWithMultipleConditions` below because that would insert a superfluous `by exact _`.
@@ -469,7 +469,7 @@ where
   postCondWithMultipleConditions (handlers : Array Term) (default : ExceptCondsDefault) : MetaM Term := do
     let handlers := Syntax.TSepArray.ofElems (sep := ",") handlers
     match default with
-    | .unit => `(post⟨$handlers,*⟩)
+    | .punit => `(post⟨$handlers,*⟩)
     -- See the comment in `post⟨_⟩` syntax for why we emit `by exact` here.
     | .false => `(by exact ⟨$handlers,*, ExceptConds.false⟩)
     | .true => `(by exact ⟨$handlers,*, ExceptConds.true⟩)

src/Std/Do/PostCond.lean

@@ -330,7 +330,7 @@ abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u :=
 
 @[inherit_doc PostCond]
 scoped macro:max "post⟨" handlers:term,+,? "⟩" : term =>
-  `(by exact ⟨$handlers,*, ()⟩)
+  `(by exact ⟨$handlers,*, PUnit.unit⟩)
   -- NB: Postponement through by exact is the entire point of this macro
   -- until https://github.com/leanprover/lean4/pull/8074 lands
 

tests/lean/run/stdDoPostUnit.lean

@@ -0,0 +1,6 @@
+import Std.Do
+open Std.Do
+
+-- This failed cryptically for `α : Type u` because the `post` macro expanded to `()` instead of `PUnit.unit`
+axiom Option.of_wp_eq {α : Type u} {x : Option α} {prog : Option α} (h : prog = x) (P : Option α → Prop) :
+    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x