diff --git a/toplevel/opttoploop.ml b/toplevel/opttoploop.ml
index c2cf2fd1badf..8b18a56ca273 100644
--- a/toplevel/opttoploop.ml
+++ b/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
diff --git a/toplevel/toploop.ml b/toplevel/toploop.ml
index e425e327edc6..87ecf2c22357 100644
--- a/toplevel/toploop.ml
+++ b/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');
diff --git a/typing/ctype.ml b/typing/ctype.ml
index b90c59c329e3..3892e4a050f8 100644
--- a/typing/ctype.ml
+++ b/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  *)
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 03f816bee679..41355f1088a4 100644
--- a/typing/ctype.mli
+++ b/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
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 8310615f330c..cac8049ef1f6 100644
--- a/typing/typeclass.ml
+++ b/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
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 714b7f65ff6f..faf17fac1694 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -77,6 +77,8 @@ type error =
   | Default_handler_mismatch of Path.t * Path.t
   | Default_handler_not_exhaustive
   | Default_handler_nonreturning of Longident.t
+  | Toplevel_no_default_handler of Path.t * string
+  | Toplevel_unknown_effects of type_expr * string
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
@@ -84,8 +86,9 @@ exception Error_forward of Location.error
 (* Forward declaration, to be filled in by Typemod.type_module *)
 
 let type_module =
-  ref ((fun env md -> assert false) :
-       Env.t -> Parsetree.module_expr -> Typedtree.module_expr)
+  ref ((fun eff env md -> assert false) :
+         Env.t -> effect_expectation ->
+           Parsetree.module_expr -> Typedtree.module_expr)
 
 (* Forward declaration, to be filled in by Typemod.type_open *)
 
@@ -337,19 +340,29 @@ let unify_exp_types loc env ty expected_ty =
 
 (* effect unification inside type_pat *)
 let unify_pat_effects loc env eff expected_eff =
-  try
-    unify env eff expected_eff
-  with
-    Unify trace ->
-      raise(Error(loc, env, Pattern_effect_clash(trace)))
+  match expected_eff with
+  | Toplevel(lr, _) ->
+      lr := (eff, loc, "pattern") :: !lr
+  | Expected expected_eff -> begin
+      try
+        unify env eff expected_eff
+      with
+        Unify trace ->
+          raise(Error(loc, env, Pattern_effect_clash(trace)))
+    end
 
 (* effect unification inside type_exp and type_expect *)
 let unify_exp_effects loc env eff expected_eff =
-  try
-    unify env eff expected_eff
-  with
-    Unify trace ->
-      raise(Error(loc, env, Expr_effect_clash(trace)))
+  match expected_eff with
+  | Toplevel(lr, _) ->
+      lr := (eff, loc, "expression") :: !lr
+  | Expected expected_eff -> begin
+      try
+        unify env eff expected_eff
+      with
+        Unify trace ->
+          raise(Error(loc, env, Expr_effect_clash(trace)))
+    end
 
 (* level at which to create the local type declarations *)
 let newtype_level = ref None
@@ -926,7 +939,7 @@ let unify_head_only loc env ty constr =
 (* Typing of patterns *)
 
 (* Simplified patterns for effect continuations *)
-let type_continuation_pat env expected_ty expected_eff sp =
+let type_continuation_pat env expected_eff expected_ty sp =
   let loc = sp.ppat_loc in
   match sp.ppat_desc with
   | Ppat_any -> None
@@ -948,10 +961,10 @@ type type_pat_mode =
    constructors and labels.
    Unification may update the typing environment. *)
 let rec type_pat ?in_handler ~constrs ~labels ~no_existentials ~mode ~env
-                 ~allow_exn cont_ty expected_eff sp expected_ty =
+                 ~allow_exn ~expected_eff ~cont_ty sp expected_ty =
   let type_pat ?(mode=mode) ?(env=env) =
     type_pat ?in_handler ~constrs ~labels ~no_existentials
-     ~mode ~env ~allow_exn:false cont_ty expected_eff
+     ~mode ~env ~allow_exn:false ~expected_eff ~cont_ty
   in
   let loc = sp.ppat_loc in
   match sp.ppat_desc with
@@ -1342,11 +1355,19 @@ let rec type_pat ?in_handler ~constrs ~labels ~no_existentials ~mode ~env
             match ty_res, scont with
             | None, None -> None
             | Some res_type, Some scont ->
+                let eff_cont =
+                  match expected_eff with
+                  | Expected eff -> eff
+                  | Toplevel(lr, _) ->
+                      let evar = Ctype.newvar Seffect in
+                      lr := (evar, loc, "continuation") :: !lr;
+                      evar
+                in
                 let ty_cont =
                   instance_def
-                    (Predef.type_continuation res_type expected_eff cont_ty)
+                    (Predef.type_continuation res_type eff_cont cont_ty)
                 in
-                Some (type_continuation_pat !env ty_cont expected_eff scont)
+                Some (type_continuation_pat !env expected_eff ty_cont scont)
             | None, Some _ ->
                 raise(Error(loc, !env,
                   Unexpected_continuation_pattern lid.txt))
@@ -1363,14 +1384,14 @@ let rec type_pat ?in_handler ~constrs ~labels ~no_existentials ~mode ~env
       raise (Error_forward (Typetexp.error_of_extension ext))
 
 let type_pat ?in_handler ?(allow_existentials=false) ?constrs ?labels
-    ?(lev=get_current_level()) ~env ~allow_exn
-    cont_ty expected_eff sp expected_ty =
+    ?(lev=get_current_level()) ~env ~allow_exn ~expected_eff
+    ~cont_ty sp expected_ty =
   newtype_level := Some lev;
   try
     let r =
       type_pat ?in_handler ~no_existentials:(not allow_existentials) ~constrs
         ~labels ~mode:Normal ~env ~allow_exn
-        cont_ty expected_eff sp expected_ty
+        ~expected_eff ~cont_ty sp expected_ty
     in
     iter_pattern (fun p -> p.pat_env <- !env) r;
     newtype_level := None;
@@ -1382,14 +1403,15 @@ let type_pat ?in_handler ?(allow_existentials=false) ?constrs ?labels
 
 (* this function is passed to Partial.parmatch
    to type check gadt nonexhaustiveness *)
-let partial_pred ~lev env cont_ty expected_ty expected_eff constrs labels p =
+let partial_pred ~lev ~env ~expected_eff ~cont_ty
+      expected_ty constrs labels p =
   let snap = snapshot () in
   try
     reset_pattern None true;
     let typed_p =
       type_pat ~allow_existentials:true ~lev
         ~constrs ~labels ~env:(ref env) ~allow_exn:true
-        cont_ty expected_eff p expected_ty
+        ~expected_eff ~cont_ty p expected_ty
     in
     backtrack snap;
     (* types are invalidated but we don't need them here *)
@@ -1398,10 +1420,10 @@ let partial_pred ~lev env cont_ty expected_ty expected_eff constrs labels p =
     backtrack snap;
     None
 
-let check_partial ?(lev=get_current_level ()) env
-                  cont_ty expected_ty expected_eff =
+let check_partial ?(lev=get_current_level ()) ~env
+                  ~expected_eff ~cont_ty expected_ty =
   Parmatch.check_partial_gadt
-    (partial_pred ~lev env cont_ty expected_ty expected_eff)
+    (partial_pred ~lev ~env ~expected_eff ~cont_ty expected_ty)
     env
 
 let rec iter3 f lst1 lst2 lst3 =
@@ -1427,13 +1449,13 @@ let add_pattern_variables ?check ?check_as env =
      pv env,
    get_ref module_variables)
 
-let type_pattern ?in_handler ~lev ~allow_exn env spat scope
-                 cont_ty expected_ty expected_eff =
+let type_pattern ?in_handler ~lev ~allow_exn env expected_eff spat scope
+                 cont_ty expected_ty =
   reset_pattern scope true;
   let new_env = ref env in
   let pat =
     type_pat ?in_handler ~allow_existentials:true ~lev ~env:new_env ~allow_exn
-             cont_ty expected_eff spat expected_ty
+             ~expected_eff ~cont_ty spat expected_ty
   in
   let new_env, unpacks =
     add_pattern_variables !new_env
@@ -1441,25 +1463,26 @@ let type_pattern ?in_handler ~lev ~allow_exn env spat scope
       ~check_as:(fun s -> Warnings.Unused_var s) in
   (pat, new_env, get_ref pattern_force, unpacks)
 
-let type_pattern_list ~allow_exn env spatl scope cont_ty
-                      expected_tys expected_eff allow =
+let type_pattern_list ~allow_exn env expected_eff spatl scope cont_ty
+                      expected_tys allow =
   reset_pattern scope allow;
   let new_env = ref env in
   let patl =
     List.map2
       (fun spat expected_ty ->
-        type_pat ~allow_exn ~env:new_env cont_ty expected_eff spat expected_ty)
+        type_pat ~allow_exn ~env:new_env ~expected_eff ~cont_ty
+          spat expected_ty)
       spatl expected_tys
   in
   let new_env, unpacks = add_pattern_variables !new_env in
   (patl, new_env, get_ref pattern_force, unpacks)
 
-let type_class_arg_pattern cl_num val_env met_env l spat eff_expected =
+let type_class_arg_pattern cl_num val_env met_env expected_eff l spat =
   reset_pattern None false;
   let nv = newvar Stype in
-  let cont = newvar Stype in
+  let cont_ty = newvar Stype in
   let pat =
-    type_pat ~allow_exn:false ~env:(ref val_env) cont eff_expected spat nv
+    type_pat ~allow_exn:false ~env:(ref val_env) ~expected_eff ~cont_ty spat nv
   in
   if has_variants pat then begin
     Parmatch.pressure_variants val_env [pat];
@@ -1486,7 +1509,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat eff_expected =
   let val_env, _ = add_pattern_variables val_env in
   (pat, pv, val_env, met_env)
 
-let type_self_pattern cl_num privty val_env met_env par_env spat eff_expected =
+let type_self_pattern cl_num privty val_env met_env par_env expected_eff spat =
   let open Ast_helper in
   let spat =
     Pat.mk (Ppat_alias (Pat.mk(Ppat_alias (spat, mknoloc "selfpat-*")),
@@ -1494,9 +1517,9 @@ let type_self_pattern cl_num privty val_env met_env par_env spat eff_expected =
   in
   reset_pattern None false;
   let nv = newvar Stype in
-  let cont = newvar Stype in
+  let cont_ty = newvar Stype in
   let pat =
-    type_pat ~allow_exn:false ~env:(ref val_env) cont eff_expected spat nv
+    type_pat ~allow_exn:false ~env:(ref val_env) ~expected_eff ~cont_ty spat nv
   in
   List.iter (fun f -> f()) (get_ref pattern_force);
   let meths = ref Meths.empty in
@@ -1945,9 +1968,9 @@ let unify_exp env exp expected_ty =
     Printtyp.raw_type_expr expected_ty; *)
     unify_exp_types exp.exp_loc env exp.exp_type expected_ty
 
-let rec type_exp env sexp eff_expected =
+let rec type_exp env expected_eff sexp =
   (* We now delegate everything to type_expect *)
-  type_expect env sexp (newvar Stype) eff_expected
+  type_expect env expected_eff sexp (newvar Stype)
 
 (* Typing of an expression with an expected type.
    This provide better error messages, and allows controlled
@@ -1955,17 +1978,19 @@ let rec type_exp env sexp eff_expected =
    In the principal case, [type_expected'] may be at generic_level.
  *)
 
-and type_expect ?in_function env sexp ty_expected eff_expected =
+and type_expect ?in_function env expected_eff sexp ty_expected =
   let previous_saved_types = Cmt_format.get_saved_types () in
   Typetexp.warning_enter_scope ();
   Typetexp.warning_attribute sexp.pexp_attributes;
-  let exp = type_expect_ ?in_function env sexp ty_expected eff_expected in
+  let exp =
+    type_expect_ ?in_function env expected_eff sexp ty_expected
+  in
   Typetexp.warning_leave_scope ();
   Cmt_format.set_saved_types
     (Cmt_format.Partial_expression exp :: previous_saved_types);
   exp
 
-and type_expect_ ?in_function env sexp ty_expected eff_expected =
+and type_expect_ ?in_function env expected_eff sexp ty_expected =
   let loc = sexp.pexp_loc in
   (* Record the expression type before unifying it with the expected type *)
   let rue exp =
@@ -1974,7 +1999,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
   in
   let rufe eff exp =
     unify_exp env (re exp) (instance env ty_expected);
-    unify_exp_effects exp.exp_loc env eff eff_expected;
+    unify_exp_effects exp.exp_loc env eff expected_eff;
     exp
   in
   match sexp.pexp_desc with
@@ -2038,7 +2063,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
     if is_format then
       let format_parsetree =
         { (type_format loc str env) with pexp_loc = sexp.pexp_loc }  in
-      type_expect ?in_function env format_parsetree ty_expected eff_expected
+      type_expect ?in_function env expected_eff format_parsetree ty_expected
     else
       rue {
         exp_desc = Texp_constant cst;
@@ -2058,10 +2083,10 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
              [{pvb_pat=spat; pvb_expr=sval; pvb_attributes=[]}], sbody)
     when contains_gadt env spat ->
     (* TODO: allow non-empty attributes? *)
-      type_expect ?in_function env
+      type_expect ?in_function env expected_eff
         {sexp with
          pexp_desc = Pexp_match (sval, [Ast_helper.Exp.case spat sbody])}
-        ty_expected eff_expected
+        ty_expected
   | Pexp_let(rec_flag, spat_sexp_list, sbody) ->
       let scp =
         match sexp.pexp_attributes, rec_flag with
@@ -2070,9 +2095,11 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         | _, Nonrecursive -> Some (Annot.Idef sbody.pexp_loc)
       in
       let (pat_exp_list, new_env, unpacks) =
-        type_let env rec_flag spat_sexp_list scp true eff_expected in
+        type_let env rec_flag spat_sexp_list scp true expected_eff in
       let body =
-        type_expect new_env (wrap_unpacks sbody unpacks) ty_expected eff_expected in
+        type_expect new_env expected_eff
+          (wrap_unpacks sbody unpacks) ty_expected
+      in
       re {
         exp_desc = Texp_let(rec_flag, pat_exp_list, body);
         exp_loc = loc; exp_extra = [];
@@ -2108,7 +2135,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
           (Exp.let_ ~loc Nonrecursive ~attrs:[mknoloc "#default",PStr []]
              [Vb.mk spat smatch] sexp)
       in
-      type_expect ?in_function env sfun ty_expected eff_expected
+      type_expect ?in_function env expected_eff sfun ty_expected
         (* TODO: keep attributes, call type_function directly *)
   | Pexp_fun (l, None, spat, sexp) ->
       type_function ?in_function loc sexp.pexp_attributes env ty_expected
@@ -2121,7 +2148,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         Syntaxerr.ill_formed_ast loc "Function application with no argument.";
       begin_def (); (* one more level for non-returning functions *)
       if !Clflags.principal then begin_def ();
-      let funct = type_exp env sfunct eff_expected in
+      let funct = type_exp env expected_eff sfunct in
       if !Clflags.principal then begin
           end_def ();
           generalize_structure funct.exp_type
@@ -2141,7 +2168,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       end_def ();
       wrap_trace_gadt_instances env (lower_args []) ty;
       begin_def ();
-      let (args, ty_res) = type_application loc env funct sargs eff_expected in
+      let (args, ty_res) = type_application env loc expected_eff funct sargs in
       end_def ();
       unify_var env (newvar Stype) funct.exp_type;
       rue {
@@ -2153,15 +2180,15 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
   | Pexp_match(sarg, caselist) ->
       let eff = newvar Seffect in
       begin_def ();
-      let arg = type_exp env sarg eff in
+      let arg = type_exp env (Expected eff) sarg in
       end_def ();
       if is_nonexpansive arg then generalize arg.exp_type
       else generalize_expansive env arg.exp_type;
       close_effects_covariant env arg.exp_type;
       check_value_case loc env caselist;
       let cases, partial, handled =
-        type_cases env ~allow_exn:true arg.exp_type
-          eff_expected ty_expected loc caselist
+        type_cases env ~allow_exn:true expected_eff
+          arg.exp_type ty_expected loc caselist
       in
       let outer_eff = newvar Seffect in
       let inner_eff =
@@ -2169,8 +2196,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
           (fun p ty -> newty (Teffect(p, ty)))
           handled outer_eff
       in
-      unify_exp_effects arg.exp_loc env eff inner_eff;
-      unify_exp_effects loc env outer_eff eff_expected;
+      unify_exp_effects arg.exp_loc env eff (Expected inner_eff);
+      unify_exp_effects loc env outer_eff expected_eff;
       re {
         exp_desc = Texp_match(arg, cases, partial);
         exp_loc = loc; exp_extra = [];
@@ -2179,11 +2206,11 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_env = env }
   | Pexp_try(sbody, caselist) ->
       let eff = newvar Seffect in
-      let body = type_expect env sbody ty_expected eff in
+      let body = type_expect env (Expected eff) sbody ty_expected in
       let caselist = make_exception_default caselist in
       let cases, _, handled =
-        type_cases env ~allow_exn:true (newvar Stype)
-          eff_expected ty_expected loc caselist
+        type_cases env ~allow_exn:true expected_eff (newvar Stype)
+         ty_expected loc caselist
       in
       let outer_eff = newvar Seffect in
       let inner_eff =
@@ -2191,8 +2218,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
           (fun p ty -> newty (Teffect(p, ty)))
           handled outer_eff
       in
-      unify_exp_effects body.exp_loc env eff inner_eff;
-      unify_exp_effects loc env outer_eff eff_expected;
+      unify_exp_effects body.exp_loc env eff (Expected inner_eff);
+      unify_exp_effects loc env outer_eff expected_eff;
       re {
         exp_desc = Texp_try(body, cases);
         exp_loc = loc; exp_extra = [];
@@ -2207,7 +2234,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       unify_exp_types loc env to_unify ty_expected;
       let expl =
         List.map2
-          (fun body ty -> type_expect env body ty eff_expected)
+          (fun body ty -> type_expect env expected_eff body ty)
           sexpl subtypes
       in
       re {
@@ -2219,7 +2246,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_env = env }
   | Pexp_construct(lid, sarg) ->
       type_construct env loc lid sarg ty_expected
-        eff_expected sexp.pexp_attributes
+        expected_eff sexp.pexp_attributes
   | Pexp_variant(l, sarg) ->
       (* Keep sharing *)
       let ty_expected0 = instance env ty_expected in
@@ -2230,7 +2257,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
           begin match row_field_repr (List.assoc l row.row_fields),
           row_field_repr (List.assoc l row0.row_fields) with
             Rpresent (Some ty), Rpresent (Some ty0) ->
-              let arg = type_argument env sarg ty ty0 eff_expected in
+              let arg = type_argument env expected_eff sarg ty ty0 in
               re { exp_desc = Texp_variant(l, Some arg);
                    exp_loc = loc; exp_extra = [];
                    exp_type = ty_expected0;
@@ -2242,7 +2269,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       with Not_found ->
         let arg =
           may_map
-            (fun sexp -> type_exp env sexp eff_expected)
+            (fun sexp -> type_exp env expected_eff sexp)
             sarg
         in
         let arg_type = may_map (fun arg -> arg.exp_type) arg in
@@ -2266,7 +2293,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
           None -> None
         | Some sexp ->
             if !Clflags.principal then begin_def ();
-            let exp = type_exp env sexp eff_expected in
+            let exp = type_exp env expected_eff sexp in
             if !Clflags.principal then begin
               end_def ();
               generalize_structure exp.exp_type
@@ -2303,7 +2330,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       let lbl_exp_list =
         wrap_disambiguate "This record expression is expected to have" ty_record
           (type_label_a_list loc closed env
-             (type_label_exp true env loc ty_record eff_expected)
+             (type_label_exp true env loc expected_eff ty_record)
              opath)
           lid_sexp_list
       in
@@ -2369,7 +2396,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       in
       if mut then begin
         let eff = instance_def (Predef.effect_io (newvar Seffect)) in
-        unify_exp_effects loc env eff eff_expected
+        unify_exp_effects loc env eff expected_eff
       end;
       re {
         exp_desc = Texp_record(lbl_exp_list, opt_exp);
@@ -2379,7 +2406,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_env = env }
   | Pexp_field(srecord, lid) ->
       let (record, label, _) =
-        type_label_access env loc srecord lid eff_expected
+        type_label_access env loc expected_eff srecord lid
       in
       let (_, ty_arg, ty_res) = instance_label false label in
       unify_exp env record ty_res;
@@ -2397,11 +2424,11 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_env = env }
   | Pexp_setfield(srecord, lid, snewval) ->
       let (record, label, opath) =
-        type_label_access env loc srecord lid eff_expected
+        type_label_access env loc expected_eff srecord lid
       in
       let ty_record = if opath = None then newvar Stype else record.exp_type in
       let (label_loc, label, newval) =
-        type_label_exp false env loc ty_record eff_expected
+        type_label_exp false env loc expected_eff ty_record
           (lid, label, snewval)
       in
       unify_exp env record ty_record;
@@ -2419,10 +2446,10 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       let to_unify = Predef.type_array ty in
       unify_exp_types loc env to_unify ty_expected;
       let argl =
-        List.map (fun sarg -> type_expect env sarg ty eff_expected) sargl
+        List.map (fun sarg -> type_expect env expected_eff sarg ty) sargl
       in
       let eff = instance_def (Predef.effect_io (newvar Seffect)) in
-      unify_exp_effects loc env eff eff_expected;
+      unify_exp_effects loc env eff expected_eff;
       re {
         exp_desc = Texp_array argl;
         exp_loc = loc; exp_extra = [];
@@ -2430,10 +2457,10 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_attributes = sexp.pexp_attributes;
         exp_env = env }
   | Pexp_ifthenelse(scond, sifso, sifnot) ->
-      let cond = type_expect env scond Predef.type_bool eff_expected in
+      let cond = type_expect env expected_eff scond Predef.type_bool in
       begin match sifnot with
         None ->
-          let ifso = type_expect env sifso Predef.type_unit eff_expected in
+          let ifso = type_expect env expected_eff sifso Predef.type_unit in
           rue {
             exp_desc = Texp_ifthenelse(cond, ifso, None);
             exp_loc = loc; exp_extra = [];
@@ -2441,8 +2468,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
             exp_attributes = sexp.pexp_attributes;
             exp_env = env }
       | Some sifnot ->
-          let ifso = type_expect env sifso ty_expected eff_expected in
-          let ifnot = type_expect env sifnot ty_expected eff_expected in
+          let ifso = type_expect env expected_eff sifso ty_expected in
+          let ifnot = type_expect env expected_eff sifnot ty_expected in
           (* Keep sharing *)
           unify_exp env ifnot ifso.exp_type;
           re {
@@ -2453,8 +2480,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
             exp_env = env }
       end
   | Pexp_sequence(sexp1, sexp2) ->
-      let exp1 = type_statement env sexp1 eff_expected in
-      let exp2 = type_expect env sexp2 ty_expected eff_expected in
+      let exp1 = type_statement env expected_eff sexp1 in
+      let exp2 = type_expect env expected_eff sexp2 ty_expected in
       re {
         exp_desc = Texp_sequence(exp1, exp2);
         exp_loc = loc; exp_extra = [];
@@ -2462,8 +2489,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_attributes = sexp.pexp_attributes;
         exp_env = env }
   | Pexp_while(scond, sbody) ->
-      let cond = type_expect env scond Predef.type_bool eff_expected in
-      let body = type_statement env sbody eff_expected in
+      let cond = type_expect env expected_eff scond Predef.type_bool in
+      let body = type_statement env expected_eff sbody in
       rue {
         exp_desc = Texp_while(cond, body);
         exp_loc = loc; exp_extra = [];
@@ -2471,8 +2498,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_attributes = sexp.pexp_attributes;
         exp_env = env }
   | Pexp_for(param, slow, shigh, dir, sbody) ->
-      let low = type_expect env slow Predef.type_int eff_expected in
-      let high = type_expect env shigh Predef.type_int eff_expected in
+      let low = type_expect env expected_eff slow Predef.type_int in
+      let high = type_expect env expected_eff shigh Predef.type_int in
       let id, new_env =
         match param.ppat_desc with
         | Ppat_any -> Ident.create "_for", env
@@ -2484,7 +2511,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         | _ ->
             raise (Error (param.ppat_loc, env, Invalid_for_loop_index))
       in
-      let body = type_statement new_env sbody eff_expected in
+      let body = type_statement new_env expected_eff sbody in
       rue {
         exp_desc = Texp_for(id, param, low, high, dir, body);
         exp_loc = loc; exp_extra = [];
@@ -2500,10 +2527,10 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         if separate then begin
           end_def ();
           generalize_structure ty;
-          (type_argument env sarg ty (instance env ty) eff_expected,
+          (type_argument env expected_eff sarg ty (instance env ty),
            instance env ty)
         end else
-          (type_argument env sarg ty ty eff_expected, ty)
+          (type_argument env expected_eff sarg ty ty, ty)
       in
       rue {
         exp_desc = arg.exp_desc;
@@ -2525,7 +2552,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
             in
             let ty' = cty'.ctyp_type in
             if separate then begin_def ();
-            let arg = type_exp env sarg eff_expected in
+            let arg = type_exp env expected_eff sarg in
             let gen =
               if separate then begin
                 end_def ();
@@ -2589,10 +2616,10 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
               end_def ();
               generalize_structure ty;
               generalize_structure ty';
-              (type_argument env sarg ty (instance env ty) eff_expected,
+              (type_argument env expected_eff sarg ty (instance env ty),
                instance env ty', Some cty, cty')
             end else
-              (type_argument env sarg ty ty eff_expected,
+              (type_argument env expected_eff sarg ty ty,
                ty', Some cty, cty')
       in
       rue {
@@ -2606,7 +2633,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       }
   | Pexp_send (e, met) ->
       if !Clflags.principal then begin_def ();
-      let obj = type_exp env e eff_expected in
+      let obj = type_exp env expected_eff e in
       begin try
         let (meth, exp, typ) =
           match obj.exp_desc with
@@ -2703,8 +2730,8 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         raise(Error(e.pexp_loc, env, Undefined_method (obj.exp_type, met)))
       end
   | Pexp_perform(lid, sarg) ->
-      type_perform env loc lid sarg ty_expected
-        eff_expected sexp.pexp_attributes
+      type_perform env loc expected_eff lid sarg
+        sexp.pexp_attributes ty_expected
   | Pexp_new cl ->
       let (cl_path, cl_decl) = Typetexp.find_class env loc cl.txt in
       begin match cl_decl.cty_new with
@@ -2725,7 +2752,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         match desc.val_kind with
           Val_ivar (Mutable, cl_num) ->
             let newval =
-              type_expect env snewval (instance env desc.val_type) eff_expected
+              type_expect env expected_eff snewval (instance env desc.val_type)
             in
             let (path_self, _) =
               Env.lookup_value (Longident.Lident ("self-" ^ cl_num)) env
@@ -2768,7 +2795,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
             begin try
               let (id, _, _, ty) = Vars.find lab.txt !vars in
               let exp =
-                type_expect env snewval (instance env ty) eff_expected
+                type_expect env expected_eff snewval (instance env ty)
               in
               (Path.Pident id, lab, exp)
             with
@@ -2793,11 +2820,11 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       begin_def ();
       Ident.set_current_time ty.level;
       let context = Typetexp.narrow () in
-      let modl = !type_module env smodl in
+      let modl = !type_module env expected_eff smodl in
       let (id, new_env) = Env.enter_module name.txt modl.mod_type env in
       Ctype.init_def(Ident.current_time());
       Typetexp.widen context;
-      let body = type_expect new_env sbody ty_expected eff_expected in
+      let body = type_expect new_env expected_eff sbody ty_expected in
       (* go back to original level *)
       end_def ();
       (* Unification of body.exp_type with the fresh variable ty
@@ -2810,8 +2837,6 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       with Unify _ ->
         raise(Error(loc, env, Scoping_let_module(name.txt, body.exp_type)))
       end;
-      let eff = instance_def (Predef.effect_io (newvar Seffect)) in
-      unify_exp_effects loc env eff eff_expected;
       re {
         exp_desc = Texp_letmodule(id, name, modl, body);
         exp_loc = loc; exp_extra = [];
@@ -2819,7 +2844,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_attributes = sexp.pexp_attributes;
         exp_env = env }
   | Pexp_assert (e) ->
-      let cond = type_expect env e Predef.type_bool eff_expected in
+      let cond = type_expect env expected_eff e Predef.type_bool in
       let exp_type =
         match cond.exp_desc with
         | Texp_construct(_, {cstr_name="false"}, _) ->
@@ -2839,7 +2864,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       let to_unify = Predef.type_lazy_t ty in
       unify_exp_types loc env to_unify ty_expected;
       let eff = Predef.effect_io (newgenty Tenil) in
-      let arg = type_expect env e ty eff in
+      let arg = type_expect env (Expected eff) e ty in
       re {
         exp_desc = Texp_lazy arg;
         exp_loc = loc; exp_extra = [];
@@ -2875,7 +2900,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       let exp =
         match (expand_head env ty).desc with
           Tpoly (ty', []) ->
-            let exp = type_expect env sbody ty' eff_expected in
+            let exp = type_expect env expected_eff sbody ty' in
             { exp with exp_type = instance env ty }
         | Tpoly (ty', tl) ->
             (* One more level to generalize locally *)
@@ -2886,12 +2911,12 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
               end_def ();
               generalize_structure ty''
             end;
-            let exp = type_expect env sbody ty'' eff_expected in
+            let exp = type_expect env expected_eff sbody ty'' in
             end_def ();
             check_univars env false "method" exp ty_expected vars;
             { exp with exp_type = instance env ty }
         | Tvar _ ->
-            let exp = type_exp env sbody eff_expected in
+            let exp = type_exp env expected_eff sbody in
             let exp = {exp with exp_type = newty (Tpoly (exp.exp_type, []))} in
             unify_exp env exp ty;
             exp
@@ -2923,7 +2948,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
       let (id, new_env) = Env.enter_type name decl env in
       Ctype.init_def(Ident.current_time());
 
-      let body = type_exp new_env sbody eff_expected in
+      let body = type_exp new_env expected_eff sbody in
       (* Replace every instance of this type constructor in the resulting
          type. *)
       let seen = Hashtbl.create 8 in
@@ -2963,7 +2988,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         | _ ->
             raise (Error (loc, env, Not_a_packed_module ty_expected))
       in
-      let (modl, tl') = !type_package env m p nl tl in
+      let (modl, tl') = !type_package env expected_eff m p nl tl in
       rue {
         exp_desc = Texp_pack modl;
         exp_loc = loc; exp_extra = [];
@@ -2972,7 +2997,7 @@ and type_expect_ ?in_function env sexp ty_expected eff_expected =
         exp_env = env }
   | Pexp_open (ovf, lid, e) ->
       let (path, newenv) = !type_open ovf env sexp.pexp_loc lid in
-      let exp = type_expect newenv e ty_expected eff_expected in
+      let exp = type_expect newenv expected_eff e ty_expected in
       { exp with
         exp_extra = (Texp_open (ovf, path, lid, newenv), loc,
                      sexp.pexp_attributes) ::
@@ -3015,7 +3040,8 @@ and type_function ?in_function loc attrs env ty_expected l caselist =
   end;
   let cases, partial, _ =
     type_cases ~allow_exn:false ~in_function:(loc_fun,ty_fun) env
-      ty_arg ty_eff ty_res loc caselist in
+      (Expected ty_eff) ty_arg ty_res loc caselist
+  in
   let not_function ty =
     let ls, tvar = list_labels env ty in
     ls = [] && not tvar
@@ -3031,9 +3057,9 @@ and type_function ?in_function loc attrs env ty_expected l caselist =
     exp_env = env }
 
 
-and type_label_access env loc srecord lid eff_expected =
+and type_label_access env loc expected_eff srecord lid =
   if !Clflags.principal then begin_def ();
-  let record = type_exp env srecord eff_expected in
+  let record = type_exp env expected_eff srecord in
   if !Clflags.principal then begin
     end_def ();
     generalize_structure record.exp_type
@@ -3295,7 +3321,7 @@ and type_format loc str env =
   with Failure msg ->
     raise (Error (loc, env, Invalid_format msg))
 
-and type_label_exp create env loc ty_expected eff_expected
+and type_label_exp create env loc expected_eff ty_expected
           (lid, label, sarg) =
   (* Here also ty_expected may be at generic_level *)
   begin_def ();
@@ -3328,7 +3354,7 @@ and type_label_exp create env loc ty_expected eff_expected
   let arg =
     let snap = if vars = [] then None else Some (Btype.snapshot ()) in
     let arg =
-      type_argument env sarg ty_arg (instance env ty_arg) eff_expected
+      type_argument env expected_eff sarg ty_arg (instance env ty_arg)
     in
     end_def ();
     try
@@ -3338,7 +3364,7 @@ and type_label_exp create env loc ty_expected eff_expected
       (* Try to retype without propagating ty_arg, cf PR#4862 *)
       may Btype.backtrack snap;
       begin_def ();
-      let arg = type_exp env sarg eff_expected in
+      let arg = type_exp env expected_eff sarg in
       end_def ();
       generalize_expansive env arg.exp_type;
       unify_exp env arg ty_arg;
@@ -3349,7 +3375,7 @@ and type_label_exp create env loc ty_expected eff_expected
   in
   (lid, label, {arg with exp_type = instance env arg.exp_type})
 
-and type_argument env sarg ty_expected' ty_expected eff_expected =
+and type_argument env expected_eff sarg ty_expected' ty_expected =
   (* ty_expected' may be generic *)
   let no_labels ty =
     let ls, tvar = list_labels env ty in
@@ -3368,7 +3394,7 @@ and type_argument env sarg ty_expected' ty_expected eff_expected =
       (* apply optional arguments when expected type is "" *)
       (* we must be very careful about not breaking the semantics *)
       if !Clflags.principal then begin_def ();
-      let texp = type_exp env sarg eff_expected in
+      let texp = type_exp env expected_eff sarg in
       if !Clflags.principal then begin
         end_def ();
         generalize_structure texp.exp_type
@@ -3434,11 +3460,11 @@ and type_argument env sarg ty_expected' ty_expected eff_expected =
                      func let_var) }
       end
   | _ ->
-      let texp = type_expect env sarg ty_expected' eff_expected in
+      let texp = type_expect env expected_eff sarg ty_expected' in
       unify_exp env texp ty_expected;
       texp
 
-and type_application loc env funct sargs eff_expected =
+and type_application env loc expected_eff funct sargs =
   (* funct.exp_type may be generic *)
   let result_type omitted ty_fun =
     List.fold_left
@@ -3449,6 +3475,14 @@ and type_application loc env funct sargs eff_expected =
     let ls, tvar = list_labels env ty_fun in
     tvar || List.mem l ls
   in
+  let eff =
+    match expected_eff with
+    | Expected eff -> eff
+    | Toplevel(lr, _) ->
+        let evar = Ctype.newvar Seffect in
+        lr := (evar, loc, "application") :: !lr;
+        evar
+  in
   let ignored = ref [] in
   let rec type_unknown_args
       (args :
@@ -3499,7 +3533,7 @@ and type_application loc env funct sargs eff_expected =
         in
         let optional = if is_optional l1 then Optional else Required in
         let arg1 () =
-          let arg1 = type_expect env sarg1 ty_arg eff_expected in
+          let arg1 = type_expect env expected_eff sarg1 ty_arg in
           if optional = Optional then
             unify_exp env arg1 (type_option (newvar Stype));
           begin try
@@ -3567,7 +3601,7 @@ and type_application loc env funct sargs eff_expected =
                   ([], more_sargs,
                    Some (fun () ->
                            unify_effect sarg0;
-                           type_argument env sarg0 ty ty0 eff_expected))
+                           type_argument env expected_eff sarg0 ty ty0))
             | _ ->
                 assert false
           end else try
@@ -3593,16 +3627,15 @@ and type_application loc env funct sargs eff_expected =
             if optional = Required || is_optional l' then
               Some (fun () ->
                       unify_effect sarg0;
-                      type_argument env sarg0 ty ty0 eff_expected)
+                      type_argument env expected_eff sarg0 ty ty0)
             else begin
               may_warn sarg0.pexp_loc
                 (Warnings.Not_principal "using an optional argument here");
               Some (fun () ->
                       unify_effect sarg0;
-                      option_some (type_argument env sarg0
+                      option_some (type_argument env expected_eff sarg0
                                      (extract_option_type env ty)
-                                     (extract_option_type env ty0)
-                                     eff_expected))
+                                     (extract_option_type env ty0)))
             end
           with Not_found ->
             sargs, more_sargs,
@@ -3642,7 +3675,7 @@ and type_application loc env funct sargs eff_expected =
       let ty_arg, ty_eff, ty_res =
         filter_arrow env (instance env funct.exp_type) ""
       in
-      let exp = type_expect env sarg ty_arg eff_expected in
+      let exp = type_expect env expected_eff sarg ty_arg in
       begin match (expand_head env exp.exp_type).desc with
       | Tarrow _ ->
           Location.prerr_warning exp.exp_loc Warnings.Partial_application
@@ -3654,11 +3687,11 @@ and type_application loc env funct sargs eff_expected =
   | _ ->
       let ty = funct.exp_type in
       if ignore_labels then
-        type_args [] [] eff_expected ty (instance env ty) ty [] sargs
+        type_args [] [] eff ty (instance env ty) ty [] sargs
       else
-        type_args [] [] eff_expected ty (instance env ty) ty sargs []
+        type_args [] [] eff ty (instance env ty) ty sargs []
 
-and type_construct env loc lid sarg ty_expected eff_expected attrs =
+and type_construct env loc lid sarg ty_expected expected_eff attrs =
   let opath =
     try
       let (p0, p,_) = extract_concrete_variant env ty_expected in
@@ -3708,7 +3741,7 @@ and type_construct env loc lid sarg ty_expected eff_expected attrs =
   let texp = {texp with exp_type = ty_res} in
   if not separate then unify_exp env texp (instance env ty_expected);
   let args =
-    List.map2 (fun e (t,t0) -> type_argument env e t t0 eff_expected)
+    List.map2 (fun e (t,t0) -> type_argument env expected_eff e t t0)
       sargs (List.combine ty_args ty_args0)
   in
   if constr.cstr_private = Private then
@@ -3717,7 +3750,7 @@ and type_construct env loc lid sarg ty_expected eff_expected attrs =
   { texp with
     exp_desc = Texp_construct(lid, constr, args) }
 
-and type_perform env loc lid sarg ty_expected eff_expected attrs =
+and type_perform env loc expected_eff lid sarg attrs ty_expected =
   let ecstr = Typetexp.find_effect_constructor env lid.loc lid.txt in
   Typetexp.check_deprecated loc ecstr.ecstr_attributes ecstr.ecstr_name;
   let sargs =
@@ -3756,9 +3789,9 @@ and type_perform env loc lid sarg ty_expected eff_expected attrs =
   if not separate then
     unify_exp_types loc env ty_res (instance env ty_expected);
   let eff = newty (Teffect(ecstr.ecstr_eff_path, newvar Seffect)) in
-  unify_exp_effects loc env eff eff_expected;
+  unify_exp_effects loc env eff expected_eff;
   let args =
-    List.map2 (fun e (t,t0) -> type_argument env e t t0 eff_expected)
+    List.map2 (fun e (t,t0) -> type_argument env expected_eff e t t0)
       sargs (List.combine ty_args ty_args0)
   in
     re {
@@ -3770,10 +3803,10 @@ and type_perform env loc lid sarg ty_expected eff_expected attrs =
 
 (* Typing of statements (expressions whose values are discarded) *)
 
-and type_statement env sexp eff_expected =
+and type_statement env expected_eff sexp =
   let loc = (final_subexpression sexp).pexp_loc in
   begin_def();
-  let exp = type_exp env sexp eff_expected in
+  let exp = type_exp env expected_eff sexp in
   end_def();
   if !Clflags.strict_sequence then
     let expected_ty = instance_def Predef.type_unit in
@@ -3797,7 +3830,7 @@ and type_statement env sexp eff_expected =
 (* Typing of match cases *)
 
 and type_cases ?in_function ?in_handler ~allow_exn
-               env ty_arg ty_eff ty_res loc caselist =
+               env expected_eff ty_arg ty_res loc caselist =
   (* ty_arg is _fully_ generalized *)
   let patterns = List.map (fun {pc_lhs=p} -> p) caselist in
   let erase_either =
@@ -3852,7 +3885,7 @@ and type_cases ?in_function ?in_handler ~allow_exn
             then Some false else None in
           let ty_arg = instance ?partial env ty_arg in
           type_pattern ~lev ?in_handler ~allow_exn
-            env pc_lhs scope ty_res ty_arg ty_eff
+            env expected_eff pc_lhs scope ty_res ty_arg
         in
         pattern_force := force @ !pattern_force;
         let pat =
@@ -3906,10 +3939,10 @@ and type_cases ?in_function ?in_handler ~allow_exn
           | None -> None
           | Some scond ->
               Some
-                (type_expect ext_env (wrap_unpacks scond unpacks)
-                   Predef.type_bool ty_eff)
+                (type_expect ext_env expected_eff (wrap_unpacks scond unpacks)
+                   Predef.type_bool)
         in
-        let exp = type_expect ?in_function ext_env sexp ty_res' ty_eff in
+        let exp = type_expect ?in_function ext_env expected_eff sexp ty_res' in
         {
          c_lhs = pat;
          c_guard = guard;
@@ -3923,7 +3956,7 @@ and type_cases ?in_function ?in_handler ~allow_exn
     List.iter (fun c -> unify_exp env c.c_rhs ty_res') cases
   end;
   let partial, handled =
-    check_partial ~lev env ty_res ty_arg ty_eff loc cases
+    check_partial ~lev ~env ~expected_eff ~cont_ty:ty_res ty_arg loc cases
   in
   add_delayed_check
     (fun () ->
@@ -3941,7 +3974,7 @@ and type_cases ?in_function ?in_handler ~allow_exn
 
 and type_let ?(check = fun s -> Warnings.Unused_var s)
              ?(check_strict = fun s -> Warnings.Unused_var_strict s)
-    env rec_flag spat_sexp_list scope allow eff_expected =
+    env rec_flag spat_sexp_list scope allow expected_eff =
   let open Ast_helper in
   begin_def();
   if !Clflags.principal then begin_def ();
@@ -3972,10 +4005,10 @@ and type_let ?(check = fun s -> Warnings.Unused_var s)
         | _ -> spat)
       spat_sexp_list in
   let nvs = List.map (fun _ -> newvar Stype) spatl in
-  let cont = newvar Stype in
+  let cont_ty = newvar Stype in
   let (pat_list, new_env, force, unpacks) =
-    type_pattern_list ~allow_exn:false env spatl scope
-      cont nvs eff_expected allow
+    type_pattern_list ~allow_exn:false env expected_eff spatl scope
+      cont_ty nvs allow
   in
   let is_recursive = (rec_flag = Recursive) in
   (* If recursive, first unify with an approximation of the expression *)
@@ -4090,11 +4123,11 @@ and type_let ?(check = fun s -> Warnings.Unused_var s)
               end_def ();
               generalize_structure ty'
             end;
-            let exp = type_expect exp_env sexp ty' eff_expected in
+            let exp = type_expect exp_env expected_eff sexp ty' in
             end_def ();
             check_univars env true "definition" exp pat.pat_type vars;
             {exp with exp_type = instance env exp.exp_type}
-        | _ -> type_expect exp_env sexp pat.pat_type eff_expected)
+        | _ -> type_expect exp_env expected_eff sexp pat.pat_type)
       spat_sexp_list pat_slot_list in
   current_slot := None;
   if is_recursive && not !rec_needed
@@ -4103,7 +4136,7 @@ and type_let ?(check = fun s -> Warnings.Unused_var s)
       Warnings.Unused_rec_flag;
   List.iter2
     (fun pat exp ->
-      ignore(check_partial env cont pat.pat_type eff_expected
+      ignore(check_partial ~env ~expected_eff ~cont_ty pat.pat_type
                pat.pat_loc [case pat exp]))
     pat_list exp_list;
   end_def();
@@ -4132,27 +4165,27 @@ and type_let ?(check = fun s -> Warnings.Unused_var s)
 
 (* Typing of toplevel bindings *)
 
-let type_binding env rec_flag spat_sexp_list eff_expected scope =
+let type_binding env expected_eff rec_flag spat_sexp_list scope =
   Typetexp.reset_type_variables();
   let (pat_exp_list, new_env, unpacks) =
     type_let
       ~check:(fun s -> Warnings.Unused_value_declaration s)
       ~check_strict:(fun s -> Warnings.Unused_value_declaration s)
-      env rec_flag spat_sexp_list scope false eff_expected
+      env rec_flag spat_sexp_list scope false expected_eff
   in
   (pat_exp_list, new_env)
 
-let type_let env rec_flag spat_sexp_list eff_expected scope =
+let type_let env expected_eff rec_flag spat_sexp_list scope =
   let (pat_exp_list, new_env, unpacks) =
-    type_let env rec_flag spat_sexp_list scope false eff_expected in
+    type_let env rec_flag spat_sexp_list scope false expected_eff in
   (pat_exp_list, new_env)
 
 (* Typing of toplevel expressions *)
 
-let type_expression env sexp eff_expected =
+let type_expression env expected_eff sexp =
   Typetexp.reset_type_variables();
   begin_def();
-  let exp = type_exp env sexp eff_expected in
+  let exp = type_exp env expected_eff sexp in
   end_def();
   if is_nonexpansive exp then generalize exp.exp_type
   else generalize_expansive env exp.exp_type;
@@ -4165,11 +4198,11 @@ let type_expression env sexp eff_expected =
   | _ -> exp
 
 (* Typing of default effect handlers *)
-let type_default_handler env path seh eff_expected =
+let type_default_handler env expected_eff path seh =
   Typetexp.reset_type_variables ();
   let cases, _, handled =
-    type_cases env ~allow_exn:true ~in_handler:path (newvar Stype)
-       eff_expected (newvar Stype) seh.peh_loc seh.peh_cases
+    type_cases env ~allow_exn:true ~in_handler:path expected_eff
+      (newvar Stype) (newvar Stype) seh.peh_loc seh.peh_cases
   in
   begin match handled with
   | [p] when Path.same p path -> ()
@@ -4179,6 +4212,14 @@ let type_default_handler env path seh eff_expected =
     eh_env = env;
     eh_loc = seh.peh_loc; }
 
+let check_expectation env expected_eff =
+  match Ctype.check_expectation env expected_eff with
+  | () -> ()
+  | exception Ctype.No_default_handler(p, loc, str) ->
+      raise (Error(loc, env, Toplevel_no_default_handler(p, str)))
+  | exception Ctype.Unknown_effects(ty, loc, str) ->
+      raise (Error(loc, env, Toplevel_unknown_effects(ty, str)))
+
 (* Error report *)
 
 open Format
@@ -4436,6 +4477,14 @@ let report_error env ppf = function
       fprintf ppf
         "@[Effect %a is nonreturning, it cannot have a default handler.@]"
         longident lid
+  | Toplevel_no_default_handler(p, str) ->
+      fprintf ppf
+        "@[This %s performs effect %a, which has no default handler.@]"
+        str Printtyp.path p
+  | Toplevel_unknown_effects(ty, str) ->
+      fprintf ppf
+        "@[This %s performs effects %a, which may not have default handlers.@]"
+        str Printtyp.type_expr ty
 
 
 let report_error env ppf err =
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 371d6f420f58..fe7466247bdb 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -19,46 +19,50 @@ open Format
 val is_nonexpansive: Typedtree.expression -> bool
 
 val type_binding:
-        Env.t -> rec_flag ->
-          Parsetree.value_binding list -> type_expr ->
+        Env.t -> effect_expectation -> rec_flag ->
+          Parsetree.value_binding list ->
           Annot.ident option ->
           Typedtree.value_binding list * Env.t
 val type_let:
-        Env.t -> rec_flag ->
-          Parsetree.value_binding list -> type_expr ->
-          Annot.ident option ->
+        Env.t -> effect_expectation -> rec_flag ->
+          Parsetree.value_binding list -> Annot.ident option ->
           Typedtree.value_binding list * Env.t
 val type_expression:
-        Env.t -> Parsetree.expression -> type_expr -> Typedtree.expression
+        Env.t -> effect_expectation ->
+        Parsetree.expression -> Typedtree.expression
 val type_class_arg_pattern:
-        string -> Env.t -> Env.t -> label -> Parsetree.pattern -> type_expr ->
-        Typedtree.pattern * (Ident.t * string loc * Ident.t * type_expr) list *
+        string -> Env.t -> Env.t -> effect_expectation -> label ->
+        Parsetree.pattern ->
+        Typedtree.pattern *
+        (Ident.t * string loc * Ident.t * type_expr) list *
         Env.t * Env.t
 val type_self_pattern:
-        string -> type_expr -> Env.t -> Env.t -> Env.t ->
-        Parsetree.pattern -> type_expr ->
+        string -> type_expr -> Env.t -> Env.t -> Env.t -> effect_expectation ->
+        Parsetree.pattern ->
         Typedtree.pattern *
         (Ident.t * type_expr) Meths.t ref *
         (Ident.t * Asttypes.mutable_flag * Asttypes.virtual_flag * type_expr)
             Vars.t ref *
         Env.t * Env.t * Env.t
 val check_partial:
-        ?lev:int -> Env.t -> type_expr -> type_expr -> type_expr ->
-	Location.t -> Typedtree.case list -> Typedtree.partial * Path.t list
+        ?lev:int -> env:Env.t -> expected_eff:effect_expectation ->
+        cont_ty:type_expr -> type_expr -> Location.t -> Typedtree.case list ->
+        Typedtree.partial * Path.t list
 val type_expect:
         ?in_function:(Location.t * type_expr) ->
-        Env.t -> Parsetree.expression -> type_expr -> type_expr ->
+        Env.t -> effect_expectation -> Parsetree.expression -> type_expr ->
         Typedtree.expression
 val type_exp:
-        Env.t -> Parsetree.expression -> type_expr -> Typedtree.expression
+        Env.t -> effect_expectation ->
+        Parsetree.expression -> Typedtree.expression
 val type_approx:
         Env.t -> Parsetree.expression -> type_expr
 val type_argument:
-        Env.t -> Parsetree.expression -> type_expr ->
-        type_expr -> type_expr -> Typedtree.expression
+        Env.t -> effect_expectation -> Parsetree.expression -> type_expr ->
+        type_expr -> Typedtree.expression
 val type_default_handler:
-        Env.t -> Path.t -> Parsetree.effect_handler ->
-        type_expr -> Typedtree.effect_handler
+        Env.t -> effect_expectation -> Path.t -> Parsetree.effect_handler ->
+        Typedtree.effect_handler
 
 val option_some: Typedtree.expression -> Typedtree.expression
 val option_none: type_expr -> Location.t -> Typedtree.expression
@@ -70,6 +74,8 @@ val force_delayed_checks: unit -> unit
 
 val self_coercion : (Path.t * Location.t list ref) list ref
 
+val check_expectation: Env.t -> effect_expectation -> unit
+
 type error =
     Polymorphic_label of Longident.t
   | Constructor_arity_mismatch of Longident.t * int * int
@@ -127,6 +133,8 @@ type error =
   | Default_handler_mismatch of Path.t * Path.t
   | Default_handler_not_exhaustive
   | Default_handler_nonreturning of Longident.t
+  | Toplevel_no_default_handler of Path.t * string
+  | Toplevel_unknown_effects of type_expr * string
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
@@ -135,7 +143,9 @@ val report_error: Env.t -> formatter -> error -> unit
  (* Deprecated.  Use Location.{error_of_exn, report_error}. *)
 
 (* Forward declaration, to be filled in by Typemod.type_module *)
-val type_module: (Env.t -> Parsetree.module_expr -> Typedtree.module_expr) ref
+val type_module:
+   (Env.t -> effect_expectation ->
+    Parsetree.module_expr -> Typedtree.module_expr) ref
 (* Forward declaration, to be filled in by Typemod.type_open *)
 val type_open:
     (override_flag -> Env.t -> Location.t -> Longident.t loc -> Path.t * Env.t)
@@ -145,8 +155,9 @@ val type_object:
   (Env.t -> Location.t -> Parsetree.class_structure ->
    Typedtree.class_structure * Types.class_signature * string list) ref
 val type_package:
-  (Env.t -> Parsetree.module_expr -> Path.t -> Longident.t list ->
-  type_expr list -> Typedtree.module_expr * type_expr list) ref
+  (Env.t -> effect_expectation -> Parsetree.module_expr -> Path.t ->
+  Longident.t list -> type_expr list ->
+  Typedtree.module_expr * type_expr list) ref
 
 val create_package_type : Location.t -> Env.t ->
   Longident.t * (Longident.t * Parsetree.core_type) list ->
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 3fde8e5cbdb2..f31ba0054ec8 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -1483,13 +1483,15 @@ let transl_effect_decl env funct_body seff =
     match handler with
     | None -> None
     | Some handler ->
-        let eff_expected =
-          Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
-        in
+        Ctype.init_def(Ident.current_time());
+        Ctype.begin_def();
+        let eff_expected = Ctype.new_toplevel_expectation () in
         let handler =
           Typecore.type_default_handler env
-            (Path.Pident id) handler eff_expected
+            eff_expected (Path.Pident id) handler
         in
+        Ctype.end_def ();
+        Typecore.check_expectation env eff_expected;
         Some handler
   in
   transl_effect_infos transl_handler has_handler env funct_body seff
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 71ee52b1f965..33b98d81dcb9 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -39,6 +39,7 @@ type error =
   | Scoping_pack of Longident.t * type_expr
   | Recursive_module_require_explicit_type
   | Apply_generative
+  | Module_effect_clash of (type_expr * type_expr) list
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
@@ -1099,7 +1100,7 @@ let wrap_constraint env arg mty explicit =
 
 (* Type a module value expression *)
 
-let rec type_module ?(alias=false) sttn funct_body anchor env smod =
+let rec type_module ?(alias=false) sttn funct_body anchor env eff smod =
   match smod.pmod_desc with
     Pmod_ident lid ->
       let path =
@@ -1127,7 +1128,7 @@ let rec type_module ?(alias=false) sttn funct_body anchor env smod =
       in rm md
   | Pmod_structure sstr ->
       let (str, sg, finalenv) =
-        type_structure funct_body anchor env sstr smod.pmod_loc in
+        type_structure funct_body anchor eff env sstr smod.pmod_loc in
       let md =
         rm { mod_desc = Tmod_structure str;
              mod_type = Mty_signature sg;
@@ -1145,17 +1146,32 @@ let rec type_module ?(alias=false) sttn funct_body anchor env smod =
       let (id, newenv), funct_body =
         match ty_arg with None -> (Ident.create "*", env), false
         | Some mty -> Env.enter_module ~arg:true name.txt mty env, true in
-      let body = type_module sttn funct_body None newenv sbody in
+      let eff =
+        Expected (Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil)))
+      in
+      let body = type_module sttn funct_body None newenv eff sbody in
       rm { mod_desc = Tmod_functor(id, name, mty, body);
            mod_type = Mty_functor(id, ty_arg, body.mod_type);
            mod_env = env;
            mod_attributes = smod.pmod_attributes;
            mod_loc = smod.pmod_loc }
   | Pmod_apply(sfunct, sarg) ->
-      let arg = type_module true funct_body None env sarg in
+      begin
+        match eff with
+        | Toplevel _ -> ()
+        | Expected eff ->
+            let io =
+              Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
+            in
+            try
+              Ctype.unify env io eff
+            with Ctype.Unify trace ->
+              raise(Error(smod.pmod_loc, env, Module_effect_clash(trace)))
+      end;
+      let arg = type_module true funct_body None env eff sarg in
       let path = path_of_module arg in
       let funct =
-        type_module (sttn && path <> None) funct_body None env sfunct in
+        type_module (sttn && path <> None) funct_body None env eff sfunct in
       begin match Env.scrape_alias env funct.mod_type with
         Mty_functor(param, mty_param, mty_res) as mty_functor ->
           let generative, mty_param =
@@ -1195,7 +1211,7 @@ let rec type_module ?(alias=false) sttn funct_body anchor env smod =
           raise(Error(sfunct.pmod_loc, env, Cannot_apply funct.mod_type))
       end
   | Pmod_constraint(sarg, smty) ->
-      let arg = type_module ~alias true funct_body anchor env sarg in
+      let arg = type_module ~alias true funct_body anchor env eff sarg in
       let mty = transl_modtype env smty in
       rm {(wrap_constraint env arg mty.mty_type (Tmodtype_explicit mty)) with
           mod_loc = smod.pmod_loc;
@@ -1204,10 +1220,7 @@ let rec type_module ?(alias=false) sttn funct_body anchor env smod =
 
   | Pmod_unpack sexp ->
       if !Clflags.principal then Ctype.begin_def ();
-      let eff_expected =
-        Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
-      in
-      let exp = Typecore.type_exp env sexp eff_expected in
+      let exp = Typecore.type_exp env eff sexp in
       if !Clflags.principal then begin
         Ctype.end_def ();
         Ctype.generalize_structure exp.exp_type
@@ -1240,7 +1253,7 @@ let rec type_module ?(alias=false) sttn funct_body anchor env smod =
   | Pmod_extension ext ->
       raise (Error_forward (Typetexp.error_of_extension ext))
 
-and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
+and type_structure ?(toplevel = false) funct_body anchor eff env sstr scope =
   let type_names = ref StringSet.empty
   and effect_names = ref StringSet.empty
   and module_names = ref StringSet.empty
@@ -1249,15 +1262,9 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
   let type_str_item env srem {pstr_loc = loc; pstr_desc = desc} =
     match desc with
     | Pstr_eval (sexpr, attrs) ->
-        let eff_expected =
-          Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
-        in
-        let expr = Typecore.type_expression env sexpr eff_expected in
+        let expr = Typecore.type_expression env eff sexpr in
         Tstr_eval (expr, attrs), [], env
     | Pstr_value(rec_flag, sdefs) ->
-        let eff_expected =
-          Ctype.instance_def (Predef.effect_io (Ctype.newty Tenil))
-        in
         let scope =
           match rec_flag with
           | Recursive ->
@@ -1272,7 +1279,8 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
               Some (Annot.Idef {scope with Location.loc_start = start})
         in
         let (defs, newenv) =
-          Typecore.type_binding env rec_flag sdefs eff_expected scope in
+          Typecore.type_binding env eff rec_flag sdefs scope
+        in
         (* Note: Env.find_value does not trigger the value_used event. Values
            will be marked as being used during the signature inclusion test. *)
         Tstr_value(rec_flag, defs),
@@ -1319,7 +1327,7 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
         check_name "module" module_names name;
         let modl =
           type_module ~alias:true true funct_body
-            (anchor_submodule name.txt anchor) env smodl in
+            (anchor_submodule name.txt anchor) env eff smodl in
         let md =
           { md_type = enrich_module_type anchor name.txt modl.mod_type env;
             md_attributes = attrs;
@@ -1366,7 +1374,7 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
             (fun {md_id=id; md_type=mty} (name, _, smodl, attrs, loc) ->
                let modl =
                  type_module true funct_body (anchor_recmodule id anchor) newenv
-                   smodl in
+                   eff smodl in
                let mty' =
                  enrich_module_type anchor (Ident.name id) modl.mod_type newenv
                in
@@ -1456,7 +1464,7 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
         new_env
     | Pstr_include sincl ->
         let smodl = sincl.pincl_mod in
-        let modl = type_module true funct_body None env smodl in
+        let modl = type_module true funct_body None env eff smodl in
         (* Rename all identifiers bound by this signature to avoid clashes *)
         let sg = Subst.signature Subst.identity
             (extract_sig_open env smodl.pmod_loc modl.mod_type) in
@@ -1525,12 +1533,21 @@ and type_structure ?(toplevel = false) funct_body anchor env sstr scope =
     (Cmt_format.Partial_structure str :: previous_saved_types);
   str, sg, final_env
 
-let type_toplevel_phrase env s =
+let type_phrase toplevel env s =
   Env.reset_required_globals ();
-  type_structure ~toplevel:true false None env s Location.none
+  Ctype.init_def(Ident.current_time());
+  Ctype.begin_def();
+  let eff_expected = Ctype.new_toplevel_expectation () in
+  let (str, sg, finalenv) =
+    type_structure ~toplevel false None eff_expected env s Location.none
+  in
+  Ctype.end_def ();
+  Typecore.check_expectation finalenv eff_expected;
+  (str, sg, finalenv)
+
 (*let type_module_alias = type_module ~alias:true true false None*)
-let type_module = type_module true false None
-let type_structure = type_structure false None
+let type_module env expected_eff md =
+  type_module true false None env expected_eff md
 
 (* Normalize types in a signature *)
 
@@ -1559,7 +1576,8 @@ let type_module_type_of env smod =
              mod_env = env;
              mod_attributes = smod.pmod_attributes;
              mod_loc = smod.pmod_loc }
-    | _ -> type_module env smod in
+    | _ -> type_module env (Expected (Ctype.newvar Seffect)) smod
+  in
   let mty = tmty.mod_type in
   (* PR#6307: expand aliases at root and submodules *)
   let mty = Mtype.remove_aliases env mty in
@@ -1576,14 +1594,14 @@ let rec get_manifest_types = function
       (Ident.name id, ty) :: get_manifest_types rem
   | _ :: rem -> get_manifest_types rem
 
-let type_package env m p nl tl =
+let type_package env expected_eff m p nl tl =
   (* Same as Pexp_letmodule *)
   (* remember original level *)
   let lv = Ctype.get_current_level () in
   Ctype.begin_def ();
   Ident.set_current_time lv;
   let context = Typetexp.narrow () in
-  let modl = type_module env m in
+  let modl = type_module env expected_eff m in
   Ctype.init_def(Ident.current_time());
   Typetexp.widen context;
   let (mp, env) =
@@ -1636,9 +1654,14 @@ let type_implementation sourcefile outputprefix modulename initial_env ast =
     let map = Typetexp.emit_external_warnings in
     ignore (map.Ast_mapper.structure map ast)
   end;
-
+  Ctype.init_def(Ident.current_time());
+  Ctype.begin_def();
+  let eff_expected = Ctype.new_toplevel_expectation () in
   let (str, sg, finalenv) =
-    type_structure initial_env ast (Location.in_file sourcefile) in
+    type_structure false None eff_expected
+      initial_env ast (Location.in_file sourcefile)
+  in
+  Ctype.end_def ();
   let simple_sg = simplify_signature sg in
   if !Clflags.print_types then begin
     Printtyp.wrap_printing_env initial_env
@@ -1658,6 +1681,7 @@ let type_implementation sourcefile outputprefix modulename initial_env ast =
       let coercion =
         Includemod.compunit initial_env sourcefile sg intf_file dclsig in
       Typecore.force_delayed_checks ();
+      Typecore.check_expectation finalenv eff_expected;
       (* It is important to run these checks after the inclusion test above,
          so that value declarations which are not used internally but exported
          are not reported as being unused. *)
@@ -1671,6 +1695,7 @@ let type_implementation sourcefile outputprefix modulename initial_env ast =
         Includemod.compunit initial_env sourcefile sg
                             "(inferred signature)" simple_sg in
       Typecore.force_delayed_checks ();
+      Typecore.check_expectation finalenv eff_expected;
       (* See comment above. Here the target signature contains all
          the value being exported. We can still capture unused
          declarations like "let x = true;; let x = 1;;", because in this
@@ -1771,7 +1796,7 @@ let package_units initial_env objfiles cmifile modulename =
 
 open Printtyp
 
-let report_error ppf = function
+let report_error env ppf = function
     Cannot_apply mty ->
       fprintf ppf
         "@[This module is not a functor; it has type@ %a@]" modtype mty
@@ -1849,9 +1874,15 @@ let report_error ppf = function
       fprintf ppf "Recursive modules require an explicit module type."
   | Apply_generative ->
       fprintf ppf "This is a generative functor. It can only be applied to ()"
+  | Module_effect_clash trace ->
+      report_unification_error ppf env trace
+        (function ppf ->
+           fprintf ppf "This module expression performs effect")
+        (function ppf ->
+           fprintf ppf "but a module expression was expected that performed")
 
 let report_error env ppf err =
-  Printtyp.wrap_printing_env env (fun () -> report_error ppf err)
+  Printtyp.wrap_printing_env env (fun () -> report_error env ppf err)
 
 let () =
   Location.register_error_of_exn
diff --git a/typing/typemod.mli b/typing/typemod.mli
index 9f8e61708690..84db45ec1bef 100644
--- a/typing/typemod.mli
+++ b/typing/typemod.mli
@@ -16,12 +16,10 @@ open Types
 open Format
 
 val type_module:
-        Env.t -> Parsetree.module_expr -> Typedtree.module_expr
-val type_structure:
-        Env.t -> Parsetree.structure -> Location.t ->
-         Typedtree.structure * Types.signature * Env.t
-val type_toplevel_phrase:
-        Env.t -> Parsetree.structure ->
+        Env.t -> effect_expectation ->
+        Parsetree.module_expr -> Typedtree.module_expr
+val type_phrase:
+        bool -> Env.t -> Parsetree.structure ->
          Typedtree.structure * Types.signature * Env.t
 val type_implementation:
   string -> string -> string -> Env.t -> Parsetree.structure ->
@@ -70,6 +68,7 @@ type error =
   | Scoping_pack of Longident.t * type_expr
   | Recursive_module_require_explicit_type
   | Apply_generative
+  | Module_effect_clash of (type_expr * type_expr) list
 
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
diff --git a/typing/types.ml b/typing/types.ml
index 20d71f71f92d..5afd4eccb8cb 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -348,3 +348,9 @@ and ext_status =
     Text_first                     (* first constructor of an extension *)
   | Text_next                      (* not first constructor of an extension *)
   | Text_exception                 (* an exception *)
+
+(* Expected effect *)
+
+type effect_expectation =
+  | Toplevel of (type_expr * Location.t * string) list ref * int
+  | Expected of type_expr
diff --git a/typing/types.mli b/typing/types.mli
index 4b7c814f55ac..d5bdd6e7f8c4 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -338,3 +338,9 @@ and ext_status =
     Text_first                     (* first constructor in an extension *)
   | Text_next                      (* not first constructor in an extension *)
   | Text_exception
+
+(* Expected effect *)
+
+type effect_expectation =
+  | Toplevel of (type_expr * Location.t * string) list ref * int
+  | Expected of type_expr