Hid region bounds.

src/constraints.ml

@@ -23,11 +23,14 @@ let empty = {
 let add_ty_constraint ty1 ty2 cstr =
   { cstr with ty_graph = Ty.add_edge ty1 ty2 cstr.ty_graph }
 
-let add_region_bound r bnd cstr =
-  { cstr with region_graph = Region.add_region_bound r bnd cstr.region_graph }
+let add_region_constraint r1 r2 cstr =
+  { cstr with region_graph = Region.add_region_constraint r1 r2 cstr.region_graph }
 
-let add_region_constraint rgn1 rgn2 cstr =
-  { cstr with region_graph = Region.add_region_constraint rgn1 rgn2 cstr.region_graph }
+let add_handled_constraint r1 r2 rs cstr =
+  { cstr with region_graph = Region.add_handled_constraint r1 r2 rs cstr.region_graph }
+
+let add_instance_constraint inst r cstr =
+  { cstr with region_graph = Region.add_instance_constraint inst r cstr.region_graph }
 
 let add_dirt_constraint drt1 drt2 cstr =
   { cstr with dirt_graph = Dirt.add_edge drt1 drt2 cstr.dirt_graph }

src/infer.ml

@@ -226,7 +226,7 @@ let rec infer_expr env (e, pos) =
         let r_in = Type.fresh_region_param () in
         let r_out = Type.fresh_region_param () in
         let chngs = [
-          Scheme.add_region_bound r_out [Region.Without (r_in, !rs)]
+          Scheme.add_handled_constraint r_in r_out !rs
         ] @ chngs
         in
         (op, r_in) :: ops_in, (op, r_out) :: ops_out, chngs
@@ -372,7 +372,7 @@ and infer_comp env (c, pos) =
           let inst = Type.fresh_instance_param () in
           let r = Type.fresh_region_param () in
           unify ctx (Tctx.effect_to_params eff params r, empty_dirt ()) ([
-            Scheme.add_region_bound r [Region.Instance inst]
+            Scheme.add_instance_constraint inst r
           ] @ chngs)
       | _ -> Error.typing ~pos "Effect type expected but %s encountered" eff
       end

src/region.ml

@@ -57,6 +57,12 @@ let add_region_bound r bnd (grph, bnds) =
   let new_bounds = List.map (fun r -> (r, bnd)) (r :: succ) in
   (grph, Common.assoc_map (Common.compose Common.uniq List.flatten) (Common.assoc_flatten (new_bounds @ bnds)))
 
+let add_instance_constraint inst r =
+  add_region_bound r [Instance inst]
+
+let add_handled_constraint r1 r2 rs =
+  add_region_bound r2 [Without (r1, rs)]
+
 let add_region_constraint rgn1 rgn2 (grph, bnds) =
   let new_grph = add_edge rgn1 rgn2 grph in
   let new_cstr = (new_grph, bnds) in

src/region.mli

@@ -1,24 +1,22 @@
 type elt = Type.region_param
 type t
 
-type region_bound =
-  | Without of Type.region_param * Type.region_param list
-  | Instance of Type.instance_param
-
 (** The empty graph. *)
 val empty : t
 
 val union : t -> t -> t
 
 val subst : Type.substitution -> t -> t
 
-val add_region_bound : elt -> region_bound list -> t -> t
+val garbage_collect : elt list -> elt list -> t -> t
+
+val pos_handled : elt list -> elt list -> t -> elt list
 
 val add_region_constraint : elt -> elt -> t -> t
 
-val garbage_collect : elt list -> elt list -> t -> t
+val add_handled_constraint : elt -> elt -> elt list -> t -> t
 
-val pos_handled : elt list -> elt list -> t -> elt list
+val add_instance_constraint : Type.instance_param -> elt -> t -> t
 
 val print : non_poly:('a, 'b, Type.region_param) Trio.t -> t -> Format.formatter -> unit
 

src/scheme.ml

@@ -39,12 +39,14 @@ let ty_param_less p q (ctx, ty, cnstrs, sbst) =
   (ctx, ty, Constraints.add_ty_constraint p q cnstrs, sbst)
 and dirt_param_less d1 d2 (ctx, ty, cnstrs, sbst) =
   (ctx, ty, Constraints.add_dirt_constraint d1 d2 cnstrs, sbst)
-and region_param_less r1 r2 (ctx, ty, cnstrs, sbst) =
-  (ctx, ty, Constraints.add_region_constraint r1 r2 cnstrs, sbst)
 and just new_cnstrs (ctx, ty, cnstrs, sbst) =
   (ctx, ty, Constraints.union new_cnstrs cnstrs, sbst)
-and add_region_bound r bnd (ctx, ty, cnstrs, sbst) =
-  (ctx, ty, Constraints.add_region_bound r bnd cnstrs, sbst)
+and region_param_less r1 r2 (ctx, ty, cnstrs, sbst) =
+  (ctx, ty, Constraints.add_region_constraint r1 r2 cnstrs, sbst)
+and add_handled_constraint r1 r2 rs (ctx, ty, cnstrs, sbst) =
+  (ctx, ty, Constraints.add_handled_constraint r1 r2 rs cnstrs, sbst)
+and add_instance_constraint iota r (ctx, ty, cnstrs, sbst) =
+  (ctx, ty, Constraints.add_instance_constraint iota r cnstrs, sbst)
 
 let rec explode_dirt ~pos p ({Type.ops = ops} as drt_new) (ctx, ty, cnstrs, sbst) =
   if ops = [] then (ctx, ty, cnstrs, sbst) else

src/scheme.mli

@@ -6,8 +6,9 @@ type change
 val refresh : ty_scheme -> ty_scheme
 
 val region_param_less : Type.region_param -> Type.region_param -> change
+val add_instance_constraint : Type.instance_param -> Type.region_param -> change
+val add_handled_constraint : Type.region_param -> Type.region_param -> Type.region_param list -> change
 val just : Constraints.t -> change
-val add_region_bound : Type.region_param -> Region.region_bound list -> change
 val dirt_less : pos:Common.position -> Type.dirt -> Type.dirt -> change
 val ty_less : pos:Common.position -> Type.ty -> Type.ty -> change
 val dirty_less : pos:Common.position -> Type.dirty -> Type.dirty -> change