Allow effects on mappings

13 files changed, 74 insertions, 63 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index d00120de..8d06b23e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -847,7 +847,7 @@ and string_of_typ_aux = function
   | Typ_fn (typ_args, typ_ret, eff) ->
      "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> "
      ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
-  | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2
+  | Typ_bidir (typ1, typ2, eff) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 ^ " effect " ^ string_of_effect eff
   | Typ_exist (kids, nc, typ) ->
      "{" ^ string_of_list " " string_of_kinded_id kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"
 and string_of_typ_arg = function
@@ -1170,10 +1170,12 @@ and typ_compare (Typ_aux (t1,_)) (Typ_aux (t2,_)) =
        | 0 -> effect_compare e1 e2
        | n -> n)
      | n -> n)
-  | Typ_bidir (t1,t2), Typ_bidir (t3,t4) ->
+  | Typ_bidir (t1,t2,e1), Typ_bidir (t3,t4,e2) ->
      (match typ_compare t1 t3 with
-     | 0 -> typ_compare t2 t3
-     | n -> n)
+      | 0 -> (match typ_compare t2 t4 with
+              | 0 -> effect_compare e1 e2
+              | n -> n)
+      | n -> n)
   | Typ_tup ts1, Typ_tup ts2 -> Util.compare_list typ_compare ts1 ts2
   | Typ_exist (ks1,nc1,t1), Typ_exist (ks2,nc2,t2) ->
      (match Util.compare_list KOpt.compare ks1 ks2 with
@@ -1378,7 +1380,7 @@ and kopts_of_typ (Typ_aux (t,_)) =
   | Typ_id _ -> KOptSet.empty
   | Typ_var kid -> KOptSet.singleton (mk_kopt K_type kid)
   | Typ_fn (ts, t, _) -> List.fold_left KOptSet.union (kopts_of_typ t) (List.map kopts_of_typ ts)
-  | Typ_bidir (t1, t2) -> KOptSet.union (kopts_of_typ t1) (kopts_of_typ t2)
+  | Typ_bidir (t1, t2, _) -> KOptSet.union (kopts_of_typ t1) (kopts_of_typ t2)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KOptSet.union s (kopts_of_typ t))
        KOptSet.empty ts
@@ -1438,11 +1440,11 @@ and tyvars_of_typ (Typ_aux (t,_)) =
   | Typ_id _ -> KidSet.empty
   | Typ_var kid -> KidSet.singleton kid
   | Typ_fn (ts, t, _) -> List.fold_left KidSet.union (tyvars_of_typ t) (List.map tyvars_of_typ ts)
-  | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
+  | Typ_bidir (t1, t2, _) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t))
        KidSet.empty ts
-  | Typ_app (_,tas) -> 
+  | Typ_app (_,tas) ->
      List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta))
        KidSet.empty tas
   | Typ_exist (kids, nc, t) ->
@@ -1761,7 +1763,7 @@ and locate_typ f (Typ_aux (typ_aux, l)) =
     | Typ_var kid -> Typ_var (locate_kid f kid)
     | Typ_fn (arg_typs, ret_typ, effect) ->
        Typ_fn (List.map (locate_typ f) arg_typs, locate_typ f ret_typ, locate_effect f effect)
-    | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2)
+    | Typ_bidir (typ1, typ2, effect) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2, locate_effect f effect)
     | Typ_tup typs -> Typ_tup (List.map (locate_typ f) typs)
     | Typ_exist (kopts, constr, typ) -> Typ_exist (List.map (locate_kinded_id f) kopts, locate_nc f constr, locate_typ f typ)
     | Typ_app (id, typ_args) -> Typ_app (locate_id f id, List.map (locate_typ_arg f) typ_args)
@@ -1980,7 +1982,7 @@ and typ_subst_aux sv subst = function
      | _ -> Typ_var kid
      end
   | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst sv subst) arg_typs, typ_subst sv subst ret_typ, effs)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2)
+  | Typ_bidir (typ1, typ2, effs) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2, effs)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_arg_subst sv subst) args)
   | Typ_exist (kopts, nc, typ) when KidSet.mem sv (KidSet.of_list (List.map kopt_kid kopts)) ->
@@ -2078,7 +2080,7 @@ let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg =
     | Typ_var _
       -> ty
     | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e))
-    | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
+    | Typ_bidir (t1,t2,e) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2,e))
     | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
     | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
     | Typ_exist (kopts,nc,t) ->
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 7012e915..f808af49 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -153,7 +153,7 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
          | _ -> [to_ast_typ ctx from_typ]
        in
        Typ_fn (from_typs, to_ast_typ ctx to_typ, to_ast_effects effects)
-    | P.ATyp_bidir (typ1, typ2) -> Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2)
+    | P.ATyp_bidir (typ1, typ2, effects) -> Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2, to_ast_effects effects)
     | P.ATyp_tup typs -> Typ_tup (List.map (to_ast_typ ctx) typs)
     | P.ATyp_app (P.Id_aux (P.Id "int", il), [n]) ->
        Typ_app (Id_aux (Id "atom", il), [to_ast_typ_arg ctx n K_int])
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 75ef8a19..874835b1 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -247,6 +247,7 @@ let ssa_name i = function
   | Name (id, _) -> Name (id, i)
   | Have_exception _ -> Have_exception i
   | Current_exception _ -> Current_exception i
+  | Throw_location _ -> Throw_location i
   | Return _ -> Return i
 
 let inline cdefs should_inline instrs =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 645f6f72..e328cce1 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -219,7 +219,7 @@ let rec contains_exist (Typ_aux (ty,l)) =
   | Typ_var _
     -> false
   | Typ_fn (t1,t2,_) -> List.exists contains_exist t1 || contains_exist t2
-  | Typ_bidir (t1, t2) -> contains_exist t1 || contains_exist t2
+  | Typ_bidir (t1, t2, _) -> contains_exist t1 || contains_exist t2
   | Typ_tup ts -> List.exists contains_exist ts
   | Typ_app (_,args) -> List.exists contains_exist_arg args
   | Typ_exist _ -> true
@@ -3530,10 +3530,10 @@ let replace_nexp_in_typ env typ orig new_nexp =
        let f1 = List.exists fst arg' in
        let f2, res = aux res in
        f1 || f2, Typ_aux (Typ_fn (List.map snd arg', res, eff),l)
-    | Typ_bidir (t1, t2) ->
+    | Typ_bidir (t1, t2, eff) ->
        let f1, t1 = aux t1 in
        let f2, t2 = aux t2 in
-       f1 || f2, Typ_aux (Typ_bidir (t1, t2), l)
+       f1 || f2, Typ_aux (Typ_bidir (t1, t2, eff), l)
     | Typ_tup typs ->
        let fs, typs = List.split (List.map aux typs) in
        List.exists (fun x -> x) fs, Typ_aux (Typ_tup typs,l)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 8899695f..98a43ebc 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -118,7 +118,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg =
      parens (separate space [string "fun"; parens (separate (comma ^^ space) args); string "->"; body])
      ^^ space ^^ arg
   | Typ_fn (typ1, typ2, _) -> string "\"FN\""
-  | Typ_bidir (t1, t2) -> string "\"BIDIR\""
+  | Typ_bidir (t1, t2, _) -> string "\"BIDIR\""
   | Typ_var kid -> string "\"VAR\""
   | Typ_exist _ -> assert false
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
@@ -144,7 +144,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
   | Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
   | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
   | Typ_fn (typs, typ, _) -> separate space [ocaml_typ ctx (Typ_aux (Typ_tup typs, l)); string "->"; ocaml_typ ctx typ]
-  | Typ_bidir (t1, t2) -> raise (Reporting.err_general l "Ocaml doesn't support bidir types")
+  | Typ_bidir _ -> raise (Reporting.err_general l "Ocaml doesn't support bidir types")
   | Typ_var kid -> zencode_kid kid
   | Typ_exist _ -> assert false
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 3147b7f4..6cb3f84d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -154,12 +154,12 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_minus of atyp * atyp (* subtraction *)
  | ATyp_exp of atyp (* exponential *)
  | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *)
- | ATyp_inc (* increasing (little-endian) *)
- | ATyp_dec (* decreasing (big-endian) *)
+ | ATyp_inc (* increasing *)
+ | ATyp_dec (* decreasing *)
  | ATyp_default_ord (* default order for increasing or decreasing signficant bits *)
  | ATyp_set of (base_effect) list (* effect set *)
- | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
- | ATyp_bidir of atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
+ | ATyp_fn of atyp * atyp * atyp (* Function type, last atyp is an effect *)
+ | ATyp_bidir of atyp * atyp * atyp (* Mapping type, last atyp is an effect *)
  | ATyp_wild
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
diff --git a/src/parser.mly b/src/parser.mly
index 0b09468c..6a579b7a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -657,9 +657,13 @@ typschm:
   | Forall typquant Dot typ MinusGt typ Effect effect_set
     { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
   | typ Bidir typ
-    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3)) s e) s e) $startpos $endpos }
+    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
   | Forall typquant Dot typ Bidir typ
-    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6)) s e) s e) $startpos $endpos }
+    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
+  | typ Bidir typ Effect effect_set
+    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, $5)) s e) s e) $startpos $endpos }
+  | Forall typquant Dot typ Bidir typ Effect effect_set
+    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, $8)) s e) s e) $startpos $endpos }
 
 typschm_eof:
   | typschm Eof
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 322c60b7..7e98f4e3 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -170,6 +170,8 @@ let rec doc_nc nc =
   in
   atomic_nc (constraint_simp nc)
 
+and doc_effects effs = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs))
+
 and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -194,13 +196,14 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   | Typ_fn (typs, typ, Effect_aux (Effect_set [], _)) ->
      separate space [doc_arg_typs typs; string "->"; doc_typ typ]
   | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
-     let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in
      if simple then
        separate space [doc_arg_typs typs; string "->"; doc_typ ~simple:simple typ]
      else
-       separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
-  | Typ_bidir (typ1, typ2) ->
+       separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; doc_effects effs]
+  | Typ_bidir (typ1, typ2, Effect_aux (Effect_set [], _)) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
+  | Typ_bidir (typ1, typ2, Effect_aux (Effect_set effs, _)) ->
+     separate space [doc_typ typ1; string "<->"; doc_typ typ2; string "effect"; doc_effects effs]
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and doc_typ_arg (A_aux (ta_aux, _)) =
   match ta_aux with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 20a1b336..35811b26 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3133,7 +3133,7 @@ let rewrite_defs_mapping_patterns env =
        let x = Env.get_val_spec mapping_id env in
 
        let typ1, typ2 = match x with
-         | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2
+         | (_, Typ_aux(Typ_bidir(typ1, typ2, _), _)) -> typ1, typ2
          | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ))
        in
 
@@ -3951,7 +3951,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     in
     let (typq, bidir_typ) = Env.get_val_spec id env in
     let (typ1, typ2, l) = match bidir_typ with
-      | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l
+      | Typ_aux (Typ_bidir (typ1, typ2, _), l) -> typ1, typ2, l
       | _ -> raise (Reporting.err_unreachable l __POS__ "non-bidir type of mapping?")
     in
     let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), l) in
diff --git a/src/slice.ml b/src/slice.ml
index a38a207c..c249fb5a 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -130,7 +130,7 @@ and typ_ids' (Typ_aux (aux, _)) =
      IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids' args))
   | Typ_fn (typs, typ, _) ->
      IdSet.union (typ_ids' typ) (List.fold_left IdSet.union IdSet.empty (List.map typ_ids' typs))
-  | Typ_bidir (typ1, typ2) ->
+  | Typ_bidir (typ1, typ2, _) ->
      IdSet.union (typ_ids' typ1) (typ_ids' typ2)
   | Typ_tup typs ->
      List.fold_left IdSet.union IdSet.empty (List.map typ_ids' typs)
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 40855eec..75f2ff6e 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -89,8 +89,8 @@ let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with
   | Typ_id name -> Nameset.add (string_of_id name) mt
   | Typ_fn (arg_typs,ret_typ,_) ->
      List.fold_left Nameset.union (free_type_names_t consider_var ret_typ) (List.map (free_type_names_t consider_var) arg_typs)
-  | Typ_bidir (t1, t2) -> Nameset.union (free_type_names_t consider_var t1)
-                                        (free_type_names_t consider_var t2)
+  | Typ_bidir (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1)
+                                         (free_type_names_t consider_var t2)
   | Typ_tup ts -> free_type_names_ts consider_var ts
   | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs)
   | Typ_exist (kopts,_,t') -> List.fold_left (fun s kopt -> Nameset.remove (string_of_kid (kopt_kid kopt)) s) (free_type_names_t consider_var t') kopts
@@ -121,7 +121,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
   | Typ_id id -> conditional_add_typ bound used id
   | Typ_fn(arg,ret,_) ->
      fv_of_typ consider_var bound (List.fold_left Nameset.union Nameset.empty (List.map (fv_of_typ consider_var bound used) arg)) ret
-  | Typ_bidir(t1, t2) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *)
+  | Typ_bidir(t1,t2,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *)
   | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used
   | Typ_app(id,targs) ->
      List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id)
diff --git a/src/specialize.ml b/src/specialize.ml
index e2b0075d..d705b83a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -92,7 +92,7 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
     | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ)
     | Typ_fn (arg_typs, ret_typ, effect) ->
        Typ_fn (List.map nexp_simp_typ arg_typs, nexp_simp_typ ret_typ, effect)
-    | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2)
+    | Typ_bidir (t1, t2, effect) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2, effect)
     | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
   in
   Typ_aux (typ_aux, l)
@@ -170,8 +170,8 @@ let string_of_instantiation instantiation =
     | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")"
     | Typ_fn (arg_typs, ret_typ, eff) ->
        "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff
-    | Typ_bidir (t1, t2) ->
-       string_of_typ t1 ^ " <-> " ^ string_of_typ t2
+    | Typ_bidir (t1, t2, eff) ->
+       string_of_typ t1 ^ " <-> " ^ string_of_typ t2 ^ " effect " ^ string_of_effect eff
     | Typ_exist (kids, nc, typ) ->
        "exist " ^ Util.string_of_list " " kid_name kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ
     | Typ_internal_unknown -> "UNKNOWN"
@@ -290,7 +290,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_exist (kopts, nc, typ) -> typ_frees ~exs:(KidSet.of_list (List.map kopt_kid kopts)) typ
   | Typ_fn (arg_typs, ret_typ, _) ->
      List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
-  | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
+  | Typ_bidir (t1, t2, _) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
   | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -308,7 +308,7 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_exist (kopts, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list (List.map kopt_kid kopts)) typ
   | Typ_fn (arg_typs, ret_typ, _) ->
      List.fold_left KidSet.union (typ_int_frees ~exs:exs ret_typ) (List.map (typ_int_frees ~exs:exs) arg_typs)
-  | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
+  | Typ_bidir (t1, t2, _) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
   | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -325,7 +325,7 @@ let rec remove_implicit (Typ_aux (aux, l) as t) =
   | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
   | Typ_tup typs -> Typ_aux (Typ_tup (List.map remove_implicit typs), l)
   | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map remove_implicit arg_typs, remove_implicit ret_typ, effs), l)
-  | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2), l)
+  | Typ_bidir (typ1, typ2, effs) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2, effs), l)
   | Typ_app (Id_aux (Id "implicit", _), args) -> Typ_aux (Typ_app (mk_id "atom", List.map remove_implicit_arg args), l)
   | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map remove_implicit_arg args), l)
   | Typ_id id -> Typ_aux (Typ_id id, l)
diff --git a/src/type_check.ml b/src/type_check.ml
index 2ba2166c..0871272b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -238,7 +238,7 @@ and strip_typ_aux : typ_aux -> typ_aux = function
   | Typ_id id -> Typ_id (strip_id id)
   | Typ_var kid -> Typ_var (strip_kid kid)
   | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map strip_typ arg_typs, strip_typ ret_typ, strip_effect effect)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (strip_typ typ1, strip_typ typ2)
+  | Typ_bidir (typ1, typ2, effect) -> Typ_bidir (strip_typ typ1, strip_typ typ2, strip_effect effect)
   | Typ_tup typs -> Typ_tup (List.map strip_typ typs)
   | Typ_exist (kopts, constr, typ) ->
      Typ_exist ((List.map strip_kinded_id kopts), strip_n_constraint constr, strip_typ typ)
@@ -272,7 +272,7 @@ let rec typ_constraints (Typ_aux (typ_aux, l)) =
   | Typ_exist (kids, nc, typ) -> typ_constraints typ
   | Typ_fn (arg_typs, ret_typ, _) ->
      List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ
-  | Typ_bidir (typ1, typ2) ->
+  | Typ_bidir (typ1, typ2, _) ->
      typ_constraints typ1 @ typ_constraints typ2
 and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -291,7 +291,7 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) =
   | Typ_exist (kids, nc, typ) -> typ_nexps typ
   | Typ_fn (arg_typs, ret_typ, _) ->
      List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
-  | Typ_bidir (typ1, typ2) ->
+  | Typ_bidir (typ1, typ2, _) ->
      typ_nexps typ1 @ typ_nexps typ2
 and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -427,7 +427,7 @@ module Env : sig
   val add_variant_clause : id -> type_union -> t -> t
   val get_variant : id -> t -> typquant * type_union list
   val get_scattered_variant_env : id -> t -> t
-  val add_mapping : id -> typquant * typ * typ -> t -> t
+  val add_mapping : id -> typquant * typ * typ * effect -> t -> t
   val add_union_id : id -> typquant * typ -> t -> t
   val get_union_id  : id -> t -> typquant * typ
   val is_register : id -> t -> bool
@@ -573,8 +573,8 @@ end = struct
   let builtin_mappings =
     List.fold_left (fun m (name, typ) -> Bindings.add (mk_id name) typ m) Bindings.empty
       [
-        ("int", Typ_bidir(int_typ, string_typ));
-        ("nat", Typ_bidir(nat_typ, string_typ));
+        ("int", Typ_bidir(int_typ, string_typ, no_effect));
+        ("nat", Typ_bidir(nat_typ, string_typ, no_effect));
       ]
 
   let bound_typ_id env id =
@@ -725,7 +725,7 @@ end = struct
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
     | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ, effs), l)
-    | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l)
+    | Typ_bidir (typ1, typ2, effs) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
     | Typ_app (id, args) ->
        (try
           begin match get_typ_synonym id env l env args with
@@ -786,7 +786,7 @@ end = struct
     | Typ_internal_unknown
     | Typ_id _ | Typ_var _ -> typ
     | Typ_fn (arg_typs, ret_typ, effect) -> Typ_aux (Typ_fn (List.map (map_nexps f) arg_typs, map_nexps f ret_typ, effect), l)
-    | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2), l)
+    | Typ_bidir (typ1, typ2, effect) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2, effect), l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (map_nexps f) typs), l)
     | Typ_exist (kids, nc, typ) -> Typ_aux (Typ_exist (kids, nc, map_nexps f typ), l)
     | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map (map_nexps_arg f) args), l)
@@ -819,9 +819,9 @@ end = struct
          typ_error env l ("Unbound type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
     | Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ
-    | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 ->
+    | Typ_bidir (typ1, typ2, _) when strip_typ typ1 = strip_typ typ2 ->
        typ_error env l "Bidirectional types cannot be the same on both sides"
-    | Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2
+    | Typ_bidir (typ1, typ2, _) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2
     | Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs
     | Typ_app (id, [A_aux (A_nexp _, _) as arg]) when string_of_id id = "implicit" ->
        wf_typ_arg ~exs:exs env arg
@@ -979,8 +979,8 @@ end = struct
        typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
        { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
 
-    | Typ_aux (Typ_bidir (typ1, typ2), l) ->
-       let env = add_mapping id (typq, typ1, typ2) env in
+    | Typ_aux (Typ_bidir (typ1, typ2, effect), l) ->
+       let env = add_mapping id (typq, typ1, typ2, effect) env in
        typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
        { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
 
@@ -1002,16 +1002,16 @@ end = struct
         env
          *)
 
-  and add_mapping id (typq, typ1, typ2) env =
+  and add_mapping id (typq, typ1, typ2, effect) env =
     typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
     let forwards_id = mk_id (string_of_id id ^ "_forwards") in
     let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
     let backwards_id = mk_id (string_of_id id ^ "_backwards") in
     let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
-    let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in
-    let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in
-    let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in
-    let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in
+    let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, effect), Parse_ast.Unknown) in
+    let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, effect), Parse_ast.Unknown) in
+    let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, effect), Parse_ast.Unknown) in
+    let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, effect), Parse_ast.Unknown) in
     let env =
       { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings }
       |> add_val_spec forwards_id (typq, forwards_typ)
@@ -1451,7 +1451,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) =
   | Typ_tup typs -> List.for_all is_typ_monomorphic typs
   | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args
   | Typ_fn (arg_typs, ret_typ, _) -> List.for_all is_typ_monomorphic arg_typs && is_typ_monomorphic ret_typ
-  | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
+  | Typ_bidir (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
   | Typ_exist _ | Typ_var _ -> false
   | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
 and is_typ_arg_monomorphic (A_aux (arg, _)) =
@@ -1650,9 +1650,10 @@ and typ_identical (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) =
      List.for_all2 typ_identical arg_typs1 arg_typs2
      && typ_identical ret_typ1 ret_typ2
      && strip_effect eff1 = strip_effect eff2
-  | Typ_bidir (typ1, typ2), Typ_bidir (typ3, typ4) ->
+  | Typ_bidir (typ1, typ2, eff1), Typ_bidir (typ3, typ4, eff2) ->
      typ_identical typ1 typ3
      && typ_identical typ2 typ4
+     && strip_effect eff1 = strip_effect eff2
   | Typ_tup typs1, Typ_tup typs2 ->
      begin
        try List.for_all2 typ_identical typs1 typs2 with
@@ -2050,7 +2051,7 @@ let rec alpha_equivalent env typ1 typ2 =
       | Typ_internal_unknown -> Typ_internal_unknown
       | Typ_id _ | Typ_var _ -> aux
       | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map relabel arg_typs, relabel ret_typ, eff)
-      | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2)
+      | Typ_bidir (typ1, typ2, eff) -> Typ_bidir (relabel typ1, relabel typ2, eff)
       | Typ_tup typs -> Typ_tup (List.map relabel typs)
       | Typ_exist (kopts, nc, typ) ->
          let kind_map = List.fold_left (fun m kopt -> KBindings.add (kopt_kid kopt) (kopt_kind kopt) m) KBindings.empty kopts in
@@ -3310,7 +3311,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
          | _ -> [typ]
        in
        match Env.expand_synonyms env mapping_typ with
-       | Typ_aux (Typ_bidir (typ1, typ2), _) ->
+       | Typ_aux (Typ_bidir (typ1, typ2, _), _) ->
           begin
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ));
@@ -3404,7 +3405,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      begin
        let (typq, mapping_typ) = Env.get_val_spec f env in
        match Env.expand_synonyms env mapping_typ with
-       | Typ_aux (Typ_bidir (typ1, typ2), _) ->
+       | Typ_aux (Typ_bidir (typ1, typ2, _), _) ->
           begin
             try
               bind_pat env pat typ2
@@ -4242,7 +4243,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
          | _ -> [typ]
        in
        match Env.expand_synonyms env mapping_typ with
-       | Typ_aux (Typ_bidir (typ1, typ2), _) ->
+       | Typ_aux (Typ_bidir (typ1, typ2, _), _) ->
           begin
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
@@ -4341,7 +4342,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
      begin
        let (typq, mapping_typ) = Env.get_val_spec f env in
        match Env.expand_synonyms env mapping_typ with
-       | Typ_aux (Typ_bidir (typ1, typ2), _) ->
+       | Typ_aux (Typ_bidir (typ1, typ2, _), _) ->
           begin
             try
               bind_mpat allow_unknown other_env env mpat typ2
@@ -4835,7 +4836,7 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
 let check_mapcl : 'a. Env.t -> 'a mapcl -> typ -> tannot mapcl =
   fun env (MCL_aux (cl, (l, _))) typ ->
     match typ with
-    | Typ_aux (Typ_bidir (typ1, typ2), _) -> begin
+    | Typ_aux (Typ_bidir (typ1, typ2, _), _) -> begin
         match cl with
         | MCL_bidir (mpexp1, mpexp2) -> begin
             let testing_env = Env.set_allow_unknowns true env in
@@ -5000,7 +5001,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
           raise err
   in
   let vtyp1, vtyp2, vl = match typ with
-    | Typ_aux (Typ_bidir (vtyp1, vtyp2), vl) -> vtyp1, vtyp2, vl
+    | Typ_aux (Typ_bidir (vtyp1, vtyp2, _), vl) -> vtyp1, vtyp2, vl
     | _ -> typ_error env l "Mapping val spec was not a mapping type"
   in
   begin match tannot_opt with