From a29e86bd97bd16b28bb16968072921d35c983d2a Mon Sep 17 00:00:00 2001
From: Patrycja Balik <root@pbalik.com>
Date: Thu, 9 Jan 2025 15:47:53 +0100
Subject: [PATCH] Update the parser, Raw and Desugar

The parser is updated to match the new version of Surface. Miscellanous
syntax changes requested in existing issues or discussed elsewhere were
made too:
* #156 method definitions no longer treat self in a special way, but
  the tests were not updated;
* #173;
* effect variable naming near the `handle` construct uses `/`;
* no more rows and `effect` or `label` fields (but the keyword `label`
  still cannot be used as an identifier).

The tests and examples should mostly parse now, though not necessarily
as expected due to the changes to method definitions.
---
 examples/LWT_lexical.fram                |  19 +-
 examples/Prolog.fram                     |  30 +-
 examples/Pythagorean.fram                |  10 +-
 examples/Tick.fram                       |   2 +-
 lib/Prelude.fram                         |   4 +-
 src/DblParser/Desugar.ml                 | 552 ++++++++++++-----------
 src/DblParser/Error.ml                   |   3 -
 src/DblParser/Error.mli                  |   1 -
 src/DblParser/Import.ml                  |   9 +-
 src/DblParser/Lexer.mll                  |  59 ++-
 src/DblParser/Raw.ml                     |  44 +-
 src/DblParser/YaccParser.mly             |  79 ++--
 test/err/tc_0000_implicitLoop.fram       |   4 +-
 test/ok/ok0010_implicit.fram             |   2 +-
 test/ok/ok0011_implicit.fram             |   2 +-
 test/ok/ok0018_namePattern.fram          |   2 +-
 test/ok/ok0025_letFuncImplicit.fram      |   2 +-
 test/ok/ok0027_explicitApp.fram          |   2 +-
 test/ok/ok0054_firstClassHandler.fram    |   2 +-
 test/ok/ok0055_complexHandlers.fram      |   4 +-
 test/ok/ok0056_complexHandlers.fram      |   6 +-
 test/ok/ok0057_dataArgLabels.fram        |   4 +-
 test/ok/ok0058_unitState.fram            |   4 +-
 test/ok/ok0059_effectArg.fram            |   4 +-
 test/ok/ok0060_returnFinally.fram        |   4 +-
 test/ok/ok0062_theLabel.fram             |   1 -
 test/ok/ok0069_effectCtorArg.fram        |   2 +-
 test/ok/ok0070_effectMethodArg.fram      |   2 +-
 test/ok/ok0074_implicitWithType.fram     |   5 +-
 test/ok/ok0075_effectsFromImplicits.fram |   5 +-
 test/ok/ok0086_optionState.fram          |   5 +-
 test/ok/ok0091_namedParamMethod.fram     |   2 +-
 test/ok/ok0100_polymorphicRecursion.fram |   2 +-
 test/ok/ok0107_polymorphicRecursion.fram |   2 +-
 test/ok/ok0118_parameter.fram            |   9 +
 test/ok/ok0119_patternOpen.fram          |   6 +
 36 files changed, 453 insertions(+), 442 deletions(-)
 delete mode 100644 test/ok/ok0062_theLabel.fram
 create mode 100644 test/ok/ok0118_parameter.fram
 create mode 100644 test/ok/ok0119_patternOpen.fram

diff --git a/examples/LWT_lexical.fram b/examples/LWT_lexical.fram
index ac534da1..2f0351ae 100644
--- a/examples/LWT_lexical.fram
+++ b/examples/LWT_lexical.fram
@@ -14,19 +14,20 @@ import List
   an additional function `update`. Implementing such an update function in
   some other languages with algebraic effects might turn out to be
   troublesome, as a handler of `update f` should call function `f` at the call
-  site of `update`, where potentially more effects (described by `Row`) are
+  site of `update`, where potentially more effects (described by `F`) are
   available. In Fram, update function can be implemented on top of more
   primitive `get` and `put`, even if it is a part of the interface. #}
-data State (effect E) X = State of
+data State E X = State of
   { get    : Unit ->[E] X
   , put    : X ->[E] Unit
-  , update : {Row} -> (X ->[E|Row] X) ->[E|Row] Unit
+  , update : {F} -> (X ->[E,F] X) ->[E,F] Unit
   }
 
 {# We declare implicit parameter named `~st`. Now, the following function may
   use `~st` as a regular variable. In such a case, `~st` together with the
   associated effect E_st will be implicitly generalized. #}
-implicit ~st {E_st} : State E_st _
+parameter E_st
+parameter ~st : State E_st _
 
 {# We define get operation that works on implicit capability `~st`. It can be
   used in any context, where a variable named ~st is available (or can be
@@ -48,7 +49,7 @@ let update f =
   a value, but more complex series of let-expressions. First, we define
   standard get and put operations, and then on top of them we define the update
   function. All three functions becomes part of the interface. #}
-handle {effect=Sched} ~st =
+handle ~st =
   let get = effect x / r => fn s => r s  s
   let put = effect s / r => fn _ => r () s
   let update f = put (f (get ())) in
@@ -78,9 +79,9 @@ let sched _ =
   the handler with the parent thread without sharing parent's continuation. 
   With dynamic handlers we can just create a new handler for the same effect,
   but this is not possible with lexical handlers. #}
-data LWT_S Row = LWT of
-  { yield : Unit ->[|Row] Unit
-  , spawn : (Unit ->[|Row] Unit) ->[|Row] Unit
+data LWT_S E = LWT of
+  { yield : Unit ->[E] Unit
+  , spawn : (Unit ->[E] Unit) ->[E] Unit
   }
 
 {# For accessing operations of LWT effect we use an another mechanism
@@ -94,7 +95,7 @@ method spawn {self = LWT {spawn}} = spawn
 {# Here we handle the LWT effect using pure lexical handlers. The problematic
   spawn operation is implemented via more primitive fork and exit functions,
   not accessible directly via the LWT interface. #}
-handle {effect=LWT} (lwt : LWT_S [LWT,IO]) =
+handle (lwt : LWT_S [LWT,IO]) / LWT =
   let yield = effect _ / r => let _ = enqueue r in sched ()
   let exit  = effect _ / _ => sched ()
   let fork  = effect _ / r =>
diff --git a/examples/Prolog.fram b/examples/Prolog.fram
index c988e98c..5a90bdf7 100644
--- a/examples/Prolog.fram
+++ b/examples/Prolog.fram
@@ -11,15 +11,15 @@ data Clause = Cl of Term, List Term
 
 {# The signature of the standard reader effect, with a single operation
   used to obtain a value of type X. While we do not need to wrap functions
-  `{effect=E} -> Unit ->[E] X` in a data type to use them as capabilities,
-  this improves readability and allows us to define methods on the type. #}
-data Reader (effect E) X = Reader of (Unit ->[E] X)
+  `{E} -> Unit ->[E] X` in a data type to use them as capabilities, this
+  improves readability and allows us to define methods on the type. #}
+data Reader E X = Reader of (Unit ->[E] X)
 
 {# We expose the `ask` operation of `Reader` as a method. #}
 method ask {E, self = Reader ask : Reader E _} = ask
 
 {# The standard state effect, with its accompanying methods. #}
-data State (effect E) X = State of
+data State E X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
@@ -30,7 +30,7 @@ method put {E, self = State { put } : State E _} = put
 method update {E, self : State E _} f = self.put (f (self.get ()))
 
 {# The standard backtracking effect. #}
-data BT (effect E) = BT of
+data BT E = BT of
   { flip : Unit ->[E] Bool
   , fail : {type X} -> Unit ->[E] X
   }
@@ -50,14 +50,14 @@ method choose {E, self : BT E} =
 
 {# The `Fresh` effect is used to model the generation of fresh variable
   identifiers in the evaluator. #}
-data Fresh (effect E) X = Fresh of (Unit ->[E] X)
+data Fresh E X = Fresh of (Unit ->[E] X)
 
 method fresh {E, self = Fresh fresh : Fresh E _} = fresh
 
 {# ========================================================================= #}
 
 {# The standard state handler, defined as a higher order function. #}
-let hState init (f : {effect=E} -> State E _ ->[E|_] _) =
+let hState init (f : {E} -> State E _ ->[E,_] _) =
   handle st = State
     { get = effect () / r => fn s => r s  s
     , put = effect s  / r => fn _ => r () s
@@ -68,7 +68,7 @@ let hState init (f : {effect=E} -> State E _ ->[E|_] _) =
 
 {# A handler for backtracking which returns the first result wrapped in Some,
   or None if no result is available. #}
-let hBT (f : {effect=E} -> BT E ->[E|_] _) =
+let hBT (f : {E} -> BT E ->[E,_] _) =
   handle bt = BT
     { flip = effect () / r =>
       match r True with
@@ -84,7 +84,7 @@ let hBT (f : {effect=E} -> BT E ->[E|_] _) =
 {# The following few functions on lists require a notion of equality, which is
   passed as the implicit parameter `~eq`. #}
 
-implicit ~eq
+parameter ~eq
 
 let rec nub xs =
   match xs with
@@ -140,7 +140,8 @@ method rename { self = Cl t ts } sub =
   containing an association list of instantiations. As this effect is pervasive
   throughout our implementation, we declare it as an implicit, so that it and
   the associated effect variable E_st are generalized automatically. #}
-implicit ~st {E_st} : State E_st (List (Pair Int Term))
+parameter E_st
+parameter ~st : State E_st (List (Pair Int Term))
 
 {# We also define a pair of functions that let us modify and read `~st`. #}
 
@@ -169,7 +170,8 @@ method rec view {self : Term} =
 
 {# As with `~st`, the capability to generate fresh identifiers ~fresh is also
   declared implicit. #}
-implicit ~fresh {E_fresh} : Fresh E_fresh Int
+parameter E_fresh
+parameter ~fresh : Fresh E_fresh Int
 
 {# To further reduce verbosity, we define a function `fresh` to call the
   `fresh` method of the implicit capability. #}
@@ -189,8 +191,10 @@ method refresh {self : Clause} =
 {# Finally, we make the interpreter's knowledge base and the backtracking
   capability implicit as well. The knowledge base is represented as a reader
   effect providing a simple list of clauses. #}
-implicit ~kb {E_kb} : Reader E_kb (List Clause)
-implicit ~bt {E_bt} : BT E_bt
+parameter E_kb
+parameter ~kb : Reader E_kb (List Clause)
+parameter E_bt
+parameter ~bt : BT E_bt
 
 let fail () = ~bt.fail ()
 
diff --git a/examples/Pythagorean.fram b/examples/Pythagorean.fram
index 52e0503d..d0758fd0 100644
--- a/examples/Pythagorean.fram
+++ b/examples/Pythagorean.fram
@@ -6,7 +6,7 @@ import List
 data Triples = Triple of Int, Int, Int
 
 {# The standard backtracking effect. #}
-data BT (effect E) = BT of
+data BT E = BT of
   { flip : Unit ->[E] Bool
   , fail : {type X} -> Unit ->[E] X
   }
@@ -31,11 +31,11 @@ method triples {E, self : BT E} (n : Int) =
   if a * a + b * b == c * c then Triple a b c
   else self.fail ()
 
-
-implicit ~bt {E_bt} : BT E_bt
+parameter E_bt
+parameter ~bt : BT E_bt
 
 {# The function `takeFirst` returns the first triple found. #}
-let takeFirst (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
+let takeFirst (f : {E} -> BT E -> Int ->[E,_] _) (n: Int) =
   handle bt = BT { flip = effect () / r =>
     match r True with
     | None   => r False
@@ -47,7 +47,7 @@ let takeFirst (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
   in f bt n
 
 {# The function `takeAll` returns list of all triples found. #}
-let takeAll (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
+let takeAll (f : {E} -> BT E -> Int ->[E,_] _) (n: Int) =
   handle bt = BT
     { flip = effect () / r => List.append (r True) (r False)
     , fail = effect () => []
diff --git a/examples/Tick.fram b/examples/Tick.fram
index b91b4826..c1e3fcdb 100644
--- a/examples/Tick.fram
+++ b/examples/Tick.fram
@@ -23,7 +23,7 @@
 
 import List
 
-let count (f : {type E} -> (_ ->[|E] _) ->[|E] _) g =
+let count (f : {type E} -> (_ ->[E] _) ->[E] _) g =
   handle tick = effect _ / k => fn (n : Int) => k () (n + 1)
     return  _ => fn n => n
     finally c => c 0
diff --git a/lib/Prelude.fram b/lib/Prelude.fram
index 77618c82..97c3ff15 100644
--- a/lib/Prelude.fram
+++ b/lib/Prelude.fram
@@ -27,11 +27,11 @@ pub let not b = if b then False else True
 
 pub let charListToStr = (extern dbl_chrListToStr : List Char -> String)
 
-pub let chr {~re : {type X} -> Unit ->[|_] X} (n : Int) = 
+pub let chr {~onError : Unit ->[_] Char} (n : Int) =
   if n >= 0 && n < 256 then
     (extern dbl_intToChr : Int -> Char) n
   else
-    ~re ()
+    ~onError ()
 
 pub let printStrLn = extern dbl_printStrLn : String ->[IO] Unit
 pub let printStr   = extern dbl_printStr   : String ->[IO] Unit
diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml
index f8462cb5..435bb446 100644
--- a/src/DblParser/Desugar.ml
+++ b/src/DblParser/Desugar.ml
@@ -5,7 +5,7 @@
 (** The first phase of desugaring and post-parsing *)
 
 open Lang.Surface
-(*
+
 (** Translation of the binary operator's name to the regular identifier. *)
 let tr_bop_id (op : string node) =
   if List.mem op.data ["&&"; "||"; ";"] then
@@ -17,11 +17,11 @@ let make_uop_id str = "(" ^ str ^ " .)"
 
 let tr_bop_to_expr (op : string node) = 
   let make data = { op with data = data } in
-  make (EPoly (make (EVar (NPName (tr_bop_id op))),[],[]))
+  make (EPoly (make (EVar (make (NPName (tr_bop_id op)))), []))
 
 let tr_uop_to_expr (op : string node) = 
   let make data = { op with data = data } in
-  make (EPoly (make (EVar (NPName (make_uop_id op.data))),[],[]))
+  make (EPoly (make (EVar (make (NPName (make_uop_id op.data)))), []))
 
 let tr_var_id (var : Raw.var_id node) =
   match var.data with
@@ -61,8 +61,8 @@ let annot_tp e tp =
   }
 
 module RawTypes = struct
-  let unit = Raw.TVar(NPName "Unit", None)
-  let bool = Raw.TVar(NPName "Bool", None)
+  let unit = Raw.TVar(with_nowhere (NPName "Unit"), None)
+  let bool = Raw.TVar(with_nowhere (NPName "Bool"), None)
 end
 
 type ty_def =
@@ -73,7 +73,7 @@ type let_pattern =
   | LP_Id of ident
     (** identifier *)
 
-  | LP_Fun of ident * named_type_arg list * named_arg list * Raw.expr list
+  | LP_Fun of ident * Raw.expr list
     (** Function definition with list of formal type, named, and explicit
       parameters *)
 
@@ -99,37 +99,20 @@ let rec map_either ~warn f xs =
       (ys, z :: zs)
     end
 
-let map_inst_like f xs =
-  map_either ~warn:Error.value_before_type_param f xs
-
 let map_h_clauses f xs =
   map_either ~warn:Error.finally_before_return_clause f xs
 
-(** Finds argument named "self" on given list. *)
-let rec find_self_arg args =
-  match args with
-  | [] -> (None, [])
-  | { pos; data = (NVar "self", arg) } :: args ->
-    begin match find_self_arg args with
-    | (None, _) -> (Some (pos, arg), args)
-    | (Some(pos, _), _) ->
-      Error.fatal (Error.multiple_self_parameters pos)
-    end
-  | arg :: args ->
-    let (self, args) = find_self_arg args in
-    (self, arg :: args)
-
-let ident_of_name ~public (name : Raw.name) =
+let ident_of_name (name : Raw.name) =
   match name with
-  | NLabel      -> IdLabel
-  | NVar x | NOptionalVar x -> IdVar(public, x)
-  | NImplicit n -> IdImplicit(public, n)
-  | NMethod   n -> IdMethod(public, n)
+  | NVar x | NOptionalVar x -> IdVar x
+  | NImplicit n -> IdImplicit n
+  | NMethod   n -> IdMethod n
 
-let rec path_append path rest =
-  match path with
-  | NPName name       -> NPSel(name, rest)
-  | NPSel(name, path) -> NPSel(name, path_append path rest)
+let rec path_append prefix rest =
+  let make data = { pos = Position.join prefix.pos rest.pos; data } in
+  match rest.data with
+  | NPName name       -> make (NPSel(prefix, name))
+  | NPSel(rest, name) -> make (NPSel(path_append prefix rest, name))
 
 let rec tr_type_expr (tp : Raw.type_expr) =
   let make data = { tp with data = data } in
@@ -143,11 +126,11 @@ let rec tr_type_expr (tp : Raw.type_expr) =
     | (None, tp2) -> make (TPureArrow(sch, tp2))
     | (Some eff, tp2) -> make (TArrow(sch, tp2, eff))
     end
-  | TEffect(tps, ee) ->
-    make (TEffect(List.map tr_type_expr tps, Option.map tr_type_expr ee))
+  | TEffect tps ->
+    make (TEffect (List.map tr_type_expr tps))
   | TApp(tp1, tp2) ->
     make (TApp(tr_type_expr tp1, tr_type_expr tp2))
-  | TRecord _ | TTypeLbl _ | TEffectLbl _ ->
+  | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 and tr_eff_type (tp : Raw.type_expr) =
@@ -178,103 +161,110 @@ and tr_scheme_expr (tp : Raw.type_expr) =
   | TParen tp ->
     { (tr_scheme_expr tp) with sch_pos = pos }
   | TArrow({ data = TRecord flds; _}, tp) ->
-    let (tvs, named) = map_inst_like tr_scheme_field flds in
+    let args = List.map tr_scheme_field flds in
     begin match tr_eff_type tp with
     | (None, tp) ->
-      { sch_pos   = pos;
-        sch_targs = tvs;
-        sch_named = named;
-        sch_body  = tp
+      { sch_pos  = pos;
+        sch_args = args;
+        sch_body = tp
       }
     | (Some _, _) ->
       Error.fatal (Error.impure_scheme pos)
     end
 
   | TWildcard | TVar _ | TArrow _ | TEffect _ | TApp _ ->
-    { sch_pos   = pos;
-      sch_targs = [];
-      sch_named = [];
-      sch_body  = tr_type_expr tp
+    { sch_pos  = pos;
+      sch_args = [];
+      sch_body = tr_type_expr tp
     }
-  | TRecord _ | TTypeLbl _ | TEffectLbl _ ->
+  | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 and tr_scheme_field (fld : Raw.ty_field) =
   let make data = { fld with data = data } in
   match fld.data with
   | FldAnonType tp ->
-    Either.Left (make (TNAnon, tr_type_arg ~public:false tp))
-  | FldEffect ->
-    Either.Left (make (TNEffect, make TA_Effect))
-  | FldEffectVal arg ->
-    Either.Left (make (TNEffect, tr_type_arg ~public:false arg))
+    let (x, k) = tr_type_var tp in
+    make (SA_Type(TNAnon, x, k))
   | FldType(x, ka) ->
     let k = Option.value ka ~default:(make KWildcard) in
-    Either.Left (make (TNVar x, make (TA_Var(false, x, k))))
+    make (SA_Type(TNVar x, x, k))
   | FldTypeVal(x, arg) ->
-    Either.Left (make (TNVar x, tr_type_arg ~public:false arg))
+    let (y, k) = tr_type_var arg in
+    make (SA_Type(TNVar x, y, k))
   | FldName n ->
     let sch =
-      { sch_pos   = fld.pos;
-        sch_targs = [];
-        sch_named = [];
-        sch_body  = make TWildcard
+      { sch_pos  = fld.pos;
+        sch_args = [];
+        sch_body = make TWildcard
       }
     in
-    Either.Right (make (n, sch))
+    make (SA_Val(n, sch))
   | FldNameVal(n, tp) ->
-    Either.Right (make (n, tr_scheme_expr tp))
-  | FldNameAnnot _ | FldModule _ ->
+    make (SA_Val(n, tr_scheme_expr tp))
+  | FldNameAnnot _ | FldModule _ | FldOpen ->
     assert false
 
-(** Translate a type expression as a type parameter *)
-and tr_type_arg ~public (tp : Raw.type_expr) =
+(** Translate a type expression as a type variable with kind annotation *)
+and tr_type_var (tp : Raw.type_expr) =
   let make data = { tp with data = data } in
   match tp.data with
-  | TParen tp -> make (tr_type_arg ~public tp).data
-  | TVar (NPName x, ka) -> 
+  | TParen tp -> tr_type_var tp
+  | TVar ({data = NPName x; _}, ka) ->
     let k = Option.value ka ~default:(make KWildcard) in
-    make (TA_Var(public, x, k))
-  | TVar (NPSel _, _) | TWildcard | TArrow _ | TEffect _ | TApp _ | TRecord _
-  | TTypeLbl _ | TEffectLbl _ ->
+    (x, k)
+  | TVar ({data = NPSel _; _}, _) | TWildcard | TArrow _ | TEffect _ | TApp _
+  | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
+(** Translate a type expression as a type parameter *)
+and tr_type_arg (tp : Raw.type_expr) =
+  let (x, k) = tr_type_var tp in
+  { tp with data = TA_Var(x, k) }
+
+(** Translate an optional type expression as a type parameter, defaulting to
+    wildcard with the supplied position if [None] *)
+let tr_type_arg_opt pos (tp : Raw.type_expr option) =
+  match tp with
+  | Some tp -> tr_type_arg tp
+  | None    -> { pos; data = TA_Wildcard }
+
 (** Translate a type expression as a named type parameter *)
 let rec tr_named_type_arg (tp : Raw.type_expr) =
   let make data = { tp with data = data } in
   match tp.data with
   | TParen tp -> make (tr_named_type_arg tp).data
-  | TVar (NPName x, ka) -> 
+  | TVar ({data = NPName x; _}, ka) ->
     let k = Option.value ka ~default:(make KWildcard) in
-    make (TNVar x, make (TA_Var(false, x, k)))
-  | TTypeLbl tp -> make (TNAnon, tr_type_arg ~public:false tp)
-  | TEffectLbl tp -> make (TNEffect, tr_type_arg ~public:false tp)
+    make (TNVar x, make (TA_Var(x, k)))
+  | TTypeLbl tp -> make (TNAnon, tr_type_arg tp)
   | TWildcard -> make (TNAnon, make (TA_Wildcard))
-  | TVar (NPSel _, _) | TArrow _ | TEffect _ | TApp _ | TRecord _ ->
+  | TVar ({data = NPSel _; _}, _) | TArrow _ | TEffect _ | TApp _
+  | TRecord _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 (** Translate a left-hand-side of the type definition. The additional
   parameter is an accumulated list of formal parameters *)
 let rec tr_type_def (tp : Raw.type_expr) args =
   match tp.data with
-  | TVar (NPName x, _) -> TD_Id(x, args)
+  | TVar ({data = NPName x; _}, _) -> TD_Id(x, args)
   | TApp(tp1, tp2) -> tr_type_def tp1 (tp2 :: args)
-  | TVar (NPSel _, _) | TWildcard | TParen _ | TArrow _ | TEffect _ | TRecord _
-  | TTypeLbl _ | TEffectLbl _ ->
+  | TVar ({data = NPSel _; _}, _) | TWildcard | TParen _ | TArrow _
+  | TEffect _ | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
-let tr_ctor_decl ~public:cd_public (d : Raw.ctor_decl) =
+let tr_ctor_decl (d : Raw.ctor_decl) =
   let make data = { d with data = data } in
   match d.data with
   | CtorDecl(cd_name, { data = TRecord flds; _ } :: schs ) ->
     let cd_name = tr_ctor_name (make cd_name) in
-    let (cd_targs, cd_named) = map_inst_like tr_scheme_field flds in
+    let cd_named_args = List.map tr_scheme_field flds in
     let cd_arg_schemes = List.map tr_scheme_expr schs in
-    make { cd_public; cd_name; cd_targs; cd_named; cd_arg_schemes }
+    make { cd_name; cd_named_args; cd_arg_schemes }
   | CtorDecl(cd_name, schs) ->
     let cd_name = tr_ctor_name (make cd_name) in
     let cd_arg_schemes = List.map tr_scheme_expr schs in
-    make { cd_public; cd_name; cd_targs = []; cd_named = []; cd_arg_schemes }
+    make { cd_name; cd_named_args = []; cd_arg_schemes }
 
 (* ========================================================================= *)
 
@@ -294,11 +284,11 @@ let rec collect_fields ~ppos (es : Raw.expr list) =
 let rec tr_ctor_pattern (p : Raw.expr) =
   let make data = { p with data = data } in
   match p.data with
-  | EUnit            -> NPName (tr_ctor_name (make Raw.CNUnit))
-  | ECtor c          -> NPName c
-  | EBOpID name      -> NPName (tr_bop_id { p with data = name})
-  | EUOpID name      -> NPName (make_uop_id name)
-  | EList []         -> NPName (tr_ctor_name (make Raw.CNNil))
+  | EUnit            -> make (NPName (tr_ctor_name (make Raw.CNUnit)))
+  | ECtor c          -> make (NPName c)
+  | EBOpID name      -> make (NPName (tr_bop_id (make name)))
+  | EUOpID name      -> make (NPName (make_uop_id name))
+  | EList []         -> make (NPName (tr_ctor_name (make Raw.CNNil)))
   | ESelect(path, p) -> path_append path (tr_ctor_pattern p)
 
   | EWildcard | ENum _ | ENum64 _ | EStr _ | EChr _ | EParen _ | EVar _
@@ -313,44 +303,39 @@ let rec tr_pattern ~public (p : Raw.expr) =
   match p.data with
   | EWildcard   -> make PWildcard
   | EUnit | ECtor _ | ESelect _ ->
-    make (PCtor(make (tr_ctor_pattern p), CNParams([], []), []))
+    make (PCtor(tr_ctor_pattern p, [], []))
   | ENum _      -> Error.fatal (Error.desugar_error p.pos)
   | ENum64 _      -> Error.fatal (Error.desugar_error p.pos)
   | EStr _      -> Error.fatal (Error.desugar_error p.pos)
   | EChr _      -> Error.fatal (Error.desugar_error p.pos)
   | EParen    p -> make (tr_pattern ~public p).data
-  | EVar      x -> make (PId (IdVar(public, x)))
-  | EBOpID    n -> make (PId (IdVar(public, tr_bop_id (make n))))
-  | EUOpID    n -> make (PId (IdVar(public, make_uop_id n)))
-  | EImplicit n -> make (PId (IdImplicit(public, n)))
+  | EVar      x -> make (PId(public, IdVar x))
+  | EBOpID    n -> make (PId(public, IdVar (tr_bop_id (make n))))
+  | EUOpID    n -> make (PId(public, IdVar (make_uop_id n)))
+  | EImplicit n -> make (PId(public, IdImplicit n))
   | EApp(p1, ps) ->
-    let cpath = { p1 with data = tr_ctor_pattern p1 } in
+    let cpath = tr_ctor_pattern p1 in
     let (flds, _, ps) = collect_fields ~ppos:p1.pos ps in
+    let named = List.map (tr_named_pattern ~public) flds in
     let ps = List.map (tr_pattern ~public) ps in
-    begin match flds with
-    | [ { data = FldModule name; _ } ] ->
-      make (PCtor(cpath, CNModule(public, name), ps))
-    | _ ->
-      let (targs, iargs) = map_inst_like (tr_named_pattern ~public) flds in
-      make (PCtor(cpath, CNParams(targs, iargs), ps))
-    end
+    make (PCtor(cpath, named, ps))
   | EAnnot(p, sch) -> make (PAnnot(tr_pattern ~public p, tr_scheme_expr sch))
   | EBOp(p1, op, p2) ->
     let c_name = {op with data = NPName (tr_bop_id op)} in
     let ps = [tr_pattern ~public p1; tr_pattern ~public p2] in
-    make (PCtor(c_name, CNParams([], []), ps))
+    make (PCtor(c_name, [], ps))
   | EUOp(op, p1) ->
     let c_name = {op with data = NPName (make_uop_id op.data)} in
-    make (PCtor(c_name, CNParams([], []), [tr_pattern ~public p1]))
+    make (PCtor(c_name, [], [tr_pattern ~public p1]))
   | EList ps ->
     let cons pe xs =
       let pe  = tr_pattern ~public pe in
       let pos = Position.join pe.pos p.pos in
       let cpath = make (NPName (tr_ctor_name' (CNBOp "::"))) in
-      { pos; data = PCtor(cpath, CNParams([], []), [pe; xs]) }
+      { pos; data = PCtor(cpath, [], [pe; xs]) }
     in
     let nil_path = make (NPName (tr_ctor_name' CNNil)) in
-    let pnil = make (PCtor(nil_path, CNParams([], []), [])) in
+    let pnil = make (PCtor(nil_path, [], [])) in
     make (List.fold_right cons ps pnil).data
   | EPub p -> make (tr_pattern ~public:true p).data
 
@@ -363,24 +348,45 @@ and tr_named_pattern ~public (fld : Raw.field) =
   match fld.data with
   | FldAnonType _ ->
     Error.fatal (Error.anon_type_pattern fld.pos)
-  | FldEffect ->
-    Either.Left (make (TNEffect, make TA_Effect))
-  | FldEffectVal arg ->
-    Either.Left (make (TNEffect, tr_type_arg ~public arg))
   | FldType(x, ka) ->
     let k = Option.value ka ~default:(make KWildcard) in
-    Either.Left (make (TNVar x, make (TA_Var(public, x, k))))
+    make (NP_Type(public, make (TNVar x, make (TA_Var(x, k)))))
   | FldTypeVal(x, arg) ->
-    Either.Left (make (TNVar x, tr_type_arg ~public arg))
+    make (NP_Type(public, make (TNVar x, tr_type_arg arg)))
   | FldName n ->
-    Either.Right (make (n, make (PId (ident_of_name ~public n))))
+    make (NP_Val(n, make (PId(public, ident_of_name n))))
   | FldNameVal(n, p) ->
-    Either.Right (make (n, tr_pattern ~public p))
+    make (NP_Val(n, tr_pattern ~public p))
   | FldNameAnnot(n, sch) ->
-    Either.Right
-      (make (n, make (PAnnot(make (PId (ident_of_name ~public n)),
-                             tr_scheme_expr sch))))
-  | FldModule _ ->
+    let arg =
+      make (PAnnot(make (PId(public, ident_of_name n)), tr_scheme_expr sch)) in
+    make (NP_Val(n, arg))
+  | FldModule { data = NPName name; _ } -> make (NP_Module name)
+  | FldModule _ -> Error.fatal (Error.desugar_error fld.pos)
+  | FldOpen     -> make NP_Open
+
+(** Translate a parameter declaration *)
+let tr_param_decl (fld : Raw.field) =
+  let make data = { fld with data = data } in
+  match fld.data with
+  | FldAnonType arg ->
+    let (x, k) = tr_type_var arg in
+    Either.Left (TNAnon, x, k)
+  | FldType(x, ka) ->
+    let k = Option.value ka ~default:(make KWildcard) in
+    Either.Left (TNVar x, x, k)
+  | FldName n ->
+    let sch =
+      { sch_pos   = fld.pos;
+        sch_args  = [];
+        sch_body  = make TWildcard
+      }
+    in
+    Either.Right (n, ident_of_name n, sch)
+  | FldNameAnnot(n, sch) ->
+    Either.Right (n, ident_of_name n, tr_scheme_expr sch)
+
+  | FldTypeVal _ | FldNameVal _ | FldModule _ | FldOpen ->
     Error.fatal (Error.desugar_error fld.pos)
 
 (** Translate a formal parameter of a function *)
@@ -388,66 +394,59 @@ let rec tr_function_arg (arg : Raw.expr) =
   match arg.data with
   | EParen arg -> tr_function_arg arg
   | EAnnot(p, sch) ->
-    ArgAnnot(tr_pattern ~public:false p, tr_scheme_expr sch)
+    { arg with data = PAnnot(tr_pattern ~public:false p, tr_scheme_expr sch) }
   | EWildcard | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EVar _
   | EImplicit _ | ECtor _ | EBOp _ | EUOp _ | EApp _ | EBOpID _ | EUOpID _
   | ESelect _ | EList _ ->
-    ArgPattern (tr_pattern ~public:false arg)
+    tr_pattern ~public:false arg
 
   | EFn _ | EEffect _ | EDefs _ | EMatch _ | EHandler _ | ERecord _
   | EMethod _ | EExtern _ | EIf _ | EPub _ | EMethodCall _ ->
     Error.fatal (Error.desugar_error arg.pos)
 
+(** Translate a field to a named pattern. *)
 let tr_named_arg (fld : Raw.field) =
   let make data = { fld with data = data } in
   match fld.data with
   | FldAnonType arg ->
-    Either.Left (make (TNAnon, tr_type_arg ~public:false arg))
-  | FldEffect ->
-    Either.Left (make (TNEffect, make TA_Effect))
-  | FldEffectVal arg ->
-    Either.Left (make (TNEffect, tr_type_arg ~public:false arg))
+    make (NP_Type(false, make (TNAnon, tr_type_arg arg)))
   | FldType(x, ka) ->
     let k = Option.value ka ~default:(make KWildcard) in
-    Either.Left (make (TNVar x, make (TA_Var(false, x, k))))
+    make (NP_Type(false, make (TNVar x, make (TA_Var(x, k)))))
   | FldTypeVal(x, arg) ->
-    Either.Left (make (TNVar x, tr_type_arg ~public:false arg))
+    make (NP_Type(false, make (TNVar x, tr_type_arg arg)))
   | FldName n ->
-    let arg = ArgPattern(make (PId (ident_of_name ~public:false n))) in
-    Either.Right (make (n, arg))
+    make (NP_Val(n, make (PId(false, ident_of_name n))))
   | FldNameVal(n, e) ->
-    Either.Right (make (n, tr_function_arg e))
+    make (NP_Val(n, tr_function_arg e))
   | FldNameAnnot(n, sch) ->
     let arg =
-      ArgAnnot(make (PId (ident_of_name ~public:false n)), tr_scheme_expr sch)
-    in
-    Either.Right (make (n, arg))
-  | FldModule _ ->
-    (* TODO: This might eventually be supported. *)
-    Error.fatal (Error.desugar_error fld.pos)
+      make (PAnnot(make (PId(false, ident_of_name n)), tr_scheme_expr sch)) in
+    make (NP_Val(n, arg))
+  | FldModule { data = NPName name; _ } -> make (NP_Module name)
+  | FldModule _    -> Error.fatal (Error.desugar_error fld.pos)
+  | FldOpen        -> make NP_Open
 
 (** Translate an expression as a let-pattern. *)
 let rec tr_let_pattern ~public (p : Raw.expr) =
   let make data = { p with data = data } in
   match p.data with
-  | EVar      x -> LP_Id(IdVar(public, x))
-  | EImplicit n -> LP_Id(IdImplicit(public, n))
-  | EBOpID    n -> LP_Id(IdVar(public, tr_bop_id (make n)))
-  | EUOpID    n -> LP_Id(IdVar(public, make_uop_id n))
+  | EVar      x -> LP_Id(IdVar x)
+  | EImplicit n -> LP_Id(IdImplicit n)
+  | EBOpID    n -> LP_Id(IdVar (tr_bop_id (make n)))
+  | EUOpID    n -> LP_Id(IdVar (make_uop_id n))
   | EApp(p1, ps) ->
     begin match p1.data with
     | EVar _ | EImplicit _  | EBOpID _ | EUOpID _->
       let id =
         match p1.data with
-        | EVar      x -> IdVar(public, x)
-        | EImplicit n -> IdImplicit(public, n)
-        | EBOpID    n -> IdVar(public, tr_bop_id (make n))
-        | EUOpID    n -> IdVar(public, make_uop_id n)
+        | EVar      x -> IdVar x
+        | EImplicit n -> IdImplicit n
+        | EBOpID    n -> IdVar (tr_bop_id (make n))
+        | EUOpID    n -> IdVar (make_uop_id n)
         | _ -> assert false
       in
-      let (flds, _, ps) = collect_fields ~ppos:p1.pos ps in
-      let (targs, iargs) = map_inst_like tr_named_arg flds in
-      LP_Fun(id, targs, iargs, ps)
+      LP_Fun(id, ps)
 
     | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | ECtor _ | ESelect _
     | EList _ ->
@@ -476,6 +475,18 @@ let rec tr_function args body =
       data = EFn(tr_function_arg arg, tr_function args body)
     }
 
+(** Translate a polymorphic function *)
+let rec tr_poly_function all_args body =
+  let (flds, _, args) = collect_fields ~ppos:Position.nowhere all_args in
+  let named = List.map tr_named_arg flds in
+  let body = tr_function args body in
+  match named with
+  | [] -> { body with data = PE_Expr body }
+  | _ :: _ ->
+    { pos  = Position.join (List.hd all_args).pos body.pos;
+      data = PE_Fn(named, body)
+    }
+
 (* ========================================================================= *)
 
 let tr_data_vis ?(public=false) (pos : Position.t) (vis : Raw.data_vis) =
@@ -492,18 +503,18 @@ let tr_data_vis ?(public=false) (pos : Position.t) (vis : Raw.data_vis) =
 let rec tr_poly_expr (e : Raw.expr) =
   let make data = { e with data = data } in
   match e.data with
-  | EUnit       -> make (EVar      (NPName (tr_ctor_name' CNUnit)))
-  | EVar      x -> make (EVar      (NPName x))
-  | EImplicit n -> make (EImplicit (NPName n))
-  | ECtor     c -> make (EVar      (NPName c))
-  | EBOpID    x -> make (EVar      (NPName (tr_bop_id (make x))))
-  | EUOpID    x -> make (EVar      (NPName (make_uop_id x)))
-  | EList    [] -> make (EVar      (NPName (tr_ctor_name' CNNil)))
+  | EUnit       -> make (EVar      (make (NPName (tr_ctor_name' CNUnit))))
+  | EVar      x -> make (EVar      (make (NPName x)))
+  | EImplicit n -> make (EImplicit (make (NPName n)))
+  | ECtor     c -> make (EVar      (make (NPName c)))
+  | EBOpID    x -> make (EVar      (make (NPName (tr_bop_id (make x)))))
+  | EUOpID    x -> make (EVar      (make (NPName (make_uop_id x))))
+  | EList    [] -> make (EVar      (make (NPName (tr_ctor_name' CNNil))))
 
   | EMethod(e, name) ->
     make (EMethod(tr_expr e, name))
   | ESelect(path, e) ->
-    let prepend_path n = path_append path (NPName n) in
+    let prepend_path n = path_append path { e with data = NPName n } in
     begin match e.data with
     | EUnit       -> make (EVar      (prepend_path (tr_ctor_name' CNUnit)))
     | EVar      x -> make (EVar      (prepend_path x))
@@ -526,12 +537,26 @@ let rec tr_poly_expr (e : Raw.expr) =
   | EMethodCall _ ->
     Error.fatal (Error.desugar_error e.pos)
 
+and tr_poly_expr_def (e : Raw.expr) =
+  let make data = { e with data = data } in
+  match e.data with
+  | EParen e -> make (tr_poly_expr_def e).data
+  | EFn(es, e) -> make (tr_poly_function es (tr_expr e)).data
+
+  | EUnit | EVar _ | EImplicit _ | ECtor _ | EMethod _ | EBOpID _ | EUOpID _ ->
+    make (PE_Poly (tr_poly_expr e))
+
+  | ENum _ | ENum64 _ | EStr _ | EChr _ | EApp _ | EMethodCall _ | EDefs _
+  | EMatch _ | EHandler _ | EEffect _ | EExtern _ | EAnnot _ | EIf _
+  | ESelect _ | EBOp _ | EUOp _ | EList _ | EWildcard | ERecord _ | EPub _ ->
+    make (PE_Expr (tr_expr e))
+
 and tr_expr (e : Raw.expr) =
   let make data = { e with data = data } in
   match e.data with
   | EParen e       -> make (tr_expr e).data
   | EUnit | EVar _ | EImplicit _ | ECtor _ | EMethod _ | EBOpID _ | EUOpID _ ->
-    make (EPoly(tr_poly_expr e, [], []))
+    make (EPoly(tr_poly_expr e, []))
   | ENum n -> make (ENum n)
   | ENum64 n -> make (ENum64 n)
   | EStr s -> make (EStr s)
@@ -542,10 +567,10 @@ and tr_expr (e : Raw.expr) =
     | [], _, es -> tr_expr_app (tr_expr e1) es
     | flds, fpos, es ->
       let e1 = tr_poly_expr e1 in
-      let (tinst, inst) = map_inst_like tr_explicit_inst flds in
+      let inst = List.map tr_explicit_inst flds in
       let e1 =
         { pos  = Position.join e1.pos fpos;
-          data = EPoly(e1, tinst, inst)
+          data = EPoly(e1, inst)
         } in
       tr_expr_app e1 es
     end
@@ -559,13 +584,14 @@ and tr_expr (e : Raw.expr) =
     let e = tr_expr h in
     let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
     make (EHandler(e, rcs, fcs))
-  | EEffect(es, rp_opt, e) ->
-    let (pos, rp) =
-      match rp_opt with
-      | None    -> (e.pos, ArgPattern (make (PId (IdVar(false, "resume")))))
-      | Some rp -> (Position.join rp.pos e.pos, tr_function_arg rp)
+  | EEffect { label; args; resumption; body } ->
+    let (pos, res) =
+      match resumption with
+      | None     -> (e.pos, make (PId(false, IdVar("resume"))))
+      | Some res -> (Position.join res.pos e.pos, tr_function_arg res)
     in
-    make (tr_function es { pos; data = EEffect(rp, tr_expr e)}).data
+    let e = EEffect(Option.map tr_expr label, res, tr_expr body) in
+    make (tr_function args { pos; data = e }).data
   | EExtern name -> make (EExtern name)
   | EAnnot(e, tp) -> make (EAnnot(tr_expr e, tr_type_expr tp))
   | EIf(e, e1, e2) ->
@@ -574,8 +600,8 @@ and tr_expr (e : Raw.expr) =
       | Some e2 -> (e1, e2)
       | None -> (annot_tp e1 RawTypes.unit, with_nowhere Raw.EUnit)
     in
-    let ctrue  = make (PCtor(make (NPName "True"), CNParams([], []), [])) in
-    let cfalse = make (PCtor(make (NPName "False"), CNParams([], []), [])) in
+    let ctrue  = make (PCtor(make (NPName "True"), [], [])) in
+    let cfalse = make (PCtor(make (NPName "False"), [], [])) in
     let cl1 = Clause(ctrue, tr_expr e1) in
     let cl2 = Clause(cfalse, tr_expr e2) in
     make (EMatch(tr_expr e, [make cl1; make cl2]))
@@ -596,22 +622,24 @@ and tr_expr (e : Raw.expr) =
         exp2
       )))
     | _ ->
-      let e1 = tr_expr exp1 and e2 = tr_expr exp2 in
+      let e1 = tr_poly_expr_def exp1 in
+      let e2 = tr_poly_expr_def exp2 in
       make (EApp(
         { pos  = Position.join e1.pos op.pos;
           data = EApp(tr_bop_to_expr op, e1)
         }, e2))
     end
   | EUOp(op,exp) ->
-    let e = tr_expr exp in 
+    let e = tr_poly_expr_def exp in
     make (EApp (tr_uop_to_expr op, e))
   | EList es ->
-    let mk_ctor name = make (EPoly(make (EVar (NPName name)), [], [])) in
+    let mk_ctor name = make (EPoly(make (EVar (make (NPName name))), [])) in
     let cons el xs =
-      let el  = tr_expr el in
+      let el  = tr_poly_expr_def el in
       let pos = Position.join el.pos e.pos in
       let make data = { pos; data } in
-      make (EApp(make (EApp(mk_ctor (tr_ctor_name' (CNBOp "::")), el)), xs))
+      make (EApp(make (EApp(mk_ctor (tr_ctor_name' (CNBOp "::")), el)),
+                 make (PE_Expr xs)))
     in
     make (List.fold_right cons es (mk_ctor (tr_ctor_name' CNNil))).data
 
@@ -624,7 +652,7 @@ and tr_expr_app (e : expr) (es : Raw.expr list) =
   | e1 :: es ->
     let e =
       { pos  = Position.join e.pos e1.pos;
-        data = EApp(e, tr_expr e1)
+        data = EApp(e, tr_poly_expr_def e1)
       } in
     tr_expr_app e es
 
@@ -639,27 +667,23 @@ and tr_explicit_inst (fld : Raw.field) =
   match fld.data with
   | FldAnonType _ ->
     Error.fatal (Error.desugar_error fld.pos)
-  | FldEffectVal eff ->
-    Either.Left (make (TNEffect, tr_type_expr eff))
   | FldType(x, None) ->
-    Either.Left (make (TNVar x, make (TVar (NPName x))))
+    make (IType(x, make (TVar (make (NPName x)))))
   | FldTypeVal(x, tp) ->
-    Either.Left (make (TNVar x, tr_type_expr tp))
+    make (IType(x, tr_type_expr tp))
   | FldName n ->
     let pe =
       match n with
-      | NLabel       -> Error.fatal (Error.desugar_error fld.pos)
-      | NVar x | NOptionalVar x -> make (EVar (NPName x))
-      | NImplicit n  -> make (EImplicit (NPName n))
+      | NVar x | NOptionalVar x -> make (EVar (make (NPName x)))
+      | NImplicit n  -> make (EImplicit (make (NPName n)))
       | NMethod   n  -> Error.fatal (Error.desugar_error fld.pos)
     in
-    Either.Right (make (n, make (EPoly(pe, [], []))))
+    make (IVal(n, make (PE_Poly pe)))
   | FldNameVal(n, e) ->
-    Either.Right (make (n, tr_expr e))
-  | FldModule _ ->
-    (* TODO: This should eventually be supported. *)
-    Error.fatal (Error.desugar_error fld.pos)
-  | FldEffect | FldNameAnnot _ | FldType(_, Some _) ->
+    make (IVal(n, tr_poly_expr_def e))
+  | FldModule path -> make (IModule path)
+  | FldOpen -> make IOpen
+  | FldNameAnnot _ | FldType(_, Some _) ->
     Error.fatal (Error.desugar_error fld.pos)
 
 and tr_def ?(public=false) (def : Raw.def) =
@@ -668,96 +692,77 @@ and tr_def ?(public=false) (def : Raw.def) =
   | DLet(pub, p, e) ->
     let public = public || pub in
     [ match tr_let_pattern ~public p with
-      | LP_Id id -> 
-        make (DLetId(id, tr_expr e))
-    | LP_Fun(id, targs, iargs, args) ->
-        make (DLetFun(id, targs, iargs, tr_function args (tr_expr e)))
-    | LP_Pat p ->
+      | LP_Id id ->
+        make (DLetId(public, id, tr_poly_expr_def e))
+      | LP_Fun(id, args) ->
+        make (DLetId(public, id, tr_poly_function args (tr_expr e)))
+      | LP_Pat p ->
         make (DLetPat(p, tr_expr e))
     ]
   | DMethod(pub, p, e) ->
     let public = public || pub in
     [ match tr_let_pattern ~public p with
-      | LP_Id (IdVar(public, x)) ->
-        make (DLetFun(IdMethod(public, x), [], [],
-          make (EFn(ArgPattern (make (PId (IdVar(false, "self")))),
-            tr_expr e))))
-      | LP_Fun(IdVar(public, x), targs, iargs, args) ->
-        let (self_arg, iargs) =
-          match find_self_arg iargs with
-          | None, iargs ->
-            (ArgPattern (make (PId (IdVar(false, "self")))), iargs)
-          | Some(_, arg), iargs -> (arg, iargs)
-        in
-        make (DLetFun(IdMethod(public, x), targs, iargs,
-          make (EFn(self_arg, tr_function args (tr_expr e)))))
-      | LP_Id (IdLabel | IdImplicit _ | IdMethod _)
-      | LP_Fun((IdLabel | IdImplicit _ | IdMethod _), _, _, _)
+      | LP_Id (IdVar x) ->
+        make (DLetId(public, IdMethod x, tr_poly_expr_def e))
+      | LP_Fun(IdVar x, args) ->
+        make (DLetId(public, IdMethod x, tr_poly_function args (tr_expr e)))
+      | LP_Id (IdImplicit _ | IdMethod _)
+      | LP_Fun((IdImplicit _ | IdMethod _), _)
       | LP_Pat _ ->
         Error.fatal (Error.desugar_error p.pos)
     ]
   | DMethodFn(pub, id1, id2) ->
     let public = public || pub in
     [ make (DMethodFn(public, tr_var_id (make id1), tr_var_id (make id2))) ]
-  | DImplicit(n, args, sch) ->
-    let args = List.map tr_named_type_arg args in
-    let sch =
-      match sch with
-      | None -> {
-          sch_pos   = def.pos;
-          sch_targs = [];
-          sch_named = [];
-          sch_body  = make TWildcard
-        }
-      | Some sch -> tr_scheme_expr sch
-    in
-    [ make (DImplicit(n, args, sch)) ]
+  | DParam fld ->
+    [ match tr_param_decl fld with
+      | Either.Left (x, y, k)    -> make (DTypeParam(x, y, k))
+      | Either.Right (x, y, sch) -> make (DValParam(x, y, sch))
+    ]
   | DRecord (vis, tp, flds) ->
-    let (pub_type, pub_ctors) = tr_data_vis ~public def.pos vis in
-    let (cd_targs, cd_named) = map_inst_like tr_scheme_field flds in
-    begin match cd_targs with
-    | [] -> ()
-    | x :: _ ->
-      Error.fatal (Error.existential_type_arg_in_record x.pos)
-    end;
+    let (public_tp, public_ctors) = tr_data_vis ~public def.pos vis in
+    let cd_named_args = List.map tr_scheme_field flds in
     begin match tr_type_def tp [] with
     | TD_Id(cd_name, args) ->
-      let named_type_args = List.map tr_named_type_arg args in
-      let ctor = make
-        { cd_public=pub_ctors; cd_name;
-          cd_targs=[]; cd_named; cd_arg_schemes=[] } in
-      let dd = make (DData(pub_type, cd_name, named_type_args, [ ctor ])) in
+      let args = List.map tr_named_type_arg args in
+      let ctors = [ make { cd_name; cd_named_args; cd_arg_schemes = [] } ] in
+      let dd =
+        make (DData { public_tp; public_ctors; tvar = cd_name; args; ctors })
+      in
       let method_named_args, pattern_gen =
-        generate_accessor_method_pattern named_type_args cd_name in
+        generate_accessor_method_pattern args cd_name in
       dd :: List.filter_map
         (create_accessor_method
-          ~public:pub_ctors method_named_args pattern_gen)
-        cd_named
+          ~public:public_ctors method_named_args pattern_gen)
+        cd_named_args
     end
   | DData(vis, tp, cs) ->
-    let (pub_type, pub_ctors) = tr_data_vis ~public def.pos vis in
+    let (public_tp, public_ctors) = tr_data_vis ~public def.pos vis in
     [ match tr_type_def tp [] with
-      | TD_Id(x, args) ->
-        make (DData(pub_type, x,
-          List.map tr_named_type_arg args,
-          List.map (tr_ctor_decl ~public:pub_ctors) cs))
+      | TD_Id(tvar, args) ->
+        let args = List.map tr_named_type_arg args in
+        let ctors = List.map tr_ctor_decl cs in
+        make (DData { public_tp; public_ctors; tvar; args; ctors })
     ]
-  | DLabel(pub, pat) ->
+  | DLabel(pub, pat, eff_opt) ->
     let public = public || pub in
-    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
-    [ make (DLabel (eff_opt, pat)) ]
-  | DHandle(pub, pat, body, hcs) ->
+    let pat = tr_pattern ~public pat in
+    let eff = tr_type_arg_opt def.pos eff_opt in
+    [ make (DLabel (eff, pat)) ]
+  | DHandle(pub, pat, eff_opt, body, hcs) ->
     let public = public || pub in
-    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let pat = tr_pattern ~public pat in
+    let eff = tr_type_arg_opt def.pos eff_opt in
     let body = tr_expr body in
     let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
     let body = { body with data = EHandler(body, rcs, fcs) } in
-    [ make (DHandlePat(eff_opt, pat, body)) ]
-  | DHandleWith(pub, pat, body) ->
+    [ make (DHandlePat(pat, eff, body)) ]
+  | DHandleWith(pub, pat, eff_opt, body) ->
     let public = public || pub in
-    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let pat = tr_pattern ~public pat in
+    let eff = tr_type_arg_opt def.pos eff_opt in
     let body = tr_expr body in
-    [ make (DHandlePat(eff_opt, pat, body)) ]
+    [ make (DHandlePat(pat, eff, body)) ]
   | DModule(pub, x, defs) ->
     let public = public || pub in
     [ make (DModule(public, x, tr_defs defs)) ]
@@ -791,17 +796,6 @@ and tr_pattern_with_fields ~public (pat : Raw.expr) =
   | _ ->
     (None, tr_pattern ~public pat)
 
-and tr_pattern_with_eff_opt ~public (pat : Raw.expr) =
-  let (flds_opt, pat) = tr_pattern_with_fields ~public pat in
-  (Option.map (tr_eff_opt_fields ~public) flds_opt, pat)
-
-and tr_eff_opt_fields ~public flds =
-  match flds with
-  | [] -> assert false
-  | [{ data = FldEffectVal tp; _ }] -> tr_type_arg ~public tp
-  | { data = FldEffectVal _; _} :: fld :: _ | fld :: _ ->
-    Error.fatal (Error.desugar_error fld.pos)
-
 and tr_h_clause (hc : Raw.h_clause) =
   let make data = { hc with data = data } in
   match hc.data with
@@ -820,50 +814,62 @@ and generate_accessor_method_pattern named_type_args type_name =
   let create_mapping i arg =
     let old_name, new_name =
       match (snd arg.data).data with
-      | TA_Var(_, name, _) -> name, name ^ "#TA_Var#" ^ string_of_int i
-      | TA_Effect -> "TNEffect", "TNEffect#TA_Effect#" ^ string_of_int i
+      | TA_Var(name, _) -> name, name ^ "#TA_Var#" ^ string_of_int i
       | TA_Wildcard -> "TNAnon", "TNAnon#TA_Wildcard#" ^ string_of_int i
     in
     let named_arg =
-      make (TNVar old_name, make (TA_Var (false, new_name, make KWildcard))) in
+      make (TNVar old_name, make (TA_Var (new_name, make KWildcard))) in
     named_arg, new_name
   in
   let (new_named_type_args, new_names : named_type_arg list * ctor_name list) =
     List.split (List.mapi create_mapping named_type_args) in
   (* function for fold that generates nested series of tapps for type
      annotation *)
-  let gen_tapps inner name = make (TApp(inner, make (TVar(NPName name)))) in
+  let gen_tapps inner name =
+    make (TApp(inner, make (TVar (make (NPName name))))) in
   let type_annot : scheme_expr =
     { sch_pos = Position.nowhere
-    ; sch_targs = []
-    ; sch_named = []
+    ; sch_args = []
     ; sch_body =
-      List.fold_left gen_tapps (make (TVar(NPName type_name))) new_names
+      List.fold_left
+        gen_tapps
+        (make (TVar (make (NPName type_name))))
+        new_names
     } in
   (* function that generates pattern for accessing field *)
   let pattern_gen field =
-    ArgAnnot(make (PCtor(
+    make (PAnnot(make (PCtor(
       make (NPName type_name),
-      CNParams([], [make (NVar field, make (PId(IdVar(false, field))))]),
-      [])), type_annot) in
+      [ make (NP_Val(NVar field, make (PId(false, IdVar field)))) ],
+      [])), type_annot))
+  in
   new_named_type_args, pattern_gen
 
 and create_accessor_method ~public named_type_args pattern_gen scheme =
   match scheme.data with
-  | NVar field, _ ->
+  | SA_Val(NVar field, _) ->
     let make data = { scheme with data } in
     (* generate accessor body, this piece of code generated accessing
     variable *)
-    let e = make (EPoly(make (EVar(NPName field)), [], [])) in
-    make (DLetFun(IdMethod(public, field),
-      named_type_args,
-      [],
-      make (EFn(pattern_gen field, e))))
-    |> Option.some
-  | (NLabel | NImplicit _ | NMethod _ | NOptionalVar _), _ ->
+    let e =
+      make (EFn(pattern_gen field,
+        make (EPoly(make (EVar (make (NPName field))), [])))) in
+    Some begin match named_type_args with
+    | [] ->
+      make (DLetId(public, IdMethod field, make (PE_Expr e)))
+    | _ :: _ ->
+      let targs =
+        List.map
+          (fun arg -> { arg with data = NP_Type(false, arg) })
+          named_type_args
+      in
+      make (DLetId(public, IdMethod field, make (PE_Fn(targs, e))))
+    end
+  | SA_Val((NImplicit _ | NMethod _ | NOptionalVar _), _) ->
     Error.warn (Error.ignored_field_in_record scheme.pos);
     None
-*)
+  | SA_Type _ ->
+    Error.fatal (Error.existential_type_arg_in_record scheme.pos)
+
 let tr_program (p : Raw.program) =
-  failwith "Not implemented: Desugar.tr_program"
-  (*{ p with data = tr_defs p.data }*)
+  { p with data = tr_defs p.data }
diff --git a/src/DblParser/Error.ml b/src/DblParser/Error.ml
index 39c47590..efd7eb95 100644
--- a/src/DblParser/Error.ml
+++ b/src/DblParser/Error.ml
@@ -75,9 +75,6 @@ let impure_scheme pos =
 let anon_type_pattern pos =
   (Some pos, "Syntax error. Anonymous types cannot be explicitly bound")
 
-let value_before_type_param pos =
-  (Some pos, "Named value parameter appears before a type parameter")
-
 let finally_before_return_clause pos =
   (Some pos, "Finally clause before return clause")
 
diff --git a/src/DblParser/Error.mli b/src/DblParser/Error.mli
index fa129dd7..aa64afbc 100644
--- a/src/DblParser/Error.mli
+++ b/src/DblParser/Error.mli
@@ -37,7 +37,6 @@ val invalid_pattern_arg : Position.t -> t
 val impure_scheme : Position.t -> t
 val anon_type_pattern : Position.t -> t
 
-val value_before_type_param : Position.t -> t
 val finally_before_return_clause : Position.t -> t
 
 val multiple_self_parameters : Position.t -> t
diff --git a/src/DblParser/Import.ml b/src/DblParser/Import.ml
index fafd0035..3a3e1dd8 100644
--- a/src/DblParser/Import.ml
+++ b/src/DblParser/Import.ml
@@ -137,18 +137,17 @@ let top_sort mods =
 (** Prepend a module alias based on the given import directive to the list
     of definitions, or open the module directly if no new name is specified. *)
 let add_import import defs =
-  failwith "Not implemented: DblParser.Import.add_import"
-(*
   let open Lang.Surface in
   let make data = { import with data } in
   let mod_id, new_name = import.data in
+  let mod_path = make (NPName mod_id) in
   match new_name with
   | Some new_name ->
-    make (DModule(false, new_name, [ make (DOpen(true, NPName mod_id)) ]))
+    make (DModule(false, new_name, [ make (DOpen(true, mod_path)) ]))
     :: defs
   | None ->
-    make (DOpen(false, NPName mod_id)) :: defs
-*)
+    make (DOpen(false, mod_path)) :: defs
+
 let add_imports = List.fold_right add_import
 
 let import_many imported imports =
diff --git a/src/DblParser/Lexer.mll b/src/DblParser/Lexer.mll
index 4cbf41c7..f1492981 100644
--- a/src/DblParser/Lexer.mll
+++ b/src/DblParser/Lexer.mll
@@ -7,36 +7,35 @@
 {
 let kw_map =
   let open YaccParser in
-  [ "abstr",    KW_ABSTR
-  ; "as",       KW_AS
-  ; "data",     KW_DATA
-  ; "effect",   KW_EFFECT
-  ; "effrow",   KW_EFFROW
-  ; "else",     KW_ELSE
-  ; "end",      KW_END
-  ; "extern",   KW_EXTERN
-  ; "finally",  KW_FINALLY
-  ; "fn",       KW_FN
-  ; "handle",   KW_HANDLE
-  ; "handler",  KW_HANDLER
-  ; "if",       KW_IF
-  ; "implicit", KW_IMPLICIT
-  ; "import",   KW_IMPORT
-  ; "in",       KW_IN
-  ; "label",    KW_LABEL
-  ; "let",      KW_LET
-  ; "match",    KW_MATCH
-  ; "method",   KW_METHOD
-  ; "module",   KW_MODULE
-  ; "of",       KW_OF
-  ; "open",     KW_OPEN
-  ; "pub",      KW_PUB
-  ; "rec",      KW_REC
-  ; "return",   KW_RETURN
-  ; "then",     KW_THEN
-  ; "type",     KW_TYPE
-  ; "with",     KW_WITH
-  ; "_",        UNDERSCORE
+  [ "abstr",     KW_ABSTR
+  ; "as",        KW_AS
+  ; "data",      KW_DATA
+  ; "effect",    KW_EFFECT
+  ; "else",      KW_ELSE
+  ; "end",       KW_END
+  ; "extern",    KW_EXTERN
+  ; "finally",   KW_FINALLY
+  ; "fn",        KW_FN
+  ; "handle",    KW_HANDLE
+  ; "handler",   KW_HANDLER
+  ; "if",        KW_IF
+  ; "import",    KW_IMPORT
+  ; "in",        KW_IN
+  ; "label",     KW_LABEL
+  ; "let",       KW_LET
+  ; "match",     KW_MATCH
+  ; "method",    KW_METHOD
+  ; "module",    KW_MODULE
+  ; "of",        KW_OF
+  ; "open",      KW_OPEN
+  ; "parameter", KW_PARAMETER
+  ; "pub",       KW_PUB
+  ; "rec",       KW_REC
+  ; "return",    KW_RETURN
+  ; "then",      KW_THEN
+  ; "type",      KW_TYPE
+  ; "with",      KW_WITH
+  ; "_",         UNDERSCORE
   ] |> List.to_seq |> Hashtbl.of_seq
 
 (* let op_map = Hashtbl.create 32 *)
diff --git a/src/DblParser/Raw.ml b/src/DblParser/Raw.ml
index 9a99a0b0..df298524 100644
--- a/src/DblParser/Raw.ml
+++ b/src/DblParser/Raw.ml
@@ -29,8 +29,7 @@ type var_id =
   | VIdUOp of op_name
 
 (** Name of a named parameter *)
-type name =
-  | NLabel
+type name = Lang.Surface.name =
   | NVar         of var
   | NOptionalVar of var
   | NImplicit    of iname
@@ -47,10 +46,10 @@ type ctor_name =
 (** Names of modules *)
 type module_name = string
 
-(** Module path to an identifier of type 'a *)
-type 'a path =
+type 'a path = 'a path_data node
+and 'a path_data = 'a Lang.Surface.path_data =
   | NPName of 'a
-  | NPSel  of module_name * 'a path
+  | NPSel  of module_name path * 'a
 
 (** Kind expressions *)
 type kind_expr = kind_expr_data node
@@ -73,12 +72,6 @@ type ('tp, 'e) field_data =
   | FldAnonType of 'tp
     (** Anonymous type *)
 
-  | FldEffect
-    (** Effect associated with effect handler *)
-
-  | FldEffectVal of 'tp
-    (** Effect associated with effect handler, together with its value *)
-
   | FldType of tvar * kind_expr option
     (** Named type, possibly kind-annotated *)
 
@@ -94,9 +87,12 @@ type ('tp, 'e) field_data =
   | FldNameAnnot of name * 'tp
     (** type-annotated implicit parameter *)
 
-  | FldModule of module_name
+  | FldModule of module_name path
     (** Module grouping named parameters *)
 
+  | FldOpen
+    (** Introduce everything from a scheme into the environment *)
+
 (** Type expressions *)
 type type_expr = type_expr_data node
 and type_expr_data =
@@ -112,8 +108,8 @@ and type_expr_data =
   | TArrow of type_expr * type_expr
     (** Arrow type. The second parameter might have an effect. *)
 
-  | TEffect of type_expr list * type_expr option
-    (** Effect: list of simple effect optionally closed by another effect *)
+  | TEffect of type_expr list
+    (** Effect: list of simple effect *)
 
   | TApp of type_expr * type_expr
     (** Type application *)
@@ -124,9 +120,6 @@ and type_expr_data =
   | TTypeLbl of type_expr
     (** Label of anonymous type parameter of ADT *)
 
-  | TEffectLbl of type_expr
-    (** Label of effect type parameter of ADT *)
-
 (** Field of record-like type *)
 and ty_field = (type_expr, type_expr) field_data node
 
@@ -196,7 +189,12 @@ and expr_data =
   | EHandler of expr * h_clause list
     (** First-class handler *)
 
-  | EEffect of expr list * expr option * expr
+  | EEffect of
+    { label      : expr option;
+      args       : expr list;
+      resumption : expr option;
+      body       : expr
+    }
     (** Handler of a single operation *)
 
   | ERecord of field list
@@ -247,8 +245,8 @@ and def_data =
   | DLet of is_public * expr * expr
     (** Let-definition *)
 
-  | DImplicit of iname * type_expr list * type_expr option
-    (** Declaration of implicit parameter *)
+  | DParam of field
+    (** Declaration of a parameter *)
 
   | DRecord of data_vis * type_expr * ty_field list
     (** Definition of record-like type *)
@@ -256,13 +254,13 @@ and def_data =
   | DData of data_vis * type_expr * ctor_decl list
     (** Definition of ADT *)
 
-  | DLabel of is_public * expr
+  | DLabel of is_public * expr * type_expr option
     (** Creating a new label *)
 
-  | DHandle of is_public * expr * expr * h_clause list
+  | DHandle of is_public * expr * type_expr option * expr * h_clause list
     (** Effect handler *)
 
-  | DHandleWith of is_public * expr * expr
+  | DHandleWith of is_public * expr * type_expr option * expr
     (** Effect handler, with first-class handler *)
 
   | DMethod of is_public * expr * expr
diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly
index 16b56f48..b3c0efa1 100644
--- a/src/DblParser/YaccParser.mly
+++ b/src/DblParser/YaccParser.mly
@@ -12,9 +12,10 @@
 %token<char> CHR
 %token BR_OPN BR_CLS SBR_OPN SBR_CLS CBR_OPN CBR_CLS
 %token ARROW ARROW2 BAR COLON COMMA DOT EQ SEMICOLON2 SLASH GT_DOT
-%token KW_ABSTR KW_AS KW_DATA KW_EFFECT KW_EFFROW KW_ELSE KW_END KW_EXTERN
-%token KW_FINALLY KW_FN KW_HANDLE KW_HANDLER KW_IF KW_IMPLICIT KW_IMPORT
-%token KW_IN KW_LABEL KW_LET KW_MATCH KW_METHOD KW_MODULE KW_OF KW_OPEN KW_PUB
+%token KW_ABSTR KW_AS KW_DATA KW_EFFECT KW_ELSE KW_END KW_EXTERN
+%token KW_FINALLY KW_FN KW_HANDLE KW_HANDLER KW_IF KW_IMPORT
+%token KW_IN KW_LABEL KW_LET KW_MATCH KW_METHOD KW_MODULE KW_OF KW_OPEN
+%token KW_PARAMETER KW_PUB
 %token KW_REC
 %token KW_RETURN KW_THEN KW_TYPE KW_WITH
 %token UNDERSCORE
@@ -67,16 +68,15 @@ var_id
 ;
 
 name
-: KW_LABEL  { NLabel       }
-| LID       { NVar $1      }
+: LID       { NVar $1      }
 | QLID      { NOptionalVar $1 }
 | TLID      { NImplicit $1 }
 | KW_METHOD LID { NMethod $2   }
 ;
 
 uid_path
-: UID              { NPName $1     }
-| UID DOT uid_path { NPSel($1, $3) }
+: UID              { make (NPName $1)     }
+| uid_path DOT UID { make (NPSel($1, $3)) }
 ;
 
 /* ========================================================================= */
@@ -157,7 +157,6 @@ ty_expr
 ty_expr_app
 : ty_expr_app ty_expr_simple { make (TApp($1, $2)) }
 | KW_TYPE   ty_expr_simple { make (TTypeLbl $2)   }
-| KW_EFFECT ty_expr_simple { make (TEffectLbl $2) }
 | ty_expr_simple { $1 }
 ;
 
@@ -187,8 +186,7 @@ kind_expr_simple
 /* ------------------------------------------------------------------------- */
 
 effect
-: ty_expr_list                    { make (TEffect($1, None))    }
-| ty_expr_list BAR ty_expr_simple { make (TEffect($1, Some $3)) }
+: ty_expr_list { make (TEffect($1)) }
 ;
 
 ty_expr_list
@@ -205,8 +203,6 @@ ty_expr_list1
 
 ty_field
 : KW_TYPE ty_expr      { make (FldAnonType $2)       }
-| KW_EFFECT            { make FldEffect              }
-| KW_EFFECT EQ ty_expr { make (FldEffectVal $3)      }
 | UID                  { make (FldType($1, None))    }
 | UID COLON kind_expr  { make (FldType($1, Some $3)) }
 | UID EQ ty_expr       { make (FldTypeVal($1, $3))   }
@@ -246,31 +242,20 @@ ctor_decl_list
 
 /* ========================================================================= */
 
-type_annot_opt
-: /* empty */   { None    }
-| COLON ty_expr { Some $2 }
-;
-
-implicit_ty_args
-: /* empty */                   { [] }
-| CBR_OPN ty_expr_list1 CBR_CLS { $2 }
-;
-
-/* ========================================================================= */
-
 expr
 : def_list1 KW_IN expr  { make (EDefs($1, $3)) }
 | KW_FN expr_250_list1 ARROW2 expr { make (EFn($2, $4))   }
-| KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr
-    { make (EEffect($2, $3, $5)) }
+| effect_label_opt KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr
+    { make (EEffect { label = $1; args = $3; resumption = $4; body = $6 }) }
 | expr_0 { $1 }
 ;
 
 expr_no_comma
 : def_list1 KW_IN expr_no_comma  { make (EDefs($1, $3)) }
 | KW_FN expr_250_list1 ARROW2 expr_no_comma { make (EFn($2, $4))   }
-| KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr_no_comma
-    { make (EEffect($2, $3, $5)) }
+| effect_label_opt KW_EFFECT expr_250_list effect_resumption_opt
+  ARROW2 expr_no_comma
+    { make (EEffect { label = $1; args = $3; resumption = $4; body = $6 }) }
 | expr_0_no_comma { $1 }
 ;
 
@@ -287,11 +272,21 @@ expr_0_no_comma
 | expr_10_no_comma{ $1 }
 ;
 
+effect_label_opt
+: /* empty */  { None    }
+| expr_300 DOT { Some $1 }
+;
+
 effect_resumption_opt
 : /* empty */ { None    }
 | SLASH expr  { Some $2 }
 ;
 
+effect_var_opt
+: /* empty */   { None    }
+| SLASH ty_expr { Some $2 }
+;
+
 expr_10
 : expr_10_open { $1 }
 | expr_10_closed { $1 }
@@ -412,15 +407,11 @@ expr_ctor
 : UID { make (ECtor $1) }
 ;
 
-expr_select
-: UID DOT expr_ctor   { (NPName $1, $3) }
-| UID DOT expr_300    { (NPName $1, $3) }
-| UID DOT expr_select { let (p, e) = $3 in (NPSel($1, p), e) }
-
 expr_250
 : expr_300    { $1 }
 | expr_ctor   { $1 }
-| expr_select { let (p, e) = $1 in make (ESelect(p, e)) }
+| uid_path DOT expr_300  { make (ESelect($1, $3)) }
+| uid_path DOT expr_ctor { make (ESelect($1, $3)) }
 ;
 
 expr_250_list1
@@ -478,14 +469,14 @@ match_clause_list
 
 field
 : KW_TYPE ty_expr       { make (FldAnonType $2)       }
-| KW_EFFECT             { make FldEffect              }
-| KW_EFFECT EQ ty_expr  { make (FldEffectVal $3)      }
 | UID                   { make (FldType($1, None))    }
 | UID EQ ty_expr        { make (FldTypeVal($1, $3))   }
+| UID COLON kind_expr   { make (FldType($1, Some $3)) }
 | name                  { make (FldName $1)           }
 | name EQ expr_no_comma { make (FldNameVal($1, $3))   }
 | name COLON ty_expr    { make (FldNameAnnot($1, $3)) }
-| KW_MODULE UID         { make (FldModule $2)         }
+| KW_MODULE uid_path    { make (FldModule $2)         }
+| KW_OPEN               { make FldOpen                }
 ;
 
 field_list
@@ -513,17 +504,17 @@ rec_opt
 
 def
 : pub KW_LET rec_opt expr_70 EQ expr { make_def $3 (DLet($1, $4, $6)) }
-| KW_IMPLICIT TLID implicit_ty_args type_annot_opt
-    { make (DImplicit($2, $3, $4)) }
+| KW_PARAMETER field { make (DParam $2) }
 | data_vis KW_DATA rec_opt ty_expr EQ bar_opt ctor_decl_list
     { make_def $3  (DData($1, $4, $7)) }
 | data_vis KW_DATA rec_opt ty_expr EQ CBR_OPN ty_field_list CBR_CLS
     { make_def $3  (DRecord($1, $4, $7)) }
-| pub KW_LABEL rec_opt expr_70 { make_def $3 (DLabel($1, $4)) }
-| pub KW_HANDLE rec_opt expr_70 EQ expr h_clauses
-    { make_def $3 (DHandle($1, $4, $6, $7)) }
-| pub KW_HANDLE rec_opt expr_70 KW_WITH expr
-    { make_def $3 (DHandleWith($1, $4, $6)) }
+| pub KW_LABEL rec_opt expr_100 effect_var_opt
+    { make_def $3 (DLabel($1, $4, $5)) }
+| pub KW_HANDLE rec_opt expr_100 effect_var_opt EQ expr h_clauses
+    { make_def $3 (DHandle($1, $4, $5, $7, $8)) }
+| pub KW_HANDLE rec_opt expr_100 effect_var_opt KW_WITH expr
+    { make_def $3 (DHandleWith($1, $4, $5, $7)) }
 | pub KW_METHOD rec_opt expr_70 EQ expr { make_def $3 (DMethod($1, $4, $6)) }
 | pub KW_METHOD KW_FN var_id { make (DMethodFn($1, $4, $4)) }
 | pub KW_METHOD KW_FN var_id EQ var_id { make (DMethodFn($1, $4, $6)) }
diff --git a/test/err/tc_0000_implicitLoop.fram b/test/err/tc_0000_implicitLoop.fram
index 2daa3cca..a8468db0 100644
--- a/test/err/tc_0000_implicitLoop.fram
+++ b/test/err/tc_0000_implicitLoop.fram
@@ -1,5 +1,5 @@
-implicit ~n
+parameter ~n
 let ~n = ~n
 let _ = ~n
 
-# @stderr: infinite loop
\ No newline at end of file
+# @stderr: infinite loop
diff --git a/test/ok/ok0010_implicit.fram b/test/ok/ok0010_implicit.fram
index 6715f9b1..8d259f05 100644
--- a/test/ok/ok0010_implicit.fram
+++ b/test/ok/ok0010_implicit.fram
@@ -1,4 +1,4 @@
-implicit ~a
+parameter ~a
 
 let foo = ~a
 
diff --git a/test/ok/ok0011_implicit.fram b/test/ok/ok0011_implicit.fram
index e527dfcf..f3a8712c 100644
--- a/test/ok/ok0011_implicit.fram
+++ b/test/ok/ok0011_implicit.fram
@@ -1,4 +1,4 @@
-implicit ~id
+parameter ~id
 
 let id = fn x => ~id (~id x)
 
diff --git a/test/ok/ok0018_namePattern.fram b/test/ok/ok0018_namePattern.fram
index 1815d2bc..e4b14cda 100644
--- a/test/ok/ok0018_namePattern.fram
+++ b/test/ok/ok0018_namePattern.fram
@@ -1,4 +1,4 @@
-implicit ~n
+parameter ~n
 
 let foo = fn x => ~n
 
diff --git a/test/ok/ok0025_letFuncImplicit.fram b/test/ok/ok0025_letFuncImplicit.fram
index 71ab32ee..4be1525c 100644
--- a/test/ok/ok0025_letFuncImplicit.fram
+++ b/test/ok/ok0025_letFuncImplicit.fram
@@ -1,4 +1,4 @@
-implicit ~f
+parameter ~f
 
 let foo x = ~f x
 
diff --git a/test/ok/ok0027_explicitApp.fram b/test/ok/ok0027_explicitApp.fram
index 25b007aa..16b801c2 100644
--- a/test/ok/ok0027_explicitApp.fram
+++ b/test/ok/ok0027_explicitApp.fram
@@ -1,3 +1,3 @@
-implicit ~n
+parameter ~n
 let foo = ~n
 let _ = foo { ~n = () }
diff --git a/test/ok/ok0054_firstClassHandler.fram b/test/ok/ok0054_firstClassHandler.fram
index 87857870..5adfee2f 100644
--- a/test/ok/ok0054_firstClassHandler.fram
+++ b/test/ok/ok0054_firstClassHandler.fram
@@ -1,4 +1,4 @@
-let runH {A} h (f : {E} -> (A ->[|E] A) ->[|E] _) =
+let runH {A} h (f : {E} -> (A ->[E] A) ->[E] _) =
   handle x with h in
   f x
 
diff --git a/test/ok/ok0055_complexHandlers.fram b/test/ok/ok0055_complexHandlers.fram
index 729b220a..e4d1a701 100644
--- a/test/ok/ok0055_complexHandlers.fram
+++ b/test/ok/ok0055_complexHandlers.fram
@@ -1,8 +1,8 @@
 data Unit = I
 
 data State E X = State of
-  { get : Unit ->[|E] X
-  , put : X ->[|E] Unit
+  { get : Unit ->[E] X
+  , put : X ->[E] Unit
   }
 
 let hState s =
diff --git a/test/ok/ok0056_complexHandlers.fram b/test/ok/ok0056_complexHandlers.fram
index 0e41913b..f544c85d 100644
--- a/test/ok/ok0056_complexHandlers.fram
+++ b/test/ok/ok0056_complexHandlers.fram
@@ -1,9 +1,9 @@
 data Unit = I
 
 data State E X = State of
-  { get    : Unit ->[|E] X
-  , put    : X ->[|E] Unit
-  , update : (X ->[|E] X) ->[|E] Unit
+  { get    : Unit ->[E] X
+  , put    : X ->[E] Unit
+  , update : (X ->[E] X) ->[E] Unit
   }
 
 let hState s =
diff --git a/test/ok/ok0057_dataArgLabels.fram b/test/ok/ok0057_dataArgLabels.fram
index b0224e86..458c2edd 100644
--- a/test/ok/ok0057_dataArgLabels.fram
+++ b/test/ok/ok0057_dataArgLabels.fram
@@ -1,9 +1,9 @@
 data Unit = I
 
-data State (effect E) (type T) = State of
+data State E (type T) = State of
   { get    : Unit ->[E] T
   , put    : T ->[E] Unit
-  , update : {R} -> (T ->[E|R] T) ->[E|R] Unit
+  , update : {F} -> (T ->[E,F] T) ->[E,F] Unit
   }
 
 let hState s =
diff --git a/test/ok/ok0058_unitState.fram b/test/ok/ok0058_unitState.fram
index d9b5e413..1bc949e6 100644
--- a/test/ok/ok0058_unitState.fram
+++ b/test/ok/ok0058_unitState.fram
@@ -1,10 +1,10 @@
 data Unit = I
 
-data State (effect E) X = State of
+data State E X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
 
 let id x = x
 
-let unitStateCap = State {effect = [], get = id, put = id}
+let unitStateCap = State {E = [], get = id, put = id}
diff --git a/test/ok/ok0059_effectArg.fram b/test/ok/ok0059_effectArg.fram
index 88200deb..2c9b9e51 100644
--- a/test/ok/ok0059_effectArg.fram
+++ b/test/ok/ok0059_effectArg.fram
@@ -1,5 +1,5 @@
-let id {effect} x = x
+let id {E : effect} x = x
 
-let id2 {effect = X} = id {effect = X}
+let id2 {E = X} = id {E = X}
 
 let hId = handler id2 end
diff --git a/test/ok/ok0060_returnFinally.fram b/test/ok/ok0060_returnFinally.fram
index f2364aa4..be6cf1c4 100644
--- a/test/ok/ok0060_returnFinally.fram
+++ b/test/ok/ok0060_returnFinally.fram
@@ -1,11 +1,11 @@
 data Unit = I
 
-data State (effect E) X = State of
+data State E X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
 
-let hState (comp : {effect=E} -> State E _ ->[E|_] _) initSt =
+let hState (comp : {E} -> State E _ ->[E,_] _) initSt =
   handle st = State
     { get = effect I / r => fn s => r s s
     , put = effect s / r => fn _ => r I s
diff --git a/test/ok/ok0062_theLabel.fram b/test/ok/ok0062_theLabel.fram
deleted file mode 100644
index 5690a684..00000000
--- a/test/ok/ok0062_theLabel.fram
+++ /dev/null
@@ -1 +0,0 @@
-let theLabel {effect} {label=x} = x
diff --git a/test/ok/ok0069_effectCtorArg.fram b/test/ok/ok0069_effectCtorArg.fram
index c9a045f9..7d046aa2 100644
--- a/test/ok/ok0069_effectCtorArg.fram
+++ b/test/ok/ok0069_effectCtorArg.fram
@@ -1,3 +1,3 @@
-data T (effect E) = C of (Unit ->[E] Unit)
+data T (E : effect) = C of (Unit ->[E] Unit)
 
 let f {E} (C g : T E) = g
diff --git a/test/ok/ok0070_effectMethodArg.fram b/test/ok/ok0070_effectMethodArg.fram
index da759883..82c8d20f 100644
--- a/test/ok/ok0070_effectMethodArg.fram
+++ b/test/ok/ok0070_effectMethodArg.fram
@@ -1,4 +1,4 @@
-data State (effect E) X = State of
+data State (E : effect) X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
diff --git a/test/ok/ok0074_implicitWithType.fram b/test/ok/ok0074_implicitWithType.fram
index bc9075f0..987f1769 100644
--- a/test/ok/ok0074_implicitWithType.fram
+++ b/test/ok/ok0074_implicitWithType.fram
@@ -1,4 +1,4 @@
-data State (effect E) X = State of
+data State E X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
@@ -6,6 +6,7 @@ data State (effect E) X = State of
 method get {E, self = State { get } : State E _ } = get
 method put {E, self = State { put } : State E _ } = put
 
-implicit ~st { State_Eff } : State State_Eff _
+parameter State_Eff
+parameter ~st : State State_Eff _
 
 let update f = ~st.put (f (~st.get ()))
diff --git a/test/ok/ok0075_effectsFromImplicits.fram b/test/ok/ok0075_effectsFromImplicits.fram
index f9a55858..112e54ac 100644
--- a/test/ok/ok0075_effectsFromImplicits.fram
+++ b/test/ok/ok0075_effectsFromImplicits.fram
@@ -1,4 +1,4 @@
-data StateSig (effect E) X = State of
+data StateSig E X = State of
   { get : Unit ->[E] X
   , put : X ->[E] Unit
   }
@@ -6,7 +6,8 @@ data StateSig (effect E) X = State of
 method get {State, self = State { get } : StateSig State _ } = get
 method put {State, self = State { put } : StateSig State _ } = put
 
-implicit ~st {State} : StateSig State _
+parameter State
+parameter ~st : StateSig State _
 
 let update f =
   ~st.put (f (~st.get ()))
diff --git a/test/ok/ok0086_optionState.fram b/test/ok/ok0086_optionState.fram
index d24752de..9f320c53 100644
--- a/test/ok/ok0086_optionState.fram
+++ b/test/ok/ok0086_optionState.fram
@@ -1,11 +1,12 @@
 data Option A = None | Some of A
 
-data State (effect E) X = State of
+data State E X = State of
   { get    : Unit ->[E] X
   , put    : X ->[E] Unit
   }
 
-implicit ~st {E_st} : State E_st _
+parameter E_st
+parameter ~st : State E_st _
 
 let get x =
   let (State { get }) = ~st in
diff --git a/test/ok/ok0091_namedParamMethod.fram b/test/ok/ok0091_namedParamMethod.fram
index d7ba8237..905f3844 100644
--- a/test/ok/ok0091_namedParamMethod.fram
+++ b/test/ok/ok0091_namedParamMethod.fram
@@ -1,7 +1,7 @@
 data rec List A = Nil | Cons of A, List A
 
 let fix {type A, type B, type E} f =
-  data rec Fix = Fix of (Fix -> A ->[|E] B)
+  data rec Fix = Fix of (Fix -> A ->[E] B)
   let fi ix x = let Fix fi = ix in f (fi ix) x in
   fi (Fix fi)
 
diff --git a/test/ok/ok0100_polymorphicRecursion.fram b/test/ok/ok0100_polymorphicRecursion.fram
index ebfa6851..4f2b3f16 100644
--- a/test/ok/ok0100_polymorphicRecursion.fram
+++ b/test/ok/ok0100_polymorphicRecursion.fram
@@ -1,7 +1,7 @@
 data Sqr A = (,) of A, A
 data rec Tree A = Leaf | Node of Tree (Sqr A)
 
-let rec (map : {A,B,E} -> (A ->[|E] B) -> Tree A ->[|E] Tree B) =
+let rec (map : {A,B,E} -> (A ->[E] B) -> Tree A ->[E] Tree B) =
   fn f t =>
     match t with
     | Leaf   => Leaf
diff --git a/test/ok/ok0107_polymorphicRecursion.fram b/test/ok/ok0107_polymorphicRecursion.fram
index a6de6e81..3b599aa6 100644
--- a/test/ok/ok0107_polymorphicRecursion.fram
+++ b/test/ok/ok0107_polymorphicRecursion.fram
@@ -1,7 +1,7 @@
 data Sqr A = (,) of A, A
 data rec Tree A = Leaf | Node of Tree (Sqr A)
 
-method rec map {A,B, self : Tree A} (f : A ->[|_] B) =
+method rec map {A,B, self : Tree A} (f : A ->[_] B) =
   match self with
   | Leaf   => Leaf
   | Node t => Node (t.map (fn (x, y) => (f x, f y)))
diff --git a/test/ok/ok0118_parameter.fram b/test/ok/ok0118_parameter.fram
new file mode 100644
index 00000000..85561501
--- /dev/null
+++ b/test/ok/ok0118_parameter.fram
@@ -0,0 +1,9 @@
+parameter X
+parameter Y : type -> type
+parameter type Z
+parameter E : effect
+parameter x
+parameter y : Y Z
+parameter ?opt
+parameter ~named : X ->[E] Z
+parameter method m : X -> X ->[] Z
diff --git a/test/ok/ok0119_patternOpen.fram b/test/ok/ok0119_patternOpen.fram
new file mode 100644
index 00000000..46914942
--- /dev/null
+++ b/test/ok/ok0119_patternOpen.fram
@@ -0,0 +1,6 @@
+data T X = C of {x : X, y : X}
+
+let f (C {open, y = z}) =
+  let x = C {x, y}
+  let y = C {y, z} in
+  C {x, y}