diff --git a/src/Lang/Unif.ml b/src/Lang/Unif.ml
index 539f24d7..d638fbe4 100644
--- a/src/Lang/Unif.ml
+++ b/src/Lang/Unif.ml
@@ -20,6 +20,8 @@ module Scope = UnifPriv.Scope
 
 module Name = UnifPriv.Name
 
+module Effect = UnifPriv.Effect
+
 module Type = struct
   include UnifPriv.TypeBase
   include UnifPriv.Type
@@ -28,10 +30,9 @@ module Type = struct
   let subst = UnifPriv.Subst.in_type
 end
 
-module Effect = UnifPriv.Effect
-
 module Scheme = struct
   let of_type        = UnifPriv.Type.mono_scheme
+  let to_type        = UnifPriv.Type.scheme_to_type
   let is_monomorphic = UnifPriv.Type.scheme_is_monomorphic
   let uvars          = UnifPriv.Type.scheme_uvars
   let collect_uvars  = UnifPriv.Type.collect_scheme_uvars
@@ -56,70 +57,22 @@ end
 module Subst = UnifPriv.Subst
 module BuiltinType = UnifPriv.BuiltinType
 
-type var = Var.t
-
-type data_def =
-  | DD_Data of
-    { tvar              : tvar;
-      proof             : var;
-      args              : named_tvar list;
-      ctors             : ctor_decl list;
-      strictly_positive : bool
-    }
-
-  | DD_Label of
-    { tvar      : tvar;
-      var       : var;
-      delim_tp  : typ;
-      delim_eff : effrow
-    }
-
-type pattern = pattern_data node
-and pattern_data =
-  | PWildcard
-  | PVar  of var * scheme
-  | PCtor of string * int * expr * ctor_decl list * tvar list * pattern list
-
-and expr = expr_data node
-and expr_data =
-  | EUnitPrf
-  | ENum        of int
-  | ENum64      of int64
-  | EStr        of string
-  | EChr        of char
-  | EVar        of var
-  | EPureFn     of var * scheme * expr
-  | EFn         of var * scheme * expr
-  | ETFun       of tvar * expr
-  | EApp        of expr * expr
-  | ETApp       of expr * typ
-  | ELet        of var * scheme * expr * expr
-  | 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 option
-  | EMatch      of expr * match_clause list * typ * effrow option
-  | 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
-  | EReplExpr   of expr * string * expr
-
-and rec_def = var * scheme * expr
-
-and match_clause = pattern * expr
-
-type program = expr
+include UnifPriv.Syntax
+
+module TypeExpr = struct
+  let to_type = UnifPriv.TypeExpr.to_type
+end
+
+module SchemeExpr = struct
+  let of_type_expr = UnifPriv.TypeExpr.mono_scheme_expr
+  let to_type_expr = UnifPriv.TypeExpr.of_scheme_expr
+  let to_scheme    = UnifPriv.TypeExpr.to_scheme
+end
+
+module NamedSchemeExpr = struct
+  let to_named_scheme = UnifPriv.TypeExpr.to_named_scheme
+end
+
+module CtorDeclExpr = struct
+  let to_ctor_decl = UnifPriv.TypeExpr.to_ctor_decl
+end
diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli
index e024e8b9..c6b75211 100644
--- a/src/Lang/Unif.mli
+++ b/src/Lang/Unif.mli
@@ -29,9 +29,6 @@ type tname =
   | TNAnon
     (** Anonymous parameter *)
 
-  | TNEffect
-    (** Effect variable associated with effect handler *)
-
   | TNVar of string
     (** Regular named type parameter *)
 
@@ -55,17 +52,20 @@ type name =
   | NMethod   of string
     (** Name of methods **)
 
+(* ========================================================================= *)
+
+(** Effects.
+
+  There are two effects in Unif. We only distinguish pure and impure
+  computations. Pure computations doesn't use any control-effects and
+  recursion, therefore they always terminate. *)
+type effect = Pure | Impure
+
 (** Types.
 
   This is an abstract type. Use [Type.view] to view it. *)
 type typ
 
-(** Effects. They are represented as types effect kind. Always ground. *)
-type effect = typ
-
-(** Effect rows. *)
-type effrow = typ
-
 (** Polymorphic type scheme *)
 type scheme = {
   sch_targs : named_tvar list;
@@ -81,9 +81,6 @@ type scheme = {
 (** Scheme with name *)
 and named_scheme = name * scheme
 
-(** Type substitution *)
-type subst
-
 (** Declaration of an ADT constructor *)
 type ctor_decl = {
   ctor_name        : string;
@@ -99,6 +96,106 @@ type ctor_decl = {
     (** Type schemes of the regular parameters *)
 }
 
+(** Type substitution *)
+type subst
+
+(* ========================================================================= *)
+(** Type expressions
+
+  Type expressions are used in a syntax, in contrast to types that are uses
+  in a type inference. Type expressions contain additional information about
+  location in the source code and effects. *)
+type type_expr = type_expr_data node
+and type_expr_data =
+  | TE_Type of typ
+    (** Placeholder for a type. It is used for representing a variable or a
+      type inferred during type inference, usually an unification variable *)
+
+  | TE_Effect of type_expr list
+    (** Effect. It is represented as a list of simpler effects. Empty list
+      is a pure effect. *)
+
+  | TE_PureArrow of scheme_expr * type_expr
+    (** Pure arrow *)
+
+  | TE_Arrow of scheme_expr * type_expr * type_expr
+    (** Impure arrow. The last parameter is an effect *)
+
+  | TE_Handler of (** First-class handler *)
+    { effect   : tvar;
+        (** Effect variable bound by this handler (it bound in [cap_type],
+          [in_type], and [in_eff] *)
+
+      cap_type : type_expr;
+        (** Type of a capability provided by this handler *)
+
+      in_type  : type_expr;
+        (** Inner type of a handler: a type of expression that can be run
+          inside this handler *)
+
+      in_eff   : type_expr;
+        (** Inner effect of a handler *)
+
+      out_type : type_expr;
+        (** Outer type of a handler: a type of the whole handler expression
+        *)
+
+      out_eff  : type_expr
+        (** Outer effect of a handler *)
+    }
+
+  | TE_Label of (** First-class label *)
+    { effect    : type_expr;
+        (** Effect of this label *)
+
+      delim_tp  : type_expr;
+        (** Type of the delimiter *)
+
+      delim_eff : type_expr
+        (** Effect of the delimiter *)
+    }
+
+  | TE_App of type_expr * type_expr
+    (** Type application *)
+
+  | TE_Option of type_expr
+    (** Implicitly introduced Option type (in optional parameter) *)
+
+(** Type-scheme expressions *)
+and scheme_expr = {
+  se_pos   : Position.t;
+    (** Location of the scheme expression *)
+
+  se_targs : named_tvar list;
+    (** Type parameters *)
+
+  se_named : named_scheme_expr list;
+    (** Named parameters *)
+
+  se_body  : type_expr
+    (** Body of the scheme *)
+}
+
+(** Named scheme expression *)
+and named_scheme_expr = name * scheme_expr
+
+(** Syntactic version of declaration of an ADT constructor *)
+type ctor_decl_expr = {
+  cde_name        : string;
+    (** Name of the constructor *)
+
+  cde_targs       : named_tvar list;
+    (** Existential type variables of the constructor *)
+
+  cde_named       : named_scheme_expr list;
+    (** Named parameters of the constructor *)
+
+  cde_arg_schemes : scheme_expr list
+    (** Type schemes of the regular parameters *)
+}
+
+(* ========================================================================= *)
+
 (** Variable *)
 type var = Var.t
 
@@ -115,7 +212,7 @@ type data_def =
       args  : named_tvar list;
         (** List of type parameters of this ADT. *)
 
-      ctors : ctor_decl list;
+      ctors : ctor_decl_expr list;
         (** List of constructors. *)
 
       strictly_positive : bool
@@ -131,10 +228,10 @@ type data_def =
       var       : var;
         (** Regular variable that would store the label *)
 
-      delim_tp  : typ;
+      delim_tp  : type_expr;
         (** Type of the delimiter *)
 
-      delim_eff : effrow
+      delim_eff : type_expr
         (** Effect of the delimiter *)
     }
 
@@ -149,10 +246,30 @@ and pattern_data =
   | PVar of var * scheme
     (** Pattern that binds a variable of given scheme *)
 
-  | PCtor of string * int * expr * ctor_decl list * tvar list * pattern list
+  | PCtor of string * int * expr * tvar list * pattern list * pattern list
     (** ADT constructor pattern. It stores a name, constructor index,
-      proof that matched type is an ADT, full list of constructor of an ADT,
-      existential type binders, and patterns for parameters. *)
+      proof that matched type is an ADT, existential type binders, patterns
+      for named parameters, and patterns for regular parameters. *)
+
+  | PAnnot of pattern * scheme_expr
+    (** Scheme annotated pattern *)
+
+(** Polymorphic expression *)
+and poly_expr = poly_expr_data node
+and poly_expr_data =
+  | EOptionPrf
+    (** The proof that Option is an ADT with None and Some constructors.
+      It expects a single type: the type of the Some parameter. *)
+
+  | EVar of var
+    (** Variable *)
+
+  | EPolyFun of tvar list * (var * scheme) list * expr
+    (** Polymorphic lambda abstraction. Always pure *)
+
+  | EHole of poly_expr option BRef.t
+    (** Placeholder for a polymorphic expression, to be filled by constraint
+      solving. *)
 
 (** Expression *)
 and expr = expr_data node
@@ -160,6 +277,9 @@ and expr_data =
   | EUnitPrf
     (** The proof that Unit is an ADT with only one constructor *)
 
+  | EInst of poly_expr * type_expr list * poly_expr list
+    (** Instantiation of polymorphic expression *)
+
   | ENum of int
     (** Integer literal *)
 
@@ -172,58 +292,55 @@ and expr_data =
   | EChr of char
     (** String literal *)
 
-  | EVar of var
-    (** Variable *)
-
   | EPureFn of var * scheme * expr
     (** Pure lambda-abstraction *)
 
   | EFn of var * scheme * expr
     (** Impure lambda-abstraction *)
 
-  | ETFun of tvar * expr
-    (** Type function *)
+  | EAppPoly of expr * poly_expr
+    (** Function application to polymorphic expression *)
 
-  | EApp of expr * expr
-    (** Function application *)
+  | EAppMono of expr * expr
+    (** Function application to regular, possibly effectful expression *)
 
-  | ETApp of expr * typ
-    (** Type application *)
+  | ELetPoly of var * poly_expr * expr
+    (** Polymorphic let-definition *)
 
-  | ELet of var * scheme * expr * expr
-    (** Let-definition *)
+  | ELetMono of var * expr * expr
+    (** Monomorphic let-definition *)
 
   | ELetRec of rec_def list * expr
     (** Mutually recursive let-definitions *)
 
-  | ECtor of expr * int * typ list * expr list
+  | ECtor of expr * int * typ list * poly_expr list * poly_expr list
     (** Fully-applied constructor of ADT. The meaning of the parameters
       is the following.
       - Computationally irrelevant proof that given that the type of the
         whole expression is an ADT.
       - An index of the constructor.
       - Existential type parameters of the constructor.
-      - Regular parameter of the constructor, including named and implicit. *)
+      - Named parameters of the constructor.
+      - Regular parameters of the constructor. *)
 
   | EData of data_def list * expr
     (** Definition of mutually recursive ADTs. *)
 
-  | EMatchEmpty of expr * expr * typ * effrow option
+  | EMatchEmpty of expr * expr * typ * effect
     (** 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. The last parameter is an optional effect of
-      the whole expression: [None] means that pattern-matching is pure. *)
+      parameter is an empty ADT. The last parameter is an effect of the whole
+      expression. *)
 
-  | EMatch of expr * match_clause list * typ * effrow option
+  | EMatch of expr * match_clause list * typ * effect
     (** 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
+  | EHandle of tvar * var * expr * expr
+    (** Handling construct. In [EHandle(a, x, 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 *)
 
@@ -237,9 +354,6 @@ and expr_data =
       delim_tp  : typ;
       (** Type of the delimiter *)
 
-      delim_eff : effect;
-      (** Effect of the delimiter *)
-
       cap_type  : typ;
       (** Type of the capability *)
 
@@ -271,17 +385,20 @@ and expr_data =
   | EExtern of string * typ
     (** Externally defined value *)
 
-  | ERepl of (unit -> expr) * typ * effrow
+  | EAnnot of expr * type_expr * type_expr
+    (** Expression explicitly annotated with a type and an effect. *)
+
+  | ERepl of (unit -> expr) * typ
     (** REPL. It is a function that prompts user for another input. It returns
       an expression to evaluate, usually containing another REPL expression.
-      This constructor stores also type and effect of a REPL expression. *)
+      *)
 
-  | EReplExpr of expr * string * expr
-    (** Print type (second parameter), evaluate and print the first expression,
-      then continue to the second expression. *)
+  | EReplExpr of expr * expr
+    (** Print the type of the first expression, evaluate and print the first
+      expression, then continue to the second expression. *)
 
 (** Definition of recursive value *)
-and rec_def = var * scheme * expr
+and rec_def = var * scheme * poly_expr
 
 (** Clause of a pattern matching *)
 and match_clause = pattern * expr
@@ -296,13 +413,8 @@ module KUVar : sig
   (** Check for equality *)
   val equal : kuvar -> kuvar -> bool
 
-  (** Set a unification variable. Returns false if given kind does not
-    satisfy non-effect constraints. *)
-  val set : kuvar -> kind -> bool
-
-  (** Set a unification variable. This function can be called only on
-    non-effect kinds *)
-  val set_safe : kuvar -> kind -> unit
+  (** Set a unification variable. *) 
+  val set : kuvar -> kind -> unit
 end
 
 (* ========================================================================= *)
@@ -314,12 +426,8 @@ module Kind : sig
       (** Kind of all types *)
 
     | KEffect
-      (** Kind of all (closed) effects. Closed effects cannot contain
-        unification variables. *)
+      (** Kind of all effects. *)
     
-    | KEffrow
-      (** Kind of all effect rows. *)
-
     | KUVar of kuvar
       (** Unification variable *)
 
@@ -329,44 +437,23 @@ module Kind : sig
   (** Kind of all types *)
   val k_type : kind
 
-  (** Kind of all (closed) effects. Closed effects cannot contain unification
-    variables. *)
+  (** Kind of all effects. *)
   val k_effect : kind
 
-  (** Kind of effect rows. Rows contain at most one unification variable or
-    type application. *)
-  val k_effrow : kind
-
-  (** Arrow kind. The result kind (the second parameter) must be non-effect
-    kind. *)
+  (** Arrow kind. *)
   val k_arrow : kind -> kind -> kind
 
   (** Create an arrow kind with multiple parameters. *)
   val k_arrows : kind list -> kind -> kind
 
-  (** Create a fresh unification kind variable. The optional [non_effect]
-    flag indicates whether this kind cannot be instantiated to effect kind.
-    The default value is false, i.e., this kind can be an effect kind. *)
-  val fresh_uvar : ?non_effect:bool -> unit -> kind
+  (** Create a fresh unification kind variable. *)
+  val fresh_uvar : unit -> kind
 
   (** Reveal a top-most constructor of a kind *)
   val view : kind -> kind_view
 
   (** Check if given kind contains given unification variable *)
   val contains_uvar : kuvar -> kind -> bool
-
-  (** Check if given kind cannot be effect kind, even if it is a unification
-    variable. The main purpose of this function is to use it in assert
-    statements. *)
-  val non_effect : kind -> bool
-
-  (** Check whether given kind is an effect kind (but not unification
-    variable). *)
-  val is_effect : kind -> bool
-
-  (** Add non-effect constraint to given kind. Returns true on success.
-    Returns false if given kind is an effect kind. *)
-  val set_non_effect : kind -> bool
 end
 
 (* ========================================================================= *)
@@ -464,9 +551,6 @@ module Name : sig
   (** Find value associated to given name on a list *)
   val assoc : name -> (name * 'a) list -> 'a option
 
-  (** Substitute in name *)
-  val subst : subst -> name -> name
-
   (** Finite sets of names *)
   module Set : Set.S with type elt = name
 
@@ -475,26 +559,23 @@ module Name : sig
 end
 
 (* ========================================================================= *)
-(** Operations on types *)
-module Type : sig
-  (** End of an effect *)
-  type effrow_end =
-    | EEClosed
-      (** Closed effect row *)
-    
-    | EEUVar of TVar.Perm.t * uvar
-      (** Open effect row with unification variable at the end. The unification
-        variable is associated with a delayed partial permutation of type
-        variables. *)
-
-    | EEVar of tvar
-      (** Open effect row with type variable at the end *)
+(** Operations on effects *)
+module Effect : sig
+  (** Join of two effects *)
+  val join : effect -> effect -> effect
 
-    | EEApp of typ * typ
-      (** Type application of an [effrow] kind *)
+  (** Join of multiple effects *)
+  val joins : effect list -> effect
+end
 
+(* ========================================================================= *)
+(** Operations on types *)
+module Type : sig
   (** View of a type *)
   type type_view =
+    | TEffect
+      (** Something of effect kind. In Unif all effects are equal *)
+
     | TUVar of TVar.Perm.t * uvar
       (** Unification variable, associated with a delayed partial permutation,
       of type variables. Mappings of variables not in scope of the
@@ -503,31 +584,18 @@ module Type : sig
     | TVar of tvar
       (** Regular type variable *)
 
-    | TEffect of TVar.Set.t
-      (** (Ground) effect *)
+    | TArrow of scheme * typ * effect
+      (** Effect annotated arrow *)
 
-    | TEffrow of TVar.Set.t * effrow_end
-      (** Effect: a set of simple effect variables together with a way of
-        closing an effect *)
-
-    | TPureArrow of scheme * typ
-      (** Pure arrow, i.e., type of function that doesn't perform any effects
-        and always terminate *)
-
-    | TArrow of scheme * typ * effrow
-      (** Impure arrow *)
-  
-    | THandler of tvar * typ * typ * effrow * typ * effect
-      (** First class handler. In [THandler(a, tp, itp, ieff, otp, oeff)]:
+    | THandler of tvar * typ * typ * typ
+      (** First class handler. In [THandler(a, tp, itp, otp)]:
         - [a] is a variable bound in [tp], [itp], and [ieff];
         - [tp] is a type of provided capability;
-        - [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. *)
+        - [itp] is a typ of handled expression.
+        - [otp] s a type of the whole handler. *)
   
-    | TLabel of effect * typ * effrow
-      (** Type of first-class label. It stores the effect of the label and
-        type and effect of the delimiter. *)
+    | TLabel of typ
+      (** Type of a first-class label. It stores the type of the delimiter. *)
 
     | TApp of typ * typ
       (** Type application *)
@@ -542,30 +610,30 @@ module Type : sig
 
   (** Weak head normal form of a type *)
   type whnf =
-    | Whnf_Neutral of neutral_head * typ list
-      (** Neutral type. Its parameters are in reversed order. *)
-
-    | Whnf_Effect  of effect
+    | Whnf_Effect
       (** Effect *)
 
-    | Whnf_Effrow of effrow
-      (** Effect rows *)
+    | Whnf_Neutral of neutral_head * typ list
+      (** Neutral type. Its parameters are in reversed order. *)
 
-    | Whnf_PureArrow of scheme * typ
-      (** Pure arrow *)
+    | Whnf_Arrow of scheme * typ * effect
+      (** Effect annotated arrow *)
   
-    | Whnf_Arrow of scheme * typ * effrow
-      (** Impure arrow *)
-  
-    | Whnf_Handler   of tvar * typ * typ * effrow * typ * effrow
+    | Whnf_Handler   of tvar * typ * typ * typ
       (** Handler type *)
 
-    | Whnf_Label of effect * typ * effrow
+    | Whnf_Label of typ
       (** Label type *)
 
+  (** Effect *)
+  val t_effect : typ
+
   (** Unit type *)
   val t_unit : typ
 
+  (** Option type *)
+  val t_option : typ -> typ
+
   (** Unification variable *)
   val t_uvar : TVar.Perm.t -> uvar -> typ
 
@@ -579,22 +647,13 @@ module Type : sig
   val t_pure_arrows : scheme list -> typ -> typ
 
   (** Arrow type *)
-  val t_arrow : scheme -> typ -> effrow -> typ
+  val t_arrow : scheme -> typ -> effect -> typ
 
   (** Type of first-class handlers *)
-  val t_handler : tvar -> typ -> typ -> effrow -> typ -> effrow -> typ
+  val t_handler : tvar -> typ -> typ -> typ -> typ
 
   (** Type of first-class label *)
-  val t_label : effect -> typ -> effrow -> typ
-
-  (** Create an effect *)
-  val t_effect : TVar.Set.t -> effect
-
-  (** Create an effect row *)
-  val t_effrow : TVar.Set.t -> effrow_end -> effrow
-
-  (** Create a closed effect row *)
-  val t_closed_effrow : TVar.Set.t -> effrow
+  val t_label : typ -> typ
 
   (** Type application *)
   val t_app : typ -> typ -> typ
@@ -611,26 +670,9 @@ module Type : sig
   (** Compute weak head normal form of a type *)
   val whnf : typ -> whnf
 
-  (** Reveal a representation of an effect: a set of effect variables. *)
-  val effect_view : effect -> TVar.Set.t
-
-  (** Reveal a representation of an effect row: a set of effect variables
-    together with a way of closing an effect row. *)
-  val effrow_view : effrow -> TVar.Set.t * effrow_end
-
   (** Get the kind of given type *)
   val kind : typ -> kind
 
-  (** Returns subtype of given type, where all closed rows on negative
-    positions are opened by a fresh unification variable. It works only
-    for proper types (of kind type) *)
-  val open_down : scope:scope -> typ -> typ
-
-  (** Returns supertype of given type, where all closed rows on positive
-    positions are opened by a fresh unification variable. It works only
-    for proper types (of kind type) *)
-  val open_up : scope:scope -> typ -> typ
-
   (** Check if given unification variable appears in given type. It is
     equivalent to [UVar.mem u (uvars tp)], but faster. *)
   val contains_uvar : uvar -> typ -> bool
@@ -651,71 +693,16 @@ module Type : sig
   val try_shrink_scope : scope:scope -> typ -> (unit, tvar) result
 end
 
-(* ========================================================================= *)
-(** Operations on effects *)
-module Effect : sig
-  (** View of effect row *)
-  type row_view =
-    | RPure
-      (** Pure effect row *)
-
-    | RUVar of TVar.Perm.t * uvar
-      (** Row unification variable (with delayed permutation) *)
-
-    | RVar  of tvar
-      (** Row variable *)
-
-    | RApp  of typ * typ
-      (** Type application of an [effrow] kind *)
-
-    | RCons of tvar * effrow
-      (** Consing an simple effect variable to an effect row *)
-
-  (** Pure effect row *)
-  val pure : effrow
-
-  (** Effect row with single IO effect *)
-  val io : effrow
-
-  (** Create a row that consists of single effect *)
-  val singleton_row : tvar -> effrow
-
-  (** Consing a single effect variable to an effect row *)
-  val cons : tvar -> effrow -> effrow
-
-  (** Consing an effect to an effect row *)
-  val cons_eff : effect -> effrow -> effrow
-
-  (** Row-like view of an effect row *)
-  val view : effrow -> row_view
-
-  (** View the end of given effect row. *) 
-  val view_end : effrow -> Type.effrow_end
-
-  (** Check if an effect row is pure *)
-  val is_pure : effrow -> bool
-end
-
-(* ========================================================================= *)
-(** Type substitutions *)
-module Subst : sig
-  (** Empty substitution *)
-  val empty : subst
-
-  (** Extend substitution with a renaming. The new version of a variable
-    must be fresh enough. *)
-  val rename_to_fresh : subst -> tvar -> tvar -> subst
-
-  (** Extend substitution. It is rather parallel extension than composition *)
-  val add_type : subst -> tvar -> typ -> subst
-end
-
 (* ========================================================================= *)
 (** Operations on type schemes *)
 module Scheme : sig
   (** Create a monomorphic type-scheme *)
   val of_type : typ -> scheme
 
+  (** Convert scheme to monomorphic type. Returns [None], when the scheme is
+    polymorphic. *)
+  val to_type : scheme -> typ option
+
   (** Check if given type-scheme is monomorphic *)
   val is_monomorphic : scheme -> bool
 
@@ -759,6 +746,20 @@ module CtorDecl : sig
   val strictly_positive : nonrec_scope:scope -> ctor_decl -> bool
 end
 
+(* ========================================================================= *)
+(** Type substitutions *)
+module Subst : sig
+  (** Empty substitution *)
+  val empty : subst
+
+  (** Extend substitution with a renaming. The new version of a variable
+    must be fresh enough. *)
+  val rename_to_fresh : subst -> tvar -> tvar -> subst
+
+  (** Extend substitution. It is rather parallel extension than composition *)
+  val add_type : subst -> tvar -> typ -> subst
+end
+
 (* ========================================================================= *)
 (** Built-in types *)
 module BuiltinType : sig
@@ -777,6 +778,47 @@ module BuiltinType : sig
   (** Unit type *)
   val tv_unit : tvar
 
+  (** Option type *)
+  val tv_option : tvar
+
+  (** IO effect *)
+  val tv_io : tvar
+
   (** List of all built-in types with their names *)
   val all : (string * tvar) list
 end
+
+(* ========================================================================= *)
+(** Type expressions *)
+module TypeExpr : sig
+  (** Convert to regular type *)
+  val to_type : type_expr -> typ
+end
+
+(* ========================================================================= *)
+(** Scheme expressions *)
+module SchemeExpr : sig
+  (** Create a monomorphic scheme expression *)
+  val of_type_expr : type_expr -> scheme_expr
+
+  (** Convert to monomorphic type expression. Returns [None] when the scheme
+    is polymorphic. *)
+  val to_type_expr : scheme_expr -> type_expr option
+
+  (** Convert to type-scheme *)
+  val to_scheme : scheme_expr -> scheme
+end
+
+(* ========================================================================= *)
+(** Named scheme expressions *)
+module NamedSchemeExpr : sig
+  (** Convert to named scheme *)
+  val to_named_scheme : named_scheme_expr -> named_scheme
+end
+
+(* ========================================================================= *)
+(** Syntactic constructor declarations *)
+module CtorDeclExpr : sig
+  (** Convert to constructor declarations *)
+  val to_ctor_decl : ctor_decl_expr -> ctor_decl
+end
diff --git a/src/Lang/UnifPriv/BuiltinType.ml b/src/Lang/UnifPriv/BuiltinType.ml
index 0aeb8eef..0e794b68 100644
--- a/src/Lang/UnifPriv/BuiltinType.ml
+++ b/src/Lang/UnifPriv/BuiltinType.ml
@@ -19,6 +19,9 @@ let tv_char = TVar.fresh KindBase.k_type
 (** Unit type *)
 let tv_unit = TVar.fresh KindBase.k_type
 
+(** Option type *)
+let tv_option = TVar.fresh (KindBase.k_arrow KindBase.k_type KindBase.k_type)
+
 (** IO effect *)
 let tv_io = TVar.fresh KindBase.k_effect
 
@@ -29,4 +32,5 @@ let all =
     "String", tv_string;
     "Char",   tv_char;
     "Unit",   tv_unit;
+    "Option", tv_option;
     "IO",     tv_io ]
diff --git a/src/Lang/UnifPriv/Effect.ml b/src/Lang/UnifPriv/Effect.ml
index 31991fcd..c6e5c30a 100644
--- a/src/Lang/UnifPriv/Effect.ml
+++ b/src/Lang/UnifPriv/Effect.ml
@@ -2,49 +2,13 @@
  * See LICENSE for details.
  *)
 
-(** Operations on effects and effect rows *)
+(** Operations on effects *)
 
 open TypeBase
 
-type row_view =
-  | RPure
-  | RUVar of TVar.Perm.t * uvar
-  | RVar  of tvar
-  | RApp  of typ * typ
-  | RCons of tvar * effrow
+let join eff1 eff2 =
+  match eff1 with
+  | Pure   -> eff2
+  | Impure -> Impure
 
-let pure = t_closed_effrow TVar.Set.empty
-
-let singleton_row x =
-  t_closed_effrow (TVar.Set.singleton x)
-
-let io = singleton_row BuiltinType.tv_io
-
-let cons x eff =
-  let (xs, ee) = effrow_view eff in
-  t_effrow (TVar.Set.add x xs) ee
-
-let cons_eff e eff =
-  let xs1 = effect_view e in
-  let (xs2, ee) = effrow_view eff in
-  t_effrow (TVar.Set.union xs1 xs2) ee
-
-let view eff =
-  let (xs, ee) = effrow_view eff in
-  match TVar.Set.choose_opt xs with
-  | Some x -> RCons(x, t_effrow (TVar.Set.remove x xs) ee)
-  | None ->
-    begin match ee with
-    | EEClosed -> RPure
-    | EEUVar(p, u) -> RUVar(p, u)
-    | EEVar x -> RVar x
-    | EEApp(tp1, tp2) -> RApp(tp1, tp2)
-    end
-
-let view_end eff =
-  snd (effrow_view eff)
-
-let is_pure eff =
-  match effrow_view eff with
-  | (xs, EEClosed) -> TVar.Set.is_empty xs
-  | _ -> false
+let joins effs = List.fold_left join Pure effs
diff --git a/src/Lang/UnifPriv/KindBase.ml b/src/Lang/UnifPriv/KindBase.ml
index 46732439..fc1f9f4d 100644
--- a/src/Lang/UnifPriv/KindBase.ml
+++ b/src/Lang/UnifPriv/KindBase.ml
@@ -4,103 +4,50 @@
 
 (** Kinds *)
 
-(** The state of kind unification variable *)
-type kuvar_state =
-  | KS_Any
-    (** This unification variable can be concretized to any kind *)
-
-  | KS_NonEffect
-    (** This unification variable cannot have an effect kind *)
-
-type kuvar = (kuvar_state, kind) Either.t BRef.t
+type kuvar = kind option BRef.t
 and kind = kind_view
 and kind_view =
   | KType
   | KEffect
-  | KEffrow
   | KUVar  of kuvar
   | KArrow of kind * kind
 
 let k_type = KType
 
 let k_effect = KEffect
-let k_effrow = KEffrow
+
+let k_arrow k1 k2 = KArrow(k1, k2)
+
+let k_arrows ks k = List.fold_right k_arrow ks k
 
 let rec view k =
   match k with
-  | KType | KEffect | KEffrow | KArrow _ -> k
+  | KType | KEffect | KArrow _ -> k
   | KUVar u ->
     begin match BRef.get u with
-    | Left _ -> k
-    | Right k ->
+    | None -> k
+    | Some k ->
       let k = view k in
-      BRef.set u (Right k);
+      BRef.set u (Some k);
       k
     end
 
-let non_effect k =
-  match view k with
-  | KType | KEffrow | KArrow _ -> true
-  | KEffect -> false
-  | KUVar u ->
-    begin match BRef.get u with
-    | Left KS_Any       -> false
-    | Left KS_NonEffect -> true
-    | Right _ -> assert false
-    end
-
-let is_effect k =
-  match view k with
-  | KEffect -> true
-  | _ -> false
-
-let set_non_effect k =
-  match view k with
-  | KType | KEffrow | KArrow _ -> true
-  | KEffect -> false
-  | KUVar u ->
-    begin match BRef.get u with
-    | Left KS_Any ->
-      BRef.set u (Left KS_NonEffect);
-      true
-    | Left KS_NonEffect -> true
-    | Right _ -> assert false
-    end
-
 module KUVar = struct
-  let fresh ~non_effect () =
-    BRef.create (Either.Left (if non_effect then KS_NonEffect else KS_Any))
+  let fresh () = BRef.create None
 
   let equal x y = x == y
 
   let set x k =
     match BRef.get x with
-    | Either.Left KS_Any ->
-      BRef.set x (Right k); true
-    | Either.Left KS_NonEffect ->
-      (** TODO: set backtracking point? *)
-      if set_non_effect k then
-        (BRef.set x (Right k); true)
-      else
-        false
-    | Either.Right _ -> assert false
-
-  let set_safe x k =
-    let r = set x k in
-    assert r
+    | None   -> BRef.set x (Some k)
+    | Some _ -> assert false
 end
 
-let fresh_uvar ?(non_effect=false) () = KUVar (KUVar.fresh ~non_effect ())
-
-let k_arrow k1 k2 =
-  assert (non_effect k2);
-  KArrow(k1, k2)
-
-let k_arrows ks k = List.fold_right k_arrow ks k
+let fresh_uvar () = KUVar (KUVar.fresh ())
 
 let rec contains_uvar x k =
   match view k with
-  | KType | KEffect | KEffrow -> false
+  | KType | KEffect -> false
   | KUVar u -> KUVar.equal x u
   | KArrow(k1, k2) ->
     contains_uvar x k1 || contains_uvar x k2
diff --git a/src/Lang/UnifPriv/KindBase.mli b/src/Lang/UnifPriv/KindBase.mli
index 2869bf09..765da064 100644
--- a/src/Lang/UnifPriv/KindBase.mli
+++ b/src/Lang/UnifPriv/KindBase.mli
@@ -11,30 +11,23 @@ type kind
 type kind_view =
   | KType
   | KEffect
-  | KEffrow
   | KUVar  of kuvar
   | KArrow of kind * kind
 
 (** Kind of all types *)
 val k_type : kind
 
-(** Kind of all (closed) effects. Closed effects cannot contain unification
-  variables. *)
+(** Kind of all effects *)
 val k_effect : kind
 
-(** Kind of effect rows. Rows contain at most one unification variable or
-  type application. *)
-val k_effrow : kind
-
-(** Arrow kind. The result kind (the second parameter) must be non-effect
-  kind. *)
+(** Arrow kind *)
 val k_arrow : kind -> kind -> kind
 
 (** Create an arrow kind with multiple parameters. *)
 val k_arrows : kind list -> kind -> kind
 
 (** Create a fresh unification kind variable *)
-val fresh_uvar : ?non_effect:bool -> unit -> kind
+val fresh_uvar : unit -> kind
 
 (** Reveal a top-most constructor of a kind *)
 val view : kind -> kind_view
@@ -42,24 +35,9 @@ val view : kind -> kind_view
 (** Check if given kind contains given unification variable *)
 val contains_uvar : kuvar -> kind -> bool
 
-(** Check if given kind cannot be effect kind, even if it is a unification
-  variable. The main purpose of this function is to use it in assert
-  statements. *)
-val non_effect : kind -> bool
-
-(** Check whether given kind is an effect kind (but not unification
-  variable). *)
-val is_effect : kind -> bool
-
-(** Add non-effect constraint to given kind. Returns true on success.
-  Returns false if given kind is an effect kind. *)
-val set_non_effect : kind -> bool
-
 (** Operations on kind unification variables *)
 module KUVar : sig
   val equal : kuvar -> kuvar -> bool
 
-  val set : kuvar -> kind -> bool
-
-  val set_safe : kuvar -> kind -> unit
+  val set : kuvar -> kind -> unit
 end
diff --git a/src/Lang/UnifPriv/Name.ml b/src/Lang/UnifPriv/Name.ml
index dfeabcf7..22f14018 100644
--- a/src/Lang/UnifPriv/Name.ml
+++ b/src/Lang/UnifPriv/Name.ml
@@ -50,7 +50,5 @@ let equal n1 n2 =
 let assoc n xs =
   List.find_map (fun (m, v) -> if equal n m then Some v else None) xs
 
-let subst = Subst.in_name
-
 module Set = Set.Make(Ordered)
 module Map = Map.Make(Ordered)
diff --git a/src/Lang/UnifPriv/Subst.ml b/src/Lang/UnifPriv/Subst.ml
index e5db863e..f9434dcb 100644
--- a/src/Lang/UnifPriv/Subst.ml
+++ b/src/Lang/UnifPriv/Subst.ml
@@ -51,35 +51,9 @@ let in_uvar sub p u =
     (fun x -> not (TVar.Map.mem (TVar.Perm.apply p x) sub.sub));
   p
 
-let in_name sub n =
-  match n with
-  | NLabel | NVar _ | NOptionalVar _ | NImplicit _ | NMethod _ -> n
-
-(* Substitute in variable of kind [effect]. Since kind [effect] can contain
-  only ground effects, substituted type is always (in some sense) a set of
-  type variables. These type variables are added to a set [ys]. *)
-let in_effvar sub x ys =
-  let x = TVar.Perm.apply sub.perm x in
-  match TVar.Map.find_opt x sub.sub with
-  | None     -> TVar.Set.add x ys
-  | Some eff -> TVar.Set.union (effect_view eff) ys
-
-let rec in_effrow_end sub ee =
-  match ee with
-  | EEClosed -> (TVar.Set.empty, ee)
-  | EEUVar(p, u) ->
-    (TVar.Set.empty, EEUVar(in_uvar sub p u, u))
-  | EEVar x  ->
-    let x = TVar.Perm.apply sub.perm x in
-    begin match TVar.Map.find_opt x sub.sub with
-    | None     -> (TVar.Set.empty, EEVar x)
-    | Some eff -> effrow_view eff
-    end
-  | EEApp(tp1, tp2) ->
-    (TVar.Set.empty, EEApp(in_type_rec sub tp1, in_type_rec sub tp2))
-
-and in_type_rec sub tp =
+let rec in_type_rec sub tp =
   match TypeBase.view tp with
+  | TEffect -> tp
   | TUVar(p, u) ->
     let p = in_uvar sub p u in
     t_uvar p u
@@ -89,39 +63,26 @@ and in_type_rec sub tp =
     | None    -> t_var x
     | Some tp -> tp
     end
-  | TEffect xs ->
-    t_effect (TVar.Set.fold (in_effvar sub) xs TVar.Set.empty)
-  | TEffrow(xs, ee) ->
-    let (ys, ee) = in_effrow_end sub ee in
-    t_effrow (TVar.Set.fold (in_effvar sub) xs ys) ee
-  | TPureArrow(sch, tp2) ->
-    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, itp, ieff, otp, oeff) ->
+    t_arrow (in_scheme_rec sub sch) (in_type_rec sub tp2) eff
+  | THandler(a, tp, itp, otp) ->
     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 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)
+    t_handler a (in_type_rec sub tp) (in_type_rec sub itp) otp
+  | TLabel tp0 ->
+    t_label (in_type_rec sub tp0)
   | TApp(tp1, tp2) ->
     t_app (in_type_rec sub tp1) (in_type_rec sub tp2)
 
 and in_scheme_rec sub sch =
   let (sub, tvars) = add_named_tvars sub sch.sch_targs in
-  let named = List.map (in_named_scheme_rec sub) sch.sch_named in
   { sch_targs = tvars;
-    sch_named = named;
+    sch_named = List.map (in_named_scheme_rec sub) sch.sch_named;
     sch_body  = in_type_rec sub sch.sch_body
   }
 
 and in_named_scheme_rec sub (n, sch) =
-  (in_name sub n, in_scheme_rec sub sch)
+  (n, in_scheme_rec sub sch)
 
 let in_type sub tp =
   if is_empty sub then tp
diff --git a/src/Lang/UnifPriv/Subst.mli b/src/Lang/UnifPriv/Subst.mli
index 94298e67..ed7d61cd 100644
--- a/src/Lang/UnifPriv/Subst.mli
+++ b/src/Lang/UnifPriv/Subst.mli
@@ -26,9 +26,6 @@ val add_named_tvars : t -> named_tvar list -> t * named_tvar list
 (** Extend substitution *)
 val add_type : t -> tvar -> typ -> t
 
-(** Substitute in name *)
-val in_name : t -> name -> name
-
 (** Substitute in type *)
 val in_type : t -> typ -> typ
 
diff --git a/src/Lang/UnifPriv/Syntax.ml b/src/Lang/UnifPriv/Syntax.ml
new file mode 100644
index 00000000..f054833b
--- /dev/null
+++ b/src/Lang/UnifPriv/Syntax.ml
@@ -0,0 +1,122 @@
+(* This file is part of DBL, released under MIT license.
+ * See LICENSE for details.
+ *)
+
+(** Syntax of the Unif Language. *)
+
+open SyntaxNode
+open TypeBase
+
+type type_expr = type_expr_data node
+and type_expr_data =
+  | TE_Type      of typ
+  | TE_Effect    of type_expr list
+  | TE_PureArrow of scheme_expr * type_expr
+  | TE_Arrow     of scheme_expr * type_expr * type_expr
+  | TE_Handler   of
+    { effect   : tvar;
+      cap_type : type_expr;
+      in_type  : type_expr;
+      in_eff   : type_expr;
+      out_type : type_expr;
+      out_eff  : type_expr
+    }
+  | TE_Label of
+    { effect    : type_expr;
+      delim_tp  : type_expr;
+      delim_eff : type_expr
+    }
+  | TE_App    of type_expr * type_expr
+  | TE_Option of type_expr
+
+and scheme_expr = {
+  se_pos   : Position.t;
+  se_targs : named_tvar list;
+  se_named : named_scheme_expr list;
+  se_body  : type_expr
+}
+
+and named_scheme_expr = name * scheme_expr
+
+type ctor_decl_expr = {
+  cde_name        : string;
+  cde_targs       : named_tvar list;
+  cde_named       : named_scheme_expr list;
+  cde_arg_schemes : scheme_expr list
+}
+
+(* ========================================================================= *)
+type var = Var.t
+
+type data_def =
+  | DD_Data of
+    { tvar  : tvar;
+      proof : var;
+      args  : named_tvar list;
+      ctors : ctor_decl_expr list;
+      strictly_positive : bool
+    }
+  | DD_Label of
+    { tvar      : tvar;
+      var       : var;
+      delim_tp  : type_expr;
+      delim_eff : type_expr
+    }
+
+type pattern = pattern_data node
+and pattern_data =
+  | PWildcard
+  | PVar   of var * scheme
+  | PCtor  of string * int * expr * tvar list * pattern list * pattern list
+  | PAnnot of pattern * scheme_expr
+
+and poly_expr = poly_expr_data node
+and poly_expr_data =
+  | EOptionPrf
+  | EVar     of var
+  | EPolyFun of tvar list * (var * scheme) list * expr
+  | EHole    of poly_expr option BRef.t
+
+and expr = expr_data node
+and expr_data =
+  | EUnitPrf
+  | EInst       of poly_expr * type_expr list * poly_expr list
+  | ENum        of int
+  | ENum64      of int64
+  | EStr        of string
+  | EChr        of char
+  | EPureFn     of var * scheme * expr
+  | EFn         of var * scheme * expr
+  | EAppPoly    of expr * poly_expr
+  | EAppMono    of expr * expr
+  | ELetPoly    of var * poly_expr * expr
+  | ELetMono    of var * expr * expr
+  | ELetRec     of rec_def list * expr
+  | ECtor       of expr * int * typ list * poly_expr list * poly_expr list
+  | EData       of data_def list * expr
+  | EMatchEmpty of expr * expr * typ * effect
+  | EMatch      of expr * match_clause list * typ * effect
+  | EHandle     of tvar * var * expr * expr
+  | EHandler    of
+    { label     : var;
+      effect    : tvar;
+      delim_tp  : typ;
+      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
+  | EAnnot      of expr * type_expr * type_expr
+  | ERepl       of (unit -> expr) * typ
+  | EReplExpr   of expr * expr
+
+and rec_def = var * scheme * poly_expr
+
+and match_clause = pattern * expr
+
+type program = expr
diff --git a/src/Lang/UnifPriv/Type.ml b/src/Lang/UnifPriv/Type.ml
index c8830ba1..207022cb 100644
--- a/src/Lang/UnifPriv/Type.ml
+++ b/src/Lang/UnifPriv/Type.ml
@@ -12,117 +12,45 @@ let fresh_uvar ~scope kind = t_uvar TVar.Perm.id (UVar.fresh ~scope kind)
 
 let t_unit = t_var BuiltinType.tv_unit
 
-let t_pure_arrows tps tp = List.fold_right t_pure_arrow tps tp
+let t_option tp = t_app (t_var BuiltinType.tv_option) tp
+
+let t_pure_arrow sch tp = t_arrow sch tp Pure
+
+let t_pure_arrows schs tp = List.fold_right t_pure_arrow schs tp
 
 let t_apps tp tps = List.fold_left t_app tp tps
 
 let rec kind tp =
   match view tp with
+  | TEffect     -> KindBase.k_effect
   | TUVar(_, u) -> UVar.kind u
   | TVar      x -> TVar.kind x
-  | TEffect   _ -> KindBase.k_effect
-  | TEffrow   _ -> KindBase.k_effrow
-  | TPureArrow _ | TArrow _ | THandler _ | TLabel _ -> KindBase.k_type
+  | TArrow _ | THandler _ | TLabel _ -> KindBase.k_type
   | TApp(tp, _) ->
     begin match KindBase.view (kind tp) with
     | KArrow(_, k) -> k
-    | KType | KEffect | KEffrow | KUVar _ ->
+    | KType | KEffect | KUVar _ ->
       failwith "Internal kind error"
     end
 
 let refresh_scheme sch =
   let (sub, tvars) = Subst.add_named_tvars Subst.empty sch.sch_targs in
-  let ims =
-    List.map
-      (fun (name, isch) -> (Subst.in_name sub name, Subst.in_scheme sub isch))
-      sch.sch_named
-  in
   { sch_targs = tvars;
-    sch_named = ims;
+    sch_named = List.map (Subst.in_named_scheme sub) sch.sch_named;
     sch_body  = Subst.in_type sub sch.sch_body
   }
 
-let open_effrow_up ~scope eff =
-  let (xs, ee) = effrow_view eff in
-  match ee with
-  | EEClosed ->
-    t_effrow xs (EEUVar(TVar.Perm.id, UVar.fresh ~scope KindBase.k_effrow))
-  | EEUVar _ | EEVar _ | EEApp _ -> eff
-
-let rec open_down ~scope tp =
-  match view tp with
-  | TUVar _ | TVar _ | TLabel _ | TApp _ -> tp
-  | TPureArrow(sch, tp2) ->
-    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, 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"
-
-and open_scheme_down ~scope sch =
-  let sch = refresh_scheme sch in
-  let scope = List.fold_left Scope.add_named scope sch.sch_targs in
-  { sch_targs = sch.sch_targs;
-    sch_named =
-      List.map (fun (name, isch) -> (name, open_scheme_up ~scope isch))
-        sch.sch_named;
-    sch_body  = open_down ~scope sch.sch_body
-  }
-
-and open_up ~scope tp =
-  match view tp with
-  | TUVar _ | TVar _ | TLabel _ | TApp _ -> tp
-  | TPureArrow(sch, tp2) ->
-    t_pure_arrow (open_scheme_down ~scope sch) (open_up ~scope tp2)
-  | TArrow(sch, tp2, eff) ->
-    t_arrow
-      (open_scheme_down ~scope sch)
-      (open_up          ~scope tp2)
-      (open_effrow_up   ~scope eff)
-  | 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"
-
-and open_scheme_up ~scope sch =
-  let sch = refresh_scheme sch in
-  let scope = List.fold_left Scope.add_named scope sch.sch_targs in
-  { sch_targs = sch.sch_targs;
-    sch_named =
-      List.map (fun (name, isch) -> (name, open_scheme_down ~scope isch))
-        sch.sch_named;
-    sch_body   = open_up ~scope sch.sch_body
-  }
-
 let rec contains_uvar u tp =
   match view tp with
-  | TVar _ | TEffect _ | TEffrow(_, (EEClosed | EEVar _)) -> false
-  | TUVar(_, u') | TEffrow(_, EEUVar(_, u')) -> UVar.equal u u'
-  | TPureArrow(sch, tp2) ->
+  | TEffect | TVar _ -> false
+  | TUVar(_, u') -> UVar.equal u u'
+  | TArrow(sch, tp2, _) ->
     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, 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) ->
+  | THandler(_, tp, itp, otp) ->
+    contains_uvar u tp || contains_uvar u itp || contains_uvar u otp
+  | TLabel tp0 ->
+    contains_uvar u tp0
+  | TApp(tp1, tp2) ->
     contains_uvar u tp1 || contains_uvar u tp2
 
 and scheme_contains_uvar u sch =
@@ -131,23 +59,18 @@ and scheme_contains_uvar u sch =
 
 let rec collect_uvars tp uvs =
   match view tp with
-  | TVar _ | TEffect _ | TEffrow(_, (EEClosed | EEVar _)) -> uvs
-  | TUVar(_, u) | TEffrow(_, EEUVar(_, u)) -> UVar.Set.add u uvs
-  | TEffrow(_, EEApp(tp1, tp2)) | TApp(tp1, tp2) ->
-    collect_uvars tp1 (collect_uvars tp2 uvs)
-  | TPureArrow(sch, tp2) ->
+  | TEffect | TVar _ -> uvs
+  | TUVar(_, u) -> UVar.Set.add u uvs
+  | TArrow(sch, tp2, _) ->
     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, itp, ieff, otp, oeff) ->
+  | THandler(_, tp, itp, otp) ->
     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))
+  | TLabel tp0 -> collect_uvars tp0 uvs
+  | TApp(tp1, tp2) ->
+    collect_uvars tp1 (collect_uvars tp2 uvs)
 
 and collect_scheme_uvars sch uvs =
   let uvs =
@@ -180,42 +103,20 @@ let shrink_uvar_scope ~scope p u =
   UVar.filter_scope u (Scope.level scope)
     (fun x -> Scope.mem scope (TVar.Perm.apply p x))
 
-let rec shrink_effrow_end_scope ~scope ee =
-  match ee with
-  | EEClosed -> ()
-  | EEUVar(p, u) -> shrink_uvar_scope ~scope p u
-  | EEVar  x -> shrink_var_scope ~scope x
-  | EEApp(tp1, tp2) ->
-    shrink_scope ~scope tp1;
-    shrink_scope ~scope tp2
-
-and shrink_scope ~scope tp =
+let rec shrink_scope ~scope tp =
   match view tp with
+  | TEffect -> ()
   | TUVar(p, u) -> shrink_uvar_scope ~scope p u
   | TVar  x -> shrink_var_scope  ~scope x
-  | TEffect xs ->
-    TVar.Set.iter (shrink_var_scope ~scope) xs
-  | TEffrow(xs, ee) ->
-    TVar.Set.iter (shrink_var_scope ~scope) xs;
-    shrink_effrow_end_scope ~scope ee
-  | TPureArrow(sch, tp2) ->
+  | TArrow(sch, tp2, _) ->
     shrink_scheme_scope ~scope sch;
     shrink_scope ~scope tp2
-  | TArrow(sch, tp2, eff) ->
-    shrink_scheme_scope ~scope sch;
-    shrink_scope ~scope tp2;
-    shrink_scope ~scope eff
-  | THandler(a, tp, itp, ieff, otp, oeff) ->
+  | THandler(a, tp, itp, otp) ->
     shrink_scope ~scope otp;
-    shrink_scope ~scope oeff;
     let scope = Scope.add scope a in
     shrink_scope ~scope tp;
-    shrink_scope ~scope itp;
-    shrink_scope ~scope ieff
-  | TLabel(eff, tp0, eff0) ->
-    shrink_scope ~scope eff;
-    shrink_scope ~scope tp0;
-    shrink_scope ~scope eff0
+    shrink_scope ~scope itp
+  | TLabel tp0 -> shrink_scope ~scope tp0
   | TApp(tp1, tp2) ->
     shrink_scope ~scope tp1;
     shrink_scope ~scope tp2
@@ -227,7 +128,6 @@ and shrink_scheme_scope ~scope sch =
   shrink_scope ~scope sch.sch_body
 
 let try_shrink_scope ~scope tp =
-  (* TODO: set backtracking point *)
   match shrink_scope ~scope tp with
   | () -> Ok ()
   | exception Escapes_scope x -> Error x
@@ -243,39 +143,20 @@ let uvar_fits_in_scope ~scope p u =
   given scope *)
 let rec fits_in_scope ~scope tp =
   match view tp with
+  | TEffect     -> true
   | 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) ->
+  | TArrow(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) ->
+  | THandler(x, tp, itp, otp) ->
     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
+      fits_in_scope ~scope itp
     end
-  | TLabel(eff0, tp, eff) ->
-    fits_in_scope ~scope eff0 &&
-    fits_in_scope ~scope tp &&
-    fits_in_scope ~scope eff
+  | TLabel tp0 -> fits_in_scope ~scope tp0
   | TApp(tp1, tp2) ->
     fits_in_scope ~scope tp1 && fits_in_scope ~scope tp2
 
@@ -288,34 +169,28 @@ 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 *)
+  scopes of unification variables fit in given scope. This function ignores
+  effects, because effect-handling always has NTerm effect. *)
 let rec strictly_positive ~nonrec_scope tp =
   match view tp with
-  | TUVar(p, u) | TEffrow(_, EEUVar(p, u)) ->
+  | TEffect | TVar _ -> true
+  | TUVar(p, u) ->
     uvar_fits_in_scope ~scope:nonrec_scope p u
-  | TVar _ | TEffect _ | TEffrow(_, (EEClosed | EEVar _)) ->
-    true
-  | TPureArrow(sch, tp) ->
+  | TArrow(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) ->
+  | THandler(x, tp, itp, otp) ->
     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
+      fits_in_scope ~scope itp
     end
   | TLabel _ ->
     fits_in_scope ~scope:nonrec_scope tp
-  | TApp(tp1, tp2) | TEffrow(_, EEApp(tp1, tp2)) ->
+  | TApp(tp1, tp2) ->
     strictly_positive ~nonrec_scope tp1 &&
     fits_in_scope ~scope:nonrec_scope tp2
 
@@ -345,7 +220,12 @@ let mono_scheme tp =
     sch_body  = tp
   }
 
-let scheme_is_monomorphic sch =
+let scheme_to_type sch =
   match sch with
-  | { sch_targs = []; sch_named = []; sch_body = _ } -> true
-  | _ -> false
+  | { sch_targs = []; sch_named = []; sch_body } -> Some sch_body
+  | _ -> None
+
+let scheme_is_monomorphic sch =
+  match scheme_to_type sch with
+  | Some _ -> true
+  | None   -> false
diff --git a/src/Lang/UnifPriv/TypeBase.ml b/src/Lang/UnifPriv/TypeBase.ml
index 31860076..ae1e8e06 100644
--- a/src/Lang/UnifPriv/TypeBase.ml
+++ b/src/Lang/UnifPriv/TypeBase.ml
@@ -11,7 +11,6 @@ type scope = Scope.t
 
 type tname =
   | TNAnon
-  | TNEffect
   | TNVar of string
 
 type named_tvar = tname * tvar
@@ -23,6 +22,8 @@ type name =
   | NImplicit    of string
   | NMethod      of string
 
+type effect = Pure | Impure
+
 type uvar = {
   uid   : UID.t;
   kind  : kind;
@@ -35,24 +36,14 @@ and uvar_state =
   | UV_Type of typ
 
 and typ = type_view
-and effect = typ
-and effrow = typ
 and type_view =
-  | TUVar      of TVar.Perm.t * uvar
-  | TVar       of tvar
-  | TEffect    of TVar.Set.t
-  | TEffrow    of TVar.Set.t * effrow_end
-  | TPureArrow of scheme * typ
-  | TArrow     of scheme * typ * effrow
-  | THandler   of tvar * typ * typ * effrow * typ * effrow
-  | TLabel     of effect * typ * effrow
-  | TApp       of typ * typ
-
-and effrow_end =
-  | EEClosed
-  | EEUVar of TVar.Perm.t * uvar
-  | EEVar  of tvar
-  | EEApp  of typ * typ
+  | TEffect
+  | TUVar    of TVar.Perm.t * uvar
+  | TVar     of tvar
+  | TArrow   of scheme * typ * effect
+  | THandler of tvar * typ * typ * typ
+  | TLabel   of typ
+  | TApp     of typ * typ
 
 and scheme = {
   sch_targs : named_tvar list;
@@ -69,30 +60,20 @@ type ctor_decl = {
   ctor_arg_schemes : scheme list
 }
 
+let t_effect = TEffect
+
 let t_uvar p u = TUVar(Scope.shrink_perm_dom (BRef.get u.scope) p, u)
 
 let t_var x = TVar x
 
-let t_effect xs = TEffect xs
-
-let t_effrow xs ee = TEffrow(xs, ee)
-
-let t_closed_effrow xs =  TEffrow(xs, EEClosed)
-
-let t_pure_arrow sch tp2 = TPureArrow(sch, tp2)
-
 let t_arrow sch tp2 eff = TArrow(sch, tp2, eff)
 
-let t_handler a tp itp ieff otp oeff = THandler(a, tp, itp, ieff, otp, oeff)
+let t_handler a tp itp otp = THandler(a, tp, itp, otp)
 
-let t_label eff tp0 eff0 = TLabel(eff, tp0, eff0)
+let t_label tp0 = TLabel tp0
 
 let t_app tp1 tp2 = TApp(tp1, tp2)
 
-let perm_name p n =
-  match n with
-  | NLabel | NVar _ | NOptionalVar _ | NImplicit _ | NMethod _ -> n
-
 let perm_named_tvar p (n, x) =
   (n, TVar.Perm.apply p x)
 
@@ -107,20 +88,7 @@ let rec view tp =
       BRef.set u.state (UV_Type tp);
       perm p tp
     end
-  | TEffrow(xs, EEUVar(p, u)) ->
-    begin match view (TUVar(p, u)) with
-    | TUVar(p, u) -> TEffrow(xs, EEUVar(p, u))
-    | TVar x  -> TEffrow(xs, EEVar x)
-    | TApp(tp1, tp2) -> TEffrow(xs, EEApp(tp1, tp2))
-    | TEffrow(ys, ee) -> TEffrow(TVar.Set.union xs ys, ee)
-
-    | TEffect _ | TPureArrow _ | TArrow _ | THandler _ | TLabel _ ->
-      failwith "Internal kind error"
-    end
-  | TEffrow(xs, ee) -> tp
-
-  | TVar _ | TEffect _ | TPureArrow _ | TArrow _ | THandler _
-  | TLabel _ | TApp _ -> tp
+  | TEffect | TVar _ | TArrow _ | THandler _ | TLabel _ | TApp _ -> tp
 
 and perm p tp =
   if TVar.Perm.is_identity p then tp
@@ -128,36 +96,20 @@ and perm p tp =
 
 and perm_rec p tp =
   match view tp with
+  | TEffect -> TEffect
   | TUVar(p', u) ->
     let p = TVar.Perm.compose p p' in
     TUVar(Scope.shrink_perm_dom (BRef.get u.scope) p, u)
   | TVar x -> TVar (TVar.Perm.apply p x)
-  | TEffect xs ->
-    TEffect (TVar.Perm.map_set p xs)
-  | TEffrow(xs, ee) ->
-    TEffrow(TVar.Perm.map_set p xs, perm_effrow_end_rec p ee)
-  | TPureArrow(sch, tp2) ->
-    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, itp, ieff, otp, oeff) ->
+    TArrow(perm_scheme_rec p sch, perm_rec p tp2, eff)
+  | THandler(a, tp, itp, otp) ->
     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)
+      perm_rec p itp, perm_rec p otp)
+  | TLabel tp0 -> TLabel (perm_rec p tp0)
   | TApp(tp1, tp2) ->
     TApp(perm_rec p tp1, perm_rec p tp2)
 
-and perm_effrow_end_rec p ee =
-  match ee with
-  | EEClosed -> EEClosed
-  | EEUVar(p', u) ->
-    let p = TVar.Perm.compose p p' in
-    EEUVar(Scope.shrink_perm_dom (BRef.get u.scope) p, u)
-  | EEVar x -> EEVar (TVar.Perm.apply p x)
-  | EEApp(tp1, tp2) ->
-    EEApp(perm_rec p tp1, perm_rec p tp2)
-
 and perm_scheme_rec p sch =
   { sch_targs = List.map (perm_named_tvar p) sch.sch_targs;
     sch_named = List.map (perm_named_scheme_rec p) sch.sch_named;
@@ -165,28 +117,7 @@ and perm_scheme_rec p sch =
   }
 
 and perm_named_scheme_rec p (n, sch) =
-  (perm_name p n, perm_scheme_rec p sch)
-
-let effect_view eff =
-  match view eff with
-  | TVar x     -> TVar.Set.singleton x
-  | TEffect xs -> xs
-
-  | TUVar _ | TApp _ -> assert false
-
-  | TEffrow _ | TPureArrow _ | TArrow _ | THandler _ | TLabel _ ->
-    failwith "Internal kind error"
-
-let effrow_view eff =
-  match view eff with
-  | TUVar(p, u)    -> (TVar.Set.empty, EEUVar(p, u))
-  | TVar  x        -> (TVar.Set.empty, EEVar x)
-  | TApp(tp1, tp2) -> (TVar.Set.empty, EEApp(tp1, tp2))
-
-  | TEffrow(xs, ee) -> (xs, ee)
-
-  | TEffect _ | TPureArrow _ | TArrow _ | THandler _ | TLabel _ ->
-    failwith "Internal kind error"
+  (n, perm_scheme_rec p sch)
 
 module UVar = struct
   module Ordered = struct
@@ -196,7 +127,6 @@ module UVar = struct
   include Ordered
 
   let fresh ~scope kind =
-    assert (KindBase.non_effect kind);
     { uid   = UID.fresh ();
       kind  = kind;
       state = BRef.create UV_UVar;
diff --git a/src/Lang/UnifPriv/TypeBase.mli b/src/Lang/UnifPriv/TypeBase.mli
index 7f9c38b5..60697f41 100644
--- a/src/Lang/UnifPriv/TypeBase.mli
+++ b/src/Lang/UnifPriv/TypeBase.mli
@@ -12,7 +12,6 @@ type scope = Scope.t
 
 type tname =
   | TNAnon
-  | TNEffect
   | TNVar of string
 
 type named_tvar = tname * tvar
@@ -24,27 +23,18 @@ type name =
   | NImplicit    of string
   | NMethod      of string
 
-type typ
-
-type effect = typ
-type effrow = typ
+type effect = Pure | Impure
 
-type effrow_end =
-  | EEClosed
-  | EEUVar of TVar.Perm.t * uvar
-  | EEVar  of tvar
-  | EEApp  of typ * typ
+type typ
 
 type type_view =
-  | TUVar      of TVar.Perm.t * uvar
-  | TVar       of tvar
-  | TEffect    of TVar.Set.t
-  | TEffrow    of TVar.Set.t * effrow_end
-  | TPureArrow of scheme * typ
-  | TArrow     of scheme * typ * effrow
-  | THandler   of tvar * typ * typ * effrow * typ * effrow
-  | TLabel     of effect * typ * effrow
-  | TApp       of typ * typ
+  | TEffect
+  | TUVar    of TVar.Perm.t * uvar
+  | TVar     of tvar
+  | TArrow   of scheme * typ * effect
+  | THandler of tvar * typ * typ * typ
+  | TLabel   of typ
+  | TApp     of typ * typ
 
 and scheme = {
   sch_targs : named_tvar list;
@@ -61,32 +51,23 @@ type ctor_decl = {
   ctor_arg_schemes : scheme list
 }
 
+(** Effect *)
+val t_effect : typ
+
 (** Unification variable *)
 val t_uvar : TVar.Perm.t -> uvar -> typ
 
 (** Regular type variable *)
 val t_var : tvar -> typ
 
-(** Pure arrow type *)
-val t_pure_arrow : scheme -> typ -> typ
-
 (** Arrow type *)
-val t_arrow : scheme -> typ -> effrow -> typ
+val t_arrow : scheme -> typ -> effect -> typ
 
 (** Type of first-class handlers *)
-val t_handler : tvar -> typ -> typ -> effrow -> typ -> effrow -> typ
+val t_handler : tvar -> typ -> typ -> typ -> typ
 
 (** Type of first-class label *)
-val t_label : effect -> typ -> effrow -> typ
-
-(** Create an effect *)
-val t_effect : TVar.Set.t -> effect
-
-(** Create an effect row *)
-val t_effrow : TVar.Set.t -> effrow_end -> effrow
-
-(** Create a closed effect row *)
-val t_closed_effrow : TVar.Set.t -> effrow
+val t_label : typ -> typ
 
 (** Type application *)
 val t_app : typ -> typ -> typ
@@ -94,13 +75,6 @@ val t_app : typ -> typ -> typ
 (** Reveal a top-most constructor of a type *)
 val view : typ -> type_view
 
-(** Reveal a representation of an effect: a set of effect variables *)
-val effect_view : effect -> TVar.Set.t
-
-(** Reveal a representation of an effect row: a set of effect variables
-  together with a way of closing an effect row. *)
-val effrow_view : effrow -> TVar.Set.t * effrow_end
-
 (** Operations on unification variables *)
 module UVar : sig
   type t = uvar
diff --git a/src/Lang/UnifPriv/TypeExpr.ml b/src/Lang/UnifPriv/TypeExpr.ml
new file mode 100644
index 00000000..f01332ea
--- /dev/null
+++ b/src/Lang/UnifPriv/TypeExpr.ml
@@ -0,0 +1,55 @@
+(* This file is part of DBL, released under MIT license.
+ * See LICENSE for details.
+ *)
+
+(** Operations on type expressions *)
+
+open TypeBase
+open Type
+open Syntax
+
+let rec to_type (tp : type_expr) =
+  match tp.data with
+  | TE_Type tp  -> tp
+  | TE_Effect _ -> t_effect
+  | TE_PureArrow(sch, tp) ->
+    t_pure_arrow (to_scheme sch) (to_type tp)
+  | TE_Arrow(sch, tp, _) ->
+    t_arrow (to_scheme sch) (to_type tp) Impure
+  | TE_Handler
+    { effect; cap_type; in_type; in_eff = _; out_type; out_eff = _ } ->
+    t_handler effect (to_type cap_type) (to_type in_type) (to_type out_type)
+  | TE_Label lbl ->
+    t_label (to_type lbl.delim_tp)
+  | TE_App(tp1, tp2) ->
+    t_app (to_type tp1) (to_type tp2)
+  | TE_Option tp ->
+    t_option (to_type tp)
+
+and to_scheme (sch : scheme_expr) =
+  { sch_targs = sch.se_targs;
+    sch_named = List.map to_named_scheme sch.se_named;
+    sch_body  = to_type sch.se_body
+  }
+
+and to_named_scheme (name, sch) =
+  (name, to_scheme sch)
+
+let to_ctor_decl (cde : ctor_decl_expr) =
+  { ctor_name  = cde.cde_name;
+    ctor_targs = cde.cde_targs;
+    ctor_named = List.map to_named_scheme cde.cde_named;
+    ctor_arg_schemes = List.map to_scheme cde.cde_arg_schemes
+  }
+
+let mono_scheme_expr (tp : type_expr) =
+  { se_pos   = tp.pos;
+    se_targs = [];
+    se_named = [];
+    se_body  = tp
+  }
+
+let of_scheme_expr (sch : scheme_expr) =
+  match sch with
+  | { se_pos = _; se_targs = []; se_named = []; se_body } -> Some se_body
+  | _ -> None
diff --git a/src/Lang/UnifPriv/TypeWhnf.ml b/src/Lang/UnifPriv/TypeWhnf.ml
index 8620704c..a69f2030 100644
--- a/src/Lang/UnifPriv/TypeWhnf.ml
+++ b/src/Lang/UnifPriv/TypeWhnf.ml
@@ -11,31 +11,26 @@ type neutral_head =
   | NH_Var  of tvar
 
 type whnf =
-  | Whnf_Neutral   of neutral_head * typ list
+  | Whnf_Effect
+  | Whnf_Neutral of neutral_head * typ list
       (* Arguments are in reversed order! *)
-  | Whnf_Effect    of effect
-  | Whnf_Effrow    of effrow
-  | Whnf_PureArrow of scheme * typ
-  | Whnf_Arrow     of scheme * typ * effrow
-  | Whnf_Handler   of tvar * typ * typ * effrow * typ * effrow
-  | Whnf_Label     of effect * typ * effrow
+  | Whnf_Arrow of scheme * typ * effect
+  | Whnf_Handler   of tvar * typ * typ * typ
+  | Whnf_Label of typ
 
 let rec whnf tp =
   match view tp with
+  | TEffect     -> Whnf_Effect
   | TUVar(p, u) -> Whnf_Neutral(NH_UVar(p, u), [])
   | TVar x      -> Whnf_Neutral(NH_Var x, [])
-  | TEffect _   -> Whnf_Effect tp
-  | TEffrow _   -> Whnf_Effrow tp
-  | TPureArrow(sch, tp) -> Whnf_PureArrow(sch, tp)
   | TArrow(sch, tp, eff) -> Whnf_Arrow(sch, tp, eff)
-  | THandler(a, tp, itp, ieff, otp, oeff) ->
-    Whnf_Handler(a, tp, itp, ieff, otp, oeff)
-  | TLabel(eff, tp0, eff0)     -> Whnf_Label(eff, tp0, eff0)
+  | THandler(a, tp, itp, otp) ->
+    Whnf_Handler(a, tp, itp, otp)
+  | TLabel tp0 -> Whnf_Label tp0
   | TApp(tp1, tp2) ->
     begin match whnf tp1 with
     | Whnf_Neutral(h, args) -> Whnf_Neutral(h, tp2 :: args)
 
-    | Whnf_Effect _ | Whnf_Effrow _ | Whnf_PureArrow _
-    | Whnf_Arrow _ | Whnf_Handler _ | Whnf_Label _ ->
+    | Whnf_Effect | Whnf_Arrow _ | Whnf_Handler _ | Whnf_Label _ ->
       failwith "Internal kind error"
     end
diff --git a/src/ToCore/Common.ml b/src/ToCore/Common.ml
index a4e53226..1ed7cd2f 100644
--- a/src/ToCore/Common.ml
+++ b/src/ToCore/Common.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Common definitions of the translation *)
-
+(*
 module S = Lang.Unif
 module T = Lang.Core
 
@@ -32,3 +32,4 @@ let v_unit_prf =
 
 let v_unit =
   T.VCtor(T.EValue v_unit_prf, 0, [], [])
+*)
diff --git a/src/ToCore/DataType.ml b/src/ToCore/DataType.ml
index 54ddf023..3fc31df0 100644
--- a/src/ToCore/DataType.ml
+++ b/src/ToCore/DataType.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Translation of datatype definitions from Unif to Core *)
-
+(*
 open Common
 
 (** Half-translated data-like definition *)
@@ -89,3 +89,4 @@ let finalize_data_def env (dd : data_def) =
 let tr_data_defs env dds =
   let (env, dds) = List.fold_left_map prepare_data_def env dds in
   (env, List.map (finalize_data_def env) dds)
+*)
diff --git a/src/ToCore/DataType.mli b/src/ToCore/DataType.mli
index a83c17e5..7c805a7d 100644
--- a/src/ToCore/DataType.mli
+++ b/src/ToCore/DataType.mli
@@ -3,8 +3,9 @@
  *)
 
 (** Translation of datatype definitions from Unif to Core *)
-
+(*
 open Common
 
 (** Translate a list of mutually recursive datatype definitions *)
 val tr_data_defs : Env.t -> S.data_def list -> Env.t * T.data_def list
+*)
diff --git a/src/ToCore/Env.ml b/src/ToCore/Env.ml
index abb61ef7..4e0b77bc 100644
--- a/src/ToCore/Env.ml
+++ b/src/ToCore/Env.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Environment of the translation *)
-
+(*
 open Common
 
 type t =
@@ -43,3 +43,4 @@ let lookup_tvar env x =
     failwith "Internal error: unbound type variable"
 
 let in_repl_mode env = env.repl_mode
+*)
diff --git a/src/ToCore/Env.mli b/src/ToCore/Env.mli
index 13eef409..723ec09d 100644
--- a/src/ToCore/Env.mli
+++ b/src/ToCore/Env.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Environment of the translation *)
-
+(*
 open Common
 
 type t
@@ -28,3 +28,4 @@ val add_tvars' : t -> S.tvar list -> T.TVar.ex list -> t
 val lookup_tvar : t -> S.tvar -> T.TVar.ex
 
 val in_repl_mode : t -> bool
+*)
diff --git a/src/ToCore/Error.ml b/src/ToCore/Error.ml
index 15bae904..06b07605 100644
--- a/src/ToCore/Error.ml
+++ b/src/ToCore/Error.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Reporting errors that may occur during the translation from Unif to Core *)
-
+(*
 type t = Position.t * string
 
 let fatal (pos, msg) =
@@ -15,3 +15,4 @@ let non_exhaustive_match ~pos ctx =
   let msg = Printf.sprintf
     "This pattern-matching is not exhaustive."
   in (pos, msg)
+*)
diff --git a/src/ToCore/Error.mli b/src/ToCore/Error.mli
index 7908111e..c5c9d857 100644
--- a/src/ToCore/Error.mli
+++ b/src/ToCore/Error.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Reporting errors that may occur during the translation from Unif to Core *)
-
+(*
 (** Abstract representation of error *)
 type t
 
@@ -11,3 +11,4 @@ type t
 val fatal : t -> 'a
 
 val non_exhaustive_match : pos:Position.t -> PatternContext.ctx -> t
+*)
diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml
index 166797a6..eae98b42 100644
--- a/src/ToCore/Main.ml
+++ b/src/ToCore/Main.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Main module of a translation from Unif to Core *)
-
+(*
 open Common
 
 (** Translate expression *)
@@ -172,6 +172,7 @@ and tr_rec_def env (x, sch, body) =
   | _ -> failwith "Internal error: non-productive recursive definition"
 
 (* ========================================================================= *)
-
+*)
 let tr_program ~repl_mode p =
-  tr_expr (Env.empty ~repl_mode) p
+  (* tr_expr (Env.empty ~repl_mode) p *)
+  failwith "not implemeted: ToCore.Main.tr_program"
diff --git a/src/ToCore/PatternContext.ml b/src/ToCore/PatternContext.ml
index 9bc95d81..79263362 100644
--- a/src/ToCore/PatternContext.ml
+++ b/src/ToCore/PatternContext.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Building counterexample of non-matched value in pattern-matching *)
-
+(*
 open Common
 
 (** Example of not-matched pattern *)
@@ -95,3 +95,4 @@ let focus_with ctx ex =
   match try_focus ctx ex with
   | Some ctx -> ctx
   | None     -> refocus_with ctx ex
+*)
diff --git a/src/ToCore/PatternMatch.ml b/src/ToCore/PatternMatch.ml
index 1f139e28..725ff9b7 100644
--- a/src/ToCore/PatternMatch.ml
+++ b/src/ToCore/PatternMatch.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Translation of pattern-matching *)
-
+(*
 open Common
 open PatternContext
 
@@ -293,3 +293,4 @@ let tr_single_match ~pos ~env ~tr_expr v cls tp eff =
   end)
   in
   M.tr_single_match env v cls
+*)
diff --git a/src/ToCore/PatternMatch.mli b/src/ToCore/PatternMatch.mli
index 69b0bdf3..fc6d17ed 100644
--- a/src/ToCore/PatternMatch.mli
+++ b/src/ToCore/PatternMatch.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Translation of pattern-matching *)
-
+(*
 open Common
 
 (** Translate a pattern-matching of a single value.
@@ -13,3 +13,4 @@ val tr_single_match :
   pos:Position.t -> env:Env.t ->
   tr_expr:(Env.t -> S.expr -> T.expr) ->
   T.value -> S.match_clause list -> T.ttype -> T.effect -> T.expr
+*)
diff --git a/src/ToCore/Type.ml b/src/ToCore/Type.ml
index 0f465ad1..dc06a483 100644
--- a/src/ToCore/Type.ml
+++ b/src/ToCore/Type.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Translation of types *)
-
+(*
 open Common
 
 let eff_cons env x eff =
@@ -141,3 +141,4 @@ 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 3fbdfe3b..0e0afdc1 100644
--- a/src/TypeInference/Common.ml
+++ b/src/TypeInference/Common.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Common definitions of type-checker *)
-
+(*
 module S = Lang.Surface
 module T = Lang.Unif
 
@@ -60,3 +60,4 @@ 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 788550f6..c5e06779 100644
--- a/src/TypeInference/DataType.ml
+++ b/src/TypeInference/DataType.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Checking and processing algebraic data types (ADTs) *)
-
+(*
 open Common
 
 type ctor_decl_list = (S.is_public * T.ctor_decl) list
@@ -69,3 +69,4 @@ let finalize_check ~nonrec_scope env x ~name args ctors =
       strictly_positive = info.adt_strictly_positive
     } in
   (env, dd)
+*)
diff --git a/src/TypeInference/DataType.mli b/src/TypeInference/DataType.mli
index 04ee264e..a004cb9a 100644
--- a/src/TypeInference/DataType.mli
+++ b/src/TypeInference/DataType.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Checking and processing algebraic data types (ADTs) *)
-
+(*
 open Common
 
 (** Internal represenation of list of constructors. *)
@@ -33,3 +33,4 @@ 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 0984cf32..e9dde3b1 100644
--- a/src/TypeInference/Def.ml
+++ b/src/TypeInference/Def.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for definitions *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -291,3 +291,4 @@ let check_defs : type dir. tcfix:tcfix ->
   | def :: defs ->
     check_def env ienv def req eff
       { run = fun env ienv req eff -> check_defs env ienv defs req eff cont }
+*)
diff --git a/src/TypeInference/Def.mli b/src/TypeInference/Def.mli
index 388b5e77..1988f89f 100644
--- a/src/TypeInference/Def.mli
+++ b/src/TypeInference/Def.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for definitions *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -22,3 +22,4 @@ val check_defs : tcfix:tcfix ->
   Env.t -> ImplicitEnv.t -> S.def list ->
     (T.typ, 'dir) request -> T.effrow -> def_cont ->
       T.expr * (T.typ, 'dir) response * ret_effect
+*)
diff --git a/src/TypeInference/Env.ml b/src/TypeInference/Env.ml
index 06512709..ed978b04 100644
--- a/src/TypeInference/Env.ml
+++ b/src/TypeInference/Env.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Environment of the type inference *)
-
+(*
 open Common
 
 module StrMap = Map.Make(String)
@@ -237,3 +237,4 @@ let leave_module env ~public name =
 
 let open_module env ~public m =
   { env with mod_stack = ModStack.open_module env.mod_stack ~public m }
+*)
diff --git a/src/TypeInference/Env.mli b/src/TypeInference/Env.mli
index 3d5d1d6d..c3b33d8b 100644
--- a/src/TypeInference/Env.mli
+++ b/src/TypeInference/Env.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Environment of the type inference *)
-
+(*
 open Common
 
 type t
@@ -152,3 +152,4 @@ val leave_module : t -> public:bool -> S.module_name -> t
 (** Introduce the given module's identifiers into scope with visibility
   specified by [~public]. *)
 val open_module : t -> public:bool -> Module.t -> t
+*)
diff --git a/src/TypeInference/Error.ml b/src/TypeInference/Error.ml
index e6e864da..f33f36ce 100644
--- a/src/TypeInference/Error.ml
+++ b/src/TypeInference/Error.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Reporting errors related to type-inference. *)
-
+(*
 type t = Position.t * string * (Position.t * string) list
 
 let report_note (pos, msg) =
@@ -509,3 +509,4 @@ let invalid_whnf_form ~pos ~env tp =
     "Got invalid whnf form when converting type %s"
     (Pretty.type_to_string pp_ctx env tp)
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+*)
diff --git a/src/TypeInference/Error.mli b/src/TypeInference/Error.mli
index f8b2b195..63dc1528 100644
--- a/src/TypeInference/Error.mli
+++ b/src/TypeInference/Error.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Reporting errors related to type-inference. *)
-
+(*
 open Common
 
 (** Abstract representation of error *)
@@ -149,3 +149,4 @@ val redundant_named_type : pos:Position.t -> T.tname -> t
 val redundant_named_parameter : pos:Position.t -> T.name -> t
 val redundant_named_pattern : pos:Position.t -> T.name -> t
 val invalid_whnf_form : pos:Position.t -> env:Env.t -> T.typ -> t
+*)
diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml
index 61c2de5b..ca9caf9e 100644
--- a/src/TypeInference/Expr.ml
+++ b/src/TypeInference/Expr.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for expressions and related syntactic categories *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -367,3 +367,4 @@ let check_expr_type ~tcfix env (e : S.expr) tp eff =
 
   | ERepl def_seq ->
     (check_repl_def_seq ~tcfix env ImplicitEnv.empty def_seq tp eff, Impure)
+*)
diff --git a/src/TypeInference/Expr.mli b/src/TypeInference/Expr.mli
index 4b4c9f41..0007af6c 100644
--- a/src/TypeInference/Expr.mli
+++ b/src/TypeInference/Expr.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for expressions and related syntactic categories *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -17,3 +17,4 @@ val infer_expr_type : tcfix:tcfix ->
   the purity of an expression. *)
 val check_expr_type : tcfix:tcfix ->
   Env.t -> S.expr -> T.typ -> T.effrow -> T.expr * ret_effect
+*)
diff --git a/src/TypeInference/ExprUtils.ml b/src/TypeInference/ExprUtils.ml
index c1cb314e..7b504ab9 100644
--- a/src/TypeInference/ExprUtils.ml
+++ b/src/TypeInference/ExprUtils.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Utility functions that help to build Unif expressions *)
-
+(*
 open Common
 
 (** Make function that takes parameters of given type schemes *)
@@ -204,3 +204,4 @@ let rec inst_args_match ims body tp eff =
     let (x, body)   = arg_match pat body tp eff in
     let (ims, body) = inst_args_match ims body tp eff in
     ((name, x, x_sch) :: ims, body)
+*)
diff --git a/src/TypeInference/ExprUtils.mli b/src/TypeInference/ExprUtils.mli
index ba200956..7088b644 100644
--- a/src/TypeInference/ExprUtils.mli
+++ b/src/TypeInference/ExprUtils.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Utility functions that help to build Unif expressions *)
-
+(*
 open Common
 
 (** Make polymorphic function with given type parameters *)
@@ -64,3 +64,4 @@ val arg_match :
 val inst_args_match :
   (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/ImplicitEnv.ml b/src/TypeInference/ImplicitEnv.ml
index e38c62ff..42ad03e8 100644
--- a/src/TypeInference/ImplicitEnv.ml
+++ b/src/TypeInference/ImplicitEnv.ml
@@ -4,7 +4,7 @@
 
 (** Additional environment used in type-checking definition blocks. It stores
   information about declared named implicits. *)
-
+(*
 open Common
 
 type t = (S.iname * T.named_tvar list * T.scheme) list (* in reversed order *)
@@ -143,3 +143,4 @@ let add_poly_id ~pos env ienv (id : S.ident) sch =
 
 let add_mono_id ~pos env ienv (id : S.ident) tp =
   add_poly_id ~pos env ienv id (T.Scheme.of_type tp)
+*)
diff --git a/src/TypeInference/ImplicitEnv.mli b/src/TypeInference/ImplicitEnv.mli
index 99cde13b..0f4782e1 100644
--- a/src/TypeInference/ImplicitEnv.mli
+++ b/src/TypeInference/ImplicitEnv.mli
@@ -4,7 +4,7 @@
 
 (** Additional environment used in type-checking definition blocks. It stores
   information about declared named implicits. *)
-
+(*
 open Common
 
 type t
@@ -53,3 +53,4 @@ val add_poly_id :
   it will be shadowed in implicit environment. *)
 val add_mono_id :
   pos:Position.t -> Env.t -> t -> S.ident -> T.typ -> Env.t * t * T.var
+*)
diff --git a/src/TypeInference/Main.ml b/src/TypeInference/Main.ml
index d2a045df..85ef6d0b 100644
--- a/src/TypeInference/Main.ml
+++ b/src/TypeInference/Main.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Main module of a type inference *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -22,9 +22,11 @@ module rec TCFix : TCFix = struct
   let check_defs env ienv defs tp_req eff cont =
     Def.check_defs ~tcfix:(module TCFix) env ienv defs tp_req eff cont
 end
-
+*)
 let tr_program p =
+(*
   let (p, _) =
     TCFix.check_expr_type Env.empty p T.Type.t_unit T.Effect.io in
   InterpLib.Error.assert_no_error ();
-  p
+  p *)
+  failwith "not implemented: TypeInference.Main.tr_program"
diff --git a/src/TypeInference/MatchClause.ml b/src/TypeInference/MatchClause.ml
index 2ca61e88..1b2a7c9b 100644
--- a/src/TypeInference/MatchClause.ml
+++ b/src/TypeInference/MatchClause.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for match clauses and related constructs *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -80,3 +80,4 @@ let tr_opt_clauses (type md rd) ~tcfix ~pos env
     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 9929d60c..047d9174 100644
--- a/src/TypeInference/MatchClause.mli
+++ b/src/TypeInference/MatchClause.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for match clauses and related constructs *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -42,3 +42,4 @@ val tr_opt_clauses : tcfix:tcfix -> pos:Position.t ->
   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/ModStack.ml b/src/TypeInference/ModStack.ml
index cd02aab8..b594ae0c 100644
--- a/src/TypeInference/ModStack.ml
+++ b/src/TypeInference/ModStack.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Stack of modules which are currently being defined *)
-
+(*
 open Common
 
 module StrMap = Map.Make(String)
@@ -73,3 +73,4 @@ let leave_module (old_top, stack) ~public name =
 
 let open_module (top, stack) ~public m =
   (Module.open_module top ~public m, stack)
+*)
diff --git a/src/TypeInference/ModStack.mli b/src/TypeInference/ModStack.mli
index cc54147c..77b9cb10 100644
--- a/src/TypeInference/ModStack.mli
+++ b/src/TypeInference/ModStack.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Stack of modules which are currently being defined *)
-
+(*
 open Common
 
 type t
@@ -63,3 +63,4 @@ val leave_module : t -> public:bool -> S.module_name -> t
 (** Introduce the given module's identifiers into scope with visibility
   specified by [~public]. *)
 val open_module : t -> public:bool -> Module.t -> t
+*)
diff --git a/src/TypeInference/Module.ml b/src/TypeInference/Module.ml
index 68a049cf..2b0b8d24 100644
--- a/src/TypeInference/Module.ml
+++ b/src/TypeInference/Module.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Represention of module definitions *)
-
+(*
 open Common
 
 module StrMap = Map.Make(String)
@@ -166,3 +166,4 @@ let open_module m ~public m' =
     ctor_map     = StrMap.union combine m.ctor_map     m'.ctor_map;
     mod_map      = StrMap.union combine m.mod_map      m'.mod_map
   }
+*)
diff --git a/src/TypeInference/Module.mli b/src/TypeInference/Module.mli
index cf84eeb2..53e68e19 100644
--- a/src/TypeInference/Module.mli
+++ b/src/TypeInference/Module.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Represention of module definitions *)
-
+(*
 open Common
 
 type t
@@ -103,3 +103,4 @@ val filter_public : t -> t
 (** Introduce the given module's identifiers into scope with visibility
   specified by [~public]. *)
 val open_module : t -> public:bool -> t -> t
+*)
diff --git a/src/TypeInference/Name.ml b/src/TypeInference/Name.ml
index f100ea70..c710093c 100644
--- a/src/TypeInference/Name.ml
+++ b/src/TypeInference/Name.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Translation of names of named parameters *)
-
+(*
 open Common
 
 let tr_tname (name : S.tname) =
@@ -19,3 +19,4 @@ let tr_name env (name : S.name) =
   | NOptionalVar x -> T.NOptionalVar x
   | NImplicit n    -> T.NImplicit n
   | NMethod   n    -> T.NMethod   n 
+*)
diff --git a/src/TypeInference/Name.mli b/src/TypeInference/Name.mli
index a2242e79..39c0e1fb 100644
--- a/src/TypeInference/Name.mli
+++ b/src/TypeInference/Name.mli
@@ -3,9 +3,10 @@
  *)
 
 (** Translation of names of named parameters *)
-
+(*
 open Common
 
 val tr_tname : S.tname -> T.tname
 
 val tr_name : Env.t -> S.name -> T.name
+*)
diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml
index fa3b3a98..8ca9fe2d 100644
--- a/src/TypeInference/Pattern.ml
+++ b/src/TypeInference/Pattern.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for patterns *)
-
+(*
 open Common
 
 type named_type    = (T.tname * S.type_arg) S.node
@@ -415,3 +415,4 @@ let rec infer_named_arg_schemes env ims =
     let (env, im, r_eff1)  = infer_named_arg_scheme env im in
     let (env, ims, r_eff2) = infer_named_arg_schemes env ims in
     (env, im :: ims, ret_effect_join r_eff1 r_eff2)
+*)
diff --git a/src/TypeInference/Pattern.mli b/src/TypeInference/Pattern.mli
index 2dded9ca..2e2da8d3 100644
--- a/src/TypeInference/Pattern.mli
+++ b/src/TypeInference/Pattern.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for patterns *)
-
+(*
 open Common
 
 (** Check if given pattern fits in given scope and has given type.
@@ -35,3 +35,4 @@ val check_arg_scheme :
 val infer_named_arg_schemes :
   Env.t -> S.named_arg list ->
     Env.t * (T.name * T.pattern * T.scheme) list * ret_effect
+*)
diff --git a/src/TypeInference/PolyExpr.ml b/src/TypeInference/PolyExpr.ml
index 270d0f0f..6b3404de 100644
--- a/src/TypeInference/PolyExpr.ml
+++ b/src/TypeInference/PolyExpr.ml
@@ -4,7 +4,7 @@
 
 (** Scheme-inference for polymorphic expressions and related constructs:
   actual parameters, and explicit instantiations. *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -185,3 +185,4 @@ let rec check_explicit_insts ~tcfix
     let ctx e0 = make (T.ELet(x, sch, e, ctx e0)) in
     let insts = (n, make (T.EVar x)) :: insts in
     (ctx, insts, ret_effect_join r_eff1 r_eff2)
+*)
diff --git a/src/TypeInference/PolyExpr.mli b/src/TypeInference/PolyExpr.mli
index 1210c083..0e74cf8c 100644
--- a/src/TypeInference/PolyExpr.mli
+++ b/src/TypeInference/PolyExpr.mli
@@ -4,7 +4,7 @@
 
 (** Scheme-inference for polymorphic expressions and related constructs:
   actual parameters, and explicit instantiations. *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -42,3 +42,4 @@ val check_explicit_insts : tcfix:tcfix ->
   Env.t ->
   T.named_scheme list -> S.inst list -> TypeHints.inst_cache -> T.effrow ->
     simple_context * (T.name * T.expr) list * ret_effect
+*)
diff --git a/src/TypeInference/PreludeTypes.ml b/src/TypeInference/PreludeTypes.ml
index f88172b6..04e2b1d9 100644
--- a/src/TypeInference/PreludeTypes.ml
+++ b/src/TypeInference/PreludeTypes.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Functions allowing the use of some of the types defined in the Prelude. *)
-
+(*
 open Common
 
 let mk_Option ~env ~pos tp_arg =
@@ -65,3 +65,4 @@ let mk_None ~env ~pos option_tp : T.expr =
       | 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/PreludeTypes.mli b/src/TypeInference/PreludeTypes.mli
index 56801bb8..e8ffc513 100644
--- a/src/TypeInference/PreludeTypes.mli
+++ b/src/TypeInference/PreludeTypes.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Functions allowing the use of some of the types defined in the Prelude. *)
-
+(*
 open Common
 
 (** Create an Option type fed with the given argument type *)
@@ -17,3 +17,4 @@ val mk_Some : env:Env.t -> pos:Position.t -> T.typ -> T.expr -> T.expr
 
 (** Create None constructor of given Option type *)
 val mk_None : env:Env.t -> pos:Position.t -> T.typ -> T.expr
+*)
diff --git a/src/TypeInference/Pretty.ml b/src/TypeInference/Pretty.ml
index d4b309a8..1b2f9c16 100644
--- a/src/TypeInference/Pretty.ml
+++ b/src/TypeInference/Pretty.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Pretty printing of types and kinds *)
-
+(*
 open Common
 
 type ctx = {
@@ -431,3 +431,4 @@ let scheme_to_string ctx env sch =
   let buf = Buffer.create 80 in
   pp_scheme buf (PPEnv.create ctx env) 0 sch;
   Buffer.contents buf
+*)
diff --git a/src/TypeInference/Pretty.mli b/src/TypeInference/Pretty.mli
index ef072c05..a3337965 100644
--- a/src/TypeInference/Pretty.mli
+++ b/src/TypeInference/Pretty.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Pretty printing of types and kinds *)
-
+(*
 open Common
 
 (** Contexts of pretty-printing *)
@@ -30,3 +30,4 @@ val scheme_to_string : ctx -> Env.t -> T.scheme -> string
 (** Pretty-print additional information about printing context, e.g.,
   locations of binders of anonymous types. *)
 val additional_info : ctx -> string
+*)
diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml
index 45949507..69c39bb9 100644
--- a/src/TypeInference/RecDefs.ml
+++ b/src/TypeInference/RecDefs.ml
@@ -1,7 +1,7 @@
 (* This file is part of DBL, released under MIT license.
  * See LICENSE for details.
  *)
-
+(*
 (** Type-inference for recursive definitions *)
 
 open Common
@@ -466,3 +466,4 @@ let check_rec_defs ~tcfix env ienv defs =
   let (env, ienv, fds) = add_rec_funs env ienv tvars ims fds in
   let fds = List.map (finalize_rec_fun fds) fds in
   (env, dds, fds, r_eff)
+*)
diff --git a/src/TypeInference/RecDefs.mli b/src/TypeInference/RecDefs.mli
index 9028e370..2bedce32 100644
--- a/src/TypeInference/RecDefs.mli
+++ b/src/TypeInference/RecDefs.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Type-inference for recursive definitions *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -14,3 +14,4 @@ open TypeCheckFix
 val check_rec_defs : tcfix:tcfix ->
   Env.t -> ImplicitEnv.t -> S.def list ->
     Env.t * T.data_def list * T.rec_def list * ret_effect
+*)
diff --git a/src/TypeInference/Type.ml b/src/TypeInference/Type.ml
index 9ea199db..dafd8cbd 100644
--- a/src/TypeInference/Type.ml
+++ b/src/TypeInference/Type.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Kind-checking and translation of type expressions *)
-
+(*
 open Common
 
 let rec tr_kind_expr (k : Lang.Surface.kind_expr) = 
@@ -203,3 +203,4 @@ let check_type_inst env targs (inst : S.type_inst) =
 
 let check_type_insts env tinst targs =
   List.filter_map (check_type_inst env targs) tinst
+*)
diff --git a/src/TypeInference/Type.mli b/src/TypeInference/Type.mli
index 96dc70c9..63be200a 100644
--- a/src/TypeInference/Type.mli
+++ b/src/TypeInference/Type.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Kind-checking and translation of type expressions *)
-
+(*
 open Common
 
 (** Check kind and translate a type expression *)
@@ -38,3 +38,4 @@ val tr_named_scheme : Env.t -> S.named_scheme -> T.named_scheme
   matter). *)
 val check_type_insts :
   Env.t -> S.type_inst list -> T.named_tvar list -> (T.tname * T.typ) list
+*)
diff --git a/src/TypeInference/TypeCheckFix.ml b/src/TypeInference/TypeCheckFix.ml
index 832db82b..9c902794 100644
--- a/src/TypeInference/TypeCheckFix.ml
+++ b/src/TypeInference/TypeCheckFix.ml
@@ -4,7 +4,7 @@
 
 (** Signatures of mutually recursive functions defined across several
   modules. *)
-
+(*
 open Common
 
 (** Type of continuation used to type-checking of definitions. It is defined
@@ -53,3 +53,4 @@ module type TCFix = sig
 end
 
 type tcfix = (module TCFix)
+*)
diff --git a/src/TypeInference/TypeHints.ml b/src/TypeInference/TypeHints.ml
index a9197919..82e029f7 100644
--- a/src/TypeInference/TypeHints.ml
+++ b/src/TypeInference/TypeHints.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Extraction of type hints *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -109,3 +109,4 @@ let extract_implicit_type_hints ~tcfix ~pos env (sch : T.scheme) inst eff =
       loop hints cache named
   in
   loop T.TVar.Map.empty [] sch.sch_named
+*)
diff --git a/src/TypeInference/TypeHints.mli b/src/TypeInference/TypeHints.mli
index 7edfa70a..cb543acb 100644
--- a/src/TypeInference/TypeHints.mli
+++ b/src/TypeInference/TypeHints.mli
@@ -11,7 +11,7 @@
   unification variables. However, for effect parameters we need another
   solution: some of type parameters are inferred based on types of actual
   parameters. *)
-
+(*
 open Common
 open TypeCheckFix
 
@@ -45,3 +45,4 @@ val type_inst_hints : T.named_tvar list -> T.typ -> T.typ -> t
 val extract_implicit_type_hints : tcfix:tcfix ->
   pos:Position.t -> Env.t -> T.scheme -> S.inst list -> T.effrow ->
     t * inst_cache
+*)
diff --git a/src/TypeInference/TypeUtils.ml b/src/TypeInference/TypeUtils.ml
index 5a39191e..a079d2fe 100644
--- a/src/TypeInference/TypeUtils.ml
+++ b/src/TypeInference/TypeUtils.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Utility function for extracting information about types *)
-
+(*
 open Common
 
 type hints = T.typ T.TVar.Map.t
@@ -58,3 +58,4 @@ let open_scheme ~pos (env : Env.t) (sch : T.scheme) =
       env
       sch.sch_named in
   (env, sch.sch_targs, ims, sch.sch_body)
+*)
diff --git a/src/TypeInference/TypeUtils.mli b/src/TypeInference/TypeUtils.mli
index 947c69f4..be323a5f 100644
--- a/src/TypeInference/TypeUtils.mli
+++ b/src/TypeInference/TypeUtils.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Utility function for extracting information about types *)
-
+(*
 open Common
 
 (** Check if type is a neutral type starting with type variable *)
@@ -17,3 +17,4 @@ val method_owner_of_scheme : pos:Position.t -> env:Env.t -> T.scheme -> T.tvar
   introduced named parameters, and the type of the scheme body. *)
 val open_scheme : pos:Position.t -> Env.t -> T.scheme ->
   Env.t * T.named_tvar list * (T.name * T.var * T.scheme) list * T.typ
+*)
diff --git a/src/TypeInference/Unification.ml b/src/TypeInference/Unification.ml
index 0d6822f0..b81522ce 100644
--- a/src/TypeInference/Unification.ml
+++ b/src/TypeInference/Unification.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Unification and subtyping of types *)
-
+(*
 open Common
 
 type arrow =
@@ -435,4 +435,4 @@ let as_label env tp =
 
   | TEffect _ | TEffrow _ ->
     failwith "Internal kind error"
-
+*)
diff --git a/src/TypeInference/Unification.mli b/src/TypeInference/Unification.mli
index 0133a141..e8651c48 100644
--- a/src/TypeInference/Unification.mli
+++ b/src/TypeInference/Unification.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Unification and subtyping of types *)
-
+(*
 open Common
 
 (** Arrow type *)
@@ -99,3 +99,4 @@ val from_handler : Env.t -> T.typ -> handler
   an unification variable, it assumes that the effect of the label is
   "the effect". *)
 val as_label : Env.t -> T.typ -> label
+*)
diff --git a/src/TypeInference/Uniqueness.ml b/src/TypeInference/Uniqueness.ml
index 4e9f54e8..465167d3 100644
--- a/src/TypeInference/Uniqueness.ml
+++ b/src/TypeInference/Uniqueness.ml
@@ -3,7 +3,7 @@
  *)
 
 (** Checking uniqueness of various mutual definitions *)
-
+(*
 open Common
 
 module StrMap = Map.Make(String)
@@ -106,3 +106,4 @@ let check_generalized_named_types ~pos tvars =
   let on_error ~pos ~ppos (name, _) =
     Error.fatal (Error.type_generalized_twice ~pos name) in
   check_uniqueness ~on_error ~name_of ~pos_of names
+*)
diff --git a/src/TypeInference/Uniqueness.mli b/src/TypeInference/Uniqueness.mli
index 8dbe28bb..7976b1a1 100644
--- a/src/TypeInference/Uniqueness.mli
+++ b/src/TypeInference/Uniqueness.mli
@@ -3,7 +3,7 @@
  *)
 
 (** Checking uniqueness of various mutual definitions *)
-
+(*
 open Common
 
 (** Ensure that each constructor in given ADT has a unique name *)
@@ -27,3 +27,4 @@ val check_ctor_named_types : T.named_tvar list -> S.named_type_arg list -> unit
 
 (** Ensure that generalized names are unique *)
 val check_generalized_named_types : pos:Position.t -> T.named_tvar list -> unit
+*)