diff --git a/src/Lang/Core.mli b/src/Lang/Core.mli
index 0aec2f8d..f7f91389 100644
--- a/src/Lang/Core.mli
+++ b/src/Lang/Core.mli
@@ -84,14 +84,19 @@ type _ typ =
         (** Effect of the delimiter *)
     } -> ktype typ
 
-  | TData    : ttype * ctor_type list -> ktype typ
+  | TData    : ttype * effect * ctor_type list -> ktype typ
     (** Proof of the shape of ADT.
       
       Algebraic data type (ADTs) are just abstract types, but each operation
       on them like constructors or pattern-matching requires additional
       computationally irrelevant parameter of type that describes the shape
       of ADTs. This approach simplifies many things, e.g., mutually recursive
-      types are not recursive at all! *)
+      types are not recursive at all!
+
+      The element of type [TData(tp, eff, ctors)] is a witness that type [tp]
+      has constructors [ctors]. The effect [eff] is an effect of
+      pattern-matching: its pure for strictly positively recursive types,
+      and impure for other types (because it may lead to non-termination). *)
 
   | TApp     : ('k1 -> 'k2) typ * 'k1 typ -> 'k2 typ
     (** Type application *)
@@ -130,8 +135,13 @@ type data_def =
       args  : TVar.ex list;
         (** List of type parameters of this ADT. *)
 
-      ctors : ctor_type list
+      ctors : ctor_type list;
         (** List of constructors. *)
+
+      strictly_positive : bool
+        (** A flag indicating if the type is strictly positively recursive (in
+          particular, not recursive at all) and therefore can be deconstructed
+          without performing NTerm effect. *)
     }
 
   | DD_Label of (** Label *)
diff --git a/src/Lang/CorePriv/SExprPrinter.ml b/src/Lang/CorePriv/SExprPrinter.ml
index 585eca96..8ea7ecaa 100644
--- a/src/Lang/CorePriv/SExprPrinter.ml
+++ b/src/Lang/CorePriv/SExprPrinter.ml
@@ -54,8 +54,9 @@ let rec tr_type : type k. k typ -> SExpr.t =
         List (List.map tr_type lbl.val_types);
         tr_type lbl.delim_tp;
         tr_type lbl.delim_eff ]
-  | TData(tp, ctors) ->
-    List (Sym "data" :: tr_type tp :: List.map tr_ctor_type ctors)
+  | TData(tp, eff, ctors) ->
+    List (Sym "data" :: tr_type tp :: List (tr_effect eff) ::
+      List.map tr_ctor_type ctors)
   | TApp _ -> tr_type_app tp []
 
 and tr_effect : effect -> SExpr.t list =
diff --git a/src/Lang/CorePriv/Subst.ml b/src/Lang/CorePriv/Subst.ml
index f2436a13..179871a2 100644
--- a/src/Lang/CorePriv/Subst.ml
+++ b/src/Lang/CorePriv/Subst.ml
@@ -55,8 +55,9 @@ let rec in_type_rec : type k. t -> k typ -> k typ =
         delim_tp  = in_type_rec sub lbl.delim_tp;
         delim_eff = in_type_rec sub lbl.delim_eff
       }
-  | TData(tp, ctors) ->
-    TData(in_type_rec sub tp, List.map (in_ctor_type_rec sub) ctors)
+  | TData(tp, eff, ctors) ->
+    TData(in_type_rec sub tp, in_type_rec sub eff,
+      List.map (in_ctor_type_rec sub) ctors)
   | TApp(tp1, tp2) ->
     TApp(in_type_rec sub tp1, in_type_rec sub tp2)
 
diff --git a/src/Lang/CorePriv/Syntax.ml b/src/Lang/CorePriv/Syntax.ml
index 2e10a032..a3adf887 100644
--- a/src/Lang/CorePriv/Syntax.ml
+++ b/src/Lang/CorePriv/Syntax.ml
@@ -10,10 +10,11 @@ type var = Var.t
 
 type data_def =
   | DD_Data of
-    { tvar  : TVar.ex;
-      proof : var;
-      args  : TVar.ex list;
-      ctors : ctor_type list
+    { tvar              : TVar.ex;
+      proof             : var;
+      args              : TVar.ex list;
+      ctors             : ctor_type list;
+      strictly_positive : bool
     }
   | DD_Label of
     { tvar      : keffect tvar;
diff --git a/src/Lang/CorePriv/Type.ml b/src/Lang/CorePriv/Type.ml
index 90793f2c..f95727c7 100644
--- a/src/Lang/CorePriv/Type.ml
+++ b/src/Lang/CorePriv/Type.ml
@@ -83,8 +83,9 @@ let rec equal : type k. k typ -> k typ -> bool =
     end
   | TLabel _, _ -> false
 
-  | TData(tp1, ctors1), TData(tp2, ctors2) ->
+  | TData(tp1, eff1, ctors1), TData(tp2, eff2, ctors2) ->
     equal tp1 tp2 &&
+    equal eff1 eff2 &&
     List.length ctors1 = List.length ctors2 &&
     List.for_all2 ctor_type_equal ctors1 ctors2
   | TData _, _ -> false
@@ -176,7 +177,11 @@ let rec subtype tp1 tp2 =
   | TLabel _, (TUVar _ | TVar _ | TArrow _ | TForall _ | TData _ | TApp _) ->
     false
 
-  | TData _, TData _ -> equal tp1 tp2
+  | TData(tp1, eff1, ctors1), TData(tp2, eff2, ctors2) ->
+    equal tp1 tp2 &&
+    subeffect eff1 eff2 &&
+    List.length ctors1 = List.length ctors2 &&
+    List.for_all2 ctor_type_equal ctors1 ctors2
   | TData _, (TUVar _ | TVar _ | TArrow _ | TForall _ | TLabel _ | TApp _) ->
     false
 
@@ -241,12 +246,13 @@ let rec type_in_scope : type k. _ -> k typ -> k typ option =
         { effect; tvars = lbl.tvars; val_types; delim_tp; delim_eff })
     | _ -> None
     end
-  | TData(tp, ctors) ->
+  | TData(tp, eff, ctors) ->
     begin match
       type_in_scope scope tp,
+      type_in_scope scope eff,
       forall_map (ctor_type_in_scope scope) ctors
     with
-    | Some tp, Some ctors -> Some (TData(tp, ctors))
+    | Some tp, Some eff, Some ctors -> Some (TData(tp, eff, ctors))
     | _ -> None
     end
   | TApp(tp1, tp2) ->
@@ -318,7 +324,7 @@ let rec supertype_in_scope scope (tp : ttype) =
   are members of given set ([scope]) *)
 and subtype_in_scope scope (tp : ttype) =
   match tp with
-  | TUVar _ | TVar _ | TLabel _ | TData _ | TApp _ -> type_in_scope scope tp
+  | TUVar _ | TVar _ | TLabel _ | TApp _ -> type_in_scope scope tp
   | TArrow(tp1, tp2, eff) ->
     begin match
       supertype_in_scope scope tp1,
@@ -333,6 +339,64 @@ and subtype_in_scope scope (tp : ttype) =
     | Some body -> Some (TForall(a, body))
     | None      -> None
     end
+  | TData(tp, eff, ctors) ->
+    begin match
+      type_in_scope scope tp,
+      subeffect_in_scope scope eff,
+      forall_map (ctor_type_in_scope scope) ctors
+    with
+    | Some tp, eff, Some ctors -> Some (TData(tp, eff, ctors))
+    | _ -> None
+    end
+
+(** Check if all types on non-strictly positive positions fits in given
+  scope. *)
+let rec strictly_positive : type k. nonrec_scope:_ -> k typ -> bool =
+  fun ~nonrec_scope tp ->
+  match tp with
+  | TUVar _ | TVar _ | TEffPure -> true
+  | TLabel _ | TData _ ->
+    begin match type_in_scope nonrec_scope tp with
+    | Some _ -> true
+    | None   -> false
+    end
+
+  | TEffJoin(eff1, eff2) ->
+    strictly_positive ~nonrec_scope eff1 &&
+    strictly_positive ~nonrec_scope eff2
+
+  | TArrow(tp1, tp2, eff) ->
+    begin match
+      type_in_scope nonrec_scope tp1,
+      strictly_positive ~nonrec_scope tp2,
+      strictly_positive ~nonrec_scope eff
+    with
+    | Some _, true, true -> true
+    | _ -> false
+    end
+
+  | TForall(a, tp) ->
+    strictly_positive ~nonrec_scope:(TVar.Set.add a nonrec_scope) tp
+
+  | TApp(tp1, tp2) ->
+    begin match
+      strictly_positive ~nonrec_scope tp1,
+      type_in_scope nonrec_scope tp2
+    with
+    | true, Some _ -> true
+    | _ -> false
+    end
+
+(** Check if all types on non-strictly positive positions fits in given
+  scope (for ADT constructors) *)
+let strictly_positive_ctor ~nonrec_scope ctor =
+  let nonrec_scope = add_tvars_to_scope ctor.ctor_tvars nonrec_scope in
+  List.for_all (strictly_positive ~nonrec_scope) ctor.ctor_arg_types
+
+(** Check if all types on non-strictly positive positions fits in given
+  scope (for list of ADT constructors) *)
+let strictly_positive_ctors ~nonrec_scope ctors =
+  List.for_all (strictly_positive_ctor ~nonrec_scope) ctors
 
 type ex = Ex : 'k typ -> ex
 
diff --git a/src/Lang/CorePriv/TypeBase.ml b/src/Lang/CorePriv/TypeBase.ml
index b8177f28..e7c6ca56 100644
--- a/src/Lang/CorePriv/TypeBase.ml
+++ b/src/Lang/CorePriv/TypeBase.ml
@@ -92,7 +92,7 @@ type _ typ =
       delim_tp  : ttype;
       delim_eff : effect
     } -> ktype typ
-  | TData    : ttype * ctor_type list -> ktype typ
+  | TData    : ttype * effect * ctor_type list -> ktype typ
   | TApp     : ('k1 -> 'k2) typ * 'k1 typ -> 'k2 typ
 
 and ttype  = ktype typ
diff --git a/src/Lang/CorePriv/WellTypedInvariant.ml b/src/Lang/CorePriv/WellTypedInvariant.ml
index 8cc5b024..d62abc43 100644
--- a/src/Lang/CorePriv/WellTypedInvariant.ml
+++ b/src/Lang/CorePriv/WellTypedInvariant.ml
@@ -135,8 +135,8 @@ let rec tr_type : type k. Env.t -> k typ -> k typ =
         delim_tp  = tr_type env lbl.delim_tp;
         delim_eff = tr_type env lbl.delim_eff
       }
-  | TData(tp, ctors) ->
-    TData(tr_type env tp, List.map (tr_ctor_type env) ctors)
+  | TData(tp, eff, ctors) ->
+    TData(tr_type env tp, tr_type env eff, List.map (tr_ctor_type env) ctors)
   | TApp(tp1, tp2) ->
     TApp(tr_type env tp1, tr_type env tp2)
 
@@ -202,14 +202,27 @@ let prepare_data_def env (dd : data_def) =
     let (env, a) = Env.add_tvar env lbl.tvar in
     (env, DD_Label { lbl with tvar = a })
 
-let finalize_data_def (env, dd_eff) dd =
+let adt_effect ~nonrec_scope strictly_positive args ctors =
+  if strictly_positive then
+    let nonrec_scope = Type.add_tvars_to_scope args nonrec_scope in
+    if Type.strictly_positive_ctors ~nonrec_scope ctors then
+      TEffPure
+    else
+      InterpLib.InternalError.report
+        ~reason:"Type is not strictly positvely recursive"
+        ()
+  else
+    Effect.nterm
+
+let finalize_data_def ~nonrec_scope (env, dd_eff) dd =
   match dd with
   | DD_Data adt ->
     let (TVar.Ex a) = adt.tvar in
     let (xs, data_tp, ctors) = check_data env (TVar a) adt.args adt.ctors in
+    let eff = adt_effect ~nonrec_scope adt.strictly_positive xs ctors in
     let env =
       Env.add_irr_var env adt.proof
-        (Type.t_foralls xs (TData(data_tp, ctors))) in
+        (Type.t_foralls xs (TData(data_tp, eff, ctors))) in
     (env, dd_eff)
 
   | DD_Label lbl ->
@@ -224,8 +237,9 @@ let finalize_data_def (env, dd_eff) dd =
     (env, Effect.join Effect.nterm dd_eff)
 
 let check_data_defs env dds =
+  let nonrec_scope = Env.scope env in
   let (env, dds) = List.fold_left_map prepare_data_def env dds in
-  List.fold_left finalize_data_def (env, TEffPure) dds
+  List.fold_left (finalize_data_def ~nonrec_scope) (env, TEffPure) dds
 
 let rec infer_type_eff env e =
   match e with
@@ -285,7 +299,7 @@ let rec infer_type_eff env e =
     let tp  = tr_type env tp in
     let eff = tr_type env eff in
     begin match infer_type_check_eff (Env.irrelevant env) proof TEffPure with
-    | TData(data_tp, ctors) when List.length cls = List.length ctors ->
+    | TData(data_tp, meff, ctors) when List.length cls = List.length ctors ->
       check_vtype env v data_tp;
       List.iter2 (fun cl ctor ->
           let xs  = cl.cl_vars in
@@ -296,7 +310,7 @@ let rec infer_type_eff env e =
           let env = List.fold_left2 Env.add_var env xs tps in
           check_type_eff env cl.cl_body tp eff
         ) cls ctors;
-      (tp, Effect.join Effect.nterm eff)
+      (tp, Effect.join meff eff)
     | _ ->
       failwith "Internal type error"
     end
@@ -375,7 +389,7 @@ and infer_vtype env v =
 and infer_ctor_type env proof n tps args check_arg =
   assert (n >= 0);
   begin match infer_type_check_eff (Env.irrelevant env) proof TEffPure with
-  | TData(tp, ctors) ->
+  | TData(tp, _, ctors) ->
     begin match List.nth_opt ctors n with
     | Some ctor ->
       let sub = tr_types_sub env Subst.empty ctor.ctor_tvars tps in
diff --git a/src/Lang/Unif.ml b/src/Lang/Unif.ml
index 781f9d28..539f24d7 100644
--- a/src/Lang/Unif.ml
+++ b/src/Lang/Unif.ml
@@ -49,6 +49,8 @@ module CtorDecl = struct
   let subst = UnifPriv.Subst.in_ctor_decl
 
   let find_index cs name = List.find_index (fun c -> c.ctor_name = name) cs
+
+  let strictly_positive = UnifPriv.Type.ctor_strictly_positive
 end
 
 module Subst = UnifPriv.Subst
@@ -58,10 +60,11 @@ type var = Var.t
 
 type data_def =
   | DD_Data of
-    { tvar  : tvar;
-      proof : var;
-      args  : named_tvar list;
-      ctors : ctor_decl list
+    { tvar              : tvar;
+      proof             : var;
+      args              : named_tvar list;
+      ctors             : ctor_decl list;
+      strictly_positive : bool
     }
 
   | DD_Label of
@@ -94,8 +97,8 @@ and expr_data =
   | ELetRec     of rec_def list * expr
   | ECtor       of expr * int * typ list * expr list
   | EData       of data_def list * expr
-  | EMatchEmpty of expr * expr * typ * effrow
-  | EMatch      of expr * match_clause list * typ * effrow
+  | EMatchEmpty of expr * expr * typ * effrow option
+  | EMatch      of expr * match_clause list * typ * effrow option
   | EHandle     of tvar * var * typ * expr * expr
   | EHandler    of
     { label     : var;
diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli
index a49fd824..e024e8b9 100644
--- a/src/Lang/Unif.mli
+++ b/src/Lang/Unif.mli
@@ -115,8 +115,13 @@ type data_def =
       args  : named_tvar list;
         (** List of type parameters of this ADT. *)
 
-      ctors : ctor_decl list
+      ctors : ctor_decl list;
         (** List of constructors. *)
+
+      strictly_positive : bool
+        (** A flag indicating if the type is strictly positively recursive (in
+          particular, not recursive at all) and therefore can be deconstructed
+          in pure way. *)
     }
 
   | DD_Label of (** Label *)
@@ -203,13 +208,15 @@ and expr_data =
   | EData of data_def list * expr
     (** Definition of mutually recursive ADTs. *)
 
-  | EMatchEmpty of expr * expr * typ * effrow
+  | EMatchEmpty of expr * expr * typ * effrow option
     (** Pattern-matching of an empty type. The first parameter is an
       irrelevant expression, that is a witness that the type of the second
-      parameter is an empty ADT *)
+      parameter is an empty ADT. The last parameter is an optional effect of
+      the whole expression: [None] means that pattern-matching is pure. *)
 
-  | EMatch of expr * match_clause list * typ * effrow
-    (** Pattern-matching. It stores type and effect of the whole expression. *)
+  | EMatch of expr * match_clause list * typ * effrow option
+    (** Pattern-matching. It stores type and effect of the whole expression.
+      If the effect is [None], the pattern-matching is pure. *)
 
   | EHandle of tvar * var * typ * expr * expr
     (** Handling construct. In [EHandle(a, x, tp, e1, e2)] the meaning of
@@ -745,6 +752,11 @@ module CtorDecl : sig
 
   (** Get the index of a constructor with a given name *)
   val find_index : ctor_decl list -> string -> int option
+
+  (** Check if given constructor is strictly positive, i.e., if all type
+    variables on non-strictly positive positions and all scopes of unification
+    variables fit in [nonrec_scope]. *)
+  val strictly_positive : nonrec_scope:scope -> ctor_decl -> bool
 end
 
 (* ========================================================================= *)
diff --git a/src/Lang/UnifPriv/Scope.ml b/src/Lang/UnifPriv/Scope.ml
index decdf8fa..bd2f6147 100644
--- a/src/Lang/UnifPriv/Scope.ml
+++ b/src/Lang/UnifPriv/Scope.ml
@@ -33,6 +33,8 @@ let filter lvl f scope =
 
 let mem scope x = TVar.Set.mem x scope.tvar_set
 
+let for_all f scope = TVar.Set.for_all f scope.tvar_set
+
 let perm p scope =
   { tvar_set = TVar.Perm.map_set p scope.tvar_set;
     level    = scope.level
diff --git a/src/Lang/UnifPriv/Scope.mli b/src/Lang/UnifPriv/Scope.mli
index 57e82b9c..a51964ab 100644
--- a/src/Lang/UnifPriv/Scope.mli
+++ b/src/Lang/UnifPriv/Scope.mli
@@ -22,6 +22,9 @@ val filter : int -> (TVar.t -> bool) -> t -> t
 (** Check if given type variable is defined in given scope *)
 val mem : t -> TVar.t -> bool
 
+(** Check if given predicate holds for each element of given scope *)
+val for_all : (TVar.t -> bool) -> t -> bool
+
 (** Permute variables in given scope *)
 val perm : TVar.Perm.t -> t -> t
 
diff --git a/src/Lang/UnifPriv/Type.ml b/src/Lang/UnifPriv/Type.ml
index fcf325b0..c8830ba1 100644
--- a/src/Lang/UnifPriv/Type.ml
+++ b/src/Lang/UnifPriv/Type.ml
@@ -234,6 +234,111 @@ let try_shrink_scope ~scope tp =
 
 (* ========================================================================= *)
 
+let uvar_fits_in_scope ~scope p u =
+  Scope.for_all
+    (fun x -> Scope.mem scope (TVar.Perm.apply p x))
+    (UVar.scope u)
+
+(** Check if all type variables and all scopes of unification variables fit in
+  given scope *)
+let rec fits_in_scope ~scope tp =
+  match view tp with
+  | TUVar(p, u) -> uvar_fits_in_scope ~scope p u
+  | TVar    x   -> Scope.mem scope x
+  | TEffect xs  ->
+    TVar.Set.for_all (Scope.mem scope) xs
+  | TEffrow(xs, ee) ->
+    TVar.Set.for_all (Scope.mem scope) xs &&
+    begin match ee with
+    | EEClosed -> true
+    | EEUVar(p, u) -> uvar_fits_in_scope ~scope p u
+    | EEVar x -> Scope.mem scope x
+    | EEApp(tp1, tp2) ->
+      fits_in_scope ~scope tp1 && fits_in_scope ~scope tp2
+    end
+  | TPureArrow(sch, tp) ->
+    scheme_fits_in_scope ~scope sch &&
+    fits_in_scope ~scope tp
+  | TArrow(sch, tp, eff) ->
+    scheme_fits_in_scope ~scope sch &&
+    fits_in_scope ~scope tp &&
+    fits_in_scope ~scope eff
+  | THandler(x, tp, itp, ieff, otp, oeff) ->
+    fits_in_scope ~scope otp &&
+    fits_in_scope ~scope oeff &&
+    begin
+      let scope = Scope.add scope x in
+      fits_in_scope ~scope tp &&
+      fits_in_scope ~scope itp &&
+      fits_in_scope ~scope otp
+    end
+  | TLabel(eff0, tp, eff) ->
+    fits_in_scope ~scope eff0 &&
+    fits_in_scope ~scope tp &&
+    fits_in_scope ~scope eff
+  | TApp(tp1, tp2) ->
+    fits_in_scope ~scope tp1 && fits_in_scope ~scope tp2
+
+and scheme_fits_in_scope ~scope sch =
+  let scope = List.fold_left Scope.add_named scope sch.sch_targs in
+  List.for_all (named_scheme_fits_in_scope ~scope) sch.sch_named &&
+  fits_in_scope ~scope sch.sch_body
+
+and named_scheme_fits_in_scope ~scope (_, sch) =
+  scheme_fits_in_scope ~scope sch
+
+(** Check if all type variables on non-strictly positive positions and all
+  scopes of unification variables fit in given scope *)
+let rec strictly_positive ~nonrec_scope tp =
+  match view tp with
+  | TUVar(p, u) | TEffrow(_, EEUVar(p, u)) ->
+    uvar_fits_in_scope ~scope:nonrec_scope p u
+  | TVar _ | TEffect _ | TEffrow(_, (EEClosed | EEVar _)) ->
+    true
+  | TPureArrow(sch, tp) ->
+    scheme_fits_in_scope ~scope:nonrec_scope sch &&
+    strictly_positive ~nonrec_scope tp
+  | TArrow(sch, tp, eff) ->
+    scheme_fits_in_scope ~scope:nonrec_scope sch &&
+    strictly_positive ~nonrec_scope tp &&
+    strictly_positive ~nonrec_scope eff
+  | THandler(x, tp, itp, ieff, otp, oeff) ->
+    strictly_positive ~nonrec_scope otp &&
+    strictly_positive ~nonrec_scope oeff &&
+    begin
+      let scope = Scope.add nonrec_scope x in
+      (* Type [tp] is on positive position, but in encoding of handler
+        types in Core it is not strictly positive. *)
+      fits_in_scope ~scope tp &&
+      fits_in_scope ~scope itp &&
+      fits_in_scope ~scope ieff
+    end
+  | TLabel _ ->
+    fits_in_scope ~scope:nonrec_scope tp
+  | TApp(tp1, tp2) | TEffrow(_, EEApp(tp1, tp2)) ->
+    strictly_positive ~nonrec_scope tp1 &&
+    fits_in_scope ~scope:nonrec_scope tp2
+
+let scheme_strictly_positive ~nonrec_scope sch =
+  let nonrec_scope =
+    List.fold_left Scope.add_named nonrec_scope sch.sch_targs in
+  List.for_all (named_scheme_fits_in_scope ~scope:nonrec_scope)
+    sch.sch_named &&
+  strictly_positive ~nonrec_scope sch.sch_body
+
+let named_scheme_strictly_positive ~nonrec_scope (_, sch) =
+  scheme_strictly_positive ~nonrec_scope sch
+
+let ctor_strictly_positive ~nonrec_scope ctor =
+  let nonrec_scope =
+    List.fold_left Scope.add_named nonrec_scope ctor.ctor_targs in
+  List.for_all (named_scheme_strictly_positive ~nonrec_scope)
+    ctor.ctor_named &&
+  List.for_all (scheme_strictly_positive ~nonrec_scope)
+    ctor.ctor_arg_schemes
+
+(* ========================================================================= *)
+
 let mono_scheme tp =
   { sch_targs = [];
     sch_named = [];
diff --git a/src/ToCore/Common.ml b/src/ToCore/Common.ml
index eaa35432..a4e53226 100644
--- a/src/ToCore/Common.ml
+++ b/src/ToCore/Common.ml
@@ -28,7 +28,7 @@ let v_unit_prf =
       T.ctor_tvars     = [];
       T.ctor_arg_types = []
     } in
-  T.VExtern("__Unit_Proof__", T.TData(T.Type.t_unit, [ ctor ]))
+  T.VExtern("__Unit_Proof__", T.TData(T.Type.t_unit, T.TEffPure, [ ctor ]))
 
 let v_unit =
   T.VCtor(T.EValue v_unit_prf, 0, [], [])
diff --git a/src/ToCore/DataType.ml b/src/ToCore/DataType.ml
index 247aa9ff..54ddf023 100644
--- a/src/ToCore/DataType.ml
+++ b/src/ToCore/DataType.ml
@@ -9,10 +9,11 @@ open Common
 (** Half-translated data-like definition *)
 type data_def =
   | DD_Data of
-    { tvar  : T.TVar.ex;
-      proof : S.var;
-      args  : S.named_tvar list;
-      ctors : S.ctor_decl list;
+    { tvar              : T.TVar.ex;
+      proof             : S.var;
+      args              : S.named_tvar list;
+      ctors             : S.ctor_decl list;
+      strictly_positive : bool;
     }
   | DD_Label of
     { tvar      : T.keffect T.tvar;
@@ -40,8 +41,13 @@ let prepare_data_def env (dd : S.data_def) =
   match dd with
   | DD_Data dd ->
     let (env, tvar) = Env.add_tvar env dd.tvar in
-    let dd =
-      DD_Data { tvar; proof = dd.proof; args = dd.args; ctors = dd.ctors } in
+    let dd = DD_Data
+      { tvar;
+        proof             = dd.proof;
+        args              = dd.args;
+        ctors             = dd.ctors;
+        strictly_positive = dd.strictly_positive
+      } in
     (env, dd)
 
   | DD_Label dd ->
@@ -63,10 +69,11 @@ let finalize_data_def env (dd : data_def) =
     let (env, args) = List.fold_left_map Env.add_named_tvar env dd.args in
     let ctors = tr_ctor_decls env dd.ctors in
     T.DD_Data {
-      tvar  = dd.tvar;
-      proof = dd.proof;
-      args  = args;
-      ctors = ctors
+      tvar              = dd.tvar;
+      proof             = dd.proof;
+      args              = args;
+      ctors             = ctors;
+      strictly_positive = dd.strictly_positive;
     }
 
   | DD_Label dd ->
diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml
index 2d01ee5a..166797a6 100644
--- a/src/ToCore/Main.ml
+++ b/src/ToCore/Main.ml
@@ -37,13 +37,13 @@ let rec tr_expr env (e : S.expr) =
   | EMatchEmpty(proof, me, tp, eff) ->
     let proof = tr_expr env proof in
     let tp  = Type.tr_ttype env tp in
-    let eff = Type.tr_effect env eff in
+    let eff = Type.tr_effect_opt env eff in
     tr_expr_v env me (fun v ->
     T.EMatch(proof, v, [], tp, eff))
 
   | EMatch(me, cls, tp, eff) ->
     let tp  = Type.tr_ttype env tp in
-    let eff = Type.tr_effect env eff in
+    let eff = Type.tr_effect_opt env eff in
     tr_expr_v env me (fun v ->
     PatternMatch.tr_single_match ~pos:e.pos ~env ~tr_expr v cls tp eff)
 
diff --git a/src/ToCore/Type.ml b/src/ToCore/Type.ml
index d0205c2d..0f465ad1 100644
--- a/src/ToCore/Type.ml
+++ b/src/ToCore/Type.ml
@@ -135,3 +135,9 @@ and tr_scheme env (sch : S.scheme) =
   T.Type.t_foralls tvars
     (T.Type.t_pure_arrows itps
       (tr_ttype env sch_body))
+
+(** Translate optional effect ([None] means pure effect) *)
+let tr_effect_opt env eff =
+  match eff with
+  | None     -> T.TEffPure
+  | Some eff -> tr_effect env eff
diff --git a/src/TypeInference/Common.ml b/src/TypeInference/Common.ml
index 6cfde484..3fbdfe3b 100644
--- a/src/TypeInference/Common.ml
+++ b/src/TypeInference/Common.ml
@@ -54,3 +54,9 @@ let ret_effect_join eff1 eff2 =
 
 let ret_effect_joins effs =
   List.fold_left ret_effect_join Pure effs
+
+(** Effect of match_clause *)
+let match_effect reff (eff : T.effect) =
+  match reff with
+  | Pure   -> None
+  | Impure -> Some eff
diff --git a/src/TypeInference/DataType.ml b/src/TypeInference/DataType.ml
index 6087c96e..788550f6 100644
--- a/src/TypeInference/DataType.ml
+++ b/src/TypeInference/DataType.ml
@@ -8,6 +8,15 @@ open Common
 
 type ctor_decl_list = (S.is_public * T.ctor_decl) list
 
+(* ========================================================================= *)
+
+(** Check if ADT definition is strictly positively recursive *)
+let adt_strictly_positive ~nonrec_scope args ctors =
+  let nonrec_scope = List.fold_left T.Scope.add_named nonrec_scope args in
+  List.for_all (T.CtorDecl.strictly_positive ~nonrec_scope) ctors
+
+(* ========================================================================= *)
+
 let kind args =
   T.Kind.k_arrows
     (List.map (fun (_, x) -> T.TVar.kind x) args)
@@ -36,23 +45,27 @@ let open_data env adt ctors =
   List.fold_left (open_data_ctor adt) (env, 0) ctors
   |> fst
 
-let finalize_check env x ~name args ctors =
+let finalize_check ~nonrec_scope env x ~name args ctors =
   let px = Var.fresh ~name () in
+  let adt_ctors = List.map snd ctors in
   let info = {
     Module.adt_proof = { T.pos = Position.nowhere; T.data = T.EVar px };
     Module.adt_args  = args;
-    Module.adt_ctors = List.map snd ctors;
+    Module.adt_ctors = adt_ctors;
     Module.adt_type  =
       T.Type.t_apps (T.Type.t_var x)
-        (List.map (fun (_, x) -> T.Type.t_var x) args)
+        (List.map (fun (_, x) -> T.Type.t_var x) args);
+    Module.adt_strictly_positive =
+      adt_strictly_positive ~nonrec_scope args adt_ctors
   } in
   let env = Env.add_data env x info in
   let env = open_data env info ctors in
   let dd =
     T.DD_Data {
-      tvar  = x;
-      proof = px;
-      args  = args;
-      ctors = info.adt_ctors
+      tvar              = x;
+      proof             = px;
+      args              = args;
+      ctors             = adt_ctors;
+      strictly_positive = info.adt_strictly_positive
     } in
   (env, dd)
diff --git a/src/TypeInference/DataType.mli b/src/TypeInference/DataType.mli
index f72c59c8..04ee264e 100644
--- a/src/TypeInference/DataType.mli
+++ b/src/TypeInference/DataType.mli
@@ -20,7 +20,16 @@ val check_ctor_decls :
   Env.t -> S.ctor_decl list -> ctor_decl_list
 
 (** Finalize checking of ADT definition. It extends environment by ADT
-  metadata (proof) and constructors. *)
+  metadata (proof) and constructors. The [nonrec_scope] parameter is a scope
+  not extended with (mutually-)recursive definitions, and is used to check if
+  a type is strictly positively recursive. Note that during type inference,
+  the type is considered as strictly positively recursive if it does not
+  contain type variables on non-strictly positive position or unification
+  variables that do not fit in this scope. This approach may lead to some
+  false-negatives, if the programmer omit some types that do not contain any
+  recursive occurrences, e.g.,
+  [ data rec T = C of (_ -> T) in ... C (fn (x : Int) => ...) ]. *)
 val finalize_check :
+  nonrec_scope:T.scope ->
   Env.t -> T.tvar -> name:S.tvar -> T.named_tvar list -> ctor_decl_list ->
     Env.t * T.data_def
diff --git a/src/TypeInference/Def.ml b/src/TypeInference/Def.ml
index 94644ab8..0984cf32 100644
--- a/src/TypeInference/Def.ml
+++ b/src/TypeInference/Def.ml
@@ -131,7 +131,7 @@ let check_def : type dir. tcfix:tcfix ->
     | Impure -> Error.report (Error.func_not_pure ~pos:def.pos)
     end;
     (* TODO: check if [tp] is in proper scope (ims2 may bind some types) *)
-    let (ims2, body) = ExprUtils.inst_args_match ims2 body tp T.Effect.pure in
+    let (ims2, body) = ExprUtils.inst_args_match ims2 body tp None in
     let (tvars1, ims1) =
       ImplicitEnv.end_generalize_pure ims1 (T.Type.uvars tp) in
     let (body, sch) =
@@ -150,9 +150,10 @@ let check_def : type dir. tcfix:tcfix ->
       Pattern.check_type ~env ~scope pat tp in
     let ienv = ImplicitEnv.shadow_names ienv names in
     let (e2, resp, r_eff3) = cont.run env ienv req eff in
+    let meff = match_effect (ret_effect_join r_eff2 r_eff3) eff in
     let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in
     let res_tp = bidir_result req resp in
-    (make e2 (T.EMatch(e1, [(pat, e2)], res_tp, eff)), resp,
+    (make e2 (T.EMatch(e1, [(pat, e2)], res_tp, meff)), resp,
       ret_effect_joins [ r_eff1; r_eff2; r_eff3 ])
 
   | DMethodFn(public, x, method_name) ->
@@ -177,7 +178,7 @@ let check_def : type dir. tcfix:tcfix ->
     in
     (make e2 (T.EData([dd],
       (make e2 (T.EMatch({ def with data = T.EVar x},
-        [(pat, e2)], res_tp, eff))))),
+        [(pat, e2)], res_tp, Some eff))))),
       resp, Impure)
 
   | DHandlePat(eff_opt, pat, e1) ->
@@ -216,7 +217,7 @@ let check_def : type dir. tcfix:tcfix ->
       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))))),
+          [(pat, e2)], tp_in, Some eff_in))))),
         resp, Impure)
     | H_No ->
       Error.fatal (Error.expr_not_handler ~pos:e1.pos ~env tp_h)
@@ -239,7 +240,8 @@ let check_def : type dir. tcfix:tcfix ->
     let kind  = DataType.kind args in
     let ctors = DataType.check_ctor_decls ~data_targs:args data_env ctors in
     let (env, x) = Env.add_tvar ~pos env ~public name kind in
-    let (env, dd) = DataType.finalize_check env x ~name args ctors in 
+    let (env, dd) =
+      DataType.finalize_check ~nonrec_scope:scope env x ~name args ctors in
     let (e, resp, r_eff) = cont.run env ienv req eff in
     let resp = type_resp_in_scope ~env ~pos:def.pos ~scope resp in
     (make e (T.EData([dd], e)), resp, r_eff)
diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml
index ff8a6dda..61c2de5b 100644
--- a/src/TypeInference/Expr.ml
+++ b/src/TypeInference/Expr.ml
@@ -91,7 +91,8 @@ let infer_expr_type ~tcfix env (e : S.expr) eff =
     let body_eff = Env.fresh_uvar env T.Kind.k_effrow in
     let (env, pat, sch, r_eff1) = Pattern.infer_arg_scheme env arg in
     let (body, r_eff2) = check_expr_type env body tp2 body_eff in
-    let (x, body) = ExprUtils.arg_match pat body tp2 body_eff in
+    let meff = match_effect (ret_effect_join r_eff1 r_eff2) body_eff in
+    let (x, body) = ExprUtils.arg_match pat body tp2 meff in
     begin match ret_effect_join r_eff1 r_eff2 with
     | Pure ->
       let b = Unification.subeffect env body_eff T.Effect.pure in
@@ -226,13 +227,13 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
       let (body, r_eff2) = check_expr_type env body tp2 T.Effect.pure in
       if ret_effect_join r_eff1 r_eff2 <> Pure then
         Error.report (Error.func_not_pure ~pos);
-      let (x, body) = ExprUtils.arg_match pat body tp2 T.Effect.pure in
+      let (x, body) = ExprUtils.arg_match pat body tp2 None in
       (make (T.EPureFn(x, sch, body)), Pure)
 
     | Arr_Impure(sch, tp2, eff) ->
       let (env, pat, _) = Pattern.check_arg_scheme env arg sch in
       let (body, _) = check_expr_type env body tp2 eff in
-      let (x, body) = ExprUtils.arg_match pat body tp2 eff in
+      let (x, body) = ExprUtils.arg_match pat body tp2 (Some eff) in
       (make (T.EFn(x, sch, body)), Pure)
 
     | Arr_No ->
@@ -249,14 +250,19 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
     (e, r_eff)
 
   | EMatch(me, []) ->
-    let (me, me_tp, _) = infer_expr_type env me eff in
+    let (me, me_tp, r_eff1) = infer_expr_type env me eff in
     begin match T.Type.whnf me_tp with
     | Whnf_Neutral(NH_Var x, targs_rev) ->
       begin match Env.lookup_adt env x with
-      | Some { adt_ctors = []; adt_proof; _ } ->
+      | Some { adt_ctors = []; adt_proof; adt_strictly_positive; _ } ->
         let targs = List.rev targs_rev in
         let proof = ExprUtils.make_tapp adt_proof targs in
-        (make (T.EMatchEmpty(proof, me, tp, eff)), Impure)
+        let (meff, r_eff2) =
+          if adt_strictly_positive then (None, Pure)
+          else (Some eff, Impure)
+        in
+        (make (T.EMatchEmpty(proof, me, tp, meff)),
+          ret_effect_join r_eff1 r_eff2)
 
       | Some { adt_ctors = _ :: _; _ } ->
         Error.fatal (Error.empty_match_on_nonempty_adt ~pos ~env me_tp)
@@ -273,10 +279,11 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
     end
 
   | EMatch(e, cls) ->
-    let (e, e_tp, _) = infer_expr_type env e eff in
-    let (cls, r_eff) =
+    let (e, e_tp, r_eff1) = infer_expr_type env e eff in
+    let (cls, r_eff2) =
       MatchClause.check_match_clauses ~tcfix env e_tp cls tp eff in
-    (make (T.EMatch(e, cls, tp, eff)), r_eff)
+    (make (T.EMatch(e, cls, tp, match_effect r_eff2 eff)),
+      ret_effect_join r_eff1 r_eff2)
 
   | EHandler(body, rcs, fcs) ->
     begin match Unification.from_handler env tp with
@@ -340,7 +347,7 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
       let (env, rpat, _) =
         Pattern.check_arg_scheme env arg (T.Scheme.of_type r_tp) in
       let (body, _) = check_expr_type env body res_tp res_eff in
-      let (x, body) = ExprUtils.arg_match rpat body res_tp res_eff in
+      let (x, body) = ExprUtils.arg_match rpat body res_tp (Some res_eff) in
       let e = make (T.EEffect(make (T.EVar lx), x, body, tp)) in
       (e, Impure)
 
diff --git a/src/TypeInference/ExprUtils.mli b/src/TypeInference/ExprUtils.mli
index 25ecade9..ba200956 100644
--- a/src/TypeInference/ExprUtils.mli
+++ b/src/TypeInference/ExprUtils.mli
@@ -53,12 +53,14 @@ val ctor_func : pos:Position.t -> int -> Module.adt_info -> T.expr
   - [body] -- an expression that should be extended with a pattern-matching,
       e.g. body of a function;
   - [tp]   -- the type of [body] expression;
-  - [eff]  -- the effect of [body] expression.
+  - [eff]  -- the optional effect of [body] expression. [None] means that both
+    body and pattern-matching is pure.
   It returns a variable that should be bound instead of pattern together with
   an extended expression. *)
-val arg_match : T.pattern -> T.expr -> T.typ -> T.effrow -> T.var * T.expr
+val arg_match :
+  T.pattern -> T.expr -> T.typ -> T.effrow option -> T.var * T.expr
 
 (** Same as [arg_match], but take multiple binders of named parameters. *)
 val inst_args_match :
-  (T.name * T.pattern * T.scheme) list -> T.expr -> T.typ -> T.effrow ->
+  (T.name * T.pattern * T.scheme) list -> T.expr -> T.typ -> T.effrow option ->
     (T.name * T.var * T.scheme) list * T.expr
diff --git a/src/TypeInference/MatchClause.ml b/src/TypeInference/MatchClause.ml
index 37ac1c67..2ca61e88 100644
--- a/src/TypeInference/MatchClause.ml
+++ b/src/TypeInference/MatchClause.ml
@@ -41,11 +41,12 @@ let make_nonempty_match ~tcfix env tp cls res_tp res_eff =
       let p2 = List.fold_left (fun _ cl -> cl.S.pos) p1 cls in
       Position.join p1 p2
   in
-  let (cls, _) = check_match_clauses ~tcfix env tp cls res_tp res_eff in
+  let (cls, r_eff) = check_match_clauses ~tcfix env tp cls res_tp res_eff in
+  let meff = match_effect r_eff res_eff in
   let x = Var.fresh () in
   let body =
     { T.pos;
-      T.data = T.EMatch({ pos; data = T.EVar x }, cls, res_tp, res_eff) }
+      T.data = T.EMatch({ pos; data = T.EVar x }, cls, res_tp, meff) }
   in (x, body)
 
 (* ------------------------------------------------------------------------- *)
diff --git a/src/TypeInference/Module.ml b/src/TypeInference/Module.ml
index a31565b0..68a049cf 100644
--- a/src/TypeInference/Module.ml
+++ b/src/TypeInference/Module.ml
@@ -22,8 +22,12 @@ type adt_info = {
   adt_ctors : T.ctor_decl list;
     (** List of constructors of an ADT *)
 
-  adt_type  : T.typ
+  adt_type  : T.typ;
     (** The type that is an ADT, already applied to [adt_args] *)
+
+  adt_strictly_positive : bool
+    (** A flag indicating that the type is strictly positively recursive, and
+      therefore pattern-matching on it is pure. *)
 }
 
 type var_info =
@@ -57,7 +61,8 @@ let unit_info =
           ctor_named       = [];
           ctor_arg_schemes = []
         } ];
-    adt_type  = T.Type.t_unit
+    adt_type  = T.Type.t_unit;
+    adt_strictly_positive = true
   }
 
 let empty =
diff --git a/src/TypeInference/Module.mli b/src/TypeInference/Module.mli
index 4106c847..cf84eeb2 100644
--- a/src/TypeInference/Module.mli
+++ b/src/TypeInference/Module.mli
@@ -20,8 +20,12 @@ type adt_info = {
   adt_ctors : T.ctor_decl list;
     (** List of constructors of an ADT *)
 
-  adt_type  : T.typ
+  adt_type  : T.typ;
     (** The type that is an ADT, already applied to [adt_args] *)
+
+  adt_strictly_positive : bool
+    (** A flag indicating that the type is strictly positively recursive, and
+      therefore pattern-matching on it is pure. *)
 }
 
 (** Information about variable-like identifier (variable, constructor, etc.) *)
diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml
index 9c7ad629..fa3b3a98 100644
--- a/src/TypeInference/Pattern.ml
+++ b/src/TypeInference/Pattern.ml
@@ -77,7 +77,7 @@ let rec check_ctor_type_args ~pos ~env ~scope ~sub
 
 (** Extend the environment by a named parameter that is not explicitly
   mentioned. The middle element of returned triple is a set of names
-  implicity bound. *)
+  implicitly bound. *)
 let introduce_implicit_name ~pos env (name : T.name) sch =
   match name with
   | NLabel ->
@@ -304,19 +304,17 @@ and check_type ~env ~scope (pat : S.pattern) tp =
       List.map (T.Scheme.subst sub2) ctor.ctor_arg_schemes in
     if List.length ctor_arg_schemes <> List.length args then
       Error.fatal (Error.ctor_arity_mismatch ~pos:pat.pos
-        cpath.data (List.length ctor_arg_schemes) (List.length args))
-    else
-      Error.check_unify_result ~is_fatal:true ~pos:pat.pos
-        (Unification.subtype env tp res_tp)
-        ~on_error:(Error.pattern_type_mismatch ~env res_tp tp);
-      let (env, ps2, bn2, _) =
-        check_pattern_schemes ~env ~scope args ctor_arg_schemes in
-      let cname = S.path_name cpath.data in
-      let pat = make
-        (T.PCtor(cname, idx, proof, ctors, tvars, ps1 @ ps2)) in
-      (* Pattern matching is always impure, as due to recursive types it can
-        be used to encode non-termination *)
-      (env, pat, union_bound_names bn1 bn2, Impure)
+        cpath.data (List.length ctor_arg_schemes) (List.length args));
+    Error.check_unify_result ~is_fatal:true ~pos:pat.pos
+      (Unification.subtype env tp res_tp)
+      ~on_error:(Error.pattern_type_mismatch ~env res_tp tp);
+    let (env, ps2, bn2, _) =
+      check_pattern_schemes ~env ~scope args ctor_arg_schemes in
+    let cname = S.path_name cpath.data in
+    let pat = make
+      (T.PCtor(cname, idx, proof, ctors, tvars, ps1 @ ps2)) in
+    let reff = if info.adt_strictly_positive then Pure else Impure in
+    (env, pat, union_bound_names bn1 bn2, reff)
 
 and check_pattern_schemes ~env ~scope pats schs =
   match pats, schs with
diff --git a/src/TypeInference/PreludeTypes.ml b/src/TypeInference/PreludeTypes.ml
index b165fbee..f88172b6 100644
--- a/src/TypeInference/PreludeTypes.ml
+++ b/src/TypeInference/PreludeTypes.ml
@@ -35,21 +35,17 @@ let mk_Some ~env ~pos tp_arg expr_arg : T.expr =
   let _, x = option_to_whnf ~env ~pos tp' in
   match Env.lookup_adt env x with
   | Some adt_info -> (
-      let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
       match
         List.find_index
           (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "Some")
-          adt_ctors
+          adt_info.adt_ctors
       with
       | Some idx ->
-          make
-            (T.ECtor
-               ( make (T.ETApp (adt_proof, tp_arg)) Position.nowhere,
-                 idx,
-                 [],
-                 [ expr_arg ] ))
-            Position.nowhere
-      | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "Some" tp'))
+        let proof =
+          make (T.ETApp(adt_info.adt_proof, tp_arg)) Position.nowhere in
+        make (T.ECtor(proof, idx, [], [ expr_arg ])) Position.nowhere
+      | None ->
+        Error.fatal (Error.ctor_not_in_type ~pos ~env "Some" tp'))
   | None -> Error.fatal (Error.unbound_adt ~pos ~env x)
 
 let mk_None ~env ~pos option_tp : T.expr =
@@ -57,16 +53,15 @@ let mk_None ~env ~pos option_tp : T.expr =
   let tp_arg, x = option_to_whnf ~env ~pos option_tp in
   match Env.lookup_adt env x with
   | Some adt_info -> (
-      let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
       match
         List.find_index
           (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "None")
-          adt_ctors
+          adt_info.adt_ctors
       with
       | Some idx ->
-          make
-            (T.ECtor
-               (make (T.ETApp (adt_proof, tp_arg)) Position.nowhere, idx, [], []))
-            Position.nowhere
-      | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "None" option_tp))
+        let proof =
+          make (T.ETApp(adt_info.adt_proof, tp_arg)) Position.nowhere in
+        make (T.ECtor(proof, idx, [], [])) Position.nowhere
+      | None ->
+        Error.fatal (Error.ctor_not_in_type ~pos ~env "None" option_tp))
   | None -> Error.fatal (Error.unbound_adt ~pos ~env x)
diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml
index dd07c722..45949507 100644
--- a/src/TypeInference/RecDefs.ml
+++ b/src/TypeInference/RecDefs.ml
@@ -89,7 +89,7 @@ let rec prepare_rec_data env (def : S.def) =
 
 (** The second pass for single definition. See [finalize_rec_data_defs] for
   more details. *)
-let rec finalize_rec_data env ienv (def : def1 T.node) =
+let rec finalize_rec_data ~nonrec_scope env ienv (def : def1 T.node) =
   match def.data with
   | D1_Blank | D1_LetVar _ | D1_LetFun _ -> (env, ienv, [], Pure)
   | D1_Label(tvar, id, tp_opt) ->
@@ -119,21 +119,25 @@ let rec finalize_rec_data env ienv (def : def1 T.node) =
     | false -> assert false
     end;
     let ctors = DataType.check_ctor_decls ~data_targs:args data_env ctors in
-    let (env, dd) = DataType.finalize_check env x ~name args ctors in 
+    let (env, dd) =
+      DataType.finalize_check ~nonrec_scope env x ~name args ctors in
     (env, ienv, [dd], Pure)
   | D1_Section defs ->
-    let (env, dds, r_eff) = finalize_rec_data_defs env ienv defs in
+    let (env, dds, r_eff) =
+      finalize_rec_data_defs ~nonrec_scope env ienv defs in
     (env, ienv, dds, r_eff)
 
 (** The main function of the second pass. It returns extended environment,
   list of data/label definitions and the effect of this block (impure, when
   new run-time labels are generated). *)
-and finalize_rec_data_defs env ienv defs =
+and finalize_rec_data_defs ~nonrec_scope env ienv defs =
   match defs with
   | [] -> (env, [], Pure)
   | def :: defs ->
-    let (env, ienv, dds1, r_eff1) = finalize_rec_data env ienv def in
-    let (env, dds2, r_eff2) = finalize_rec_data_defs env ienv defs in
+    let (env, ienv, dds1, r_eff1) =
+      finalize_rec_data ~nonrec_scope env ienv def in
+    let (env, dds2, r_eff2) =
+      finalize_rec_data_defs ~nonrec_scope env ienv defs in
     (env, dds1 @ dds2, ret_effect_join r_eff1 r_eff2)
 
 (* ========================================================================= *)
@@ -305,7 +309,7 @@ let rec check_rec_fun ~tcfix env (def : def3 T.node) =
     end;
     let (named, body) =
       ExprUtils.inst_args_match sch_info.rsi_named body
-        sch_info.rsi_body_tp T.Effect.pure in
+        sch_info.rsi_body_tp None in
     let body = ExprUtils.make_nfun named body in
     { def with
       data = D4_LetFun(fd.var, fd.scheme, fd.name, sch_info.rsi_tvars, body)
@@ -450,8 +454,10 @@ let finalize_rec_fun (fds : def6 list) (fd : def6) =
 (* ========================================================================= *)
 
 let check_rec_defs ~tcfix env ienv defs =
+  let nonrec_scope = Env.scope env in
   let (env, defs) = List.fold_left_map prepare_rec_data env defs in
-  let (env, dds, r_eff) = finalize_rec_data_defs env ienv defs in
+  let (env, dds, r_eff) =
+    finalize_rec_data_defs ~nonrec_scope env ienv defs in
   let (rec_env, ims) = ImplicitEnv.begin_generalize env ienv in
   let (rec_env, fds) = prepare_rec_funs rec_env ienv defs in
   let fds = List.map (check_rec_fun ~tcfix rec_env) fds in
diff --git a/test/err/tc_0010_impureNonPositiveRecord.fram b/test/err/tc_0010_impureNonPositiveRecord.fram
new file mode 100644
index 00000000..676657fd
--- /dev/null
+++ b/test/err/tc_0010_impureNonPositiveRecord.fram
@@ -0,0 +1,7 @@
+data rec T = { foo : T -> T }
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure (fn (x : T) => x.foo)
+
+// @stderr::5:19-39: error:
diff --git a/test/err/tc_0011_nonPositiveUVar.fram b/test/err/tc_0011_nonPositiveUVar.fram
new file mode 100644
index 00000000..54d3f2f3
--- /dev/null
+++ b/test/err/tc_0011_nonPositiveUVar.fram
@@ -0,0 +1,9 @@
+data rec T = C of _
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure (fn (C x) => x)
+
+let _ = C (fn (C x) => C x)
+
+// @stderr::5:19-33: error:
diff --git a/test/err/tc_0012_impureExprInPureMatch.fram b/test/err/tc_0012_impureExprInPureMatch.fram
new file mode 100644
index 00000000..e3f9b563
--- /dev/null
+++ b/test/err/tc_0012_impureExprInPureMatch.fram
@@ -0,0 +1,8 @@
+let foo (f : Unit ->[] Unit) =
+  match f () with x => x end
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure foo
+
+// @stderr::6:19-21: error:
diff --git a/test/ok/ok0079_impureMethod.fram b/test/ok/ok0079_impureMethod.fram
index 4b035b77..6951857e 100644
--- a/test/ok/ok0079_impureMethod.fram
+++ b/test/ok/ok0079_impureMethod.fram
@@ -1,5 +1,5 @@
-data U = I
+data rec U = I of (U -> U)
 
-method foo {self = I} = I
+method foo {self = I f} = f (I f)
 
-let baz I (x : U) = x.foo
+let baz (I _) (x : U) = x.foo
diff --git a/test/ok/ok0112_pureRecord.fram b/test/ok/ok0112_pureRecord.fram
new file mode 100644
index 00000000..14cbcd01
--- /dev/null
+++ b/test/ok/ok0112_pureRecord.fram
@@ -0,0 +1,6 @@
+data Vec X = { x : X, y : X }
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure (fn (v : Vec Unit) => v.x)
+let _ = checkPure (fn (v : Vec Unit) => v.y)
diff --git a/test/ok/ok0113_pureMatchingNonrecUVar.fram b/test/ok/ok0113_pureMatchingNonrecUVar.fram
new file mode 100644
index 00000000..965c88b8
--- /dev/null
+++ b/test/ok/ok0113_pureMatchingNonrecUVar.fram
@@ -0,0 +1,7 @@
+data T = C of _
+let get (C x) = x
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure get
+let _ = C ()
diff --git a/test/ok/ok0114_pureTail.fram b/test/ok/ok0114_pureTail.fram
new file mode 100644
index 00000000..2355d52f
--- /dev/null
+++ b/test/ok/ok0114_pureTail.fram
@@ -0,0 +1,11 @@
+data rec List X = [] | (::) of X, List X
+
+let tail xs =
+  match xs with
+  | []      => []
+  | _ :: xs => xs
+  end
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure (tail : List Unit -> List Unit)
diff --git a/test/ok/ok0115_purePatternMatching.fram b/test/ok/ok0115_purePatternMatching.fram
new file mode 100644
index 00000000..21f01658
--- /dev/null
+++ b/test/ok/ok0115_purePatternMatching.fram
@@ -0,0 +1,14 @@
+rec
+  data Trie X = Node of X, TrieList X
+  data TrieList X = [] | (::) of Trie X, TrieList X
+end
+
+let get t =
+  match t with
+  | Node _ (_ :: _ :: Node _ (_ :: Node x _ :: _) :: _) => x
+  | _ => ()
+  end
+
+let checkPure (f : _ -> _) = ()
+
+let _ = checkPure get