From b0aa53f2e4526dac152c5ae1bfed7aca193a3465 Mon Sep 17 00:00:00 2001
From: Piotr Polesiuk <ppolesiuk@cs.uni.wroc.pl>
Date: Wed, 7 Aug 2024 13:55:23 +0200
Subject: [PATCH] Return and finally clauses in first class handlers

Return and finally clauses now are attached to first class handlers,
making possible to define more intuitive first class handlers for e.g.
state or backtracking. The delimiter's type and effect are not visible
in the type of first-class-handlers, therefore, the dynamic labels of
handlers do not work.
---
 src/DblParser/Desugar.ml              |  70 ++++---------
 src/DblParser/Raw.ml                  |   4 +-
 src/DblParser/YaccParser.mly          |   7 +-
 src/Lang/Surface.ml                   |  32 ++----
 src/Lang/Unif.ml                      |  25 +++--
 src/Lang/Unif.mli                     |  77 ++++++++------
 src/Lang/UnifPriv/Subst.ml            |   9 +-
 src/Lang/UnifPriv/Type.ml             |  41 ++++++--
 src/Lang/UnifPriv/TypeBase.ml         |  10 +-
 src/Lang/UnifPriv/TypeBase.mli        |   4 +-
 src/Lang/UnifPriv/TypeWhnf.ml         |   5 +-
 src/ToCore/Main.ml                    |  49 +++++----
 src/ToCore/Type.ml                    |  21 ++--
 src/TypeInference/Def.ml              | 142 ++++++--------------------
 src/TypeInference/Error.ml            |  24 +++++
 src/TypeInference/Error.mli           |   7 ++
 src/TypeInference/Expr.ml             |  86 +++++++++++++---
 src/TypeInference/MatchClause.ml      |  61 +++++------
 src/TypeInference/MatchClause.mli     |  51 ++++-----
 src/TypeInference/Pretty.ml           |  27 +++--
 src/TypeInference/Unification.ml      |  58 +++++++----
 src/TypeInference/Unification.mli     |   2 +-
 test/ok/ok0053_firstClassHandler.fram |   2 +-
 test/ok/ok0054_firstClassHandler.fram |   2 +-
 test/ok/ok0055_complexHandlers.fram   |  14 ++-
 test/ok/ok0056_complexHandlers.fram   |  16 +--
 test/ok/ok0057_dataArgLabels.fram     |  16 +--
 test/ok/ok0059_effectArg.fram         |   2 +-
 test/ok/ok0077_effectResume.fram      |   2 +-
 29 files changed, 447 insertions(+), 419 deletions(-)

diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml
index 0605e6e..37846f7 100644
--- a/src/DblParser/Desugar.ml
+++ b/src/DblParser/Desugar.ml
@@ -542,7 +542,10 @@ and tr_expr (e : Raw.expr) =
     tr_expr_app (tr_expr e1) es
   | EDefs(defs, e) -> make (EDefs(tr_defs defs, tr_expr e))
   | EMatch(e, cls) -> make (EMatch(tr_expr e, List.map tr_match_clause cls))
-  | EHandler h     -> make (EHandler (tr_expr h))
+  | EHandler(h, hcs) ->
+    let e = tr_expr h in
+    let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
+    make (EHandler(e, rcs, fcs))
   | EEffect(es, rp_opt, e) ->
     let (pos, rp) =
       match rp_opt with
@@ -728,18 +731,20 @@ and tr_def ?(public=false) (def : Raw.def) =
     ]
   | DLabel(pub, pat) ->
     let public = public || pub in
-    let (eff_opt, pat) = tr_label_pattern ~public pat in
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
     [ make (DLabel (eff_opt, pat)) ]
-  | DHandle(pub, pat, h, hcs) ->
+  | DHandle(pub, pat, body, hcs) ->
     let public = public || pub in
-    let (lbl_opt, eff_opt, pat)  = tr_handle_pattern ~public pat in
-    let body = { h with data = EHandler(tr_expr h) } in
-    [ make_handle ~pos:def.pos lbl_opt eff_opt pat body hcs ]
-  | DHandleWith(pub, pat, e, hcs) ->
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let body = tr_expr body in
+    let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
+    let body = { body with data = EHandler(body, rcs, fcs) } in
+    [ make (DHandlePat(eff_opt, pat, body)) ]
+  | DHandleWith(pub, pat, body) ->
     let public = public || pub in
-    let (lbl_opt, eff_opt, pat)  = tr_handle_pattern ~public pat in
-    let body = tr_expr e in
-    [ make_handle ~pos:def.pos lbl_opt eff_opt pat body hcs ]
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let body = tr_expr body in
+    [ make (DHandlePat(eff_opt, pat, body)) ]
   | DModule(pub, x, defs) ->
     let public = public || pub in
     [ make (DModule(public, x, tr_defs defs)) ]
@@ -765,42 +770,17 @@ and tr_pattern_with_fields ~public (pat : Raw.expr) =
   | _ ->
     (None, tr_pattern ~public pat)
 
-and tr_label_pattern ~public (pat : Raw.expr) =
+and tr_pattern_with_eff_opt ~public (pat : Raw.expr) =
   let (flds_opt, pat) = tr_pattern_with_fields ~public pat in
-  (Option.map (tr_label_fields ~public) flds_opt, pat)
+  (Option.map (tr_eff_opt_fields ~public) flds_opt, pat)
 
-and tr_handle_pattern ~public (pat : Raw.expr) =
-  let (flds_opt, pat) = tr_pattern_with_fields ~public pat in
-  match flds_opt with
-  | Some flds ->
-    let (lbl_opt, eff_opt) = tr_handle_fields ~public flds in
-    (lbl_opt, eff_opt, pat)
-  | None -> (None, None, pat)
-
-and tr_label_fields ~public flds =
+and tr_eff_opt_fields ~public flds =
   match flds with
   | [] -> assert false
   | [{ data = FldEffectVal tp; _ }] -> tr_type_arg ~public tp
   | { data = FldEffectVal _; _} :: fld :: _ | fld :: _ ->
     Error.fatal (Error.desugar_error fld.pos)
 
-and tr_handle_fields ~public flds =
-  match flds with
-  | [] -> assert false
-  | [{ data = FldNameVal(NLabel, e); _ }] ->
-    (Some (tr_expr e), None)
-  | [{ data = FldEffectVal eff; _ }] ->
-    (None, Some (tr_type_arg ~public eff))
-  | [{ data = FldNameVal(NLabel, e); _ }; { data = FldEffectVal eff; _ }]
-  | [{ data = FldEffectVal eff; _ }; { data = FldNameVal(NLabel, e); _ }] ->
-    (Some (tr_expr e), Some (tr_type_arg ~public eff))
-  | { data=FldNameVal(NLabel, _); _} :: { data=FldEffectVal _; _ } :: fld :: _
-  | { data=FldEffectVal _; _ } :: { data=FldNameVal(NLabel, _); _} :: fld :: _
-  | { data=FldNameVal(NLabel, _); _} :: fld :: _
-  | { data=FldEffectVal _; _ } :: fld :: _
-  | fld :: _ ->
-    Error.fatal (Error.desugar_error fld.pos)
-
 and tr_h_clause (hc : Raw.h_clause) =
   let make data = { hc with data = data } in
   match hc.data with
@@ -809,19 +789,7 @@ and tr_h_clause (hc : Raw.h_clause) =
   | HCFinally(pat, body) ->
     Either.Right (make (Clause(tr_pattern ~public:false pat, tr_expr body)))
 
-and make_handle ~pos lbl_opt eff_opt pat body hcs =
-  let make data = { pos; data } in
-  let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
-  make (DHandlePat
-    { label       = lbl_opt;
-      effect      = eff_opt;
-      cap_pat     = pat;
-      capability  = body;
-      ret_clauses = rcs;
-      fin_clauses = fcs
-    })
-
-(** Returns: list of explicit type adnotations with fresh type variable names
+(** Returns: list of explicit type annotations with fresh type variable names
     and a function that given a field name returns piece of code that
     represents pattern which pulls out this variable, making it easy to use in
     generated code *)
diff --git a/src/DblParser/Raw.ml b/src/DblParser/Raw.ml
index 7f6ac57..b52d690 100644
--- a/src/DblParser/Raw.ml
+++ b/src/DblParser/Raw.ml
@@ -195,7 +195,7 @@ and expr_data =
   | EMatch of expr * match_clause list
     (** Pattern-matching *)
 
-  | EHandler of expr
+  | EHandler of expr * h_clause list
     (** First-class handler *)
 
   | EEffect of expr list * expr option * expr
@@ -264,7 +264,7 @@ and def_data =
   | DHandle of is_public * expr * expr * h_clause list
     (** Effect handler *)
 
-  | DHandleWith of is_public * expr * expr * h_clause list
+  | DHandleWith of is_public * expr * expr
     (** Effect handler, with first-class handler *)
 
   | DMethod of is_public * expr * expr
diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly
index ef14961..8381aa9 100644
--- a/src/DblParser/YaccParser.mly
+++ b/src/DblParser/YaccParser.mly
@@ -263,7 +263,6 @@ expr
 | KW_FN expr_250_list1 ARROW2 expr { make (EFn($2, $4))   }
 | KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr
     { make (EEffect($2, $3, $5)) }
-| KW_HANDLER expr { make (EHandler $2) }
 | expr_0 { $1 }
 ;
 
@@ -272,7 +271,6 @@ expr_no_comma
 | KW_FN expr_250_list1 ARROW2 expr_no_comma { make (EFn($2, $4))   }
 | KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr_no_comma
     { make (EEffect($2, $3, $5)) }
-| KW_HANDLER expr_no_comma { make (EHandler $2) }
 | expr_0_no_comma { $1 }
 ;
 
@@ -454,6 +452,7 @@ expr_simple
 | KW_MATCH expr KW_WITH KW_END   { make (EMatch($2, [])) }
 | KW_MATCH expr KW_WITH bar_opt match_clause_list KW_END
   { make (EMatch($2, $5)) }
+| KW_HANDLER expr h_clauses KW_END { make (EHandler($2, $3)) }
 | CBR_OPN field_list CBR_CLS { make (ERecord $2) }
 | BR_OPN op BR_CLS           { make (EBOpID ($2).data)}
 | BR_OPN op DOT BR_CLS       { make (EUOpID ($2).data)}
@@ -523,8 +522,8 @@ def
 | pub KW_LABEL rec_opt expr_70 { make_def $3 (DLabel($1, $4)) }
 | pub KW_HANDLE rec_opt expr_70 EQ expr h_clauses
     { make_def $3 (DHandle($1, $4, $6, $7)) }
-| pub KW_HANDLE rec_opt expr_70 KW_WITH expr h_clauses
-    { make_def $3 (DHandleWith($1, $4, $6, $7)) }
+| pub KW_HANDLE rec_opt expr_70 KW_WITH expr
+    { make_def $3 (DHandleWith($1, $4, $6)) }
 | pub KW_METHOD rec_opt expr_70 EQ expr { make_def $3 (DMethod($1, $4, $6)) }
 | pub KW_METHOD KW_FN var_id { make (DMethodFn($1, $4, $4)) }
 | pub KW_METHOD KW_FN var_id EQ var_id { make (DMethodFn($1, $4, $6)) }
diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml
index d01f0d6..ad73439 100644
--- a/src/Lang/Surface.ml
+++ b/src/Lang/Surface.ml
@@ -226,8 +226,9 @@ and expr_data =
   | EMatch of expr * match_clause list
     (** Pattern-matching *)
 
-  | EHandler of expr
-    (** First-class handler *)
+  | EHandler of expr * match_clause list * match_clause list
+    (** First-class handler, with return and finally clauses. For each of these
+      clause list, empty list means the default identity clause *)
 
   | EEffect of arg * expr
     (** Effectful operation. The only argument is a continuation. Other
@@ -266,26 +267,13 @@ and def_data =
     (** Creating a new label. Optional type argument binds newly created
       effect. *)
 
-  | DHandlePat of (* Effect handler combined with pattern matching *)
-    { label   : expr option;
-      (** Effect label of the handled effect. [None] means that handler is
-        lexical and generates its own label. *)
-
-      effect : type_arg option;
-      (** Optional name for the handled effect *)
-
-      cap_pat : pattern;
-      (** Pattern matched against the effect capability *)
-
-      capability : expr;
-      (** An expression providing capability to this handler *)
-
-      ret_clauses : match_clause list;
-      (** List of return clauses. Empty list means the default clause. *)
-
-      fin_clauses : match_clause list
-      (** List of finally clauses. Empty list means the default clause. *)
-    }
+  | DHandlePat of type_arg option * pattern * expr
+    (** Effect handler combined with pattern matching. In
+      [DHandlePat(eff, pat, body)] the meaning of parameters is the following.
+      - [eff]  -- Optional name for the handled effect.
+      - [pat]  -- Pattern matched against the effect capability.
+      - [body] -- An expression that should evaluate to fist class handler,
+          providing the capability of the handled effect. *)
 
   | DImplicit of iname * named_type_arg list * scheme_expr
     (** Declaration of implicit. The second parameter is a list of types
diff --git a/src/Lang/Unif.ml b/src/Lang/Unif.ml
index 430cb7c..781f9d2 100644
--- a/src/Lang/Unif.ml
+++ b/src/Lang/Unif.ml
@@ -96,17 +96,20 @@ and expr_data =
   | EData       of data_def list * expr
   | EMatchEmpty of expr * expr * typ * effrow
   | EMatch      of expr * match_clause list * typ * effrow
-  | EHandle     of
-    { label      : expr;
-      effect     : effect;
-      cap_var    : var;
-      body       : expr;
-      capability : expr;
-      ret_var    : var;
-      ret_body   : expr;
-      result_tp  : typ;
-      result_eff : effrow }
-  | EHandler    of tvar * var * typ * effrow * expr
+  | EHandle     of tvar * var * typ * expr * expr
+  | EHandler    of
+    { label     : var;
+      effect    : tvar;
+      delim_tp  : typ;
+      delim_eff : effect;
+      cap_type  : typ;
+      cap_body  : expr;
+      ret_var   : var;
+      body_tp   : typ;
+      ret_body  : expr;
+      fin_var   : var;
+      fin_body  : expr;
+    }
   | EEffect     of expr * var * expr * typ
   | EExtern     of string * typ
   | ERepl       of (unit -> expr) * typ * effrow
diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli
index 4933558..ea06874 100644
--- a/src/Lang/Unif.mli
+++ b/src/Lang/Unif.mli
@@ -208,44 +208,51 @@ and expr_data =
   | EMatch of expr * match_clause list * typ * effrow
     (** Pattern-matching. It stores type and effect of the whole expression. *)
 
-  | EHandle of (** Handler *)
-    { label : expr;
-      (** Label of the handler *)
+  | EHandle of tvar * var * typ * expr * expr
+    (** Handling construct. In [EHandle(a, x, tp, e1, e2)] the meaning of
+      parameters is the following.
+      - [a]  -- effect variable that represent introduced effect
+      - [x]  -- capability variable
+      - [tp] -- type of the capability
+      - [e1] -- expression that should evaluate to first-class handler
+      - [e2] -- body of the handler *)
+
+  | EHandler of (** First class handler *)
+    { label     : var;
+      (** Variable, that binds the runtime-label *)
+
+      effect    : tvar;
+      (** Effect variable *)
 
-      effect : effect;
-      (** Effect handled by the label *)
+      delim_tp  : typ;
+      (** Type of the delimiter *)
 
-      cap_var : var;
-      (** Variable that binds effect capability *)
+      delim_eff : effect;
+      (** Effect of the delimiter *)
 
-      body : expr;
-      (** Handled expression *)
+      cap_type  : typ;
+      (** Type of the capability *)
 
-      capability : expr;
-      (** An expression providing capability to this handler *)
+      cap_body  : expr;
+      (** An expression that should evaluate to effect capability. It can use
+        [label] and [effect]. It should be pure and have type [cap_type]. *)
 
-      ret_var : var;
+      ret_var   : var;
       (** An argument to the return clause *)
 
-      ret_body : expr;
-      (** A body of the return clause *)
+      body_tp   : typ;
+      (** Type of the handled expression. It is also a type of an argument
+        [ret_var] to the return clause *)
 
-      result_tp : typ;
-      (** The type of the whole handler *)
+      ret_body  : expr;
+      (** Body of the return clause *)
 
-      result_eff : effrow }
-      (** The effect of the whole handler *)
+      fin_var   : var;
+      (** An argument to the finally clause. It has type [delim_tp] *)
 
-  | EHandler of tvar * var * typ * effrow * expr
-    (** First-class handler. In [EHandler(a, lx, tp, eff, h)] the meaning of
-      parameter is the following:
-      - [a] -- binder of an effect variable (of kind [effect]). The variable
-        is bound in other arguments of [EHandler] expression.
-      - [lx] -- label variable bound by the handler. Its type should be
-        [TLabel(Effect.singleton a, tp, eff)].
-      - [tp] -- type of the delimiter ([EHandle]).
-      - [eff] -- effect of the delimiter.
-      - [h] -- body of the handler. *)
+      fin_body  : expr;
+      (** Body of the finally clause *)
+    }
 
   | EEffect of expr * var * expr * typ
     (** Capability of effectful functional operation. It stores dynamic label,
@@ -500,11 +507,13 @@ module Type : sig
     | TArrow of scheme * typ * effrow
       (** Impure arrow *)
   
-    | THandler of tvar * typ * typ * effrow
-      (** First class handler. In [THandler(a, tp, tp0, eff0)]:
-        - [a] is a variable bound in [tp], [tp0], and [eff0];
+    | THandler of tvar * typ * typ * effrow * typ * effect
+      (** First class handler. In [THandler(a, tp, itp, ieff, otp, oeff)]:
+        - [a] is a variable bound in [tp], [itp], and [ieff];
         - [tp] is a type of provided capability;
-        - [tp0] and [eff0] are type and effects of the whole delimiter. *)
+        - [itp] and [ieff] are type and effects of handled expression.
+          The variable [a] in [ieff] can be omitted.
+        - [otp] and [oeff] are type and effects of the whole handler. *)
   
     | TLabel of effect * typ * effrow
       (** Type of first-class label. It stores the effect of the label and
@@ -538,7 +547,7 @@ module Type : sig
     | Whnf_Arrow of scheme * typ * effrow
       (** Impure arrow *)
   
-    | Whnf_Handler of tvar * typ * typ * effrow
+    | Whnf_Handler   of tvar * typ * typ * effrow * typ * effrow
       (** Handler type *)
 
     | Whnf_Label of effect * typ * effrow
@@ -563,7 +572,7 @@ module Type : sig
   val t_arrow : scheme -> typ -> effrow -> typ
 
   (** Type of first-class handlers *)
-  val t_handler : tvar -> typ -> typ -> effrow -> typ
+  val t_handler : tvar -> typ -> typ -> effrow -> typ -> effrow -> typ
 
   (** Type of first-class label *)
   val t_label : effect -> typ -> effrow -> typ
diff --git a/src/Lang/UnifPriv/Subst.ml b/src/Lang/UnifPriv/Subst.ml
index baf4e58..af88fd1 100644
--- a/src/Lang/UnifPriv/Subst.ml
+++ b/src/Lang/UnifPriv/Subst.ml
@@ -98,10 +98,15 @@ and in_type_rec sub tp =
     t_pure_arrow (in_scheme_rec sub sch) (in_type_rec sub tp2)
   | TArrow(sch, tp2, eff) ->
     t_arrow (in_scheme_rec sub sch) (in_type_rec sub tp2) (in_type_rec sub eff)
-  | THandler(a, tp, tp0, eff0) ->
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    let otp  = in_type_rec sub otp in
+    let oeff = in_type_rec sub oeff in
     let (sub, a) = add_tvar sub a in
     t_handler a (in_type_rec sub tp)
-      (in_type_rec sub tp0) (in_type_rec sub eff0)
+      (in_type_rec sub itp)
+      (in_type_rec sub ieff)
+      otp
+      oeff
   | TLabel(eff, tp0, eff0) ->
     t_label (in_type_rec sub eff) (in_type_rec sub tp0) (in_type_rec sub eff0)
   | TApp(tp1, tp2) ->
diff --git a/src/Lang/UnifPriv/Type.ml b/src/Lang/UnifPriv/Type.ml
index ff6210c..fcf325b 100644
--- a/src/Lang/UnifPriv/Type.ml
+++ b/src/Lang/UnifPriv/Type.ml
@@ -56,8 +56,15 @@ let rec open_down ~scope tp =
     t_pure_arrow (open_scheme_up ~scope sch) (open_down ~scope tp2)
   | TArrow(sch, tp2, eff) ->
     t_arrow (open_scheme_up ~scope sch) (open_down ~scope tp2) eff
-  | THandler(a, tp, tp0, eff0) ->
-    t_handler a (open_down ~scope:(Scope.add scope a) tp) tp0 eff0
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    let otp  = open_down ~scope otp in
+    let scope = Scope.add scope a in
+    t_handler a
+      (open_down ~scope tp)
+      (open_up   ~scope itp)
+      (open_effrow_up ~scope ieff)
+      otp
+      oeff
 
   | TEffect _ | TEffrow _ ->
     failwith "Internal kind error"
@@ -82,8 +89,11 @@ and open_up ~scope tp =
       (open_scheme_down ~scope sch)
       (open_up          ~scope tp2)
       (open_effrow_up   ~scope eff)
-  | THandler(a, tp, tp0, eff0) ->
-    t_handler a (open_up ~scope:(Scope.add scope a) tp) tp0 eff0
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    let otp  = open_up ~scope otp in
+    let oeff = open_effrow_up ~scope oeff in
+    let scope = Scope.add scope a in
+    t_handler a (open_up ~scope tp) (open_down ~scope itp) ieff otp oeff
 
   | TEffect _ | TEffrow _ ->
     failwith "Internal kind error"
@@ -106,8 +116,10 @@ let rec contains_uvar u tp =
     scheme_contains_uvar u sch || contains_uvar u tp2
   | TArrow(sch, tp2, eff) ->
     scheme_contains_uvar u sch || contains_uvar u tp2 || contains_uvar u eff
-  | THandler(_, tp, tp0, eff0) ->
-    contains_uvar u tp || contains_uvar u tp0 || contains_uvar u eff0
+  | THandler(_, tp, itp, ieff, otp, oeff) ->
+    contains_uvar u tp ||
+    contains_uvar u itp || contains_uvar u ieff ||
+    contains_uvar u otp || contains_uvar u oeff
   | TLabel(eff, tp0, eff0) ->
     contains_uvar u eff || contains_uvar u tp0 || contains_uvar u eff0
   | TEffrow(_, EEApp(tp1, tp2)) | TApp(tp1, tp2) ->
@@ -127,8 +139,13 @@ let rec collect_uvars tp uvs =
     collect_scheme_uvars sch (collect_uvars tp2 uvs)
   | TArrow(sch, tp2, eff) ->
     collect_scheme_uvars sch (collect_uvars tp2 (collect_uvars eff uvs))
-  | THandler(_, tp, tp0, eff0) ->
-    collect_uvars tp (collect_uvars tp0 (collect_uvars eff0 uvs))
+  | THandler(_, tp, itp, ieff, otp, oeff) ->
+    uvs
+    |> collect_uvars tp
+    |> collect_uvars itp
+    |> collect_uvars ieff
+    |> collect_uvars otp
+    |> collect_uvars oeff
   | TLabel(eff, tp0, eff0) ->
     collect_uvars eff (collect_uvars tp0 (collect_uvars eff0 uvs))
 
@@ -188,11 +205,13 @@ and shrink_scope ~scope tp =
     shrink_scheme_scope ~scope sch;
     shrink_scope ~scope tp2;
     shrink_scope ~scope eff
-  | THandler(a, tp, tp0, eff0) ->
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    shrink_scope ~scope otp;
+    shrink_scope ~scope oeff;
     let scope = Scope.add scope a in
     shrink_scope ~scope tp;
-    shrink_scope ~scope tp0;
-    shrink_scope ~scope eff0
+    shrink_scope ~scope itp;
+    shrink_scope ~scope ieff
   | TLabel(eff, tp0, eff0) ->
     shrink_scope ~scope eff;
     shrink_scope ~scope tp0;
diff --git a/src/Lang/UnifPriv/TypeBase.ml b/src/Lang/UnifPriv/TypeBase.ml
index effc034..a8a3344 100644
--- a/src/Lang/UnifPriv/TypeBase.ml
+++ b/src/Lang/UnifPriv/TypeBase.ml
@@ -43,7 +43,7 @@ and type_view =
   | TEffrow    of TVar.Set.t * effrow_end
   | TPureArrow of scheme * typ
   | TArrow     of scheme * typ * effrow
-  | THandler   of tvar * typ * typ * effrow
+  | THandler   of tvar * typ * typ * effrow * typ * effrow
   | TLabel     of effect * typ * effrow
   | TApp       of typ * typ
 
@@ -82,7 +82,7 @@ let t_pure_arrow sch tp2 = TPureArrow(sch, tp2)
 
 let t_arrow sch tp2 eff = TArrow(sch, tp2, eff)
 
-let t_handler a tp tp0 eff0 = THandler(a, tp, tp0, eff0)
+let t_handler a tp itp ieff otp oeff = THandler(a, tp, itp, ieff, otp, oeff)
 
 let t_label eff tp0 eff0 = TLabel(eff, tp0, eff0)
 
@@ -139,9 +139,9 @@ and perm_rec p tp =
     TPureArrow(perm_scheme_rec p sch, perm_rec p tp2)
   | TArrow(sch, tp2, eff) ->
     TArrow(perm_scheme_rec p sch, perm_rec p tp2, perm_rec p eff)
-  | THandler(a, tp, tp0, eff0) ->
-    THandler(TVar.Perm.apply p a,
-      perm_rec p tp, perm_rec p tp0, perm_rec p eff0)
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    THandler(TVar.Perm.apply p a, perm_rec p tp,
+      perm_rec p itp, perm_rec p ieff, perm_rec p otp, perm_rec p oeff)
   | TLabel(eff, tp0, eff0) ->
     TLabel(perm_rec p tp, perm_rec p tp0, perm_rec p eff0)
   | TApp(tp1, tp2) ->
diff --git a/src/Lang/UnifPriv/TypeBase.mli b/src/Lang/UnifPriv/TypeBase.mli
index 2c6848f..bcbe627 100644
--- a/src/Lang/UnifPriv/TypeBase.mli
+++ b/src/Lang/UnifPriv/TypeBase.mli
@@ -41,7 +41,7 @@ type type_view =
   | TEffrow    of TVar.Set.t * effrow_end
   | TPureArrow of scheme * typ
   | TArrow     of scheme * typ * effrow
-  | THandler   of tvar * typ * typ * effrow
+  | THandler   of tvar * typ * typ * effrow * typ * effrow
   | TLabel     of effect * typ * effrow
   | TApp       of typ * typ
 
@@ -73,7 +73,7 @@ val t_pure_arrow : scheme -> typ -> typ
 val t_arrow : scheme -> typ -> effrow -> typ
 
 (** Type of first-class handlers *)
-val t_handler : tvar -> typ -> typ -> effrow -> typ
+val t_handler : tvar -> typ -> typ -> effrow -> typ -> effrow -> typ
 
 (** Type of first-class label *)
 val t_label : effect -> typ -> effrow -> typ
diff --git a/src/Lang/UnifPriv/TypeWhnf.ml b/src/Lang/UnifPriv/TypeWhnf.ml
index adb20a3..8620704 100644
--- a/src/Lang/UnifPriv/TypeWhnf.ml
+++ b/src/Lang/UnifPriv/TypeWhnf.ml
@@ -17,7 +17,7 @@ type whnf =
   | Whnf_Effrow    of effrow
   | Whnf_PureArrow of scheme * typ
   | Whnf_Arrow     of scheme * typ * effrow
-  | Whnf_Handler   of tvar * typ * typ * effrow
+  | Whnf_Handler   of tvar * typ * typ * effrow * typ * effrow
   | Whnf_Label     of effect * typ * effrow
 
 let rec whnf tp =
@@ -28,7 +28,8 @@ let rec whnf tp =
   | TEffrow _   -> Whnf_Effrow tp
   | TPureArrow(sch, tp) -> Whnf_PureArrow(sch, tp)
   | TArrow(sch, tp, eff) -> Whnf_Arrow(sch, tp, eff)
-  | THandler(a, tp, tp0, eff0) -> Whnf_Handler(a, tp, tp0, eff0)
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    Whnf_Handler(a, tp, itp, ieff, otp, oeff)
   | TLabel(eff, tp0, eff0)     -> Whnf_Label(eff, tp0, eff0)
   | TApp(tp1, tp2) ->
     begin match whnf tp1 with
diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml
index d50e4f6..2d01ee5 100644
--- a/src/ToCore/Main.ml
+++ b/src/ToCore/Main.ml
@@ -47,16 +47,11 @@ let rec tr_expr env (e : S.expr) =
     tr_expr_v env me (fun v ->
     PatternMatch.tr_single_match ~pos:e.pos ~env ~tr_expr v cls tp eff)
 
-  | EHandle { label; effect; cap_var; body; capability;
-      ret_var; ret_body; result_tp; result_eff } ->
-    tr_expr_v env label (fun lv ->
-    tr_expr_v env capability (fun hv ->
-    let h_eff = Type.tr_effect env effect in
-    let hx  = Var.fresh () in
-    let r_body = tr_expr env ret_body in
-    T.ELet(hx, T.ETApp(hv, h_eff),
-      T.ELet(cap_var, T.EApp(T.VVar hx, lv),
-        T.EReset(lv, [], [], tr_expr env body, ret_var, r_body)))))
+  | EHandle(a, x, tp, e1, e2) ->
+    tr_expr_v env e1 (fun v1 ->
+    let (env, Ex a) = Env.add_tvar env a in
+    let tp = Type.tr_ttype env tp in
+    T.EApp(v1, T.VTFun(a, T.EValue (T.VFn(x, tp, tr_expr env e2)))))
 
   | EEffect(l, x, body, tp) ->
     tr_expr_v env l (fun lv ->
@@ -118,20 +113,36 @@ and tr_expr_v env (e : S.expr) cont =
     let (env, dds) = DataType.tr_data_defs env dds in
     T.EData(dds, tr_expr_v env e cont)
 
-  | EHandler(a, lx, tp, eff, h) ->
-    let (env, Ex a) = Env.add_tvar env a in
+  | EHandler h ->
+    let (env, Ex a) = Env.add_tvar env h.effect in
     begin match T.TVar.kind a with
     | KEffect ->
-      let tp  = Type.tr_ttype  env tp in
-      let eff = Type.tr_effect env eff in
-      let lbl_tp = T.TLabel
-        { effect    = TVar a;
+      let delim_tp  = Type.tr_ttype env h.delim_tp in
+      let delim_eff = Type.tr_effect env h.delim_eff in
+      let cap_tp    = Type.tr_ttype env h.cap_type in
+      let body_tp   = Type.tr_ttype env h.body_tp in
+      let comp_x    = Var.fresh () in (* a parameter to handler: computation *)
+      let comp_y    = Var.fresh () in (* partially applied computation *)
+      let comp_eff  = T.Effect.join (TVar a) delim_eff in
+      let comp_tp   =
+        T.TForall(a, T.TArrow(cap_tp, body_tp, comp_eff)) in
+      let label_def = T.DD_Label
+        { tvar      = a;
+          var       = h.label;
           tvars     = [];
           val_types = [];
-          delim_tp  = tp;
-          delim_eff = eff
+          delim_tp  = delim_tp;
+          delim_eff = delim_eff;
         } in
-      cont (T.VTFun(a, T.EValue(T.VFn(lx, lbl_tp, tr_expr env h))))
+      cont (VFn(comp_x, comp_tp,
+        T.EData([label_def],
+        T.ELet(h.fin_var,
+          T.EReset(T.VVar h.label, [], [],
+            tr_expr_v env h.cap_body (fun cap_v ->
+            T.ELetPure(comp_y, T.ETApp(T.VVar comp_x, T.TVar a),
+            T.EApp(T.VVar comp_y, cap_v))),
+            h.ret_var, tr_expr env h.ret_body),
+          tr_expr env h.fin_body))))
     | _ ->
       failwith "Internal kind error"
     end
diff --git a/src/ToCore/Type.ml b/src/ToCore/Type.ml
index 10bc32c..d0205c2 100644
--- a/src/ToCore/Type.ml
+++ b/src/ToCore/Type.ml
@@ -71,22 +71,19 @@ and tr_type env tp =
     T.Type.Ex (TArrow(tr_scheme env sch, tr_ttype env tp2, TEffPure))
   | TArrow(sch, tp2, eff) ->
     T.Type.Ex (TArrow(tr_scheme env sch, tr_ttype env tp2, tr_effect env eff))
-  | THandler(x, tp, tp0, eff0) ->
+  | THandler(x, tp, itp, ieff, otp, oeff) ->
+    let otp  = tr_ttype env otp in
+    let oeff = tr_effect env oeff in
     let (env, Ex x) = Env.add_tvar env x in
     begin match T.TVar.kind x with
     | KEffect ->
       let tp   = tr_ttype env tp in
-      let tp0  = tr_ttype env tp0 in
-      let eff0 = tr_effect env eff0 in
-      T.Type.Ex (TForall(x,
-        TArrow(TLabel
-          { effect    = TVar x;
-            tvars     = [];
-            val_types = [];
-            delim_tp  = tp0;
-            delim_eff = eff0
-          }, tp, TEffPure)))
-    | _ ->
+      let itp  = tr_ttype env itp in
+      let ieff = tr_effect env ieff in
+      T.Type.Ex (TArrow(
+        TForall(x, TArrow(tp, itp, T.Effect.join (TVar x) ieff)),
+        otp, oeff))
+    | KType | KArrow _ ->
       failwith "Internal kind error"
     end
   | TLabel(eff, tp0, eff0) ->
diff --git a/src/TypeInference/Def.ml b/src/TypeInference/Def.ml
index 30900d7..94644ab 100644
--- a/src/TypeInference/Def.ml
+++ b/src/TypeInference/Def.ml
@@ -180,120 +180,46 @@ let check_def : type dir. tcfix:tcfix ->
         [(pat, e2)], res_tp, eff))))),
       resp, Impure)
 
-  | DHandlePat
-    { label; effect = eff_opt; cap_pat = pat; capability = eh;
-      ret_clauses = rcs; fin_clauses = fcs } ->
+  | DHandlePat(eff_opt, pat, e1) ->
     let env0 = env in
-    let (lbl, env) =
-      match label with
-      | None ->
-        let (env, l_eff) = Env.add_the_effect env in
-        let env =
-          Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var l_eff) in
-        let tp0  = Env.fresh_uvar env T.Kind.k_type in
-        let eff0 = Env.fresh_uvar env T.Kind.k_effrow in
-        let (env, x) = Env.add_the_label env (T.Type.t_var l_eff) tp0 eff0 in
-        let ctx e =
-          let dd = T.DD_Label {
-              tvar = l_eff; var = x;
-              delim_tp = tp0; delim_eff = eff0
-            } in
-          { T.pos  = Position.join def.pos e.T.pos;
-            T.data = T.EData([dd], e)
-          }
-        in
-        { l_expr      = { T.pos = def.pos; T.data = T.EVar x };
-          l_ctx       = ctx;
-          l_eff       = T.Type.t_var l_eff;
-          l_sub       =
-            (* It might be tempting to use [T.Subst.rename_to_fresh] here, but
-              we cannot ensure that this freshly generated type variable do
-              not appear in component of the handler type (and it is easy to
-              find counter-example). However, for monomorphic handlers it
-              could be done better. *)
-            (fun a ->
-              if is_monomorphic_var env eh then
-                T.Subst.rename_to_fresh T.Subst.empty a l_eff
-              else
-                T.Subst.add_type T.Subst.empty a (T.Type.t_var l_eff));
-          l_delim_tp  = tp0;
-          l_delim_eff = eff0
-        }, env
-      | Some le ->
-        let (env', ims) = ImplicitEnv.begin_generalize env ienv in
-        let (le, le_tp, _) = infer_expr_type env' le eff in
-        ImplicitEnv.end_generalize_impure ~env:env' ~pos:le.pos ims le_tp;
-        begin match Unification.as_label env le_tp with
-        | L_Label(l_eff, tp0, eff0) ->
-          let env = Type.check_type_alias_binder_opt env eff_opt l_eff in
-          let env = Env.add_the_effect_alias env l_eff in
-          let (env, l_var) = Env.add_the_label env l_eff tp0 eff0 in
-          let ctx e =
-            { T.pos  = Position.join def.pos e.T.pos;
-              T.data = T.ELet(l_var, T.Scheme.of_type le_tp, le, e)
-            } in
-          { l_expr      = { le with data = T.EVar l_var };
-            l_ctx       = ctx;
-            l_eff       = l_eff;
-            l_sub       = (fun a -> T.Subst.add_type T.Subst.empty a l_eff);
-            l_delim_tp  = tp0;
-            l_delim_eff = eff0
-          }, env
-
-        | L_NoEffect ->
-          Error.fatal (Error.unbound_the_effect ~pos:le.pos)
-
-        | L_No ->
-          Error.fatal (Error.expr_not_label ~pos:le.pos ~env le_tp)
-        end
-    in
-    let env_f = env in
-    let (env_h, ims) = ImplicitEnv.begin_generalize env ienv in
-    let (eh, eh_tp, _) = infer_expr_type env_h eh eff in
-    (* TODO: effect capability may have a scheme instead of type *)
-    ImplicitEnv.end_generalize_impure ~env:env_h ~pos:eh.pos ims eh_tp;
-    begin match Unification.to_handler env eh_tp with
-    | H_Handler(a, cap_tp, res_tp, res_eff) ->
-      let sub = lbl.l_sub a in
-      let cap_tp  = T.Type.subst sub cap_tp  in
-      let res_tp  = T.Type.subst sub res_tp  in
-      let res_eff = T.Type.subst sub res_eff in
-      Error.check_unify_result ~pos:def.pos
-        (Unification.unify_type env lbl.l_delim_tp res_tp)
-        ~on_error:(Error.delim_type_mismatch ~env lbl.l_delim_tp res_tp);
-      Error.check_unify_result ~pos:def.pos
-        (Unification.unify_type env lbl.l_delim_eff res_eff)
-        ~on_error:(Error.delim_effect_mismatch ~env lbl.l_delim_eff res_eff);
+    let (env1, ims) = ImplicitEnv.begin_generalize env ienv in
+    let (e1, tp_h, r_eff1) = infer_expr_type env1 e1 eff in
+    ImplicitEnv.end_generalize_impure ~env:env1 ~pos:e1.pos ims tp_h;
+    begin match Unification.to_handler env tp_h with
+    | H_Handler(a, cap_tp, tp_in, eff_in, tp_out, eff_out) ->
+      (* extend the environment *)
+      let (env, eff_tvar) = Env.add_the_effect ~pos env in
+      let env =
+        Type.check_type_alias_binder_opt env eff_opt (T.Type.t_var eff_tvar) in
+      let sub = T.Subst.rename_to_fresh T.Subst.empty a eff_tvar in
+      let cap_tp = T.Type.subst sub cap_tp in
+      let tp_in  = T.Type.subst sub tp_in in
+      let eff_in = T.Effect.cons eff_tvar (T.Type.subst sub eff_in) in
       let (env, pat, names, _) =
         Pattern.check_type ~env ~scope:(Env.scope env) pat cap_tp in
       let ienv = ImplicitEnv.shadow_names ienv names in
-      let (ret_x, body_tp, ret_body) =
-        MatchClause.check_return_clauses ~tcfix env rcs res_tp res_eff in
-      let body_eff = T.Effect.cons_eff lbl.l_eff res_eff in
-      let (body, Checked, _) = cont.run env ienv (Check body_tp) body_eff in
-      let (x, body) = ExprUtils.arg_match pat body body_tp body_eff in
-      let pos = Position.join def.pos body.pos in
+      (* check result's type and effect *)
+      let resp : (_, dir) response =
+        match req with
+        | Infer    -> Infered tp_out
+        | Check tp ->
+          Error.check_unify_result ~pos
+            (Unification.subtype env0 tp_out tp)
+            ~on_error:(Error.expr_type_mismatch ~env:env0 tp_out tp);
+          Checked
+      in
       Error.check_unify_result ~pos
-        (Unification.subeffect env0 res_eff eff)
-        ~on_error:(Error.expr_effect_mismatch ~env:env0 res_eff eff);
-      let e =
-        make body (T.EHandle
-          { label      = lbl.l_expr;
-            effect     = lbl.l_eff;
-            cap_var    = x;
-            body       = body;
-            capability = eh;
-            ret_var    = ret_x;
-            ret_body   = ret_body;
-            result_tp  = res_tp;
-            result_eff = res_eff
-          }) in
-      let (e, tp, r_eff) =
-        MatchClause.check_finally_clauses ~tcfix env_f fcs e res_tp req eff in
-      (lbl.l_ctx e, tp, r_eff)
-
+        (Unification.subeffect env0 eff_out eff)
+        ~on_error:(Error.expr_effect_mismatch ~env:env0 eff_out eff);
+      (* check the body *)
+      let (e2, Checked, _) = cont.run env ienv (Check tp_in) eff_in in
+      let cap_x = Var.fresh ~name:"cap" () in
+      (make e2 (T.EHandle(eff_tvar, cap_x, cap_tp, e1,
+        (make e2 (T.EMatch({def with data = T.EVar cap_x},
+          [(pat, e2)], tp_in, eff_in))))),
+        resp, Impure)
     | H_No ->
-      Error.fatal (Error.expr_not_handler ~pos:eh.pos ~env eh_tp)
+      Error.fatal (Error.expr_not_handler ~pos:e1.pos ~env tp_h)
     end
 
   | DImplicit(n, args, sch) ->
diff --git a/src/TypeInference/Error.ml b/src/TypeInference/Error.ml
index 10d9706..77ac4b3 100644
--- a/src/TypeInference/Error.ml
+++ b/src/TypeInference/Error.ml
@@ -179,6 +179,30 @@ let method_effect_mismatch ~pos ~env eff1 eff2 =
     (Pretty.type_to_string pp_ctx env eff2)
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
 
+let return_type_mismatch ~pos ~env tp1 tp2 =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "Return clause has type %s, but was expected to have type %s"
+    (Pretty.type_to_string pp_ctx env tp1)
+    (Pretty.type_to_string pp_ctx env tp2)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+
+let finally_type_mismatch ~pos ~env tp1 tp2 =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "Finally clause has type %s, but was expected to have type %s"
+    (Pretty.type_to_string pp_ctx env tp1)
+    (Pretty.type_to_string pp_ctx env tp2)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+
+let finally_effect_mismatch ~pos ~env eff1 eff2 =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "Finally clause has effect %s, which is not a supereffect of the delimiter's effect %s"
+    (Pretty.type_to_string pp_ctx env eff2)
+    (Pretty.type_to_string pp_ctx env eff1)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+
 let func_not_pure ~pos =
   (pos, "Cannot ensure that this function is pure and always terminates", [])
 
diff --git a/src/TypeInference/Error.mli b/src/TypeInference/Error.mli
index 3718072..f6eb07c 100644
--- a/src/TypeInference/Error.mli
+++ b/src/TypeInference/Error.mli
@@ -60,6 +60,13 @@ val func_effect_mismatch :
 val method_effect_mismatch :
   pos:Position.t -> env:Env.t -> T.effrow -> T.effrow -> t
 
+val return_type_mismatch :
+  pos:Position.t -> env:Env.t -> T.typ -> T.typ -> t
+val finally_type_mismatch :
+  pos:Position.t -> env:Env.t -> T.typ -> T.typ -> t
+val finally_effect_mismatch :
+  pos:Position.t -> env:Env.t -> T.effrow -> T.effrow -> t
+
 val func_not_pure : pos:Position.t -> t
 val impure_handler : pos:Position.t -> t
 
diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml
index fde31cf..ff8a6dd 100644
--- a/src/TypeInference/Expr.ml
+++ b/src/TypeInference/Expr.ml
@@ -121,19 +121,45 @@ let infer_expr_type ~tcfix env (e : S.expr) eff =
     in
     (e, tp, r_eff)
 
-  | EHandler h ->
+  | EHandler(h, rcs, fcs) ->
+    (* TODO: effect and label could be named here *)
     let (env, a) = Env.add_the_effect ~pos:e.pos env in
-    let res_tp  = Env.fresh_uvar env T.Kind.k_type in
-    let res_eff = Env.fresh_uvar env T.Kind.k_effrow in
+    let delim_tp  = Env.fresh_uvar env T.Kind.k_type in
+    let delim_eff = Env.fresh_uvar env T.Kind.k_effrow in
     let (env, lx) =
-      Env.add_the_label env (T.Type.t_var a) res_tp res_eff in
+      Env.add_the_label env (T.Type.t_var a) delim_tp delim_eff in
     let (h, tp, r_eff) = infer_expr_type env h T.Effect.pure in
     begin match r_eff with
     | Pure -> ()
     | Impure -> Error.report (Error.impure_handler ~pos:e.pos)
     end;
-    let e = make (T.EHandler(a, lx, res_tp, res_eff, h)) in
-    (e, T.Type.t_handler a tp res_tp res_eff, Pure)
+    let (ret_x, Infered body_tp, ret_body, Checked) =
+      MatchClause.tr_opt_clauses ~tcfix ~pos:e.pos env Infer rcs
+        (Check delim_tp) delim_eff
+        ~on_error:(fun ~pos -> assert false) in
+    let fin_eff = Env.fresh_uvar env T.Kind.k_effrow in
+    let (fin_x, Checked, fin_body, Infered fin_tp) =
+      MatchClause.tr_opt_clauses ~tcfix ~pos:e.pos env (Check delim_tp) fcs
+        Infer fin_eff
+        ~on_error:(fun ~pos -> assert false) in
+    Error.check_unify_result ~pos
+      (Unification.subeffect env delim_eff fin_eff)
+      ~on_error:(Error.finally_effect_mismatch ~env delim_eff fin_eff);
+    let e =
+      make (T.EHandler {
+        label     = lx;
+        effect    = a;
+        delim_tp  = delim_tp;
+        delim_eff = delim_eff;
+        cap_type  = tp;
+        cap_body  = h;
+        ret_var   = ret_x;
+        body_tp   = body_tp;
+        ret_body  = ret_body;
+        fin_var   = fin_x;
+        fin_body  = fin_body;
+      }) in
+    (e, T.Type.t_handler a tp body_tp delim_eff fin_tp fin_eff, Pure)
 
   | EAnnot(e, tp) ->
     let tp = Type.tr_ttype env tp in
@@ -252,21 +278,51 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
       MatchClause.check_match_clauses ~tcfix env e_tp cls tp eff in
     (make (T.EMatch(e, cls, tp, eff)), r_eff)
 
-  | EHandler h ->
+  | EHandler(body, rcs, fcs) ->
     begin match Unification.from_handler env tp with
-    | H_Handler(b, tp, tp0, eff0) ->
+    | H_Handler(b, cap_tp, tp_in, eff_in, tp_out, eff_out) ->
       let (env, a) = Env.add_the_effect ~pos env in
-      let sub  = T.Subst.rename_to_fresh T.Subst.empty b a in
-      let tp   = T.Type.subst sub tp in
-      let tp0  = T.Type.subst sub tp0 in
-      let eff0 = T.Type.subst sub eff0 in
-      let (env, l) = Env.add_the_label env (T.Type.t_var a) tp0 eff0 in
-      let (h, r_eff) = check_expr_type env h tp T.Effect.pure in
+      let sub    = T.Subst.rename_to_fresh T.Subst.empty b a in
+      let cap_tp = T.Type.subst sub cap_tp in
+      let tp_in  = T.Type.subst sub tp_in in
+      let eff_in = T.Type.subst sub eff_in in
+      let delim_tp  = Env.fresh_uvar env T.Kind.k_type in
+      let delim_eff = Env.fresh_uvar env T.Kind.k_effrow in
+      Error.check_unify_result ~pos
+        (Unification.subeffect env eff_in (T.Effect.cons a delim_eff))
+        ~on_error:(fun ~pos -> assert false);
+      let (env, lx) =
+        Env.add_the_label env (T.Type.t_var a) delim_tp delim_eff in
+      let (body, r_eff) = check_expr_type env body cap_tp T.Effect.pure in
       begin match r_eff with
       | Pure -> ()
       | Impure -> Error.report (Error.impure_handler ~pos)
       end;
-      let e = make (T.EHandler(a, l, tp0, eff0, h)) in
+      let (ret_var, Checked, ret_body, Checked) =
+        MatchClause.tr_opt_clauses ~tcfix ~pos env
+          (Check tp_in) rcs (Check delim_tp) delim_eff
+          ~on_error:(Error.return_type_mismatch ~env tp_in delim_tp) in
+      Error.check_unify_result ~pos
+        (Unification.subeffect env delim_eff eff_out)
+        ~on_error:(Error.finally_effect_mismatch ~env delim_eff eff_out);
+      let (fin_var, Checked, fin_body, Checked) =
+        MatchClause.tr_opt_clauses ~tcfix ~pos env
+          (Check delim_tp) fcs (Check tp_out) eff_out
+          ~on_error:(Error.finally_type_mismatch ~env delim_tp tp_out) in
+      let e =
+        make (T.EHandler {
+          label     = lx;
+          effect    = a;
+          delim_tp  = delim_tp;
+          delim_eff = delim_eff;
+          cap_type  = cap_tp;
+          cap_body  = body;
+          ret_var   = ret_var;
+          body_tp   = tp_in;
+          ret_body  = ret_body;
+          fin_var   = fin_var;
+          fin_body  = fin_body;
+        }) in
       (e, Pure)
 
     | H_No ->
diff --git a/src/TypeInference/MatchClause.ml b/src/TypeInference/MatchClause.ml
index 5955c2d..37ac1c6 100644
--- a/src/TypeInference/MatchClause.ml
+++ b/src/TypeInference/MatchClause.ml
@@ -49,40 +49,33 @@ let make_nonempty_match ~tcfix env tp cls res_tp res_eff =
   in (x, body)
 
 (* ------------------------------------------------------------------------- *)
-let check_return_clauses ~tcfix env rcs res_tp res_eff =
-  match rcs with
-  | [] ->
-    let x = Var.fresh () in
-    (x, res_tp, { T.pos = Position.nowhere; T.data = T.EVar x })
-  | _ ->
+let default_clause ~pos res1 res2 =
+  let x = Var.fresh () in
+  (x, res1, { T.pos; T.data = T.EVar x }, res2)
+
+let guess_type (type d) env (req : (_, d) request) : _ * (_, d) response =
+  match req with
+  | Check tp -> (tp, Checked)
+  | Infer    ->
     let tp = Env.fresh_uvar env T.Kind.k_type in
-    let (x, body) = make_nonempty_match ~tcfix env tp rcs res_tp res_eff in
-    (x, tp, body)
+    (tp, Infered tp)
 
-(* ------------------------------------------------------------------------- *)
-let check_finally_clauses (type dir)
-  ~tcfix env fcs hexpr htp (req : (T.typ, dir) request) eff :
-    T.expr * (T.typ, dir) response * ret_effect =
-  match fcs with
-  | [] ->
-    begin match req with
-    | Infer -> (hexpr, Infered htp, Impure)
-    | Check tp ->
-      Error.check_unify_result ~pos:hexpr.pos
-        (Unification.subtype env htp tp)
-        ~on_error:(Error.expr_type_mismatch ~env htp tp);
-      (hexpr, Checked, Impure)
-    end
+let tr_opt_clauses (type md rd) ~tcfix ~pos env
+  (mtp_req : (_, md) request) cls (rtp_req : (_, rd) request) eff ~on_error :
+    _ * (_, md) response * _ * (_, rd) response =
+  match mtp_req, cls, rtp_req with
+  | Check tp, [], Infer ->
+    default_clause ~pos Checked (Infered tp)
+  | Infer, [], Check tp ->
+    default_clause ~pos (Infered tp) Checked
+  | Infer, [], Infer ->
+    let tp = Env.fresh_uvar env T.Kind.k_type in
+    default_clause ~pos (Infered tp) (Infered tp)
+  | Check tp1, [], Check tp2 ->
+    Error.check_unify_result ~pos (Unification.subtype env tp1 tp2) ~on_error;
+    default_clause ~pos Checked Checked
   | _ ->
-    let (tp, (resp : (T.typ, dir) response)) =
-      match req with
-      | Infer ->
-        let tp = Env.fresh_uvar env T.Kind.k_type in
-        (tp, Infered tp)
-      | Check tp -> (tp, Checked)
-    in
-    let (x, body) = make_nonempty_match ~tcfix env htp fcs tp eff in
-    let expr =
-      { T.pos  = Position.join body.pos hexpr.pos;
-        T.data = T.ELet(x, T.Scheme.of_type htp, hexpr, body) }
-    in (expr, resp, Impure)
+    let (mtp, mtp_resp) = guess_type env mtp_req in
+    let (rtp, rtp_resp) = guess_type env rtp_req in
+    let (x, body) = make_nonempty_match ~tcfix env mtp cls rtp eff in
+    (x, mtp_resp, body, rtp_resp)
diff --git a/src/TypeInference/MatchClause.mli b/src/TypeInference/MatchClause.mli
index a40783a..9929d60 100644
--- a/src/TypeInference/MatchClause.mli
+++ b/src/TypeInference/MatchClause.mli
@@ -20,36 +20,25 @@ val check_match_clauses : tcfix:tcfix ->
     T.match_clause list * ret_effect
 
 (* ------------------------------------------------------------------------- *)
-(** Check return clauses of handler.
-  In [check_return_clauses env rcs res_tp res_eff] the meaning of the
-  parameters is the following.
-  - [env]     -- the environment.
-  - [rcs]     -- list of clauses. If this list is empty, then the default
-      identity clause is created.
-  - [res_tp]  -- the expected of the return clause
-  - [ref_eff] -- the expected effect of the return clause
-
-  This function returns triple: a variable bound by the return clause,
-  its type, and the body of the clause (including pattern-matching). *)
-val check_return_clauses : tcfix:tcfix ->
-  Env.t -> S.match_clause list -> T.typ -> T.effrow ->
-    T.var * T.typ * T.expr
+(** Check pattern-matching clauses, taking default identity clause if given
+  clause list is empty. This function is used for checking return and finally
+  clauses of a handler.
+  In [tr_opt_clauses ~tcfix ~pos env mtp_req cls rtp_req eff] the parameters
+  have the following meaning
+  - [env]     -- an environment
+  - [mtp_req] -- request for bidirectional type-checking of matched expression
+  - [cls]     -- list of clauses: empty list means single identity clause
+  - [rtp_req] -- request for bidirectional type-checking of returned type
+  - [eff]     -- returned effect
 
-(** Check finally clauses of handler.
-  In [check_finally_clauses env fcs hexpr htp req eff] the meaning of the
-  parameters is the following.
-  - [env]   -- the environment.
-  - [fcs]   -- list of clauses. If this list is empty, then the equivalent of
-      the default identity clause is created.
-  - [hexpr] -- the handler expression, to be wrapped around the finally
-      clauses.
-  - [htp]   -- the type of the handler expression
-  - [req]   -- type request of the bidirectional type-checking.
-  - [eff]   -- the expected effect of the clauses.
+  The [on_error] parameter is called, when requested types (both in
+  check-mode) do not match in case of empty clause list.
 
-  This function returns a triple with the same meaning as the triple returned
-  by [tr_expr] function. Handlers are always impure. *)
-val check_finally_clauses : tcfix:tcfix ->
-  Env.t -> S.match_clause list -> T.expr -> T.typ ->
-    (T.typ, 'dir) request -> T.effrow ->
-      T.expr * (T.typ, 'dir) response * ret_effect
+  Returns the tuple: a variable bound by this return/finally clause,
+  bidirectional response of its type, the body of the clause, and response
+  with the type of the body. *)
+val tr_opt_clauses : tcfix:tcfix -> pos:Position.t ->
+  Env.t -> (T.typ, 'md) request ->
+  S.match_clause list -> (T.typ, 'rd) request -> T.effrow ->
+  on_error:(pos:Position.t -> Error.t) ->
+    T.var * (T.typ, 'md) response * T.expr * (T.typ, 'rd) response
diff --git a/src/TypeInference/Pretty.ml b/src/TypeInference/Pretty.ml
index 328f022..b6b642b 100644
--- a/src/TypeInference/Pretty.ml
+++ b/src/TypeInference/Pretty.ml
@@ -223,10 +223,12 @@ let rec fresh_for_type env name tp =
     fresh_for_scheme env name sch &&
     fresh_for_type env name tp &&
     fresh_for_type env name eff
-  | THandler(_, tp, tp0, eff0) ->
+  | THandler(_, tp, itp, ieff, otp, oeff) ->
     fresh_for_type env name tp &&
-    fresh_for_type env name tp0 &&
-    fresh_for_type env name eff0
+    fresh_for_type env name itp &&
+    fresh_for_type env name ieff &&
+    fresh_for_type env name otp &&
+    fresh_for_type env name oeff
   | TLabel(eff, tp0, eff0) ->
     fresh_for_type env name eff &&
     fresh_for_type env name tp0 &&
@@ -274,22 +276,27 @@ let rec pp_type buf env prec tp =
       pp_effrow_end buf env ee;
       Buffer.add_string buf "] ";
       pp_type buf env 0 tp)
-  | THandler(x, tp, tp0, eff0) ->
+  | THandler(x, tp, itp, ieff, otp, oeff) ->
     paren buf prec 0 (fun () ->
       let name = gen_tvar_name
         (fun n -> 
           fresh_for_type env n tp &&
-          fresh_for_type env n tp0 && fresh_for_type env n eff0)
+          fresh_for_type env n itp && fresh_for_type env n ieff &&
+          fresh_for_type env n otp && fresh_for_type env n oeff)
         "E" in
-      let env = PPEnv.add_tvar env name x in
+      let env1 = PPEnv.add_tvar env name x in
       Buffer.add_string buf "handler ";
       Buffer.add_string buf name;
-      Buffer.add_string buf " => ";
-      pp_type buf env 1 tp;
+      Buffer.add_string buf ", ";
+      pp_type buf env1 1 tp;
       Buffer.add_string buf " @ ";
-      pp_type buf env 1 tp0;
+      pp_type buf env1 1 itp;
       Buffer.add_string buf " / ";
-      pp_type buf env 1 eff0)
+      pp_type buf env1 1 ieff;
+      Buffer.add_string buf " => ";
+      pp_type buf env 1 otp;
+      Buffer.add_string buf " / ";
+      pp_type buf env 1 oeff)
   | TLabel(eff, tp0, eff0) ->
     paren buf prec 0 (fun () ->
       Buffer.add_string buf "label ";
diff --git a/src/TypeInference/Unification.ml b/src/TypeInference/Unification.ml
index 6339a56..3e93c30 100644
--- a/src/TypeInference/Unification.ml
+++ b/src/TypeInference/Unification.ml
@@ -14,7 +14,7 @@ type arrow =
 
 type handler =
   | H_No
-  | H_Handler of T.tvar * T.typ * T.typ * T.effrow
+  | H_Handler of T.tvar * T.typ * T.typ * T.effrow * T.typ * T.effrow
 
 type label =
   | L_No
@@ -197,14 +197,18 @@ and unify env tp1 tp2 =
     unify_at_kind env eff1 eff2 T.Kind.k_effrow
   | TArrow _, _ -> raise Error
 
-  | THandler(a1, tp1, rtp1, reff1), THandler(a2, tp2, rtp2, reff2) ->
+  | THandler(a1, tp1, itp1, ieff1, otp1, oeff1),
+    THandler(a2, tp2, itp2, ieff2, otp2, oeff2) ->
+    unify env otp1 otp2;
+    unify_at_kind env oeff1 oeff2 T.Kind.k_effrow;
     let (env, a) = Env.add_anon_tvar env T.Kind.k_effect in
     let sub1 = T.Subst.rename_to_fresh T.Subst.empty a1 a in
     let sub2 = T.Subst.rename_to_fresh T.Subst.empty a2 a in
     unify env (T.Type.subst sub1 tp1) (T.Type.subst sub2 tp2);
-    unify env (T.Type.subst sub1 rtp1) (T.Type.subst sub2 rtp2);
-    unify_at_kind env
-      (T.Type.subst sub1 reff1) (T.Type.subst sub2 reff2) T.Kind.k_effrow
+    unify env (T.Type.subst sub1 itp1) (T.Type.subst sub2 itp2);
+    unify_at_kind env (T.Effect.cons a (T.Type.subst sub1 ieff1))
+                      (T.Effect.cons a (T.Type.subst sub2 ieff2))
+                      T.Kind.k_effrow
   | THandler _, _ -> raise Error
 
   | TLabel(eff1, rtp1, reff1), TLabel(eff2, rtp2, reff2) ->
@@ -276,14 +280,20 @@ let rec check_subtype env tp1 tp2 =
     check_subeffect env eff1 eff2
   | TArrow _, _ -> raise Error
 
-  | THandler(a1, tp1, rtp1, reff1), THandler(a2, tp2, rtp2, reff2) ->
+  | THandler(a1, tp1, itp1, ieff1, otp1, oeff1),
+    THandler(a2, tp2, itp2, ieff2, otp2, oeff2) ->
+    check_subtype env otp1 otp2;
+    check_subeffect env oeff1 oeff2;
     let (env, a) = Env.add_anon_tvar env T.Kind.k_effect in
     let sub1 = T.Subst.rename_to_fresh T.Subst.empty a1 a in
     let sub2 = T.Subst.rename_to_fresh T.Subst.empty a2 a in
     check_subtype env (T.Type.subst sub1 tp1) (T.Type.subst sub2 tp2);
-    unify env (T.Type.subst sub1 rtp1) (T.Type.subst sub2 rtp2);
-    unify_at_kind env
-      (T.Type.subst sub1 reff1) (T.Type.subst sub2 reff2) T.Kind.k_effrow
+    (* contravariant *)
+    check_subtype env (T.Type.subst sub2 itp2) (T.Type.subst sub1 otp1);
+    (* contravariant *)
+    check_subeffect env
+      (T.Effect.cons a (T.Type.subst sub2 ieff2))
+      (T.Effect.cons a (T.Type.subst sub1 ieff1))
   | THandler _, _ -> raise Error
 
   | TLabel(eff1, rtp1, reff1), TLabel(eff2, rtp2, reff2) ->
@@ -370,13 +380,15 @@ let to_handler env tp =
   | TUVar(p, u) ->
     let (env1, a) = Env.add_anon_tvar env T.Kind.k_effect in
     let tp   = Env.fresh_uvar env1 T.Kind.k_type in
-    let tp0  = Env.fresh_uvar env1 T.Kind.k_type in
-    let eff0 = Env.fresh_uvar env1 T.Kind.k_effrow in
-    set_uvar env p u (T.Type.t_handler a tp tp0 eff0);
-    H_Handler(a, tp, tp0, eff0)
+    let itp  = Env.fresh_uvar env1 T.Kind.k_type in
+    let ieff = Env.fresh_uvar env1 T.Kind.k_effrow in
+    let otp  = Env.fresh_uvar env  T.Kind.k_type in
+    let oeff = Env.fresh_uvar env  T.Kind.k_effrow in
+    set_uvar env p u (T.Type.t_handler a tp itp ieff otp oeff);
+    H_Handler(a, tp, itp, ieff, otp, oeff)
 
-  | THandler(a, tp, tp0, eff0) ->
-    H_Handler(a, tp, tp0, eff0)
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    H_Handler(a, tp, itp, ieff, otp, oeff)
 
   | TVar _ | TPureArrow _ | TArrow _ | TLabel _ | TApp _ -> H_No
 
@@ -388,13 +400,15 @@ let from_handler env tp =
   | TUVar(p, u) ->
     let (env1, a) = Env.add_anon_tvar env T.Kind.k_effect in
     let tp   = Env.fresh_uvar env1 T.Kind.k_type in
-    let tp0  = Env.fresh_uvar env1 T.Kind.k_type in
-    let eff0 = Env.fresh_uvar env1 T.Kind.k_effrow in
-    set_uvar env p u (T.Type.t_handler a tp tp0 eff0);
-    H_Handler(a, tp, tp0, eff0)
-
-  | THandler(a, tp, tp0, eff0) ->
-    H_Handler(a, tp, tp0, eff0)
+    let itp  = Env.fresh_uvar env1 T.Kind.k_type in
+    let ieff = Env.fresh_uvar env1 T.Kind.k_effrow in
+    let otp  = Env.fresh_uvar env T.Kind.k_type in
+    let oeff = Env.fresh_uvar env T.Kind.k_effrow in
+    set_uvar env p u (T.Type.t_handler a tp itp ieff otp oeff);
+    H_Handler(a, tp, itp, ieff, otp, oeff)
+
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    H_Handler(a, tp, itp, ieff, otp, oeff)
 
   | TVar _ | TPureArrow _ | TArrow _ | TLabel _ | TApp _ -> H_No
 
diff --git a/src/TypeInference/Unification.mli b/src/TypeInference/Unification.mli
index dc595d7..0133a14 100644
--- a/src/TypeInference/Unification.mli
+++ b/src/TypeInference/Unification.mli
@@ -26,7 +26,7 @@ type handler =
   | H_No
     (** Type is not a handler *)
 
-  | H_Handler of T.tvar * T.typ * T.typ * T.effrow
+  | H_Handler of T.tvar * T.typ * T.typ * T.effrow * T.typ * T.effrow
     (** Handler type *)
 
 (** Label type *)
diff --git a/test/ok/ok0053_firstClassHandler.fram b/test/ok/ok0053_firstClassHandler.fram
index 62de684..a09f06d 100644
--- a/test/ok/ok0053_firstClassHandler.fram
+++ b/test/ok/ok0053_firstClassHandler.fram
@@ -1,4 +1,4 @@
-let hId = handler effect x / r => r x
+let hId = handler effect x / r => r x end
 
 handle id with hId
 
diff --git a/test/ok/ok0054_firstClassHandler.fram b/test/ok/ok0054_firstClassHandler.fram
index a3d6bbc..8785787 100644
--- a/test/ok/ok0054_firstClassHandler.fram
+++ b/test/ok/ok0054_firstClassHandler.fram
@@ -2,4 +2,4 @@ let runH {A} h (f : {E} -> (A ->[|E] A) ->[|E] _) =
   handle x with h in
   f x
 
-let _ = runH (handler effect x / r => r ()) (fn op => op ())
+let _ = runH (handler effect x / r => r () end) (fn op => op ())
diff --git a/test/ok/ok0055_complexHandlers.fram b/test/ok/ok0055_complexHandlers.fram
index dfcf3f1..729b220 100644
--- a/test/ok/ok0055_complexHandlers.fram
+++ b/test/ok/ok0055_complexHandlers.fram
@@ -5,8 +5,12 @@ data State E X = State of
   , put : X ->[|E] Unit
   }
 
-let hState = handler
-  State
-    { get = effect I / r => fn s => r s s
-	, put = effect s / r => fn _ => r I s
-	}
+let hState s =
+  handler
+    State
+      { get = effect I / r => fn s => r s s
+      , put = effect s / r => fn _ => r I s
+      }
+  return  x => fn _ => x
+  finally f => f s
+  end
diff --git a/test/ok/ok0056_complexHandlers.fram b/test/ok/ok0056_complexHandlers.fram
index 55395ca..0e41913 100644
--- a/test/ok/ok0056_complexHandlers.fram
+++ b/test/ok/ok0056_complexHandlers.fram
@@ -6,9 +6,13 @@ data State E X = State of
   , update : (X ->[|E] X) ->[|E] Unit
   }
 
-let hState = handler
-  let get I = effect / r => fn s => r s s
-  let put s = effect / r => fn s => r I s
-  let update f = put (f (get I))
-  in
-  State { get, put, update }
+let hState s =
+  handler
+    let get I = effect / r => fn s => r s s
+    let put s = effect / r => fn s => r I s
+    let update f = put (f (get I))
+    in
+    State { get, put, update }
+  return  x => fn _ => x
+  finally f => f s
+  end
diff --git a/test/ok/ok0057_dataArgLabels.fram b/test/ok/ok0057_dataArgLabels.fram
index 72a9979..b0224e8 100644
--- a/test/ok/ok0057_dataArgLabels.fram
+++ b/test/ok/ok0057_dataArgLabels.fram
@@ -6,9 +6,13 @@ data State (effect E) (type T) = State of
   , update : {R} -> (T ->[E|R] T) ->[E|R] Unit
   }
 
-let hState = handler
-  let get I = effect / r => fn s => r s s
-  let put s = effect / r => fn s => r I s
-  let update f = put (f (get I))
-  in
-  State { get, put, update }
+let hState s =
+  handler
+    let get I = effect / r => fn s => r s s
+    let put s = effect / r => fn s => r I s
+    let update f = put (f (get I))
+    in
+    State { get, put, update }
+  return  x => fn _ => x
+  finally f => f s
+  end
diff --git a/test/ok/ok0059_effectArg.fram b/test/ok/ok0059_effectArg.fram
index ac839b8..88200de 100644
--- a/test/ok/ok0059_effectArg.fram
+++ b/test/ok/ok0059_effectArg.fram
@@ -2,4 +2,4 @@ let id {effect} x = x
 
 let id2 {effect = X} = id {effect = X}
 
-let hId = handler id2
+let hId = handler id2 end
diff --git a/test/ok/ok0077_effectResume.fram b/test/ok/ok0077_effectResume.fram
index a7dca0d..2bec7ce 100644
--- a/test/ok/ok0077_effectResume.fram
+++ b/test/ok/ok0077_effectResume.fram
@@ -1 +1 @@
-let h = handler effect x => resume x
+let h = handler effect x => resume x end