Disallow impure global let bindings

Effectful expressions are monadic in Lem, causing type errors when binding them
to global immutable variables.

3 files changed, 9 insertions, 3 deletions

diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail
index b56a1a98..15f14a3b 100644
--- a/test/typecheck/pass/pure_record.sail
+++ b/test/typecheck/pass/pure_record.sail
@@ -5,7 +5,9 @@ struct State ('a : Type) = {
   Z : vector(1, dec, bit)
 }
 
-let myStateM : State(bit) = {
+val myStateM : unit -> State(bit) effect {undef}
+
+function myStateM () = {
   r : State(bit) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index 2ca42541..cbdb2c9d 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -5,7 +5,9 @@ struct State ('a : Type) ('n : Int) = {
   Z : vector(1, dec, bit)
 }
 
-let myStateM : State(bit, 1) = {
+val myStateM : unit -> State(bit, 1) effect {undef}
+
+function myStateM () = {
   r : State(bit, 1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index 6db6dc5e..cd3e849a 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -7,7 +7,9 @@ struct State ('a : Type) ('n : Int) = {
 
 register procState : State(bit, 1)
 
-let myStateM : State(bit, 1) = {
+val myStateM : unit -> State(bit, 1) effect {undef}
+
+function myStateM () = {
   r : State(bit, 1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;