ST.Ref type unsafety

Stream: lean4

[Mario Carneiro]

#eval runST fun σ => do
  let r ← ST.Prim.mkRef 1
  let r' : ST.Ref σ String := ⟨r.1, ⟨""⟩⟩
  r'.get

This doesn't cause any unsoundness that I can tell, but it can be used to cause memory unsafety. This code will just crash the lean server if you run it.

[Sebastian Ullrich]

Looks like another case for https://github.com/leanprover/lean4/issues/418

[Mario Carneiro]

I think that rather than private, this needs unsafe

[Mario Carneiro]

specifically, ST.Ref.mk is unsafe