fix: make IO.RealWorld opaque (#9631)

This PR makes `IO.RealWorld` opaque. It also adds a new compiler -only
`lcRealWorld` constant to represent this type within the compiler. By
default, an opaque type definition is treated like `lcAny`, whereas we
want a more efficient representation. At the moment, this isn't a big
difference, but in the future we would like to completely erase
`IO.RealWorld` at runtime.

src/Init/Prelude.lean

@@ -141,6 +141,9 @@ unsafe axiom lcErased : Type
 /-- Marker for type dependency that has been erased by the code generator. -/
 unsafe axiom lcAny : Type
 
+/-- Internal representation of `IO.RealWorld` in the compiler. -/
+unsafe axiom lcRealWorld : Type
+
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 

src/Init/System/IO.lean

@@ -16,15 +16,16 @@ public section
 
 open System
 
+opaque IO.RealWorld.nonemptyType : NonemptyType.{0}
+
 /--
 A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
 reordered.
 -/
-/- Like <https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld>.
-   Makes sure we never reorder `IO` operations.
+@[expose] def IO.RealWorld : Type := IO.RealWorld.nonemptyType.type
 
-   TODO: mark opaque -/
-@[expose] def IO.RealWorld : Type := Unit
+instance IO.RealWorld.instNonempty : Nonempty IO.RealWorld :=
+  by exact IO.RealWorld.nonemptyType.property
 
 /--
 A monad that can have side effects on the external world or throw exceptions of type `ε`.
@@ -152,7 +153,7 @@ duplicate, or delete calls to this function. The side effect may even be hoisted
 causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
 @[noinline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
-  match fn.run () with
+  match fn.run (unsafeCast Unit.unit) with
   | EStateM.Result.ok a _ => a
 
 /--

src/Lean/Compiler/IR/ToIRType.lean

@@ -54,6 +54,7 @@ where fillCache : CoreM IRType := do
     -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
     -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
     | ``Int => return .tobject
+    | ``lcRealWorld => return .tagged
     | _ =>
       let env ← Lean.getEnv
       let some (.inductInfo inductiveVal) := env.find? name | return .tobject

src/Lean/Compiler/LCNF/Types.lean

@@ -140,6 +140,8 @@ partial def toLCNFType (type : Expr) : MetaM Expr := do
   | .forallE .. => visitForall type #[]
   | .app ..  => type.withApp visitApp
   | .fvar .. => visitApp type #[]
+  | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
+    return mkConst ``lcRealWorld
   | _        => return mkConst ``lcAny
 where
   whnfEta (type : Expr) : MetaM Expr := do

src/Std/Do/WP/IO.lean

@@ -28,16 +28,16 @@ open Std.Do
 This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`.
 However, `IO.RealWorld` is omitted in the `PredShape`.
 -/
-scoped instance instWP : WP (EIO ε) (.except ε .pure) where
+noncomputable scoped instance instWP : WP (EIO ε) (.except ε .pure) where
   wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
-    { apply := fun Q => match x () with
+    { apply := fun Q => match x Classical.ofNonempty with
         | .ok a _rw => Q.1 a
         | .error e _rw => Q.2.1 e
       conjunctive := by
         intro _ _
         apply SPred.bientails.of_eq
         dsimp
-        cases (x ()) <;> rfl
+        cases (x Classical.ofNonempty) <;> rfl
     }
 
 instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))

src/stdlib_flags.h

@@ -1,5 +1,5 @@
 #include "util/options.h"
-
+// Please update stage0
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/baseIO.lean.expected.out

@@ -1,12 +1,12 @@
 [Compiler.saveBase] size: 11
-    def test a.1 : EStateM.Result Empty PUnit UInt32 :=
+    def test a.1 : EStateM.Result Empty lcRealWorld UInt32 :=
       let _x.2 := 42;
       let _x.3 := @ST.Prim.mkRef _ _ _x.2 a.1;
-      cases _x.3 : EStateM.Result Empty PUnit UInt32
+      cases _x.3 : EStateM.Result Empty lcRealWorld UInt32
       | EStateM.Result.ok a.4 a.5 =>
         let _x.6 := 10;
         let _x.7 := @ST.Prim.Ref.set _ _ a.4 _x.6 a.5;
-        cases _x.7 : EStateM.Result Empty PUnit UInt32
+        cases _x.7 : EStateM.Result Empty lcRealWorld UInt32
         | EStateM.Result.ok a.8 a.9 =>
           let _x.10 := @ST.Prim.Ref.get _ _ a.4 a.9;
           return _x.10

tests/lean/jpClosureIssue.lean.expected.out

@@ -1,6 +1,6 @@
 [Compiler.saveMono] size: 7
-    def foo b a.1 : EStateM.Result IO.Error PUnit PUnit :=
-      cases b : EStateM.Result IO.Error PUnit PUnit
+    def foo b a.1 : EStateM.Result IO.Error lcRealWorld PUnit :=
+      cases b : EStateM.Result IO.Error lcRealWorld PUnit
       | Bool.false =>
         let _x.2 := 1;
         let _x.3 := print _x.2 a.1;

tests/lean/lcnfTypes.lean.expected.out

@@ -17,17 +17,22 @@ MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} →
 Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive lcAny) → (◾ → motive lcAny) → motive lcAny
 Lean.getConstInfo : {m : Type → Type} → [Monad m] → [MonadEnv m] → [MonadError m] → Name → m ConstantInfo
 Lean.Meta.instMonadMetaM : Monad fun α =>
-  Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit α
+  Context →
+    ST.Ref lcRealWorld State →
+      Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld α
 Lean.Meta.inferType : Expr →
-  Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr
+  Context →
+    ST.Ref lcRealWorld State →
+      Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
 Lean.Elab.Term.elabTerm : Syntax →
   Option Expr →
     Bool →
       Bool →
         Elab.Term.Context →
-          ST.Ref PUnit Elab.Term.State →
+          ST.Ref lcRealWorld Elab.Term.State →
             Context →
-              ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr
+              ST.Ref lcRealWorld State →
+                Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
 Nat.add : Nat → Nat → Nat
 Magma.mul : Magma → lcAny → lcAny → lcAny
 weird1 : Bool → lcAny
@@ -44,11 +49,12 @@ MonadControl.restoreM : {m n : lcErased} → [self : MonadControl lcAny lcAny]
 Decidable.casesOn : {p motive : lcErased} → Bool → (lcErased → lcAny) → (lcErased → lcAny) → lcAny
 Lean.getConstInfo : {m : lcErased} → [Monad lcAny] → [MonadEnv lcAny] → [MonadError lcAny] → Name → lcAny
 Lean.Meta.instMonadMetaM : Monad lcAny
-Lean.Meta.inferType : Expr → Context → lcAny → Core.Context → lcAny → PUnit → EStateM.Result Exception PUnit Expr
+Lean.Meta.inferType : Expr → Context → lcAny → Core.Context → lcAny → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
 Lean.Elab.Term.elabTerm : Syntax →
   Option Expr →
     Bool →
       Bool →
-        Elab.Term.Context → lcAny → Context → lcAny → Core.Context → lcAny → PUnit → EStateM.Result Exception PUnit Expr
+        Elab.Term.Context →
+          lcAny → Context → lcAny → Core.Context → lcAny → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
 Nat.add : Nat → Nat → Nat
 Fin.add : {n : Nat} → Nat → Nat → Nat

tests/lean/run/emptyLcnf.lean

@@ -12,9 +12,9 @@ trace: [Compiler.result] size: 0
       ⊥
 ---
 trace: [Compiler.result] size: 5
-    def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception PUnit PUnit :=
+    def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
       let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
-      cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
+      cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
       | EStateM.Result.ok a.11 a.12 =>
         let _x.13 := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
         return _x.13
@@ -41,7 +41,7 @@ trace: [Compiler.result] size: 5
       let _x.3 := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 8
-    def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception PUnit PUnit :=
+    def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
       let _x.4 := _eval._closed_0;
       let _x.5 := _eval._closed_1;
       let _x.6 := 1;

tests/lean/run/erased.lean

@@ -27,14 +27,14 @@ trace: [Compiler.result] size: 1
 ---
 trace: [Compiler.result] size: 5
     def _eval._lam_0 (_x.1 : Array
-       Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : PUnit) : EStateM.Result
-      Lean.Exception PUnit PUnit :=
-      let _x.10 : EStateM.Result Lean.Exception PUnit PUnit := compile _x.1 _y.7 _y.8 _y.9;
-      cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
-      | EStateM.Result.ok (a.11 : PUnit) (a.12 : PUnit) =>
-        let _x.13 : EStateM.Result Lean.Exception PUnit PUnit := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
+       Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcRealWorld) : EStateM.Result
+      Lean.Exception lcRealWorld PUnit :=
+      let _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit := compile _x.1 _y.7 _y.8 _y.9;
+      cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
+      | EStateM.Result.ok (a.11 : PUnit) (a.12 : lcRealWorld) =>
+        let _x.13 : EStateM.Result Lean.Exception lcRealWorld PUnit := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
         return _x.13
-      | EStateM.Result.error (a.14 : Lean.Exception) (a.15 : PUnit) =>
+      | EStateM.Result.error (a.14 : Lean.Exception) (a.15 : lcRealWorld) =>
         return _x.10
 [Compiler.result] size: 1
     def _eval._closed_0 : String :=
@@ -62,8 +62,8 @@ trace: [Compiler.result] size: 5
       let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 9
-    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : PUnit) : EStateM.Result Lean.Exception PUnit
-      PUnit :=
+    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result Lean.Exception
+      lcRealWorld PUnit :=
       let _x.4 : String := _eval._closed_0;
       let _x.5 : String := _eval._closed_1;
       let _x.6 : Lean.Name := _eval._closed_2;
@@ -75,8 +75,9 @@ trace: [Compiler.result] size: 5
         lcAny →
           Lean.Meta.Context →
             lcAny →
-              Lean.Core.Context → lcAny → PUnit → EStateM.Result Lean.Exception PUnit PUnit := _eval._lam_0 _x.9 _x.10;
-      let _x.12 : EStateM.Result Lean.Exception PUnit
+              Lean.Core.Context →
+                lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0 _x.9 _x.10;
+      let _x.12 : EStateM.Result Lean.Exception lcRealWorld
         PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12
 -/

tests/lean/seqToCodeIssue.lean.expected.out

@@ -1,14 +1,14 @@
 [Compiler.saveMono] size: 12
-    def f b a.1 : EStateM.Result IO.Error PUnit PUnit :=
-      jp _jp.2 a _y.3 : EStateM.Result IO.Error PUnit PUnit :=
+    def f b a.1 : EStateM.Result IO.Error lcRealWorld PUnit :=
+      jp _jp.2 a _y.3 : EStateM.Result IO.Error lcRealWorld PUnit :=
         let _x.4 := print a _y.3;
-        cases _x.4 : EStateM.Result IO.Error PUnit PUnit
+        cases _x.4 : EStateM.Result IO.Error lcRealWorld PUnit
         | EStateM.Result.ok a.5 a.6 =>
           let _x.7 := print a a.6;
           return _x.7
         | EStateM.Result.error a.8 a.9 =>
           return _x.4;
-      cases b : EStateM.Result IO.Error PUnit PUnit
+      cases b : EStateM.Result IO.Error lcRealWorld PUnit
       | Bool.false =>
         let _x.10 := 1;
         goto _jp.2 _x.10 a.1