4 files changed, 19 insertions, 7 deletions
diff --git a/src/type_check.ml b/src/type_check.ml
index ff4240aa..74e7cc80 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3425,13 +3425,19 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
   begin
     match letbind with
     | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) ->
-       let checked_bind = crule check_exp orig_env (strip_exp bind) typ_annot in
+       let checked_bind = propagate_exp_effect (crule check_exp orig_env (strip_exp bind) typ_annot) in
        let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in
-       [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+       if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects)
+       then
+         [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+       else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
     | LB_val (pat, bind) ->
-       let inferred_bind = irule infer_exp orig_env (strip_exp bind) in
+       let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in
        let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in
-       [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
+       if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects)
+       then
+         [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
+       else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind))
   end
 
 let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
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;