fix: uses `PUnit`, `pure ()` forces implicit universe parameter to be `1`

Remark: we should probably elaborate `def`s like we elaborate theorems
when the resulting type is provided.

src/Init/Data/Option/Instances.lean

diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean
index 991aba1..0d1cd9c 100644
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@@ -72,7 +72,7 @@
 
 /-- Map a monadic function which returns `Unit` over an `Option`. -/
 @[inline] protected def forM [Pure m] : Option α → (α → m PUnit) → m PUnit
-  | none  , _ => pure ()
+  | none  , _ => pure ⟨⟩
   | some a, f => f a
 
 instance : ForM m (Option α) α :=