Allow effects with default handlers at top level

toplevel/opttoploop.ml

@@ -228,8 +228,7 @@ let execute_phrase print_outcome ppf phr =
       phrase_name := Printf.sprintf "TOP%i" !phrase_seqid;
       Compilenv.reset ?packname:None !phrase_name;
       Typecore.reset_delayed_checks ();
-      let (str, sg, newenv) = Typemod.type_structure oldenv sstr Location.none
-      in
+      let (str, sg, newenv) = Typemod.type_phrase false oldenv sstr in
       if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
       Typecore.force_delayed_checks ();
       let res = Translmod.transl_store_phrases !phrase_name str in

toplevel/toploop.ml

@@ -251,7 +251,7 @@ let execute_phrase print_outcome ppf phr =
   | Ptop_def sstr ->
       let oldenv = !toplevel_env in
       Typecore.reset_delayed_checks ();
-      let (str, sg, newenv) = Typemod.type_toplevel_phrase oldenv sstr in
+      let (str, sg, newenv) = Typemod.type_phrase true oldenv sstr in
       if !Clflags.dump_typedtree then Printtyped.implementation ppf str;
       let sg' = Typemod.simplify_signature sg in
       ignore (Includemod.signatures oldenv sg sg');

typing/ctype.ml

@@ -899,6 +899,7 @@ let rec normalize_package_path env p =
   | Some (Mty_signature _ | Mty_functor _ | Mty_alias _) | None -> p
 
 let rec update_level env level ty =
+ try
   let ty = repr ty in
   if ty.level > level then begin
     begin match Env.gadt_instance_level env ty with
@@ -955,6 +956,12 @@ let rec update_level env level ty =
         (* XXX what about abbreviations in Tconstr ? *)
         iter_type_expr (update_level env level) ty
   end
+  with Unify _ as exn ->
+   if !Clflags.dump_lambda then begin
+     Format.eprintf "Level %d, Type: %a"
+       level !Btype.print_raw ty
+   end;
+   raise exn
 
 (* Generalize and lower levels of contravariant branches simultaneously *)
 
@@ -4759,6 +4766,47 @@ let rec normalize_type_rec env visited ty =
 let normalize_type env ty =
   normalize_type_rec env (ref TypeSet.empty) ty
 
+                              (*****************************)
+                              (* Checking default handlers *)
+                              (*****************************)
+
+exception No_default_handler of Path.t * Location.t * string
+exception Unknown_effects of type_expr * Location.t * string
+
+let new_toplevel_expectation () =
+  Toplevel(ref [], !current_level)
+
+let rec check_default_handlers env loc str level ty =
+  let ty = repr ty in
+  match ty.desc with
+  | Teffect(p, ty) ->
+    let eff =
+      match Env.find_effect p env with
+      | eff -> eff
+      | exception Not_found ->
+          raise (No_default_handler(p, loc, str))
+    in
+    if not eff.eff_handler then
+      raise (No_default_handler(p, loc, str));
+    check_default_handlers env loc str level ty
+  | Tenil -> ()
+  | Tvar _ ->
+      if ty.level < level then
+        raise (Unknown_effects(ty, loc, str))
+  | _ ->
+    match !forward_try_expand_once env ty with
+    | ty -> check_default_handlers env loc str level ty
+    | exception Cannot_expand ->
+        raise (Unknown_effects(ty, loc, str))
+
+let check_expectation env = function
+  | Expected _ -> ()
+  | Toplevel(lr, level) ->
+      List.iter
+      (fun (ty, loc, str) ->
+        check_default_handlers env loc str level ty)
+      !lr
+
 
                               (*************************)
                               (*  Remove dependencies  *)

typing/ctype.mli

@@ -94,6 +94,13 @@ val equal_effect_constructor:
         Env.t -> effect_constructor_description ->
         effect_constructor_description -> bool
 
+exception No_default_handler of Path.t * Location.t * string
+exception Unknown_effects of type_expr * Location.t * string
+
+val new_toplevel_expectation : unit -> effect_expectation
+
+val check_expectation: Env.t -> effect_expectation -> unit
+
 val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
 val iterative_generalization: int -> type_expr list -> type_expr list

typing/typeclass.ml

@@ -602,7 +602,7 @@ let rec class_field self_loc cl_num self_type meths vars
       if !Clflags.principal then Ctype.begin_def ();
       let eff = Predef.effect_io (Btype.newgenty Tenil) in
       let exp =
-        try type_exp val_env sexp eff with Ctype.Unify [(ty, _)] ->
+        try type_exp val_env (Expected eff) sexp with Ctype.Unify [(ty, _)] ->
           raise(Error(loc, val_env, Make_nongen_seltype ty))
       in
       if !Clflags.principal then begin
@@ -683,8 +683,9 @@ let rec class_field self_loc cl_num self_type meths vars
             Btype.newgenty (Tarrow("", self_type, eff, ty, Cok)) in
           Ctype.raise_nongen_level ();
           vars := vars_local;
+          let eff = Btype.newgenty Tenil in
           let texp =
-            type_expect met_env meth_expr meth_type (Btype.newgenty Tenil)
+            type_expect met_env (Expected eff) meth_expr meth_type
           in
           Ctype.end_def ();
           mkcf (Tcf_method (lab, priv, Tcfk_concrete (ovf, texp)))
@@ -711,8 +712,9 @@ let rec class_field self_loc cl_num self_type meths vars
               (Tarrow ("", self_type, eff,
                        Ctype.instance_def Predef.type_unit, Cok)) in
           vars := vars_local;
+          let eff = Btype.newgenty Tenil in
           let texp =
-            type_expect met_env expr meth_type (Btype.newgenty Tenil)
+            type_expect met_env (Expected eff) expr meth_type
           in
           Ctype.end_def ();
           mkcf (Tcf_initializer texp)
@@ -747,7 +749,8 @@ and class_structure cl_num final val_env met_env loc
   (* Self binder *)
   let self_eff = Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil)) in
   let (pat, meths, vars, val_env, meth_env, par_env) =
-    type_self_pattern cl_num private_self val_env met_env par_env spat self_eff
+    type_self_pattern cl_num private_self
+      val_env met_env par_env (Expected self_eff) spat
   in
   let public_self = pat.pat_type in
 
@@ -933,11 +936,12 @@ and class_expr cl_num val_env met_env scl =
       class_expr cl_num val_env met_env sfun
   | Pcl_fun (l, None, spat, scl') ->
       if !Clflags.principal then Ctype.begin_def ();
-      let eff_expected =
+      let eff =
         Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
       in
       let (pat, pv, val_env', met_env) =
-        Typecore.type_class_arg_pattern cl_num val_env met_env l spat eff_expected
+        Typecore.type_class_arg_pattern cl_num
+          val_env met_env (Expected eff) l spat
       in
       if !Clflags.principal then begin
         Ctype.end_def ();
@@ -965,8 +969,8 @@ and class_expr cl_num val_env met_env scl =
       in
       let cont = Ctype.newvar Stype in
       let partial, _ =
-        Typecore.check_partial val_env cont pat.pat_type
-          eff_expected pat.pat_loc
+        Typecore.check_partial val_env (Expected eff) cont pat.pat_type
+          pat.pat_loc
           [{c_lhs=pat;
             c_guard=None;
             c_rhs = (* Dummy expression *)
@@ -1024,7 +1028,7 @@ and class_expr cl_num val_env met_env scl =
             let name = Btype.label_name l
             and optional =
               if Btype.is_optional l then Optional else Required in
-            let eff_expected =
+            let eff =
               Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
             in
             let sargs, more_sargs, arg =
@@ -1037,8 +1041,8 @@ and class_expr cl_num val_env met_env scl =
                       raise(Error(sarg0.pexp_loc, val_env,
                                   Apply_wrong_label l'))
                     else ([], more_sargs,
-                          Some (type_argument val_env sarg0
-                                  ty ty0 eff_expected))
+                          Some (type_argument val_env (Expected eff)
+                                  sarg0 ty ty0))
                 | _ ->
                     assert false
               end else try
@@ -1057,12 +1061,12 @@ and class_expr cl_num val_env met_env scl =
                     (Warnings.Nonoptional_label l);
                 sargs, more_sargs,
                 if optional = Required || Btype.is_optional l' then
-                  Some (type_argument val_env sarg0 ty ty0 eff_expected)
+                  Some (type_argument val_env (Expected eff) sarg0 ty ty0)
                 else
                   let ty' = extract_option_type val_env ty
                   and ty0' = extract_option_type val_env ty0 in
                   let arg =
-                    type_argument val_env sarg0 ty' ty0' eff_expected
+                    type_argument val_env (Expected eff) sarg0 ty' ty0'
                   in
                   Some (option_some arg)
               with Not_found ->
@@ -1103,12 +1107,12 @@ and class_expr cl_num val_env met_env scl =
           cl_attributes = scl.pcl_attributes;
          }
   | Pcl_let (rec_flag, sdefs, scl') ->
-      let eff_expected =
+      let eff =
         Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
       in
       let (defs, val_env) =
         try
-          Typecore.type_let val_env rec_flag sdefs eff_expected None
+          Typecore.type_let val_env (Expected eff) rec_flag sdefs None
         with Ctype.Unify [(ty, _)] ->
           raise(Error(scl.pcl_loc, val_env, Make_nongen_seltype ty))
       in