/-

  From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ensuring.20naive.20purity

  Will revisit later

-/

-- def natFun : Nat → ByteArray :=
--   IO.getRandomBytes 8 |>.run'

--   -- | k => match (IO.getRandomBytes 8 |>.run' ()) with
--   --   | some bytes => bytes.toUInt64BE!.toNat % 256
--   --   | none => k

-- -- #eval natFun 4

/-

type mismatch
  EStateM.set s
has type
  EStateM ?m.273 (?m.61 → EStateM.Result ?m.60 ?m.61 ?m.61) PUnit : Type
but is expected to have type
  Id Unit : Type

-/
-- def ohNo : Unit := Id.run do
--   let s ← EStateM.get
--   IO.println "Oh no"
--   EStateM.set s

-- #eval ohNo



def anyway : IO Unit := do
  -- v4.32: `IO` is no longer an `EStateM`, so the naive-purity attempt below no longer
  -- typechecks (see the live `ohNo` guard); the remainder of the experiment just draws
  -- random bytes without touching any state.
  let x := ← (·.toUInt64BE!.toNat % 256) <$> IO.getRandomBytes 8
  let y := ← (·.toUInt64BE!.toNat % 256) <$> IO.getRandomBytes 8
  let z := ← (·.toUInt64BE!.toNat % 256) <$> IO.getRandomBytes 8
  IO.println f!"{x} {y} {z}"
-- v4.32: `IO.getRandomBytes` depends on a `sorry`-based core definition, so plain `#eval` aborts;
-- use `#eval!` to force evaluation.
#eval!
73 64 3
 
anyway: IO Unit
anyway

The naive-purity attempt itself now fails to typecheck (previously IO was an EStateM, so EStateM.get/EStateM.set compiled). The guard keeps the failure visible while the file still elaborates.

error: Type mismatch IO.println "Oh no" has type IO Unit but is expected to have type Id Unit

error: Type mismatch EStateM.set s has type EStateM ?m.9 (?m.4 → EStateM.Result ?m.3 ?m.4 ?m.4) PUnit but is expected to have type Id Unit

#guard_msgs
Error: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: Type mismatch
+   IO.println "Oh no"
+ has type
+   IO Unit
+ but is expected to have type
+   Id Unit
+ ---
+ error: Type mismatch
+   EStateM.set s
+ has type
+   EStateM ?m.9 (?m.4 → EStateM.Result ?m.3 ?m.4 ?m.4) PUnit
+ but is expected to have type
+   Id Unit
 in
def 
ohNo: Unit
ohNo : 
Unit: Type
Unit := 
Id.run: {α : Type} → Id α → α
Id.run do
  let 
s: ?m.4 → EStateM.Result ?m.3 ?m.4 ?m.4
s ← 
EStateM.get: {ε σ : Type} → EStateM ε σ σ
EStateM.get
  
IO.println: {α : Type} → [ToString α] → α → IO Unit
IO.println 
"Oh no": String
"Oh no"
Error: Type mismatch
  IO.println "Oh no"
has type
  IO Unit
but is expected to have type
  Id Unit
  
EStateM.set: {ε σ : Type} → σ → EStateM ε σ PUnit
EStateM.set 
s: ?m.4 → EStateM.Result ?m.3 ?m.4 ?m.4
s
Error: Type mismatch
  EStateM.set s
has type
  EStateM ?m.9 (?m.4 → EStateM.Result ?m.3 ?m.4 ?m.4) PUnit
but is expected to have type
  Id Unit


example: 1 + 1 = 2
example : 
1: Nat
1 + 
1: Nat
1 = 
2: Nat
2 := by
Goals accomplished! 🐙
  rfl
Goals accomplished! 🐙
  done
Goals accomplished! 🐙


structure 
Two: Type
Two where
  
x: Two → Nat
x : 
Nat: Type
Nat
  
property: ∀ (self : Two), self.x = 2
property : 
x: Nat
x = 
2: Nat
2 := by decide

def 
a: Two
a : 
Two: Type
Two := {x := 
2: Nat
2}
def 
b: Two
b := 
Two.mk: (x : Nat) → autoParam (x = 2) Two.property._autoParam → Two
Two.mk 
2: Nat
2
def 
c: Two
c : 
Two: Type
Two := ⟨
2: Nat
2, 
rfl: ∀ {α : Type} {a : α}, a = a
rfl⟩ -- hope to omit rfl