Repository: tweag/nickel
Pull request #616 (2022-02-18 15:41:00)

Uniterm
Merge the feature branch bringing the unified syntax for terms and types (RFC002). Skipping review as it has already been reviewed in two parts in #609 and #612.


Patch:
diff --git a/examples/config-gcc/config-gcc.ncl b/examples/config-gcc/config-gcc.ncl
index a944eba9..ee01c987 100644
--- a/examples/config-gcc/config-gcc.ncl
+++ b/examples/config-gcc/config-gcc.ncl
@@ -52,15 +52,15 @@ let OptLevel = fun label value =>
 
 let Contract = {
   path_libc | doc "Path to libc."
-           | #Path
-           | #SharedObjectFile
-           | default = "/lib/x86_64-linux-gnu/libc.so",
+            | Path
+            | SharedObjectFile
+            | default = "/lib/x86_64-linux-gnu/libc.so",
 
   flags | doc "
             Additional flags to pass to GCC. Either provide a string without the
             leading `-`, or a structured value `{flag : Str, arg: Str}`.
           "
-        | List #GccFlag
+        | List GccFlag
         | default = [],
 
   optimization_level | doc "
@@ -70,11 +70,11 @@ let Contract = {
                         - *1*: normal
                         - *2*: use optimizations
                       "
-                    | #OptLevel
-                    | default = 1,
+                     | OptLevel
+                     | default = 1,
 } in
 
 {
   flags = ["Wextra", {flag = "o", arg = "stuff.o"}],
   optimization_level = 2,
-} | #Contract
+} | Contract
diff --git a/examples/record-contract/record-contract.ncl b/examples/record-contract/record-contract.ncl
index 90b98e7a..232abe2d 100644
--- a/examples/record-contract/record-contract.ncl
+++ b/examples/record-contract/record-contract.ncl
@@ -12,17 +12,17 @@ let PortElt
   | doc "A contract for a port element of a Kubernetes configuration"
   = {
     name | Str,
-    containerPort | #Port,
+    containerPort | Port,
   } in
 
 let Container = {
   name | Str,
   image | Str,
-  ports | List #PortElt,
+  ports | List PortElt,
 } in
 
 let KubernetesConfig = {
-  kind | <ReplicationController, ReplicaSet, Pod>
+  kind | [| ReplicationController, ReplicaSet, Pod |]
        | doc "The kind of the element being configured."
        | default = `Pod,
 
@@ -34,7 +34,7 @@ let KubernetesConfig = {
   },
 
   spec = {
-    replicas | #nums.PosNat
+    replicas | nums.PosNat
              | doc "The number of replicas"
              | default = 1,
 
@@ -42,7 +42,7 @@ let KubernetesConfig = {
 
     template = {
       metadata.labels.app | Str,
-      spec.containers | List #Container,
+      spec.containers | List Container,
     },
   },
 } in
@@ -81,4 +81,4 @@ let metadata_ = {
         }
     }
   }
-} | #KubernetesConfig
+} | KubernetesConfig
diff --git a/examples/simple-contracts/simple-contract-bool.ncl b/examples/simple-contracts/simple-contract-bool.ncl
index f636bd69..411daa4f 100644
--- a/examples/simple-contracts/simple-contract-bool.ncl
+++ b/examples/simple-contracts/simple-contract-bool.ncl
@@ -14,5 +14,5 @@ let AlwaysFalse = EqualsTo false in
 // promise that the return value is false.
 // Try passing `false` to `not`, or to use the identity function (replacing `!x`
 // by `x`) to see contract errors appear.
-let not | #AlwaysTrue -> #AlwaysFalse = fun x => !x in
+let not | AlwaysTrue -> AlwaysFalse = fun x => !x in
 not true
diff --git a/examples/simple-contracts/simple-contract-div.ncl b/examples/simple-contracts/simple-contract-div.ncl
index 90655cce..8e33eef5 100644
--- a/examples/simple-contracts/simple-contract-div.ncl
+++ b/examples/simple-contracts/simple-contract-div.ncl
@@ -12,5 +12,5 @@ let DivBy3 = fun label value =>
   else
     contracts.blame label in
 // Will cause an error! 4 is no divided by 3.
-(4 | #Even
-   | #DivBy3)
+(4 | Even
+   | DivBy3)
diff --git a/flake.lock b/flake.lock
index af4da6bf..bcfdee51 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "flake-utils": {
       "locked": {
-        "lastModified": 1644229661,
-        "narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=",
+        "lastModified": 1642700792,
+        "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797",
+        "rev": "846b2ae0fc4cc943637d3d1def4454213e203cba",
         "type": "github"
       },
       "original": {
@@ -32,11 +32,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1644525281,
-        "narHash": "sha256-D3VuWLdnLmAXIkooWAtbTGSQI9Fc1lkvAr94wTxhnTU=",
+        "lastModified": 1643805626,
+        "narHash": "sha256-AXLDVMG+UaAGsGSpOtQHPIKB+IZ0KSd9WS77aanGzgc=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "48d63e924a2666baf37f4f14a18f19347fbd54a2",
+        "rev": "554d2d8aa25b6e583575459c297ec23750adb6cb",
         "type": "github"
       },
       "original": {
@@ -87,11 +87,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1644633594,
-        "narHash": "sha256-Te6mBYYirUwsoqENvVx1K1EEoRq2CKrTnNkWF42jNgE=",
+        "lastModified": 1644027577,
+        "narHash": "sha256-PnmH8XLZr2bH/AtdjJX5RDl9j/jvror4Udqwz4ljvSo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "14c48021a9a5fe6ea8ae6b21c15caa106afa9d19",
+        "rev": "01b7c9b7130faa2856a1d3f226f5e42dcaae744b",
         "type": "github"
       },
       "original": {
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 329d4459..f078c51c 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -1,3 +1,39 @@
+//! The Nickel grammar.
+//!
+//! # Uniterm
+//!
+//! Nickel uses the uniterm grammar since
+//! [RFC002](../rfcs/002-merge-types-terms-syntax.md). Uniterm is a common
+//! grammar for both term and types. However, it is only a front-end: the rest of
+//! the interpreter pipeline needs terms and types to be separate objects.
+//!
+//! Most of the time, grammar constructs determine unambiguously if an expression
+//! should be considered as a type or a term. Typically, `e1 -> e2` will always
+//! be a type, and `e1 + e2` a term. This doesn't contradict the fact that `e1 ->
+//! e2` can be used as a term: the point is, even in the latter case, we still
+//! parse `e1 -> e2` as a type first, and then derive a term from it wherever it
+//! is used in a context expecting a term.
+//!
+//! This is not the case of all rules. Record literals and variables can both be
+//! interpreted in a different way, depending on how their usage. In
+//! `x : {foo : Num}`, `{foo : Num}` is interpreted as a record type. In `{foo :
+//! Num}.foo`, it is a record literal with a missing definition for `foo`. The
+//! first interpretation is **not** equivalent to first interpreting it as a
+//! term, and then as a type.
+//!
+//! For those reasons, the `uniterm` module introduces a new AST definition, that
+//! just wraps `RichTerm` and `Types`, together with dedicated variants for the
+//! common constructs that are variables and records. As long as a common
+//! construct is not used in a term or a type context, it can be still
+//! interpreted as both. Once the usage determines the nature of a record or a
+//! variable, it is converted to either a `RichTerm` or a `Types` (although still
+//! possibly wrapped as a `UniTerm`).
+//!
+//! In consequence, this grammar uses three main types `RichTerm`, `Types` and
+//! `UniTerm`, as well as conversion macros `AsTerm`, `AsType` and `AsUniTerm`.
+//! Some rules that are known to only produce `RichTerm` or `Types` may have the
+//! corresponding more precise return type. Other rules that produce or just
+//! propagate general uniterms have to return a `UniTerm`.
 use std::{
     collections::HashMap,
     ffi::OsString,
@@ -12,7 +48,7 @@ use super::{
     utils::*,
     lexer::{Token, NormalToken, StringToken, MultiStringToken},
     error::ParseError,
-    uniterm::UniRecord,
+    uniterm::*,
 };
 
 use crate::{
@@ -37,15 +73,28 @@ AsTerm<Rule>: RichTerm = <ut: WithPos<Rule>> =>?
     RichTerm::try_from(ut)
         .map_err(|e| lalrpop_util::ParseError::User{error: e});
 
-AsTypes<Rule>: Types = <ut: WithPos<Rule>> =>?
+AsType<Rule>: Types = <ut: WithPos<Rule>> =>?
     Types::try_from(ut)
         .map_err(|e| lalrpop_util::ParseError::User{error: e});
 
-AnnotAtom: MetaValue = {
-    "|" <l: @L> <ty_res: Types> <r: @R> => MetaValue {
+AsUniTerm<Rule>: UniTerm = <l: @L> <ut: Rule> <r: @R> =>
+    UniTerm::from(ut).with_pos(mk_pos(src_id, l, r));
+
+// A single type or meta-data annotation. The `Types` rule forbids the use of
+// constructs that can themselves have annotation on the right, such as a `let`.
+// Otherwise, `foo | let x = 1 in x : Num` is ambiguous (the annotation could be
+// either `foo | (let x = 1 in (x : Num))` or `(foo | let x = 1 in x) : Num`).
+//
+// The rule to use for type annotations is given as a parameter. We always use a
+// rule that is syntactically equivalent to the `Types` rule. The parameter is
+// here to control if the type should have its variables fixed now (`FixedType`)
+// or later (bare `Types`). Almost all rules are of the former kind, and use
+// `FixedType` (see `FixedType` and `parser::utils::fix_type_vars`).
+AnnotAtom<TypeRule>: MetaValue = {
+    "|" <l: @L> <ty: TypeRule> <r: @R> => MetaValue {
         doc: None,
         types: None,
-        contracts: vec![Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}],
+        contracts: vec![Contract {types: ty.clone(), label: mk_label(ty, src_id, l, r)}],
         priority: Default::default(),
         value: None,
     },
@@ -63,27 +112,40 @@ AnnotAtom: MetaValue = {
         priority: Default::default(),
         value: None,
     },
-    ":" <l: @L> <ty_res: Types> <r: @R> => MetaValue {
+    ":" <l: @L> <ty: TypeRule> <r: @R> => MetaValue {
         doc: None,
-        types: Some(Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}),
+        types: Some(Contract {types: ty.clone(), label: mk_label(ty, src_id, l, r)}),
         contracts: Vec::new(),
         priority: Default::default(),
         value: None,
     },
 };
 
-DefaultAnnot: MetaValue = "?" <t: Term> => MetaValue {
-    priority: MergePriority::Default,
-    value: Some(t),
-    ..Default::default()
-};
+// An annotation, with possibly many metadata annotations chained.
+Annot<TypeRule>: MetaValue = <anns: AnnotAtom<TypeRule>+> => anns.into_iter().fold(MetaValue::new(), MetaValue::flatten);
 
-Annot: MetaValue = <anns: AnnotAtom+> => anns.into_iter().fold(MetaValue::new(), MetaValue::flatten);
+// A general term. Wrap the root of the grammar as a `RichTerm`.
+pub Term: RichTerm = AsTerm<UniTerm>;
 
-pub Term: RichTerm = WithPos<RootTerm>;
+// A general type. Chosen such that it can't have top-level annotations.
+// (see `AnnotAtom`)
+Types: Types = {
+    AsType<InfixExpr>,
+    Forall,
+};
 
+// A type with type variables fixed. See `parser::utils::fix_type_vars`.
+FixedType: Types = {
+    <mut ty: Types> => {
+        fix_type_vars(&mut ty);
+        ty
+    }
+};
+
+// Either a term or a top-level let-binding (a let-binding without an `in`).
+// Used exclusively for the REPL.
 pub ExtendedTerm: ExtendedTerm = {
-    "let" <id: Ident> <meta: Annot?> "=" <t: Term> => {
+    "let" <id: Ident> <meta: Annot<FixedType>?> "=" <t: Term> => {
         let t = if let Some(mut meta) = meta {
             let pos = t.pos;
             meta.value = Some(t);
@@ -92,14 +154,20 @@ pub ExtendedTerm: ExtendedTerm = {
         else {
             t
         };
+
         ExtendedTerm::ToplevelLet(id, t)
     },
     Term => ExtendedTerm::RichTerm(<>),
-}
+};
 
-RootTerm: RichTerm = {
-    "let" <pat:Pattern> <meta: Annot?> "=" <t1: Term> "in"
-        <t2: Term> => {
+// A general uniterm. The root of the grammar.
+UniTerm: UniTerm = {
+    InfixExpr,
+    AnnotatedInfixExpr,
+    AsUniTerm<Forall>,
+    "let" <pat:Pattern> <meta: Annot<FixedType>?>
+        "=" <t1: Term>
+        "in" <t2: Term> => {
         let t1 = if let Some(mut meta) = meta {
             let pos = t1.pos;
             meta.value = Some(t1);
@@ -109,16 +177,18 @@ RootTerm: RichTerm = {
             t1
         };
 
-        mk_term::let_pat(pat.0, pat.1, t1, t2)
+        UniTerm::from(mk_term::let_pat(pat.0, pat.1, t1, t2))
     },
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
-        pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
+        let rt = pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
             term: SharedTerm::new(Term::FunPattern(id, destruct, t)),
             pos,
-        })
+        });
+
+        UniTerm::from(rt)
     },
-    "switch" "{" <cases: (switch_case ",")*> <last: switch_case?> "}"
+    "switch" "{" <cases: (SwitchCase ",")*> <last: SwitchCase?> "}"
         <exp: Term> => {
         let mut acc = HashMap::with_capacity(cases.len());
         let mut default = None;
@@ -132,7 +202,7 @@ RootTerm: RichTerm = {
             };
         }
 
-        RichTerm::from(
+        UniTerm::from(
             Term::Switch(
                 exp,
                 acc,
@@ -141,59 +211,89 @@ RootTerm: RichTerm = {
         )
     },
     "if" <cond: Term> "then" <t1: Term> "else" <t2: Term> =>
-        mk_app!(Term::Op1(UnaryOp::Ite(), cond), t1, t2),
-    AnnotatedTerm,
-    <l: @L> <t: !> <r: @R> => { errors.push(t); RichTerm { term: SharedTerm::new(Term::ParseError), pos: mk_pos(src_id, l, r)} },
-};
+        UniTerm::from(mk_app!(Term::Op1(UnaryOp::Ite(), cond), t1, t2)),
+    <l: @L> <t: !> <r: @R> => {
+        let pos = mk_pos(src_id, l, r);
+        errors.push(t);
 
-AnnotatedTerm: RichTerm = {
-    <t: WithPos<Infix>> <meta: Annot?> => {
-        if let Some(mut meta) = meta {
-            let pos = t.pos;
-            meta.value = Some(t);
-            RichTerm::new(Term::MetaValue(meta), pos)
-        }
-        else {
-            t
-        }
+        UniTerm::from(RichTerm::new(Term::ParseError, pos))
     },
 };
 
-Infix: RichTerm = {
-    InfixExpr,
+AnnotatedInfixExpr: UniTerm = {
+    <t: AsTerm<InfixExpr>> <mut meta: Annot<FixedType>> => {
+        let pos = t.pos;
+        meta.value = Some(t);
+        UniTerm::from(RichTerm::new(Term::MetaValue(meta), pos))
+    },
 };
 
-Applicative: RichTerm = {
-    "import" <s: StaticString> => RichTerm::from(Term::Import(OsString::from(s))),
-    <t1:WithPos<Applicative>> <t2: WithPos<RecordOperand>> => mk_app!(t1, t2),
-    <op: UOp> <t: WithPos<RecordOperand>> => mk_term::op1(op, t),
-    <op: BOpPre> <t1: WithPos<RecordOperand>> <t2: WithPos<Atom>> => mk_term::op2(op, t1, t2),
-    NOpPre<WithPos<RecordOperand>>,
+Forall: Types =
+    "forall" <ids: Ident+> "." <ty: Types> => {
+        ids.into_iter().rev().fold(
+            ty,
+            |acc, id| Types(AbsType::Forall(id, Box::new(acc)))
+        )
+    };
+
+// A n-ary application-like expression (n may be 0, in the sense that this rule
+// also includes previous levels).
+Applicative: UniTerm = {
+    "import" <s: StaticString> => UniTerm::from(Term::Import(OsString::from(s))),
+    <t1: AsTerm<Applicative>> <t2: AsTerm<RecordOperand>> =>
+        UniTerm::from(mk_app!(t1, t2)),
+    <op: UOp> <t: AsTerm<RecordOperand>> => UniTerm::from(mk_term::op1(op, t)),
+    <op: BOpPre> <t1: AsTerm<RecordOperand>> <t2: AsTerm<Atom>>
+        => UniTerm::from(mk_term::op2(op, t1, t2)),
+    NOpPre<AsTerm<RecordOperand>>,
     RecordOperand,
 };
 
-RecordOperand: RichTerm = {
+// The list type, potentially with an argument. Take precedence over
+// application: `List Foo` is always interpreted as the type `List` parametrized
+// by `Foo`, rather than the dynamic list type `List Dyn` aliased to `List` and
+// seen as a contract applied to term `Foo`.
+TypeList: Types =
+    "List" <TypeListParam?> => {
+        let ty = Box::new(<>.unwrap_or(Types(AbsType::Dyn())));
+        Types(AbsType::List(ty))
+    };
+
+// Possible parameter for the list type. It's `TypeAtom` augmented with an
+// argument-less `List`, which allows to parse `List List`. We can't add
+// argument-less `List` to type atoms directly, as it would make `List Foo`
+// ambiguous: could be parsed both as `List` as a term applied to `List` as a
+// term, or as the parametrized type `List List`).
+TypeListParam: Types = {
+    "List" => Types(AbsType::List(Box::new(Types(AbsType::Dyn())))),
+    AsType<Atom>,
+};
+
+RecordOperand: UniTerm = {
     Atom,
-    RecordOperationChain,
-}
+    AsUniTerm<RecordOperationChain>,
+};
 
+// A record operation chain, such as `{foo = data}.bar.baz`.
 RecordOperationChain: RichTerm = {
-    <t: WithPos<RecordOperand>> "." <id: Ident> => mk_term::op1(UnaryOp::StaticAccess(id), t),
-    <t: WithPos<RecordOperand>> "." <t_id: WithPos<StrChunks>> => mk_access(t_id, t),
-    <t: WithPos<RecordOperand>> "-$" <t_id: WithPos<Atom>> => mk_term::op2(BinaryOp::DynRemove(), t_id, t),
-    <r: WithPos<RecordOperand>> "$[" <id: Term> "=" <t: Term> "]" =>
+    <t: AsTerm<RecordOperand>> "." <id: Ident> => mk_term::op1(UnaryOp::StaticAccess(id), t),
+    <t: AsTerm<RecordOperand>> "." <t_id: WithPos<StrChunks>> => mk_access(t_id, t),
+    <t: AsTerm<RecordOperand>> "-$" <t_id: AsTerm<Atom>> => mk_term::op2(BinaryOp::DynRemove(), t_id, t),
+    <r: AsTerm<RecordOperand>> "$[" <id: Term> "=" <t: Term> "]" =>
         mk_app!(mk_term::op2(BinaryOp::DynExtend(), id, r), t),
 };
 
 RowTail: Types = {
     <Ident> => Types(AbsType::Var(<>)),
     "Dyn" => Types(AbsType::Dyn()),
-}
+};
 
+// A record, that can be later interpreted either as a record literal or as a
+// record type.
 UniRecord: UniRecord = {
    "{" <fields: (<RecordField> ",")*>
-       <last: RecordLastField?>
-       <l: @L> <tail: (";" RowTail)?> <r: @R>
+       <last_l: @L> <last: RecordLastField?> <last_r: @R>
+       <tail_l: @L> <tail: (";" RowTail)?> <tail_r: @R>
    "}" => {
         let (last_field, attrs) = match last {
             Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
@@ -202,35 +302,48 @@ UniRecord: UniRecord = {
             None => (None, Default::default())
         };
 
+        let pos_ellipsis = if attrs.open {
+                mk_pos(src_id, last_l, last_r)
+            }
+            else {
+                TermPos::None
+            };
+
         let fields : Vec<_> = fields.into_iter().chain(last_field.into_iter()).collect();
         UniRecord {
             fields,
-            tail: tail.map(|t| (t.1, mk_pos(src_id, l, r))),
+            tail: tail.map(|t| (t.1, mk_pos(src_id, tail_l, tail_r))),
             attrs,
-            pos: TermPos::None
+            pos: TermPos::None,
+            pos_ellipsis,
         }
     },
 };
 
-Atom: RichTerm = {
-    "(" <CurriedOp> ")",
-    "(" <Term> ")",
-    "num literal" => RichTerm::from(Term::Num(<>)),
-    "null" => RichTerm::from(Term::Null),
-    Bool => RichTerm::from(Term::Bool(<>)),
-    StrChunks,
-    Ident => RichTerm::from(Term::Var(<>)),
-    AsTerm<UniRecord>,
-    "`" <EnumTag> => RichTerm::from(Term::Enum(<>)),
-     "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
+Atom: UniTerm = {
+    "(" <AsUniTerm<CurriedOp>> ")",
+    "(" <UniTerm> ")",
+    "num literal" => UniTerm::from(Term::Num(<>)),
+    "null" => UniTerm::from(Term::Null),
+    Bool => UniTerm::from(Term::Bool(<>)),
+    AsUniTerm<StrChunks>,
+    Ident => UniTerm::from(UniTermNode::Var(<>)),
+    UniRecord => UniTerm::from(UniTermNode::Record(<>)),
+    "`" <EnumTag> => UniTerm::from(Term::Enum(<>)),
+    "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
         let terms : Vec<RichTerm> = terms.into_iter()
             .chain(last.into_iter()).collect();
-        RichTerm::from(Term::List(terms))
-    }
+
+        UniTerm::from(Term::List(terms))
+    },
+    AsUniTerm<TypeAtom>,
 };
 
-RecordField: (FieldPathElem, RichTerm) = {
-    <l: @L> <path: FieldPath> <ann: Annot?> <r: @R> <t: ("=" <Term>)?> => {
+// A record field definition. The is the only place where we don't fix the type
+// variables inside the annotation right away (note the `Annot<Types>` instead
+// of `Annot<Fixed>`).
+RecordField: (FieldPath, RichTerm) = {
+    <l: @L> <path: FieldPath> <ann: Annot<Types>?> <r: @R> <t: ("=" <Term>)?> => {
         let pos = t.as_ref()
             .map(|t| t.pos.clone())
             .unwrap_or(mk_pos(src_id, l, r));
@@ -244,18 +357,19 @@ RecordField: (FieldPathElem, RichTerm) = {
                 RichTerm::new(Term::Null, pos)
             }
         };
-        elaborate_field_path(path, term)
+
+        (path, term)
     }
-}
+};
 
 RecordLastField: RecordLastField = {
     <RecordField> => RecordLastField::Field(<>),
     ".." => RecordLastField::Ellipsis,
-}
+};
 
+// A field path syntax in a field definition, as in `{foo."bar bar".baz = "value"}`.
 FieldPath: Vec<FieldPathElem> = {
-    <elems: (<FieldPathElem> ".")*> <last: FieldPathElem> => {
-        let mut elems = elems;
+    <mut elems: (<FieldPathElem> ".")*> <last: FieldPathElem> => {
         elems.push(last);
         elems
     }
@@ -266,59 +380,74 @@ FieldPathElem: FieldPathElem = {
     <WithPos<StrChunks>> => FieldPathElem::Expr(<>),
 };
 
-#[inline]
-Pattern: (Option<Ident>,Destruct) = {
-    <id:(<Ident> "@")?> <pat:Destruct> => (id,pat),
-    Ident => (Some(<>),Destruct::Empty),
-};
-
+// A full pattern at the left-hand side of a destructuring let.
 Destruct: Destruct = {
     "{" <mut matches: (<Match> ",")*> <last:LastMatch?> "}" => {
         let (open, rst) = match last {
-	    Some(LastMatch::Match(m)) => {
-	        matches.push(m);
-	        (false,None)
-	    },
-	    Some(LastMatch::Ellipsis(rst)) => (true, rst),
-	    _ => (false, None),
-	};
-	Destruct::Record(matches, open, rst)
+            Some(LastMatch::Match(m)) => {
+                matches.push(m);
+                (false,None)
+            },
+            Some(LastMatch::Ellipsis(rst)) => (true, rst),
+            _ => (false, None),
+        };
+
+        Destruct::Record(matches, open, rst)
     },
 };
 
+// A binding `ident = <pattern>` inside a destructuring pattern.
 Match: Match = {
-    <left:Ident> <anns: Annot?> <default: DefaultAnnot?> "=" <right: Pattern> => {
-	let meta = match (default, anns) {
-	    (Some(d), Some(m)) => MetaValue::flatten(d,m),
-	    (Some(m),_) | (_,Some(m)) => m,
-  	    _ => MetaValue::new(),
-	};
-	Match::Assign(left, meta, right)
+    <left:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> "=" <right: Pattern> => {
+        let meta = match (default, anns) {
+            (Some(d), Some(m)) => MetaValue::flatten(d,m),
+            (Some(m),_) | (_,Some(m)) => m,
+              _ => MetaValue::new(),
+        };
+
+        Match::Assign(left, meta, right)
     },
-    <id:Ident> <anns: Annot?> <default: DefaultAnnot?> => {
-	let meta = match (default, anns) {
-	    (Some(d), Some(m)) => MetaValue::flatten(d,m),
-	    (Some(m),_) | (_,Some(m)) => m,
-  	    _ => MetaValue::new(),
-	};
-	Match::Simple(id, meta)
+    <id:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> => {
+        let meta = match (default, anns) {
+            (Some(d), Some(m)) => MetaValue::flatten(d,m),
+            (Some(m),_) | (_,Some(m)) => m,
+            _ => MetaValue::new(),
+        };
+
+        Match::Simple(id, meta)
     },
 };
 
 LastMatch: LastMatch = {
     Match => LastMatch::Match(<>),
-    ".."<Ident?> => LastMatch::Ellipsis(<>),
+    ".." <Ident?> => LastMatch::Ellipsis(<>),
+};
+
+// The right hand side of an `=` inside a destructuring pattern.
+#[inline]
+Pattern: (Option<Ident>,Destruct) = {
+    <id:(<Ident> "@")?> <pat:Destruct> => (id,pat),
+    Ident => (Some(<>),Destruct::Empty),
+};
+
+// A default annotation in a pattern.
+DefaultAnnot: MetaValue = "?" <t: Term> => MetaValue {
+    priority: MergePriority::Default,
+    value: Some(t),
+    ..Default::default()
 };
 
-Ident: Ident = <l:@L> <i: "identifier"> <r:@R>
-    => Ident { label: i.to_string(), pos: mk_pos(src_id, l, r) };
+
+Ident: Ident = <l:@L> <i: "identifier"> <r:@R> =>
+    Ident { label: i.to_string(), pos: mk_pos(src_id, l, r) };
 
 Bool: bool = {
     "true" => true,
     "false" => false,
 };
 
-StrChunks : RichTerm = {
+// Strings that support interpolation.
+StrChunks: RichTerm = {
   <start: StringStart> <fst: ChunkLiteral?> <chunks: (ChunkExpr+ChunkLiteral)*> <lasts:ChunkExpr*> <end: StringEnd> => {
         debug_assert_eq!(start, end);
 
@@ -378,12 +507,11 @@ EnumTag: Ident = {
     <StaticString> => <>.into(),
 }
 
-
 ChunkLiteralPart: ChunkLiteralPart<'input> = {
     "str literal" => ChunkLiteralPart::Str(<>),
     "multstr literal" => ChunkLiteralPart::Str(<>),
     "str esc char" => ChunkLiteralPart::Char(<>),
-    };
+};
 
 UOp: UnaryOp = {
     "is_num" => UnaryOp::IsNum(),
@@ -422,11 +550,14 @@ UOp: UnaryOp = {
     "enum_from" => UnaryOp::EnumFromStr(),
 };
 
-switch_case: SwitchCase = {
+SwitchCase: SwitchCase = {
     "`" <id: EnumTag> "=>" <t: Term> => SwitchCase::Normal(id, t),
     "_" "=>" <t: Term> => SwitchCase::Default(<>),
 }
 
+// Infix operators by precedence levels. Lowest levels take precedence over
+// highest ones.
+
 InfixBOp2: BinaryOp = {
     "++" => BinaryOp::StrConcat(),
     "@" => BinaryOp::ListConcat(),
@@ -491,7 +622,8 @@ InfixOp: InfixOp = {
 }
 
 CurriedOp: RichTerm = {
-    <l: @L> <op: InfixOp> <r: @R> => op.eta_expand(mk_pos(src_id, l, r)),
+    <l: @L> <op: InfixOp> <r: @R> =>
+        op.eta_expand(mk_pos(src_id, l, r)),
     <l: @L> "|>" <r: @R> =>
         mk_fun!("x1", "x2",
             mk_app!(mk_term::var("x2"), mk_term::var("x1"))
@@ -508,24 +640,40 @@ CurriedOp: RichTerm = {
             )
             .with_pos(mk_pos(src_id, l, r))
         ),
+    //<l: @L> "->" <r: @R> =>?
+    //    UniTerm::from(
+    //        mk_fun!("x1", "x2",
+    //            mk_term::op1(
+    //                UnaryOp::BoolNot(),
+    //                Term::Op2(BinaryOp::Eq(),
+    //                    mk_term::var("x2"),
+    //                    mk_term::var("x1")
+    //                )
+    //            )
+    //            .with_pos(mk_pos(src_id, l, r))
+    //        )
+    //    ),
 }
 
-InfixUOpApp<UOp, Expr>: RichTerm =
-  <op: UOp> <t: WithPos<Expr>> => mk_term::op1(op, t);
+InfixUOpApp<UOp, Expr>: UniTerm =
+  <op: UOp> <t: AsTerm<Expr>> => UniTerm::from(mk_term::op1(op, t));
 
-InfixBOpApp<BOp, LExpr, RExpr>: RichTerm =
-  <t1: WithPos<LExpr>> <op: BOp> <t2: WithPos<RExpr>> => mk_term::op2(op, t1, t2);
+InfixBOpApp<BOp, LExpr, RExpr>: UniTerm =
+  <t1: AsTerm<LExpr>> <op: BOp> <t2: AsTerm<RExpr>> =>
+      UniTerm::from(mk_term::op2(op, t1, t2));
 
-InfixLazyBOpApp<UOp, LExpr, RExpr>: RichTerm =
-  <t1: WithPos<LExpr>> <op: UOp> <t2: WithPos<RExpr>> =>
-    mk_app!(mk_term::op1(op, t1), t2);
+InfixLazyBOpApp<UOp, LExpr, RExpr>: UniTerm =
+  <t1: AsTerm<LExpr>> <op: UOp> <t2: AsTerm<RExpr>> =>
+    UniTerm::from(mk_app!(mk_term::op1(op, t1), t2));
 
-InfixExpr: RichTerm = {
+InfixExpr: UniTerm = {
     #[precedence(level="0")]
     Applicative,
+    AsUniTerm<TypeList>,
 
     #[precedence(level="1")]
-    "-" <WithPos<InfixExpr>> => mk_term::op2(BinaryOp::Sub(), Term::Num(0.0), <>),
+    "-" <AsTerm<InfixExpr>> =>
+        UniTerm::from(mk_term::op2(BinaryOp::Sub(), Term::Num(0.0), <>)),
 
     #[precedence(level="2")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp2, InfixExpr, InfixExpr>,
@@ -541,21 +689,28 @@ InfixExpr: RichTerm = {
 
     #[precedence(level="6")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp6, InfixExpr, InfixExpr>,
-    <t1: WithPos<InfixExpr>> "|>" <t2: WithPos<InfixExpr>> => mk_app!(t2, t1),
+    <t1: AsTerm<InfixExpr>> "|>" <t2: AsTerm<InfixExpr>> =>
+        UniTerm::from(mk_app!(t2, t1)),
 
     #[precedence(level="7")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp7, InfixExpr, InfixExpr>,
 
     #[precedence(level="8")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp8, InfixExpr, InfixExpr>,
-    <t1: WithPos<InfixExpr>> "!=" <t2: WithPos<InfixExpr>> =>
-        mk_term::op1(UnaryOp::BoolNot(), Term::Op2(BinaryOp::Eq(), t1, t2)),
+    <t1: AsTerm<InfixExpr>> "!=" <t2: AsTerm<InfixExpr>> =>
+        UniTerm::from(
+            mk_term::op1(UnaryOp::BoolNot(), Term::Op2(BinaryOp::Eq(), t1, t2))
+        ),
 
     #[precedence(level="9")] #[assoc(side="left")]
     InfixLazyBOpApp<InfixLazyBOp9, InfixExpr, InfixExpr>,
 
     #[precedence(level="10")] #[assoc(side="left")]
     InfixLazyBOpApp<InfixLazyBOp10, InfixExpr, InfixExpr>,
+
+    #[precedence(level="11")] #[assoc(side="right")]
+    <s: AsType<InfixExpr>> "->" <t: AsType<InfixExpr>> =>
+        UniTerm::from(Types(AbsType::Arrow(Box::new(s), Box::new(t)))),
 }
 
 BOpPre: BinaryOp = {
@@ -575,46 +730,25 @@ BOpPre: BinaryOp = {
     "str_is_match" => BinaryOp::StrIsMatch(),
 }
 
-NOpPre<ArgRule>: RichTerm = {
+NOpPre<ArgRule>: UniTerm = {
     "str_replace" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        mk_opn!(NAryOp::StrReplace(), t1, t2, t3),
+        UniTerm::from(mk_opn!(NAryOp::StrReplace(), t1, t2, t3)),
     "str_replace_regex" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        mk_opn!(NAryOp::StrReplaceRegex(), t1, t2, t3),
+        UniTerm::from(mk_opn!(NAryOp::StrReplaceRegex(), t1, t2, t3)),
     "str_substr" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        mk_opn!(NAryOp::StrSubstr(), t1, t2, t3),
+        UniTerm::from(mk_opn!(NAryOp::StrSubstr(), t1, t2, t3)),
 }
 
-Types: Types = {
-    "forall" <ids: Ident+> "." <ty: Arrows> =>
-        ids.into_iter().rev().fold(
-            ty,
-            |acc, id| Types(AbsType::Forall(id, Box::new(acc)))
-        ),
-    <Arrows>
-}
-
-Arrows: Types = {
-    <s: subType> "->" <t:Arrows> => Types(AbsType::Arrow(Box::new(s), Box::new(t))),
-    <subType>,
-};
-
-BaseType: Types = {
+TypeBuiltin: Types = {
     "Dyn" => Types(AbsType::Dyn()),
     "Num" => Types(AbsType::Num()),
     "Bool" => Types(AbsType::Bool()),
     "Str" => Types(AbsType::Str()),
-};
+}
 
-subType : Types = {
-    <BaseType>,
-    "List" <ty: subType?> => {
-        let ty = Box::new(ty.unwrap_or(Types(AbsType::Dyn())));
-        Types(AbsType::List(ty))
-    },
-    <Ident> => Types(AbsType::Var(<>)),
-    "#" <WithPos<RecordOperand>> => Types(AbsType::Flat(<>)),
-    "(" <Types> ")",
-    "<" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: ("|" <EnumTag>)?> ">" => {
+TypeAtom: Types = {
+    <TypeBuiltin>,
+    "[|" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: (";" <EnumTag>)?> "|]" => {
         let ty = rows.into_iter()
             .chain(last.into_iter())
             // As we build row types as a linked list via a fold on the original
@@ -633,9 +767,8 @@ subType : Types = {
             );
         Types(AbsType::Enum(Box::new(ty)))
     },
-    AsTypes<UniRecord>,
     "{" "_" ":" <Types> "}" => Types(AbsType::DynRecord(Box::new(<>))),
-};
+}
 
 extern {
     type Location = usize;
@@ -773,5 +906,7 @@ extern {
         "<=" => Token::Normal(NormalToken::LessOrEq),
         ">" => Token::Normal(NormalToken::RAngleBracket),
         ">=" => Token::Normal(NormalToken::GreaterOrEq),
+        "[|" => Token::Normal(NormalToken::EnumOpen),
+        "|]" => Token::Normal(NormalToken::EnumClose),
     }
 }
diff --git a/src/identifier.rs b/src/identifier.rs
index 570aab72..b096827c 100644
--- a/src/identifier.rs
+++ b/src/identifier.rs
@@ -4,7 +4,7 @@ use std::{fmt, hash::Hash};
 
 use crate::position::TermPos;
 
-#[derive(Debug, Clone, Deserialize, Serialize)]
+#[derive(Debug, Clone, Default, Deserialize, Serialize)]
 #[serde(into = "String", from = "String")]
 pub struct Ident {
     pub label: String,
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 671f8d76..ac237c61 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -282,6 +282,10 @@ pub enum NormalToken<'input> {
     RAngleBracket,
     #[token(">=")]
     GreaterOrEq,
+    #[token("[|")]
+    EnumOpen,
+    #[token("|]")]
+    EnumClose,
     #[regex("//[^\n]*")]
     LineComment,
 }
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
index 4a70384c..cf09bb1b 100644
--- a/src/parser/uniterm.rs
+++ b/src/parser/uniterm.rs
@@ -1,37 +1,175 @@
 //! Additional AST nodes for the common UniTerm syntax (see RFC002 for more details).
 use super::*;
-use crate::types::UnboundTypeVariableError;
 use error::ParseError;
-use utils::{build_record, FieldPathElem};
+use utils::{build_record, elaborate_field_path, FieldPath, FieldPathElem};
 
 use crate::{
     position::{RawSpan, TermPos},
-    term::{MergePriority, MetaValue, RecordAttrs, RichTerm, Term},
-    types::{AbsType, Types},
+    term::{Contract, MergePriority, MetaValue, RecordAttrs, RichTerm, SharedTerm, Term},
+    types::{AbsType, Types, UnboundTypeVariableError},
 };
 
-use std::convert::TryFrom;
+use std::{borrow::Cow, collections::HashSet, convert::TryFrom};
 
-/// A record in the UniTerm syntax.
+/// A node of the uniterm AST. We only define new variants for those constructs that are common to
+/// types and terms. Otherwise, we piggyback on the existing ASTs to avoid duplicating methods and
+/// type definitions.
+///
+/// During parsing, some constructs are common to both terms and types, such as variables or record
+/// literals ([`UniRecord`]s). They may be the source of ambiguities in the grammar, if we add two
+/// different derivation for them. This happens inside rules that accepts both a term and and a
+/// type, say the operands of an arrow `lhs -> rhs`. Take for example `lhs` to be a variable `a`.
+/// It's hard not to end up having two possible derivation for `a`, one going first through term
+/// rules and then types rules (a custom contract `#a` in the old syntax), and vice-versa (a type
+/// variable `a` in the old syntax).
+///
+/// To avoid the issue, we parse the source as a `UniTermNode`s, and give only one possible
+/// derivation - we will continue with the variable example in the following - through the parsing
+/// rules. As long as we can't decide yet how to see this variable, we keep it as a
+/// `UniTermNode::Var`.
+///
+/// As soon as this variable is used in a compound expression, the top-level rule tells us how to
+/// translate it. For example, if we see an arrow `a -> Num`, then we will convert it to a type
+/// variable, and return `UniTermNode::Types(AbsType::Arrow(..))` (there is actually a subtelty:
+/// see [`fix_type_vars`], but let's ignore it here). If, on the other hand, we enter the rule for
+/// an infix operator as in `a + 1`, `a` will be converted to a `Term::Var` and the resulting
+/// uniterm will be `UniTermNode::Term(Term::Op2(..))`.
+pub enum UniTermNode {
+    /// A variable. Can refer both to a term variable or a type variable.
+    Var(Ident),
+    /// A record. Can refer both to a record literal or a record type.
+    Record(UniRecord),
+    /// A uniterm that has been determined to be a term.
+    Term(RichTerm),
+    /// A uniterm that has been determined to be a type.
+    Types(Types),
+}
+
+/// A uniterm with positional information.
+pub struct UniTerm {
+    node: UniTermNode,
+    pos: TermPos,
+}
+
+impl From<UniTermNode> for UniTerm {
+    fn from(node: UniTermNode) -> Self {
+        UniTerm {
+            node,
+            pos: TermPos::None,
+        }
+    }
+}
+
+impl UniTerm {
+    pub fn with_pos(mut self, pos: TermPos) -> Self {
+        self.pos = pos;
+        self
+    }
+}
+
+impl TryFrom<UniTerm> for Types {
+    type Error = ParseError;
+
+    fn try_from(ut: UniTerm) -> Result<Self, ParseError> {
+        match ut.node {
+            UniTermNode::Var(id) => Ok(Types(AbsType::Var(id))),
+            UniTermNode::Record(r) => Types::try_from(r),
+            UniTermNode::Types(ty) => Ok(ty),
+            UniTermNode::Term(rt) => Ok(Types(AbsType::Flat(rt))),
+        }
+    }
+}
+
+impl TryFrom<UniTerm> for RichTerm {
+    type Error = ParseError;
+
+    fn try_from(ut: UniTerm) -> Result<Self, ParseError> {
+        let UniTerm { node, pos } = ut;
+        let rt = match node {
+            UniTermNode::Var(id) => RichTerm::new(Term::Var(id), pos),
+            UniTermNode::Record(r) => RichTerm::try_from(r)?,
+            UniTermNode::Types(ty) => {
+                ty.contract().map_err(|UnboundTypeVariableError(id)| {
+                    // We unwrap the position of the identifier, which must be set at this stage of parsing
+                    let pos = id.pos;
+                    ParseError::UnboundTypeVariables(vec![id], pos.unwrap())
+                })?
+            }
+            UniTermNode::Term(rt) => rt,
+        };
+
+        Ok(rt.with_pos(pos))
+    }
+}
+
+impl From<RichTerm> for UniTerm {
+    fn from(rt: RichTerm) -> Self {
+        let pos = rt.pos;
+
+        UniTerm {
+            node: UniTermNode::Term(rt),
+            pos,
+        }
+    }
+}
+
+impl From<Term> for UniTerm {
+    fn from(t: Term) -> Self {
+        Self::from(RichTerm::from(t))
+    }
+}
+
+impl From<Types> for UniTerm {
+    fn from(ty: Types) -> Self {
+        UniTerm {
+            node: UniTermNode::Types(ty),
+            pos: TermPos::None,
+        }
+    }
+}
+
+impl From<UniRecord> for UniTerm {
+    fn from(ur: UniRecord) -> Self {
+        let pos = ur.pos;
+
+        UniTerm {
+            node: UniTermNode::Record(ur),
+            pos,
+        }
+    }
+}
+
+/// A record in the `UniTerm` syntax.
 #[derive(Clone)]
 pub struct UniRecord {
-    pub fields: Vec<(FieldPathElem, RichTerm)>,
+    pub fields: Vec<(FieldPath, RichTerm)>,
     pub tail: Option<(Types, TermPos)>,
     pub attrs: RecordAttrs,
     pub pos: TermPos,
+    /// The position of the final ellipsis `..`, if any. Used for error reporting. `pos_ellipsis`
+    /// must be different from `TermPos::None` if and only if `attrs.open` is `true`.
+    pub pos_ellipsis: TermPos,
 }
 
 /// Error indicating that a construct is not allowed when trying to interpret an `UniRecord` as a
-/// record type in a strict way. See [`into_type_strict`]. Hold the position of the illegal
-/// construct.
+/// record type in a strict way. See [`UniRecord::into_type_strict`]. Hold the position of the
+/// illegal construct.
 pub struct InvalidRecordTypeError(pub TermPos);
 
 impl UniRecord {
-    /// Try to convert a `UniRecord` to a type. The strict part means that if the `UniRecord` must
-    /// be a plain record type, uniquely containing fields of the form `fields: Type`. Currently,
-    /// it doesn't support the field path syntax: `{foo.bar.baz : Type}.into_type_strict()` returns
-    /// an `Err`.
+    /// Try to convert a `UniRecord` to a type. The strict part means that the `UniRecord` must be
+    /// a plain record type, uniquely containing fields of the form `fields: Type`. Currently, it
+    /// doesn't support the field path syntax: `{foo.bar.baz : Type}.into_type_strict()` returns an
+    /// `Err`.
     pub fn into_type_strict(self) -> Result<Types, InvalidRecordTypeError> {
+        // An open record (with an ellipsis `..` at the end) can't be translated to a record type.
+        // `pos_ellipsis` should be set iff `attrs.open` is true.
+        debug_assert!((self.pos_ellipsis == TermPos::None) == !self.attrs.open);
+
+        if let Some(raw_span) = self.pos_ellipsis.into_opt() {
+            return Err(InvalidRecordTypeError(TermPos::Original(raw_span)));
+        }
+
         let ty = self
             .fields
             .into_iter()
@@ -43,35 +181,55 @@ impl UniRecord {
                 self.tail
                     .map(|(tail, _)| tail)
                     .unwrap_or(Types(AbsType::RowEmpty())),
-                |acc, (path_elem, rt)| {
-                    match path_elem {
-                        FieldPathElem::Ident(id) => {
-                            // At parsing stage, all `Rc`s must be 1-counted. We can thus call
-                            // `into_owned()` without risking to actually clone anything.
-                            match rt.term.into_owned() {
-                                Term::MetaValue(MetaValue {
-                                    doc: None,
-                                    types: Some(ctrt),
-                                    contracts,
-                                    priority: MergePriority::Normal,
-                                    value: None,
-                                }) if contracts.is_empty() => Ok(Types(AbsType::RowExtend(
-                                    id,
-                                    Some(Box::new(ctrt.types)),
-                                    Box::new(acc),
-                                ))),
-                                _ => {
-                                    // Position of identifiers must always be set at this stage
-                                    // (parsing)
-                                    let span_id = id.pos.unwrap();
-                                    let term_pos = rt.pos.into_opt().unwrap_or(span_id);
-                                    Err(InvalidRecordTypeError(TermPos::Original(
-                                        RawSpan::fuse(span_id, term_pos).unwrap(),
-                                    )))
+                |acc, (mut path, rt)| {
+                    // We don't support compound paths for types, yet.
+                    if path.len() > 1 {
+                        let span = path
+                            .into_iter()
+                            .map(|path_elem| match path_elem {
+                                FieldPathElem::Ident(id) => id.pos.into_opt(),
+                                FieldPathElem::Expr(rt) => rt.pos.into_opt(),
+                            })
+                            .reduce(|acc, pos| {
+                                acc.zip(pos)
+                                    .and_then(|(acc, span)| RawSpan::fuse(acc, span))
+                            })
+                            .flatten();
+
+                        Err(InvalidRecordTypeError(
+                            span.map_or(TermPos::None, TermPos::Original),
+                        ))
+                    } else {
+                        let elem = path.pop().unwrap();
+                        match elem {
+                            FieldPathElem::Ident(id) => {
+                                // At parsing stage, all `Rc`s must be 1-counted. We can thus call
+                                // `into_owned()` without risking to actually clone anything.
+                                match rt.term.into_owned() {
+                                    Term::MetaValue(MetaValue {
+                                        doc: None,
+                                        types: Some(ctrt),
+                                        contracts,
+                                        priority: MergePriority::Normal,
+                                        value: None,
+                                    }) if contracts.is_empty() => Ok(Types(AbsType::RowExtend(
+                                        id,
+                                        Some(Box::new(ctrt.types)),
+                                        Box::new(acc),
+                                    ))),
+                                    _ => {
+                                        // Position of identifiers must always be set at this stage
+                                        // (parsing)
+                                        let span_id = id.pos.unwrap();
+                                        let term_pos = rt.pos.into_opt().unwrap_or(span_id);
+                                        Err(InvalidRecordTypeError(TermPos::Original(
+                                            RawSpan::fuse(span_id, term_pos).unwrap(),
+                                        )))
+                                    }
                                 }
                             }
+                            FieldPathElem::Expr(rt) => Err(InvalidRecordTypeError(rt.pos)),
                         }
-                        FieldPathElem::Expr(rt) => Err(InvalidRecordTypeError(rt.pos)),
                     }
                 },
             )?;
@@ -89,7 +247,11 @@ impl TryFrom<UniRecord> for RichTerm {
 
     /// Convert a `UniRecord` to a term. If the `UniRecord` has a tail, it is first interpreted as
     /// a type and then converted to a contract. Otherwise it is interpreted as a record directly.
-    /// Fail if the `UniRecord` has a tail but isn't syntactically a record type either.
+    /// Fail if the `UniRecord` has a tail but isn't syntactically a record type either. Elaborate
+    /// field paths `foo.bar = value` to the expanded form `{foo = {bar = value}}`.
+    ///
+    /// We also fix the type variables of the type appearing inside annotations (see
+    /// [`fix_type_vars`]).
     fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
         let pos = ur.pos;
 
@@ -99,16 +261,20 @@ impl TryFrom<UniRecord> for RichTerm {
                 .map_err(|InvalidRecordTypeError(pos)| {
                     ParseError::InvalidUniRecord(pos.unwrap(), tail_pos.unwrap(), pos.unwrap())
                 })
-                .and_then(|ty| {
+                .and_then(|mut ty| {
+                    fix_type_vars(&mut ty);
                     ty.contract().map_err(|UnboundTypeVariableError(id)| {
                         ParseError::UnboundTypeVariables(vec![id], pos.unwrap())
                     })
                 })
         } else {
-            Ok(RichTerm::from(build_record(
-                ur.fields.into_iter(),
-                ur.attrs,
-            )))
+            let UniRecord { fields, attrs, .. } = ur;
+            let elaborated = fields.into_iter().map(|(path, mut rt)| {
+                fix_field_types(&mut rt);
+                elaborate_field_path(path, rt)
+            });
+
+            Ok(RichTerm::from(build_record(elaborated, attrs)))
         };
 
         result.map(|rt| rt.with_pos(pos))
@@ -120,8 +286,8 @@ impl TryFrom<UniRecord> for Types {
 
     /// Convert a `UniRecord` to a type. If the `UniRecord` has a tail, it is interpreted strictly
     /// as a type and fail if it isn't a plain record type. Otherwise, we first try to interpret it
-    /// as a plain record type, and if that doesn't work, we interpret it as a term and wrap it as
-    /// a flat type.
+    /// as a plain record type, and if that doesn't work, we interpret it as a term and wrap it
+    /// back as a user-defined contract.
     fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
         let pos = ur.pos;
 
@@ -141,3 +307,105 @@ impl TryFrom<UniRecord> for Types {
         }
     }
 }
+
+/// Post-process a type at the right hand side of an annotation by replacing each unbound type
+/// variable by a term variable with the same identifier seen as a custom contract
+/// (`AbsType::Var(id)` to `AbsType::Flat(Term::Var(id))`).
+///
+/// Since parsing is done bottom-up, and given the specification of the uniterm syntax for
+/// variables occurring in types, we often can't know right away if a such a variable occurrence
+/// will eventually be a type variable or a term variable seen as a custom contract.
+///
+/// Take for example `a -> b`. At this stage, `a` and `b` could be both variables referring to a
+/// contract (e.g. in `x | a -> b`) or a type variable (e.g. in `x | forall a b. a -> b`),
+/// depending on enclosing `forall`s. To handle both cases, we initially parse all variables inside
+/// types as type variables. When reaching the right-hand side of an annotation, because `forall`s
+/// can only bind locally in a type, we can then decide the actual nature of each occurrence. We
+/// thus recurse into the newly constructed type to change those type variables that are not
+/// actually bound by a `forall` to be term variables. This is the role of `fix_type_vars()`.
+///
+/// Once again because `forall`s only bind variables locally, and don't bind inside contracts, we
+/// don't have to recurse into contracts and this pass will only visit each node of the AST at most
+/// once in total.
+///
+/// There is one subtlety with unirecords, though. A unirecord can still be in interpreted as a
+/// record type later. Take the following example:
+///
+/// ```nickel
+/// let mk_pair : forall a b. a -> b -> {fst: a, snd: b} = <exp>
+/// ```
+///
+/// Since this unirecord will eventually be interpreted as a record type, we can't know yet when
+/// parsing `fst: a` if `a` will be a type variable or a term variable (while, for all other
+/// constructs, an annotation is a boundary that `forall` binders can't cross). In this example,
+/// there is indeed an enclosing forall binding `a`. With unirecords, before fixing type variables,
+/// we have to wait until we eventually convert the unirecord to a term (in which case we fix all the
+/// top-level annotations) or a type (in which case we do nothing: the enclosing type will trigger
+/// the fix once it's fully constructed). Fixing a unirecord prior to a conversion to a term is
+/// done by [`fix_fields_types`].
+pub fn fix_type_vars(ty: &mut Types) {
+    fn fix_type_vars_aux(ty: &mut Types, mut bound_vars: Cow<HashSet<Ident>>) {
+        match ty.0 {
+            AbsType::Dyn()
+            | AbsType::Num()
+            | AbsType::Bool()
+            | AbsType::Str()
+            | AbsType::Sym()
+            | AbsType::Flat(_)
+            | AbsType::RowEmpty() => (),
+            AbsType::Arrow(ref mut s, ref mut t) => {
+                fix_type_vars_aux(s.as_mut(), Cow::Borrowed(bound_vars.as_ref()));
+                fix_type_vars_aux(t.as_mut(), bound_vars);
+            }
+            AbsType::Var(ref mut id) => {
+                if !bound_vars.contains(id) {
+                    let id = std::mem::take(id);
+                    let pos = id.pos;
+                    ty.0 = AbsType::Flat(RichTerm::new(Term::Var(id), pos));
+                }
+            }
+            AbsType::Forall(ref id, ref mut ty) => {
+                bound_vars.to_mut().insert(id.clone());
+                fix_type_vars_aux(&mut *ty, bound_vars);
+            }
+            AbsType::RowExtend(_, ref mut ty_opt, ref mut tail) => {
+                if let Some(ref mut ty) = *ty_opt {
+                    fix_type_vars_aux(ty.as_mut(), Cow::Borrowed(bound_vars.as_ref()));
+                }
+
+                // We don't touch a row tail that is a type variable, because the typechecker
+                // relies on row types being well-formed, which the parser must ensure.
+                // Well-formedness requires that only type variables and `Dyn` may appear in a row
+                // tail position, so we don't turn such variables into term variables (having a
+                // contract in tail position doesn't make sense, in the current model at least,
+                // both for typechecking and at evaluation).
+                if !matches!((**tail).0, AbsType::Var(_)) {
+                    fix_type_vars_aux(tail.as_mut(), bound_vars);
+                }
+            }
+            AbsType::DynRecord(ref mut ty)
+            | AbsType::List(ref mut ty)
+            | AbsType::Enum(ref mut ty)
+            | AbsType::StaticRecord(ref mut ty) => fix_type_vars_aux(ty.as_mut(), bound_vars),
+        }
+    }
+
+    fix_type_vars_aux(ty, Cow::Owned(HashSet::new()))
+}
+
+/// Fix the type variables of types appearing as annotations of record fields. See
+/// [`fix_type_vars`].
+pub fn fix_field_types(rt: &mut RichTerm) {
+    match SharedTerm::make_mut(&mut rt.term) {
+        Term::MetaValue(ref mut m) => {
+            if let Some(Contract { ref mut types, .. }) = m.types {
+                fix_type_vars(types);
+            }
+
+            for ctr in m.contracts.iter_mut() {
+                fix_type_vars(&mut ctr.types);
+            }
+        }
+        _ => (),
+    }
+}
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index e890ca5f..196c39ac 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -43,6 +43,8 @@ pub enum FieldPathElem {
     Expr(RichTerm),
 }
 
+pub type FieldPath = Vec<FieldPathElem>;
+
 /// A string chunk literal atom, being either a string or a single char.
 ///
 /// Because of the way the lexer handles escaping and interpolation, a contiguous static string
@@ -56,7 +58,7 @@ pub enum ChunkLiteralPart<'input> {
 /// The last field of a record, that can either be a normal field declaration or an ellipsis.
 #[derive(Clone, Debug)]
 pub enum RecordLastField {
-    Field((FieldPathElem, RichTerm)),
+    Field((FieldPath, RichTerm)),
     Ellipsis,
 }
 
diff --git a/src/position.rs b/src/position.rs
index 5a634b8e..5cc3107d 100644
--- a/src/position.rs
+++ b/src/position.rs
@@ -52,6 +52,12 @@ pub enum TermPos {
     None,
 }
 
+impl Default for TermPos {
+    fn default() -> Self {
+        TermPos::None
+    }
+}
+
 impl TermPos {
     /// Apply a transformation to the inner position, if any.
     pub fn map<F: FnOnce(RawSpan) -> RawSpan>(self, f: F) -> Self {
diff --git a/src/typecheck/error.rs b/src/typecheck/error.rs
index aa3a5502..05136420 100644
--- a/src/typecheck/error.rs
+++ b/src/typecheck/error.rs
@@ -36,6 +36,8 @@ pub enum RowUnifError {
     WithConst(usize, TypeWrapper),
     /// Tried to unify two distinct type constants.
     ConstMismatch(usize, usize),
+    /// An unbound type variable was referenced.
+    UnboundTypeVariable(Ident),
 }
 
 impl RowUnifError {
@@ -62,6 +64,7 @@ impl RowUnifError {
             RowUnifError::UnsatConstr(id, tyw) => UnifError::RowConflict(id, tyw, left, right),
             RowUnifError::WithConst(c, tyw) => UnifError::WithConst(c, tyw),
             RowUnifError::ConstMismatch(c1, c2) => UnifError::ConstMismatch(c1, c2),
+            RowUnifError::UnboundTypeVariable(id) => UnifError::UnboundTypeVariable(id),
         }
     }
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index bcf09f67..3d9c9bfc 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -1095,10 +1095,13 @@ pub fn unify_(
                         err.into_unif_err(mk_tyw_record!(; r1), mk_tyw_record!(; r2))
                     })
                 }
-                (TypeWrapper::Concrete(r), _) if !r.is_row_type() => {
-                    Err(UnifError::IllformedType(mk_tyw_record!(; r)))
+                (TypeWrapper::Concrete(AbsType::Var(id)), _)
+                | (_, TypeWrapper::Concrete(AbsType::Var(id))) => {
+                    Err(UnifError::UnboundTypeVariable(id))
                 }
-                (_, TypeWrapper::Concrete(r)) if !r.is_row_type() => {
+                (TypeWrapper::Concrete(r), _) | (_, TypeWrapper::Concrete(r))
+                    if !r.is_row_type() =>
+                {
                     Err(UnifError::IllformedType(mk_tyw_record!(; r)))
                 }
                 (tyw1, tyw2) => unify_(state, tyw1, tyw2),
@@ -1156,6 +1159,7 @@ pub fn unify_rows(
     t2: AbsType<Box<TypeWrapper>>,
 ) -> Result<(), RowUnifError> {
     match (t1, t2) {
+        (AbsType::Var(id), _) | (_, AbsType::Var(id)) => Err(RowUnifError::UnboundTypeVariable(id)),
         (AbsType::RowEmpty(), AbsType::RowEmpty()) | (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
         (AbsType::RowEmpty(), AbsType::Dyn()) => Err(RowUnifError::ExtraDynTail()),
         (AbsType::Dyn(), AbsType::RowEmpty()) => Err(RowUnifError::MissingDynTail()),
diff --git a/src/types.rs b/src/types.rs
index c058cb06..99014929 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -389,7 +389,7 @@ impl fmt::Display for Types {
                 }
             }
             AbsType::Sym() => write!(f, "Sym"),
-            AbsType::Flat(ref t) => write!(f, "#{}", t.as_ref().shallow_repr()),
+            AbsType::Flat(ref t) => write!(f, "{}", t.as_ref().shallow_repr()),
             AbsType::Var(var) => write!(f, "{}", var),
             AbsType::Forall(i, ref ty) => {
                 let mut curr: &Types = ty.as_ref();
@@ -400,7 +400,7 @@ impl fmt::Display for Types {
                 }
                 write!(f, ". {}", curr)
             }
-            AbsType::Enum(row) => write!(f, "<{}>", row),
+            AbsType::Enum(row) => write!(f, "[|{}|]", row),
             AbsType::StaticRecord(row) => write!(f, "{{{}}}", row),
             AbsType::DynRecord(ty) => write!(f, "{{_: {}}}", ty),
             AbsType::RowEmpty() => Ok(()),
@@ -480,8 +480,8 @@ mod test {
         assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool ; r}");
         assert_format_eq("{x: Bool, y: Bool, z: Bool}");
 
-        // assert_format_eq("<a, b, c, d>");
-        // assert_format_eq("forall r. <tag1, tag2, tag3 ; r>");
+        assert_format_eq("[|a, b, c, d|]");
+        assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
 
         assert_format_eq("List");
         assert_format_eq("List Num");
diff --git a/stdlib/builtins.ncl b/stdlib/builtins.ncl
index b0d609b3..115cdb8a 100644
--- a/stdlib/builtins.ncl
+++ b/stdlib/builtins.ncl
@@ -84,14 +84,14 @@
       "#m
     = fun x => %is_record% x,
 
-    typeof : Dyn -> <
+    typeof : Dyn -> [|
       TypeNum,
       TypeBool,
       TypeStr,
       TypeFun,
       TypeList,
       TypeRecord,
-      Other>
+      Other |]
     | doc m#"
       Results in a value representing the type of the typed value.
 
@@ -144,7 +144,7 @@
       "#m
     = fun x y => %deep_seq% x y,
 
-    hash : <Md5, Sha1, Sha256, Sha512> -> Str -> Str
+    hash : [| Md5, Sha1, Sha256, Sha512 |] -> Str -> Str
     | doc m#"
       Hashes the given string provided the desired hash algorithm.
 
@@ -156,7 +156,7 @@
       "#m
     = fun type s => %hash% type s,
 
-    serialize : <Json, Toml, Yaml> -> Dyn -> Str
+    serialize : [| Json, Toml, Yaml |] -> Dyn -> Str
     | doc m#"
       Serializes the given value to the desired representation.
 
@@ -171,7 +171,7 @@
       "#m
     = fun format x => %serialize% format (%deep_seq% x x),
 
-    deserialize : <Json, Toml, Yaml> -> Str -> Dyn
+    deserialize : [| Json, Toml, Yaml |] -> Str -> Dyn
     | doc m#"
       Deserializes the given string to a nickel value given the encoding of the string.
 
diff --git a/stdlib/lists.ncl b/stdlib/lists.ncl
index 6507f820..4ccacead 100644
--- a/stdlib/lists.ncl
+++ b/stdlib/lists.ncl
@@ -254,7 +254,7 @@
         "#m
       = fun f n => %generate% n f,
 
-    sort : forall a. (a -> a -> <Less, Equal, Greater>) -> List a -> List a
+    sort : forall a. (a -> a -> [| Less, Equal, Greater |]) -> List a -> List a
       | doc m#"
         Sorts the given lists based on the provided comparison operator.
 
diff --git a/stdlib/strings.ncl b/stdlib/strings.ncl
index 7a92b38a..1ec5f687 100644
--- a/stdlib/strings.ncl
+++ b/stdlib/strings.ncl
@@ -177,7 +177,7 @@
       "#m
     = fun s => %str_chars% s,
 
-    code | #CharLiteral -> Num
+    code | CharLiteral -> Num
     | doc m#"
       Results in the ascii code of the given character.
 
@@ -193,7 +193,7 @@
       "#m
     = fun s => %char_code% s,
 
-    from_code | Num -> #CharLiteral
+    from_code | Num -> CharLiteral
     | doc m#"
       Results in the character for a given ascii code. Any number outside the ascii range results in an error.
 
@@ -382,7 +382,7 @@
       "#m
     = fun b => %to_str% b,
 
-    to_num | #NumLiteral -> Num
+    to_num | NumLiteral -> Num
     | doc m#"
       Converts a string that represents an integer to that integer.
 
@@ -394,7 +394,7 @@
       "#m
     = fun s => %num_from_str% s,
 
-    to_bool | #BoolLiteral -> Bool
+    to_bool | BoolLiteral -> Bool
     | doc m#"
       Converts a string that represents a boolean to that boolean.
 
@@ -410,7 +410,7 @@
     = fun s => s == "true",
 
     // to_enum | #Ident -> < | Dyn> = fun s => %enum_from_str% s,
-    to_enum | #Ident -> Dyn
+    to_enum | Ident -> Dyn
     | doc m#"
       Converts any string that represents an enum variant to that enum variant.
 


Test patch:
diff --git a/tests/basics_fail.rs b/tests/basics_fail.rs
index 07cae89e..cfc12e50 100644
--- a/tests/basics_fail.rs
+++ b/tests/basics_fail.rs
@@ -42,7 +42,7 @@ fn comparisons() {
 #[test]
 fn boolean_ops() {
     assert_matches!(
-        eval("let throw | #fail = null in false || true && throw"),
+        eval("let throw | fail = null in false || true && throw"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 5ae5316c..48defd0d 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -16,9 +16,9 @@ macro_rules! assert_raise_blame {
 #[test]
 fn flat_contract_fail() {
     assert_raise_blame!(
-        "let alwaysTrue = fun l t => let boolT | Bool = t in
+        "let AlwaysTrue = fun l t => let boolT | Bool = t in
         if boolT then boolT else %blame% l in
-        (false | #alwaysTrue)"
+        (false | AlwaysTrue)"
     );
 }
 
@@ -32,9 +32,9 @@ fn id_fail() {
 
 #[test]
 fn enum_simple() {
-    assert_raise_blame!("`far | <foo, bar>");
-    assert_raise_blame!("123 | <foo, bar>");
-    assert_raise_blame!("`foo | < >");
+    assert_raise_blame!("`far | [|foo, bar|]");
+    assert_raise_blame!("123 | [|foo, bar|]");
+    assert_raise_blame!("`foo | [| |]");
 }
 
 #[test]
@@ -58,7 +58,7 @@ fn merge_compose_contract() {
         format!(
             "let Even = fun l x => if x % 2 == 0 then x else %blame% l in
         let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
-        let composed = {{a | #Even}} & {{a | #DivBy3}} in
+        let composed = {{a | Even}} & {{a | DivBy3}} in
         (({{a = {},}}) & composed).a",
             arg
         )
@@ -174,7 +174,7 @@ fn lists_contracts() {
 fn records_contracts_closed() {
     assert_raise_blame!("{a=1} | {}");
     assert_raise_blame!("{a=1, b=2} | {a | Num}");
-    assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | #Contract)");
+    assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | Contract)");
 }
 
 // #[test]
diff --git a/tests/pass/annotations.ncl b/tests/pass/annotations.ncl
index f00e6c3d..81a6aa2e 100644
--- a/tests/pass/annotations.ncl
+++ b/tests/pass/annotations.ncl
@@ -4,24 +4,24 @@ let Assert = fun l x => x || %blame% l in
   // left_annot_precedence
   (let dummy = null in
     let LocalAssert = Assert in
-    true | #LocalAssert),
+    true | LocalAssert),
 
   (if false then
       null
     else
       let dummy = null in
       let LocalAssert = Assert in
-      true | #LocalAssert),
+      true | LocalAssert),
 
   (let f = fun x =>
       let dummy = null in
       let LocalAssert = Assert in
-      x | #LocalAssert in
+      x | LocalAssert in
     f true),
 
   // others_precedence
-  ((fun x => x | #Assert) true),
+  ((fun x => x | Assert) true),
   (let AssertOk = fun l t => if t == `Ok then t else %blame% l in
-    switch {`Ok => true, `Err => false} `Ok | #AssertOk),
+    switch {`Ok => true, `Err => false} `Ok | AssertOk),
 ]
 |> lists.foldl (fun x y => x && y) true
diff --git a/tests/pass/basics.ncl b/tests/pass/basics.ncl
index a876f9b3..593590c3 100644
--- a/tests/pass/basics.ncl
+++ b/tests/pass/basics.ncl
@@ -34,4 +34,4 @@ let Assert = fun l x => x || %blame% l in
   // This test checks that the terms of a switch are closured
   let x = 3 in (switch { `foo => 1, _ => x} (3 + 2)) == 3,
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/builtins.ncl b/tests/pass/builtins.ncl
index 5ba3dcf8..c005ea70 100644
--- a/tests/pass/builtins.ncl
+++ b/tests/pass/builtins.ncl
@@ -27,4 +27,4 @@ let Assert = fun l x => x || %blame% l in
    |> builtins.deserialize `Json
    == [3,4],
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/complete.ncl b/tests/pass/complete.ncl
index 0ab8bc49..be0c3958 100644
--- a/tests/pass/complete.ncl
+++ b/tests/pass/complete.ncl
@@ -7,4 +7,4 @@ let fibo : Num -> Num = Y (fun fibo =>
   (fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
 let val : Num = 4 in
 
-(fibo val | #(AssertEq 5))
+(fibo val | AssertEq 5)
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 60d6833a..1006a487 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -7,7 +7,7 @@ let Assert = fun l x => x || %blame% l in
   let AlwaysFalse = fun l t =>
     let boolT | Bool = t in
     if boolT then %blame% l else boolT
-  in let not | #AlwaysTrue -> #AlwaysFalse = fun b => if b then false else true in
+  in let not | AlwaysTrue -> AlwaysFalse = fun b => if b then false else true in
   not true == false,
 
   // id_polymorphic_contract
@@ -28,27 +28,27 @@ let Assert = fun l x => x || %blame% l in
   ("hello" ++ " world" | Str) == "hello world",
 
   // enums_simple
-  (`foo | <foo, bar>) == `foo,
-  (`bar | forall r. <foo, bar | r>) == `bar,
+  (`foo | [| foo, bar |]) == `foo,
+  (`bar | forall r. [| foo, bar ; r|]) == `bar,
 
   // enums_escaped
-  (`"foo:baz" | <"foo:baz", "bar:baz">) == `"foo:baz",
-  (`"bar:baz" | forall r. <"foo:baz", "bar:baz" | r>) == `"bar:baz",
+  (`"foo:baz" | [| "foo:baz", "bar:baz" |]) == `"foo:baz",
+  (`"bar:baz" | forall r. [| "foo:baz", "bar:baz" ; r |]) == `"bar:baz",
 
   // enums_complex
-  let f : forall r. <foo, bar | r> -> Num =
+  let f : forall r. [| foo, bar ; r |] -> Num =
     fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
   f `bar == 2,
 
-  let f : forall r. <foo, bar | r> -> Num =
+  let f : forall r. [| foo, bar ; r |] -> Num =
     fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
   f `boo == 3,
 
-  let f : forall r. <foo, "bar:baz" | r> -> Num =
+  let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
     fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
   f `"bar:baz" == 2,
 
-  let f : forall r. <foo, "bar:baz" | r> -> Num =
+  let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
     fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
   f `"boo,grr" == 3,
 
@@ -67,19 +67,19 @@ let Assert = fun l x => x || %blame% l in
     let remove | forall a. {foo: Num ; a} -> { ; a} = fun x =>
       x -$ "foo" in
 
-    (id {} == {} | #Assert) &&
-    (id {a = 1, b = false} == {a = 1, b = false} | #Assert) &&
-    (extend {} == {foo = 1} | #Assert) &&
-    (extend {bar = false} == {foo = 1, bar = false} | #Assert) &&
-    (remove {foo = 1} == {} | #Assert) &&
-    (remove {foo = 1, bar = 1} == {bar = 1} | #Assert) &&
-    (remove (extend {}) == {} | #Assert) &&
-    (extend (remove {foo = 2}) == {foo =1} | #Assert) &&
+    (id {} == {} | Assert) &&
+    (id {a = 1, b = false} == {a = 1, b = false} | Assert) &&
+    (extend {} == {foo = 1} | Assert) &&
+    (extend {bar = false} == {foo = 1, bar = false} | Assert) &&
+    (remove {foo = 1} == {} | Assert) &&
+    (remove {foo = 1, bar = 1} == {bar = 1} | Assert) &&
+    (remove (extend {}) == {} | Assert) &&
+    (extend (remove {foo = 2}) == {foo =1} | Assert) &&
     (let f | forall a b. {f: a -> a, arg: a ; b} -> a =
         fun rec => rec.f (rec.arg) in
       f { f = fun x => x ++ " suffix", arg = "foo" }
       == "foo suffix"
-      | #Assert)
+      | Assert)
   ),
 
   // records_dynamic_tail
@@ -89,13 +89,13 @@ let Assert = fun l x => x || %blame% l in
   ((fun r => r.b) | {a: Num ; Dyn} -> Dyn) {a = 1, b = 2} == 2,
 
   // records_open_contracts
-  ({a = 0, b = 0} | #{a | Num, ..}) == {a = 0, b = 0},
+  ({a = 0, b = 0} | {a | Num, ..}) == {a = 0, b = 0},
   let Contract = {a | Num} & {..} in
-  ({a = 0, b = 0} | #Contract) == {a = 0, b = 0},
+  ({a = 0, b = 0} | Contract) == {a = 0, b = 0},
   let Contract = {..} & {b | Num} in
-  ({a = 0, b = 0} | #Contract) == {a = 0, b = 0},
+  ({a = 0, b = 0} | Contract) == {a = 0, b = 0},
   let Contract = {a | Num, ..} & {b | Num, ..} in
-  ({a = 0, b = 0, c = 0} | #Contract) == {a = 0, b = 0, c = 0},
+  ({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
 
   // lists
   ([1, "2", false] | List) == [1, "2", false],
@@ -111,12 +111,12 @@ let Assert = fun l x => x || %blame% l in
   // Regression test for #402
   let MyContract = { x | Str } in
   {
-    foo | #MyContract | default = { x = "From foo" },
-    bar | #{..} | default = foo
+    foo | MyContract | default = { x = "From foo" },
+    bar | {..} | default = foo
   } == { foo.x = "From foo", bar.x = "From foo"},
 
   // mixing type and record contracts
-  let f | #{foo | Num} -> #{bar | Num} = fun r =>
+  let f | {foo | Num} -> {bar | Num} = fun r =>
     {bar = r.foo} in
   (f {foo = 1}).bar == 1,
   // user-written contract application
@@ -128,8 +128,8 @@ let Assert = fun l x => x || %blame% l in
     contracts.apply derived label value in
   let Contract = Extend {bar | Num, ..} in
   let Id = Extend (fun label value => value) in
-  ({bar = 1, foo = 1} | #Contract)
-    & ({baz = 1} | #Id)
-  == {foo = 1, bar = 1, baz = 1},
+  ({bar = 1, foo = 1} | Contract)
+    & ({baz = 1} | Id)
+   == {foo = 1, bar = 1, baz = 1},
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/eq.ncl b/tests/pass/eq.ncl
index 7fcf18af..2ad1dcd3 100644
--- a/tests/pass/eq.ncl
+++ b/tests/pass/eq.ncl
@@ -75,4 +75,4 @@ let Assert = fun l x => x || %blame% l in
       == false
   ),
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/functions.ncl b/tests/pass/functions.ncl
index 6afbaebb..30f67b40 100644
--- a/tests/pass/functions.ncl
+++ b/tests/pass/functions.ncl
@@ -15,4 +15,4 @@ let Assert = fun l x => x || %blame% l in
     g true
     == 4,
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/import.ncl b/tests/pass/import.ncl
index f6ae0ee0..0850f46e 100644
--- a/tests/pass/import.ncl
+++ b/tests/pass/import.ncl
@@ -1,3 +1,3 @@
 let Assert = fun l x => x || %blame% l in
 
-(import "imported.ncl" 3 == 3 | #Assert)
+(import "imported.ncl" 3 == 3 | Assert)
diff --git a/tests/pass/imported.ncl b/tests/pass/imported.ncl
index 54d96487..0d72daea 100644
--- a/tests/pass/imported.ncl
+++ b/tests/pass/imported.ncl
@@ -1,3 +1,2 @@
 // This isn’t really a test, mostly an auxiliary file used by `import.ncl`
-
 fun x => x
diff --git a/tests/pass/lists.ncl b/tests/pass/lists.ncl
index 5576e6f1..cfb3efdf 100644
--- a/tests/pass/lists.ncl
+++ b/tests/pass/lists.ncl
@@ -33,4 +33,4 @@ let Assert = fun l x => x || %blame% l in
     let isZ = fun x => x == 0 in
     all isZ [0, 0, 0, 1] == false,
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/metavalues.ncl b/tests/pass/metavalues.ncl
index c000e388..e4e5706c 100644
--- a/tests/pass/metavalues.ncl
+++ b/tests/pass/metavalues.ncl
@@ -28,29 +28,29 @@ let Assert = fun l x => x || %blame% l in
   // composed
   let Even = fun l x => if x % 2 == 0 then x else %blame% l in
     let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
-    let composed = {a | #Even} & {a | #DivBy3} in
-    (composed & {a = 6} == {a = 6} | #Assert) &&
-    (composed & {a = 12} == {a = 12} | #Assert),
+    let composed = {a | Even} & {a | DivBy3} in
+    (composed & {a = 6} == {a = 6} | Assert) &&
+    (composed & {a = 12} == {a = 12} | Assert),
 
 
   // Check that the environments of contracts are correctly saved and restored when merging. See
   // issue [#117](https://github.com/tweag/nickel/issues/117)
-  (let ctr_num = let x = num in {a | #x} in
-    let ctr_id = let x = fun l x => x in {a | #x} in
+  (let ctr_num = let x = num in {a | x} in
+    let ctr_id = let x = fun l x => x in {a | x} in
     let val = let x = 1 in {a = x} in
     let def = let x = 2 in {a | default = x} in
     let def2 = let x = (1 + 1) in {a | default = x} in
   // contract/contract -> contract/value -> value/default
-  ((ctr_num & ctr_id & val & def).a == 1 | #Assert) &&
+  ((ctr_num & ctr_id & val & def).a == 1 | Assert) &&
   // default/value <- value/contract
-  ((def & (val & ctr_num)).a == 1 | #Assert) &&
+  ((def & (val & ctr_num)).a == 1 | Assert) &&
   // default/contract-> contract-default/contract-default <- contract/default
-  (((def & ctr_num) & (ctr_id & def2)).a == 2 | #Assert) &&
+  (((def & ctr_num) & (ctr_id & def2)).a == 2 | Assert) &&
   // default/contract -> contract-default/contract -> contract-default/value
-  ((def & ctr_num & ctr_id & val).a == 1 | #Assert) &&
+  ((def & ctr_num & ctr_id & val).a == 1 | Assert) &&
   // default/contract -> contract-default/default
-  ((def & ctr_num & def2).a == 2 | #Assert) &&
+  ((def & ctr_num & def2).a == 2 | Assert) &&
   // value/contract-default <- contract/contract-default
-  ((val & (ctr_num & def)).a == 1 | #Assert)),
+  ((val & (ctr_num & def)).a == 1 | Assert)),
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/overriding.ncl b/tests/pass/overriding.ncl
index f05240ff..c0515472 100644
--- a/tests/pass/overriding.ncl
+++ b/tests/pass/overriding.ncl
@@ -71,4 +71,4 @@ let Assert = contracts.from_predicate functions.id in
   ({foo | default = 1, bar = foo} & {foo = 2}).bar == 2,
   ({foo | default = 1, bar = foo, baz = bar} & {foo = 2}).baz == 2,
 ]
-|> lists.foldl (fun next acc => (next | #Assert) && acc) true
+|> lists.foldl (fun next acc => (next | Assert) && acc) true
diff --git a/tests/pass/record-defs.ncl b/tests/pass/record-defs.ncl
index bb6e1eeb..443a6e89 100644
--- a/tests/pass/record-defs.ncl
+++ b/tests/pass/record-defs.ncl
@@ -40,4 +40,4 @@ let Assert = fun l x => x || %blame% l in
   let x = "foo" in {"#{x}" = bar, bar = 1} == {foo = 1, bar = 1},
   ({"#foo"."#bar".baz = other + 1, other = 0}."#foo"."#bar".baz == 1),
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/records.ncl b/tests/pass/records.ncl
index 7ed6ff00..837670d6 100644
--- a/tests/pass/records.ncl
+++ b/tests/pass/records.ncl
@@ -104,12 +104,12 @@ let Assert = fun l x => x || %blame% l in
   let Name = fun b label name => if b then "hijack" else contracts.blame label in
   let Config = {
       b | Bool,
-      name | #(Name b),
+      name | Name b,
   } in
-  let data | #Config = {
+  let data | Config = {
       b = true,
       name = "name",
   } in
   data.name == "hijack",
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/serialize-package.ncl b/tests/pass/serialize-package.ncl
index 1c5b2e7d..1f59153c 100644
--- a/tests/pass/serialize-package.ncl
+++ b/tests/pass/serialize-package.ncl
@@ -9,7 +9,7 @@ let ctr = {
     buildInputs | doc "
                   The list of inputs for this package, specified as a
                   `NixPackage`."
-                | List #NixPackage,
+                | List NixPackage,
     // Many more missing
   },
 
@@ -25,7 +25,7 @@ let ctr = {
                ```
                myPkg = {
                  name  = \"myPkg\",
-                 buildInputs | List #NixPackage = [{package = \"hello\"}]\",
+                 buildInputs | List NixPackage = [{package = \"hello\"}]\",
                }
                ```
                This will give the following attribute sets once imported in Nix:
@@ -57,7 +57,7 @@ builtins.serialize `Json (
   {
     name = "nickel",
     buildInputs = [{package = "hello"}],
-  } | #ctr.Shell
+  } | ctr.Shell
 ) == builtins.serialize `Json {
   name = "nickel",
   buildInputs = [{input = "nixpkgs", package = "hello", "_type" = "package"}],
diff --git a/tests/pass/serialize.ncl b/tests/pass/serialize.ncl
index ff3ff8c2..1c8340d5 100644
--- a/tests/pass/serialize.ncl
+++ b/tests/pass/serialize.ncl
@@ -29,4 +29,4 @@ let assertDeserInv = fun x =>
       baz = {subfoo = true, subbar = 0}
     },
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/strings.ncl b/tests/pass/strings.ncl
index 6ed8c7b9..52db2961 100644
--- a/tests/pass/strings.ncl
+++ b/tests/pass/strings.ncl
@@ -21,4 +21,4 @@ let Assert = fun l x => x || %blame% l in
   let s = "Hello" in m##""###{s}" World"##m == "\"#Hello\" World",
   m##""##s"##m == "\"##s",
 ]
-|> lists.foldl (fun x y => (x | #Assert) && y) true
+|> lists.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 8d476f8b..8ae8353f 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -19,7 +19,7 @@ let typecheck = [
   (fun id => (id 4) + (id true: Bool)) (fun x => x),
   // contracts are opaque types
   (let AlwaysTrue = fun l t => if t then t else %blame% l in
-  ((fun x => x) : #alwaysTrue -> #alwaysTrue)),
+  ((fun x => x) : AlwaysTrue -> AlwaysTrue)),
 
   // simple_polymorphism
   let f : forall a. a -> a = fun x => x in
@@ -49,28 +49,28 @@ let typecheck = [
     ((if (f true) then (f 2) else 3) : Num),
 
   // enums_simple
-  (`bla : <bla>),
-  (`blo : <bla, blo>),
-  (`bla : forall r. <bla | r>),
-  (`bla : forall r. <bla, blo | r>),
+  (`bla : [|bla |]),
+  (`blo : [|bla, blo |]),
+  (`bla : forall r. [|bla ; r |]),
+  (`bla : forall r. [|bla, blo ; r |]),
   ((switch {`bla => 3} `bla) : Num),
   ((switch {`bla => 3, _ => 2} `blo) : Num),
 
   // enums_complex
-  ((fun x => switch {`bla => 1, `ble => 2} x) : <bla, ble> -> Num),
+  ((fun x => switch {`bla => 1, `ble => 2} x) : [|bla, ble |] -> Num),
   ((fun x => switch {`bla => 1, `ble => 2, `bli => 4} (%embed% bli x))
-    : <bla, ble> -> Num),
+    : [|bla, ble |] -> Num),
   ((fun x =>
       (switch {`bla => 3, `bli => 2} x)
       + (switch {`bli => 6, `bla => 20} x))
     `bla
     : Num),
 
-  let f : forall r. <blo, ble | r> -> Num = fun x =>
+  let f : forall r. [|blo, ble ; r |] -> Num = fun x =>
     switch {`blo => 1, `ble => 2, _ => 3} x in
             (f `bli : Num),
 
-  let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
+  let f : forall r. (forall p. [|blo, ble ; r |] -> [|bla, bli ; p |]) =
     fun x => switch {`blo => `bla, `ble => `bli, _ => `bla} x in
     f `bli,
 
diff --git a/tests/pass/types.ncl b/tests/pass/types.ncl
index 1cea0bd7..ac3e0bd1 100644
--- a/tests/pass/types.ncl
+++ b/tests/pass/types.ncl
@@ -1,4 +1,4 @@
 let Assert = fun l x => x || %blame% l in
 
 (let plus : Num -> Num -> Num = fun x => fun y => x + y in
- plus (54 : Num) (6 : Num) == 60 | #Assert)
+ plus (54 : Num) (6 : Num) == 60 | Assert)
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 2e82d86d..2334c563 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -29,6 +29,7 @@ macro_rules! assert_typecheck_fails {
 
 #[test]
 fn unbound_variable_always_throws() {
+    type_check_expr("x").map_err(|err| println!("{:#?}", err));
     assert_matches!(
         type_check_expr("x"),
         Err(TypecheckError::UnboundIdentifier(..))
@@ -52,7 +53,7 @@ fn promise_complicated() {
     // no implicit polymorphism
     assert_typecheck_fails!("(fun id => (id 4 : Num) + (id true : Bool)) (fun x => x)");
     // contract equality (to be fair, the current implementation is full of issues: to be reworked)
-    assert_typecheck_fails!("(fun x => x) : #(fun l t => t) -> #(fun l t => t)");
+    assert_typecheck_fails!("(fun x => x) : (fun l t => t) -> (fun l t => t)");
 }
 
 #[test]
@@ -77,7 +78,7 @@ fn simple_forall() {
 
 #[test]
 fn enum_simple() {
-    assert_typecheck_fails!("`foo : <bar>");
+    assert_typecheck_fails!("`foo : [| bar |]");
     assert_typecheck_fails!("switch { `foo => 3} `bar : Num");
     assert_typecheck_fails!("switch { `foo => 3, `bar => true} `bar : Num");
 }
@@ -85,7 +86,7 @@ fn enum_simple() {
 #[test]
 fn enum_complex() {
     assert_typecheck_fails!(
-        "(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : <bla, ble> -> Num"
+        "(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : [| bla, ble |] -> Num"
     );
     // TODO typecheck this, I'm not sure how to do it with row variables
     // LATER NOTE: this requires row subtyping, not easy
@@ -95,12 +96,12 @@ fn enum_complex() {
             (switch {`bla => 6, `blo => 20} x)) `bla : Num"
     );
     assert_typecheck_fails!(
-        "let f : forall r. <blo, ble | r> -> Num =
+        "let f : forall r. [| blo, ble ; r |] -> Num =
             fun x => (switch {`blo => 1, `ble => 2, `bli => 3} x) in
         f"
     );
     assert_typecheck_fails!(
-        "let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
+        "let f : forall r. (forall p. [| blo, ble ; r |] -> [| bla, bli ; p |]) =
             fun x => (switch {`blo => `bla, `ble => `bli, _ => `blo} x) in
         f `bli"
     );
diff --git a/tests/unbound_type_variables.rs b/tests/unbound_type_variables.rs
index ffb871b0..13d8ee78 100644
--- a/tests/unbound_type_variables.rs
+++ b/tests/unbound_type_variables.rs
@@ -1,6 +1,9 @@
+// Since [RFC002](../rfcs/002-merge-types-terms-syntax.md), the following tests don't raise an
+// unbound type variable error anymore. Instead, the variable is interpreted as a term variable:
+// the tests should still fail, but they can now fail with a standard unbound identifier error.
 use assert_matches::assert_matches;
 use nickel::{
-    error::{Error, ParseError, ParseErrors},
+    error::{Error, EvalError, ParseError, ParseErrors, TypecheckError},
     identifier::Ident,
 };
 
@@ -9,12 +12,25 @@ use utilities::eval;
 macro_rules! assert_unbound {
     ( $term:expr, $var:expr ) => {
         let res = eval($term);
-        assert_matches!(res, Err(Error::ParseErrors(_)));
+        // Because expressions inside user-defined contracts are not currently typechecked, the
+        // error should be an `EvalError::UnboundIdentifier` at the time of writing this comment.
+        // Since it may not be the case forever, we accept alternative errors that make sense.
+        assert_matches!(res, Err(Error::ParseErrors(_)) | Err(Error::TypecheckError(_)) | Err(Error::EvalError(_)));
 
         match res {
-            Err(Error::ParseErrors(ParseErrors {errors})) => {
-                assert_matches!(errors.as_slice(), [ParseError::UnboundTypeVariables(vars, _)] if vars.contains(&Ident::from($var)) && vars.len() == 1)
-            }
+            Err(Error::ParseErrors(ParseErrors {errors})) =>
+                assert_matches!(errors.as_slice(),
+                    [ParseError::UnboundTypeVariables(vars, _)]
+                    if vars.contains(&Ident::from($var)) && vars.len() == 1),
+            Err(Error::TypecheckError(err)) =>
+                assert_matches!(err,
+                    TypecheckError::UnboundIdentifier(id, ..)
+                    | TypecheckError::UnboundTypeVariable(id, ..)
+                    if id.label.as_str() == $var),
+            Err(Error::EvalError(err)) =>
+                assert_matches!(err,
+                    EvalError::UnboundIdentifier(id, ..)
+                    if id.label.as_str() == $var),
             _ => unreachable!(),
         };
     }
@@ -24,12 +40,21 @@ macro_rules! assert_unbound {
 fn unbound_type_variables() {
     assert_unbound!("1 | a", "a");
     assert_unbound!(
-        "null | forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: b; Dyn}",
+        "let f | forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: a; Dyn}
+           = fun bar_ _g => {foo = [{field = 1}], bar = bar_} in
+         (f 1 (fun _x => [])).foo == [{field = 1}]",
         "d"
     );
     assert_unbound!(
-        "null | forall a b c. a -> (b -> List c) -> {foo : List {_ : a}, bar: b; e}",
+        "let f : forall a b c. a -> (b -> List c) -> {foo : List {field : a}, bar: a; e}
+           = fun bar_ _g => {foo = [{field = bar_}], bar = bar_} in
+         null",
         "e"
     );
-    assert_unbound!("null | a -> (forall a. a -> a)", "a");
+    assert_unbound!(
+        "let f | a -> (forall a. a -> a)
+                       = fun x => builtins.seq x null in
+                       f null",
+        "a"
+    );
 }