From 3e052aa29f38316648b05757f95ed67ed49c8806 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Fri, 14 Sep 2018 15:05:27 +0100
Subject: Type_check: allow mappings to contain escape effects

---
 src/type_check.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 071b4160..6dd96e79 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4341,10 +4341,10 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
   let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in
   let eff = List.fold_left union_effects no_effect (List.map mapcl_effect mapcls) in
   let env = Env.define_val_spec id env in
-  if equal_effects eff no_effect then
+  if equal_effects eff no_effect || equal_effects eff (mk_effect [BE_escape]) || !opt_no_effects then
     vs_def @ [DEF_mapdef (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, None)))], env
   else
-    typ_error l ("Mapping not pure: " ^ string_of_effect eff ^ " found")
+    typ_error l ("Mapping not pure (or escape only): " ^ string_of_effect eff ^ " found")
 
 
 (* Checking a val spec simply adds the type as a binding in the
-- 
cgit v1.2.3