Repository: tweag/nickel
Pull request #589 (2022-01-21 18:38:54)

[RFC002] Unified syntax #1: one record to rule them all
First step of the implementation of RFC002 (#589). This PR adds the `UniTerm` syntax for records, which should be the most involved part. The plan is to avoid introducing another duplicate AST for the `UniTerm` syntax in general, and just convert on-the-fly to `Types` or `Terms` when parsing. Records and records types, as noted in the RFC, should be the only intersecting part of the union of the previous syntaxes, and thus do need a bit more machinery.

The most interesting changes are in `parser/uniterm.rs` and `grammar.lalrpop`. Other changes include fixing the syntax for row tails in tests and examples, and propagating unbound variables errors at different stage of the interpreter pipeline. Indeed, we could previously afford to check at parsing time if type variables were unbound, and then always assume there were in the rest of the code, but this isn't the case anymore with the `UniTerm` syntax.


Patch:
diff --git a/src/cache.rs b/src/cache.rs
index d7145ebf..b6cd2ba7 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -8,6 +8,7 @@ use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
 use crate::typecheck;
 use crate::typecheck::{linearization::StubHost, type_check};
+use crate::types::UnboundTypeVariableError;
 use crate::{eval, parser, transform};
 use codespan::{FileId, Files};
 use io::Read;
@@ -443,7 +444,10 @@ impl Cache {
     /// or do nothing if the entry has already been transformed. Require that the corresponding
     /// source has been parsed.
     /// If the source contains imports, recursively perform transformations on the imports too.
-    pub fn transform(&mut self, file_id: FileId) -> Result<CacheOp<()>, CacheError<()>> {
+    pub fn transform(
+        &mut self,
+        file_id: FileId,
+    ) -> Result<CacheOp<()>, CacheError<UnboundTypeVariableError>> {
         match self.entry_state(file_id) {
             Some(state) if state >= EntryState::Transformed => Ok(CacheOp::Cached(())),
             Some(state) if state >= EntryState::Parsed => {
@@ -451,7 +455,7 @@ impl Cache {
                     let CachedTerm {
                         term, parse_errs, ..
                     } = self.terms.remove(&file_id).unwrap();
-                    let term = transform::transform(term);
+                    let term = transform::transform(term)?;
                     self.terms.insert(
                         file_id,
                         CachedTerm {
@@ -504,29 +508,38 @@ impl Cache {
                 } = self.terms.remove(&file_id).unwrap();
 
                 if state < EntryState::Transforming {
+                    let pos = term.pos;
+
                     match SharedTerm::make_mut(&mut term.term) {
                         Term::Record(ref mut map, _) => {
-                            let map_res = std::mem::take(map)
+                            let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| (id, transform::transform(t)))
+                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
                                 .collect();
-                            *map = map_res;
+                            *map = map_res.map_err(|err| {
+                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
+                            })?;
                         }
                         Term::RecRecord(ref mut map, ref mut dyn_fields, _) => {
-                            let map_res = std::mem::take(map)
-                                .into_iter()
-                                .map(|(id, t)| (id, transform::transform(t)))
-                                .collect();
-
-                            let dyn_fields_res = std::mem::take(dyn_fields)
+                            let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id_t, t)| {
-                                    (transform::transform(id_t), transform::transform(t))
-                                })
+                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
                                 .collect();
 
-                            *map = map_res;
-                            *dyn_fields = dyn_fields_res;
+                            let dyn_fields_res: Result<_, UnboundTypeVariableError> =
+                                std::mem::take(dyn_fields)
+                                    .into_iter()
+                                    .map(|(id_t, t)| {
+                                        Ok((transform::transform(id_t)?, transform::transform(t)?))
+                                    })
+                                    .collect();
+
+                            *map = map_res.map_err(|err| {
+                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
+                            })?;
+                            *dyn_fields = dyn_fields_res.map_err(|err| {
+                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
+                            })?;
                         }
                         _ => panic!("cache::transform_inner(): not a record"),
                     }
@@ -632,9 +645,15 @@ impl Cache {
             result = CacheOp::Done(());
         };
 
-        let transform_res = self.transform(file_id).unwrap_or_else(|_| {
-            panic!("cache::prepare(): expected source to be parsed before transformations",)
-        });
+        let transform_res = self.transform(file_id).map_err(|cache_err| {
+            Error::ParseErrors(
+                cache_err
+                    .unwrap_error(
+                        "cache::prepare(): expected source to be parsed before transformations",
+                    )
+                    .into(),
+            )
+        })?;
 
         if transform_res == CacheOp::Done(()) {
             result = CacheOp::Done(());
@@ -660,7 +679,7 @@ impl Cache {
         }
         let (term, pending) = import_resolution::resolve_imports(term, self)?;
         type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
-        let term = transform::transform(term);
+        let term = transform::transform(term).map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
     }
 
diff --git a/src/error.rs b/src/error.rs
index 374e6fb8..415c30c4 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -291,6 +291,21 @@ pub enum ParseError {
     ),
     /// Unbound type variable
     UnboundTypeVariables(Vec<Ident>, RawSpan),
+    /// Illegal record literal in the uniterm syntax. In practice, this is a record with a
+    /// polymorphic tail that contains a construct that wasn't permitted inside a record type in
+    /// the original syntax. Typically, a field assignment:
+    ///
+    /// ```nickel
+    /// forall a. {foo : Num; a} // allowed
+    /// forall a. {foo : Num = 1; a} // InvalidUniRecord error: giving a value to foo is forbidden
+    /// ```
+    ///
+    /// See [RFC002](../../rfcs/002-merge-types-terms-syntax.md) for more details.
+    InvalidUniRecord(
+        RawSpan, /* illegal (in conjunction with a tail) construct position */
+        RawSpan, /* tail position */
+        RawSpan, /* whole record position */
+    ),
 }
 
 /// An error occurring during the resolution of an import.
@@ -444,6 +459,9 @@ impl ParseError {
                 InternalParseError::UnboundTypeVariables(idents, span) => {
                     ParseError::UnboundTypeVariables(idents, span)
                 }
+                InternalParseError::InvalidUniRecord(illegal_pos, tail_pos, pos) => {
+                    ParseError::InvalidUniRecord(illegal_pos, tail_pos, pos)
+                }
             },
         }
     }
@@ -1195,6 +1213,17 @@ impl ToDiagnostic<FileId> for ParseError {
                         .join(",")
                 ))
                 .with_labels(vec![primary(span)]),
+            ParseError::InvalidUniRecord(illegal_span, tail_span, span) => Diagnostic::error()
+                .with_message(format!("invalid record literal"))
+                .with_labels(vec![
+                    primary(span),
+                    secondary(illegal_span).with_message("can't use this record construct"),
+                    secondary(tail_span).with_message("in presence of a tail"),
+                ])
+                .with_notes(vec![
+                    String::from("Using a polymorphic tail in a record `{ ..; a}` requires the rest of the record to be only composed of type annotations, of the form `<field>: <type>`."),
+                    String::from("Value assignements, such as `<field> = <expr>`, metadata, etc. are forbidden."),
+                ]),
         };
 
         vec![diagnostic]
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index f5b55d94..a578881a 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -258,7 +258,7 @@ pub fn merge(
                         &env1,
                         types2.iter().chain(contracts2.iter()),
                         &env2,
-                    );
+                    )?;
                     (Some(v), e)
                 }
                 v1 => (v1, env1.clone()),
@@ -275,7 +275,7 @@ pub fn merge(
                         &env2,
                         types1.iter().chain(contracts1.iter()),
                         &env1,
-                    );
+                    )?;
                     (Some(v), e)
                 }
                 v2 => (v2, env2.clone()),
@@ -433,21 +433,26 @@ pub fn merge(
 fn cross_apply_contracts<'a>(
     t1: RichTerm,
     env1: &Environment,
-    it2: impl Iterator<Item = &'a Contract>,
+    mut it2: impl Iterator<Item = &'a Contract>,
     env2: &Environment,
-) -> (RichTerm, Environment) {
+) -> Result<(RichTerm, Environment), EvalError> {
     let mut env = Environment::new();
     let mut env1_local = env1.clone();
 
     let pos = t1.pos.into_inherited();
     let result = it2
-        .fold(t1, |acc, ctr| {
+        .try_fold(t1, |acc, ctr| {
             let ty_closure = ctr.types.clone().closurize(&mut env1_local, env2.clone());
-            mk_term::assume(ty_closure, ctr.label.clone(), acc).with_pos(pos)
-        })
+            mk_term::assume(ty_closure, ctr.label.clone(), acc)
+                .map_err(|crate::types::UnboundTypeVariableError(id)| {
+                    let pos = id.pos;
+                    EvalError::UnboundIdentifier(id, pos)
+                })
+                .map(|rt| rt.with_pos(pos))
+        })?
         .closurize(&mut env, env1_local);
 
-    (result, env)
+    Ok((result, env))
 }
 
 /// Merge the two optional documentations of a metavalue.
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index abc99361..329d4459 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -1,30 +1,48 @@
-use std::collections::HashMap;
-use std::ffi::OsString;
+use std::{
+    collections::HashMap,
+    ffi::OsString,
+    convert::TryFrom,
+};
 
 use codespan::FileId;
-
 use lalrpop_util::ErrorRecovery;
 
-use super::ExtendedTerm;
-use super::utils::*;
-use super::lexer::{Token, NormalToken, StringToken, MultiStringToken};
+use super::{
+    ExtendedTerm,
+    utils::*,
+    lexer::{Token, NormalToken, StringToken, MultiStringToken},
+    error::ParseError,
+    uniterm::UniRecord,
+};
 
-use crate::{mk_app, mk_opn, mk_fun};
-use crate::identifier::Ident;
-use crate::destruct::{Match, LastMatch, Destruct};
-use crate::parser::error::ParseError;
-use crate::term::{BinaryOp, RichTerm, Term, UnaryOp, StrChunk, MetaValue,
-    MergePriority, Contract, NAryOp, RecordAttrs, SharedTerm};
-use crate::term::make as mk_term;
-use crate::types::{Types, AbsType};
+use crate::{
+    mk_app,
+    mk_opn,
+    mk_fun,
+    identifier::Ident,
+    destruct::{Match, LastMatch, Destruct},
+    term::{
+        BinaryOp, RichTerm, Term, UnaryOp, StrChunk, MetaValue,
+        MergePriority, Contract, NAryOp, RecordAttrs, SharedTerm,
+        make as mk_term},
+    types::{Types, AbsType},
+    position::TermPos,
+};
 
 grammar<'input, 'err>(src_id: FileId, errors: &'err mut Vec<ErrorRecovery<usize, Token<'input>, ParseError>>);
 
-WithPos<Rule>: RichTerm = <l: @L> <t: Rule> <r: @R> => t.with_pos(mk_pos(src_id, l, r));
-CheckUnbound<Rule>: Types = <l: @L> <t: Rule> <r: @R> =>? check_unbound(&t, mk_span(src_id, l, r)).map_err(|e| lalrpop_util::ParseError::User{error: e}).and(Ok(t));
+WithPos<Rule>: Rule = <l: @L> <t: Rule> <r: @R> => t.with_pos(mk_pos(src_id, l, r));
+
+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>> =>?
+    Types::try_from(ut)
+        .map_err(|e| lalrpop_util::ParseError::User{error: e});
 
 AnnotAtom: MetaValue = {
-    "|" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
+    "|" <l: @L> <ty_res: Types> <r: @R> => MetaValue {
         doc: None,
         types: None,
         contracts: vec![Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}],
@@ -45,7 +63,7 @@ AnnotAtom: MetaValue = {
         priority: Default::default(),
         value: None,
     },
-    ":" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
+    ":" <l: @L> <ty_res: Types> <r: @R> => MetaValue {
         doc: None,
         types: Some(Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}),
         contracts: Vec::new(),
@@ -167,6 +185,33 @@ RecordOperationChain: RichTerm = {
         mk_app!(mk_term::op2(BinaryOp::DynExtend(), id, r), t),
 };
 
+RowTail: Types = {
+    <Ident> => Types(AbsType::Var(<>)),
+    "Dyn" => Types(AbsType::Dyn()),
+}
+
+UniRecord: UniRecord = {
+   "{" <fields: (<RecordField> ",")*>
+       <last: RecordLastField?>
+       <l: @L> <tail: (";" RowTail)?> <r: @R>
+   "}" => {
+        let (last_field, attrs) = match last {
+            Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
+            Some(RecordLastField::Ellipsis) =>
+                (None, RecordAttrs { open: true }),
+            None => (None, Default::default())
+        };
+
+        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))),
+            attrs,
+            pos: TermPos::None
+        }
+    },
+};
+
 Atom: RichTerm = {
     "(" <CurriedOp> ")",
     "(" <Term> ")",
@@ -175,19 +220,9 @@ Atom: RichTerm = {
     Bool => RichTerm::from(Term::Bool(<>)),
     StrChunks,
     Ident => RichTerm::from(Term::Var(<>)),
+    AsTerm<UniRecord>,
     "`" <EnumTag> => RichTerm::from(Term::Enum(<>)),
-    "{" <fields: (<RecordField> ",")*> <last: RecordLastField?> "}" => {
-        let (last_field, attrs) = match last {
-            Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
-            Some(RecordLastField::Ellipsis) =>
-                (None, RecordAttrs { open: true }),
-            None => (None, Default::default())
-        };
-
-        let fields = fields.into_iter().chain(last_field.into_iter());
-        RichTerm::from(build_record(fields, attrs))
-    },
-    "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
+     "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
         let terms : Vec<RichTerm> = terms.into_iter()
             .chain(last.into_iter()).collect();
         RichTerm::from(Term::List(terms))
@@ -570,11 +605,6 @@ BaseType: Types = {
     "Str" => Types(AbsType::Str()),
 };
 
-RowTail: Types = {
-    <Ident> => Types(AbsType::Var(<>)),
-    "Dyn" => Types(AbsType::Dyn()),
-}
-
 subType : Types = {
     <BaseType>,
     "List" <ty: subType?> => {
@@ -603,25 +633,7 @@ subType : Types = {
             );
         Types(AbsType::Enum(Box::new(ty)))
     },
-    "{" <rows:(<Ident> ":" <Types> ",")*>
-        <last:(<Ident> ":" <Types>)?>
-        <tail: ("|" <RowTail>)?> "}" => {
-        let ty = rows.into_iter()
-            .chain(last.into_iter())
-            // As we build row types as a linked list via a fold on the original
-            // iterator, the order of identifiers is reversed. This not a big deal
-            // but it's less confusing to the user to print them in the original
-            // order for error reporting.
-            .rev()
-            .fold(
-                tail.unwrap_or(Types(AbsType::RowEmpty())),
-                |t, i_ty| {
-                    let (i, ty) = i_ty;
-                    Types(AbsType::RowExtend(i, Some(Box::new(ty)), Box::new(t)))
-                }
-            );
-        Types(AbsType::StaticRecord(Box::new(ty)))
-    },
+    AsTypes<UniRecord>,
     "{" "_" ":" <Types> "}" => Types(AbsType::DynRecord(Box::new(<>))),
 };
 
@@ -650,6 +662,7 @@ extern {
 
         "?" => Token::Normal(NormalToken::QuestionMark),
         "," => Token::Normal(NormalToken::Comma),
+        ";" => Token::Normal(NormalToken::Semicolon),
         ":" => Token::Normal(NormalToken::Colon),
         "$" => Token::Normal(NormalToken::Dollar),
         "=" => Token::Normal(NormalToken::Equals),
diff --git a/src/parser/error.rs b/src/parser/error.rs
index 6d71bdf5..18e310d5 100644
--- a/src/parser/error.rs
+++ b/src/parser/error.rs
@@ -1,5 +1,4 @@
-use crate::identifier::Ident;
-use crate::position::RawSpan;
+use crate::{identifier::Ident, position::RawSpan};
 
 #[derive(Clone, PartialEq, Debug)]
 pub enum LexicalError {
@@ -19,4 +18,19 @@ pub enum ParseError {
     Lexical(LexicalError),
     /// Unbound type variable(s)
     UnboundTypeVariables(Vec<Ident>, RawSpan),
+    /// Illegal record literal in the uniterm syntax. In practice, this is a record with a
+    /// polymorphic tail that contains a construct that wasn't permitted inside a record type in
+    /// the original syntax. Typically, a field assignment:
+    ///
+    /// ```nickel
+    /// forall a. {foo : Num; a} // allowed
+    /// forall a. {foo : Num = 1; a} // InvalidUniRecord error: giving a value to foo is forbidden
+    /// ```
+    ///
+    /// See [RFC002](../../rfcs/002-merge-types-terms-syntax.md) for more details.
+    InvalidUniRecord(
+        RawSpan, /* illegal (in conjunction with a tail) construct position */
+        RawSpan, /* tail position */
+        RawSpan, /* whole record position */
+    ),
 }
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 322843df..6fefb10e 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -82,6 +82,8 @@ pub enum NormalToken<'input> {
     QuestionMark,
     #[token(",")]
     Comma,
+    #[token(";")]
+    Semicolon,
     #[token(":")]
     Colon,
     #[token("$")]
diff --git a/src/parser/mod.rs b/src/parser/mod.rs
index 7ffbf90f..d01afdf0 100644
--- a/src/parser/mod.rs
+++ b/src/parser/mod.rs
@@ -11,9 +11,11 @@ lalrpop_mod!(
 
 pub mod error;
 pub mod lexer;
+pub mod uniterm;
+pub mod utils;
+
 #[cfg(test)]
 mod tests;
-pub mod utils;
 
 /// Either a term or a toplevel let declaration.
 pub enum ExtendedTerm {
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
new file mode 100644
index 00000000..4a70384c
--- /dev/null
+++ b/src/parser/uniterm.rs
@@ -0,0 +1,143 @@
+//! 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 crate::{
+    position::{RawSpan, TermPos},
+    term::{MergePriority, MetaValue, RecordAttrs, RichTerm, Term},
+    types::{AbsType, Types},
+};
+
+use std::convert::TryFrom;
+
+/// A record in the UniTerm syntax.
+#[derive(Clone)]
+pub struct UniRecord {
+    pub fields: Vec<(FieldPathElem, RichTerm)>,
+    pub tail: Option<(Types, TermPos)>,
+    pub attrs: RecordAttrs,
+    pub pos: 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.
+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`.
+    pub fn into_type_strict(self) -> Result<Types, InvalidRecordTypeError> {
+        let ty = self
+            .fields
+            .into_iter()
+            // Because we build row types as a linked list by folding on the original iterator, the
+            // order of identifiers is reversed. This not a big deal but it's less confusing to the
+            // user to print them in the original order for error reporting.
+            .rev()
+            .try_fold(
+                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(),
+                                    )))
+                                }
+                            }
+                        }
+                        FieldPathElem::Expr(rt) => Err(InvalidRecordTypeError(rt.pos)),
+                    }
+                },
+            )?;
+        Ok(Types(AbsType::StaticRecord(Box::new(ty))))
+    }
+
+    pub fn with_pos(mut self, pos: TermPos) -> Self {
+        self.pos = pos;
+        self
+    }
+}
+
+impl TryFrom<UniRecord> for RichTerm {
+    type Error = ParseError;
+
+    /// 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.
+    fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
+        let pos = ur.pos;
+
+        let result = if let Some((_, tail_pos)) = ur.tail {
+            ur.into_type_strict()
+                // We unwrap all positions: at this stage of the parsing, they must all be set
+                .map_err(|InvalidRecordTypeError(pos)| {
+                    ParseError::InvalidUniRecord(pos.unwrap(), tail_pos.unwrap(), pos.unwrap())
+                })
+                .and_then(|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,
+            )))
+        };
+
+        result.map(|rt| rt.with_pos(pos))
+    }
+}
+
+impl TryFrom<UniRecord> for Types {
+    type Error = ParseError;
+
+    /// 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.
+    fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
+        let pos = ur.pos;
+
+        if let Some((_, tail_pos)) = ur.tail {
+            ur.into_type_strict()
+                .map_err(|InvalidRecordTypeError(illegal_pos)| {
+                    ParseError::InvalidUniRecord(
+                        illegal_pos.unwrap(),
+                        tail_pos.unwrap(),
+                        pos.unwrap(),
+                    )
+                })
+        } else {
+            ur.clone()
+                .into_type_strict()
+                .or_else(|_| RichTerm::try_from(ur).map(|rt| Types(AbsType::Flat(rt))))
+        }
+    }
+}
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 73471720..563125ff 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -1,7 +1,7 @@
 //! Various helpers and companion code for the parser are put here to keep the grammar definition
 //! uncluttered.
 use std::collections::hash_map::Entry;
-use std::collections::{HashMap, HashSet};
+use std::collections::HashMap;
 use std::fmt::Debug;
 
 use codespan::FileId;
@@ -10,10 +10,9 @@ use crate::{
     identifier::Ident,
     label::Label,
     mk_app, mk_fun,
-    parser::error::ParseError,
     position::{RawSpan, TermPos},
     term::{make as mk_term, BinaryOp, MetaValue, RecordAttrs, RichTerm, StrChunk, Term, UnaryOp},
-    types::{AbsType, Types},
+    types::Types,
 };
 
 /// Distinguish between the standard string separators `"`/`"` and the multi-line string separators
@@ -534,64 +533,3 @@ pub fn strip_indent_doc(doc: String) -> String {
         .next()
         .expect("expected non-empty chunks after indentation of documentation")
 }
-
-/// Recursively checks for unbound type variables in a type
-pub fn check_unbound(types: &Types, span: RawSpan) -> Result<(), ParseError> {
-    // heavy lifting function, recurses into a type expression and returns a set of unbound vars
-    fn find_unbound_vars(types: &Types, unbound_set: &mut HashSet<Ident>) {
-        match &types.0 {
-            AbsType::Var(ident) => {
-                unbound_set.insert(ident.clone());
-            }
-            AbsType::Forall(ident, ty) => {
-                // forall needs a "scoped" set for the variables in its nodes
-                let mut forall_unbound_vars = HashSet::new();
-                find_unbound_vars(ty, &mut forall_unbound_vars);
-
-                forall_unbound_vars.remove(ident);
-
-                // once the forall vars are recursed into and analyzed, the parent set and
-                // the forall set are merged
-                unbound_set.extend(forall_unbound_vars);
-            }
-            AbsType::Arrow(s, t) => {
-                find_unbound_vars(s, unbound_set);
-                find_unbound_vars(t, unbound_set);
-            }
-            AbsType::DynRecord(ty)
-            | AbsType::StaticRecord(ty)
-            | AbsType::List(ty)
-            | AbsType::Enum(ty) => {
-                find_unbound_vars(ty, unbound_set);
-            }
-            AbsType::RowExtend(_, opt_ty, ty) => {
-                if let Some(ty) = opt_ty {
-                    find_unbound_vars(ty, unbound_set);
-                }
-
-                find_unbound_vars(ty, unbound_set);
-            }
-            AbsType::Dyn()
-            | AbsType::Bool()
-            | AbsType::Num()
-            | AbsType::Str()
-            | AbsType::Sym()
-            | AbsType::Flat(_)
-            | AbsType::RowEmpty() => {}
-        }
-    }
-
-    let mut unbound_set: HashSet<Ident> = HashSet::new();
-
-    // recurse into type and find unbound type vars
-    find_unbound_vars(types, &mut unbound_set);
-
-    if !unbound_set.is_empty() {
-        return Err(ParseError::UnboundTypeVariables(
-            unbound_set.into_iter().collect(),
-            span,
-        ));
-    }
-
-    Ok(())
-}
diff --git a/src/position.rs b/src/position.rs
index 9f5fb0d1..5a634b8e 100644
--- a/src/position.rs
+++ b/src/position.rs
@@ -4,7 +4,7 @@
 //! raw byte indices.  They are prefixed with Raw to differentiate them from codespan's types and
 //! indicate that they do not store human friendly data like lines and columns.
 use codespan::{ByteIndex, FileId};
-use std::cmp::Ordering;
+use std::cmp::{max, min, Ordering};
 
 /// A position identified by a byte offset in a file.
 #[derive(Debug, Clone, Copy, Eq, PartialEq)]
@@ -23,6 +23,22 @@ pub struct RawSpan {
     pub end: ByteIndex,
 }
 
+impl RawSpan {
+    /// Fuse two spans if they are from the same source file. The resulting span is the smallest
+    /// span that contain both `span1` and `span2`.
+    pub fn fuse(span1: RawSpan, span2: RawSpan) -> Option<RawSpan> {
+        if span1.src_id == span2.src_id {
+            Some(RawSpan {
+                src_id: span1.src_id,
+                start: min(span1.start, span2.start),
+                end: max(span1.end, span2.end),
+            })
+        } else {
+            None
+        }
+    }
+}
+
 /// The position span of a term.
 #[derive(Debug, Clone, Copy, Eq, PartialEq, Hash)]
 pub enum TermPos {
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index 08c76699..210ca64c 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -118,56 +118,60 @@ impl ReplImpl {
             return Err(parse_errs.into());
         }
 
+        // Because we don't use the cache for input, we have to perform recursive import
+        // resolution/typechecking/transformation by ourselves.
+        //
+        // `id` must be set to `None` for normal lets and to `Some(id_)` for top-level lets. In the
+        // latter case, we need to update the current type environment before doing program
+        // transformations in the case of a top-level let.
+        fn prepare(
+            repl_impl: &mut ReplImpl,
+            id: Option<Ident>,
+            t: RichTerm,
+        ) -> Result<RichTerm, Error> {
+            let (t, pending) = import_resolution::resolve_imports(t, &mut repl_impl.cache)?;
+            for id in &pending {
+                repl_impl.cache.resolve_imports(*id).unwrap();
+            }
+
+            typecheck::type_check_in_env(&t, &repl_impl.env.type_env, &repl_impl.cache)?;
+
+            if let Some(id) = id {
+                typecheck::Envs::env_add(
+                    &mut repl_impl.env.type_env,
+                    id.clone(),
+                    &t,
+                    &repl_impl.cache,
+                );
+            }
+
+            for id in &pending {
+                repl_impl
+                    .cache
+                    .typecheck(*id, &repl_impl.init_type_env)
+                    .map_err(|cache_err| {
+                        cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
+                    })?;
+            }
+
+            let t = transform::transform(t).map_err(|err| Error::ParseErrors(err.into()))?;
+            for id in &pending {
+                repl_impl
+                    .cache
+                    .transform(*id)
+                    .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
+            }
+
+            Ok(t)
+        }
+
         match term {
-            // Because we don't use the cache for input, we have to perform recursive import
-            // resolution/typechecking/transformation by oursleves.
             ExtendedTerm::RichTerm(t) => {
-                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
-                for id in &pending {
-                    self.cache.resolve_imports(*id).unwrap();
-                }
-
-                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
-                for id in &pending {
-                    self.cache
-                        .typecheck(*id, &self.init_type_env)
-                        .map_err(|cache_err| {
-                            cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
-                        })?;
-                }
-
-                let t = transform::transform(t);
-                for id in &pending {
-                    self.cache
-                        .transform(*id)
-                        .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
-                }
-
+                let t = prepare(self, None, t)?;
                 Ok(eval_function(t, &self.env.eval_env, &mut self.cache)?.into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
-                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
-                for id in &pending {
-                    self.cache.resolve_imports(*id).unwrap();
-                }
-
-                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
-                typecheck::Envs::env_add(&mut self.env.type_env, id.clone(), &t, &self.cache);
-                for id in &pending {
-                    self.cache
-                        .typecheck(*id, &self.init_type_env)
-                        .map_err(|cache_err| {
-                            cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
-                        })?;
-                }
-
-                let t = transform::transform(t);
-                for id in &pending {
-                    self.cache
-                        .transform(*id)
-                        .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
-                }
-
+                let t = prepare(self, Some(id.clone()), t)?;
                 let local_env = self.env.eval_env.clone();
                 eval::env_add(&mut self.env.eval_env, id.clone(), t, local_env);
                 Ok(EvalResult::Bound(id))
diff --git a/src/term.rs b/src/term.rs
index 03a8c340..5c3bf65e 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -21,7 +21,7 @@ use crate::identifier::Ident;
 use crate::label::Label;
 use crate::match_sharedterm;
 use crate::position::TermPos;
-use crate::types::{AbsType, Types};
+use crate::types::{AbsType, Types, UnboundTypeVariableError};
 use codespan::FileId;
 use serde::{Deserialize, Serialize};
 use std::collections::HashMap;
@@ -910,7 +910,7 @@ impl fmt::Display for NAryOp {
 }
 
 #[derive(Copy, Clone)]
-pub enum TraverseMethod {
+pub enum TraverseOrder {
     TopDown,
     BottomUp,
 }
@@ -952,21 +952,21 @@ impl RichTerm {
         self
     }
 
-    /// Apply a transformation on a whole term by mapping a function `f` on each node in
-    /// manner defined by the method.
+    /// Apply a transformation on a whole term by mapping a faillible function `f` on each node in
+    /// manner as prescribed by the order.
     /// `f` may return a generic error `E` and use the state `S` which is passed around.
     pub fn traverse<F, S, E>(
         self,
         f: &mut F,
         state: &mut S,
-        method: TraverseMethod,
+        method: TraverseOrder,
     ) -> Result<RichTerm, E>
     where
         F: FnMut(RichTerm, &mut S) -> Result<RichTerm, E>,
     {
         let rt = match method {
-            TraverseMethod::TopDown => f(self, state)?,
-            TraverseMethod::BottomUp => self,
+            TraverseOrder::TopDown => f(self, state)?,
+            TraverseOrder::BottomUp => self,
         };
         let pos = rt.pos;
 
@@ -1168,8 +1168,8 @@ impl RichTerm {
         };
 
         match method {
-            TraverseMethod::TopDown => Ok(result),
-            TraverseMethod::BottomUp => f(result, state),
+            TraverseOrder::TopDown => Ok(result),
+            TraverseOrder::BottomUp => f(result, state),
         }
     }
 }
@@ -1394,14 +1394,14 @@ pub mod make {
         Term::OpN(op, args.into_iter().map(T::into).collect()).into()
     }
 
-    pub fn assume<T>(types: Types, l: Label, t: T) -> RichTerm
+    pub fn assume<T>(types: Types, l: Label, t: T) -> Result<RichTerm, UnboundTypeVariableError>
     where
         T: Into<RichTerm>,
     {
-        mk_app!(
-            op2(BinaryOp::Assume(), types.contract(), Term::Lbl(l)),
+        Ok(mk_app!(
+            op2(BinaryOp::Assume(), types.contract()?, Term::Lbl(l)),
             t.into()
-        )
+        ))
     }
 
     pub fn string<S>(s: S) -> RichTerm
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
index ab1f02fd..b4162d36 100644
--- a/src/transform/apply_contracts.rs
+++ b/src/transform/apply_contracts.rs
@@ -8,37 +8,42 @@
 //!
 //! It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
 //! value is unwrapped.
-use crate::term::{make as mk_term, BinaryOp, RichTerm, Term};
-use crate::{match_sharedterm, mk_app};
+use crate::{
+    match_sharedterm, mk_app,
+    term::{make as mk_term, BinaryOp, RichTerm, Term},
+    types::UnboundTypeVariableError,
+};
 
 /// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the inner
 /// value.  Otherwise, return the term unchanged.
-pub fn transform_one(rt: RichTerm) -> RichTerm {
+/// Fail if an unbound type variable is encountered.
+pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
     let pos = rt.pos;
-    match_sharedterm! {rt.term,
+    let result = match_sharedterm! {rt.term,
         with {
             Term::MetaValue(meta) if meta.value.is_some() => {
                 let mut meta = meta;
                 let pos_inh = pos.into_inherited();
-                let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
+                let inner = meta.types.iter().chain(meta.contracts.iter()).try_fold(
                     meta.value.take().unwrap(),
                     |acc, ctr| {
-                        mk_app!(
+                        Ok(mk_app!(
                             mk_term::op2(
                                 BinaryOp::Assume(),
-                                ctr.types.contract(),
+                                ctr.types.contract()?,
                                 Term::Lbl(ctr.label.clone())
                             )
                             .with_pos(pos_inh),
                             acc
                         )
-                        .with_pos(pos_inh)
+                        .with_pos(pos_inh))
                     },
-                );
+                )?;
 
                 meta.value.replace(inner);
                 RichTerm::new(Term::MetaValue(meta), pos)
             }
         } else rt
-    }
+    };
+    Ok(result)
 }
diff --git a/src/transform/import_resolution.rs b/src/transform/import_resolution.rs
index 8b013f41..f79a8505 100644
--- a/src/transform/import_resolution.rs
+++ b/src/transform/import_resolution.rs
@@ -3,7 +3,7 @@
 //! identifier directly.
 use super::ImportResolver;
 use crate::error::ImportError;
-use crate::term::{RichTerm, Term, TraverseMethod};
+use crate::term::{RichTerm, Term, TraverseOrder};
 use codespan::FileId;
 use std::path::PathBuf;
 
@@ -55,7 +55,7 @@ where
             Ok(rt)
         },
         &mut state,
-        TraverseMethod::BottomUp,
+        TraverseOrder::BottomUp,
     )?;
 
     Ok((transformed, stack))
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index c27467b2..3c918888 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -1,9 +1,12 @@
 //! Various post transformations of nickel code.
-use crate::cache::ImportResolver;
-use crate::eval::{lazy::Thunk, Closure, Environment, IdentKind};
-use crate::identifier::Ident;
-use crate::term::{Contract, RichTerm, Term, TraverseMethod};
-use crate::types::{AbsType, Types};
+use crate::{
+    cache::ImportResolver,
+    eval::{lazy::Thunk, Closure, Environment, IdentKind},
+    identifier::Ident,
+    term::{Contract, RichTerm, Term, TraverseOrder},
+    types::{AbsType, Types, UnboundTypeVariableError},
+};
+
 use simple_counter::*;
 
 generate_counter!(FreshVarCounter, usize);
@@ -19,30 +22,29 @@ pub mod share_normal_form;
 /// Do not perform transformations on the imported files. If needed, either do it yourself using
 /// pending imports returned by [`resolve_imports`](../fn.resolve_imports.html) or use the
 /// [`Cache`](../../cache/struct.Cache.html)
-pub fn transform(rt: RichTerm) -> RichTerm {
-    let rt = rt
+pub fn transform(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+    let rt = rt.traverse(
+        &mut |rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
+            // before anything, we have to desugar the syntax
+            let rt = desugar_destructuring::transform_one(rt);
+            // We need to do contract generation before wrapping stuff in variables
+            let rt = apply_contracts::transform_one(rt)?;
+            Ok(rt)
+        },
+        &mut (),
+        TraverseOrder::TopDown,
+    )?;
+
+    Ok(rt
         .traverse(
             &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
-                // before anything, we have to desugar the syntax
-                let rt = desugar_destructuring::transform_one(rt);
-                // We need to do contract generation before wrapping stuff in variables
-                let rt = apply_contracts::transform_one(rt);
+                let rt = share_normal_form::transform_one(rt);
                 Ok(rt)
             },
             &mut (),
-            TraverseMethod::TopDown,
+            TraverseOrder::BottomUp,
         )
-        .unwrap();
-
-    rt.traverse(
-        &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
-            let rt = share_normal_form::transform_one(rt);
-            Ok(rt)
-        },
-        &mut (),
-        TraverseMethod::BottomUp,
-    )
-    .unwrap()
+        .unwrap())
 }
 
 /// Generate a new fresh variable which do not clash with user-defined variables.
@@ -105,7 +107,7 @@ impl Closurizable for RichTerm {
         //
         //
         // We currently only do this optimization for generated variables (introduced by the share
-        // normal form). We could do it for non-generated identifiers as well, but be we would be
+        // normal form). We could do it for non-generated identifiers as well, but we would be
         // renaming user-supplied variables by gibberish generated names. It may hamper error
         // reporting, so for the time being, we restrict ourselves to generated identifiers. Note
         // that performing or not performing this optimization for user-supplied variables doesn't
@@ -140,7 +142,9 @@ impl Closurizable for Types {
     /// Extract the underlying contract, closurize it and wrap it back as a flat type (an opaque
     /// type defined by a custom contract).
     fn closurize(self, env: &mut Environment, with_env: Environment) -> Types {
-        Types(AbsType::Flat(self.contract().closurize(env, with_env)))
+        Types(AbsType::Flat(
+            self.contract().unwrap().closurize(env, with_env),
+        ))
     }
 }
 
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 657f27af..bcf09f67 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -50,7 +50,7 @@ use crate::{mk_tyw_arrow, mk_tyw_enum, mk_tyw_enum_row, mk_tyw_record, mk_tyw_ro
 use std::collections::{HashMap, HashSet};
 use std::convert::TryInto;
 
-use self::linearization::{Linearization, Linearizer, ScopeId, StubHost};
+use self::linearization::{Linearization, Linearizer, StubHost};
 
 pub mod error;
 pub mod linearization;
@@ -620,10 +620,8 @@ fn type_check_<L: Linearizer>(
             unify(state, strict, ty, ty_ret)
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
-            tys_op
-                .into_iter()
-                .zip(args.iter())
-                .try_for_each(|(ty_t, t)| {
+            tys_op.into_iter().zip(args.iter()).try_for_each(
+                |(ty_t, t)| -> Result<_, TypecheckError> {
                     type_check_(
                         state,
                         envs.clone(),
@@ -634,7 +632,8 @@ fn type_check_<L: Linearizer>(
                         ty_t,
                     )?;
                     Ok(())
-                })?;
+                },
+            )?;
 
             Ok(())
         }
diff --git a/src/types.rs b/src/types.rs
index b3c0e0ab..c058cb06 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -51,6 +51,7 @@
 //! otherwise.  Contract checks are introduced by `Promise` and `Assume` blocks or alternatively by
 //! enriched values `Contract` or `ContractDefault`. They ensure sane interaction between typed and
 //! untyped parts.
+use crate::error::{ParseError, ParseErrors, TypecheckError};
 use crate::identifier::Ident;
 use crate::term::make as mk_term;
 use crate::term::{RichTerm, Term, UnaryOp};
@@ -149,6 +150,29 @@ impl<Ty> AbsType<Ty> {
     }
 }
 
+#[derive(Clone, Debug)]
+pub struct UnboundTypeVariableError(pub Ident);
+
+impl From<UnboundTypeVariableError> for TypecheckError {
+    fn from(err: UnboundTypeVariableError) -> Self {
+        let pos = err.0.pos;
+        TypecheckError::UnboundTypeVariable(err.0, pos)
+    }
+}
+
+impl From<UnboundTypeVariableError> for ParseError {
+    fn from(err: UnboundTypeVariableError) -> Self {
+        let pos = err.0.pos;
+        ParseError::UnboundTypeVariables(vec![err.0], pos.unwrap())
+    }
+}
+
+impl From<UnboundTypeVariableError> for ParseErrors {
+    fn from(err: UnboundTypeVariableError) -> Self {
+        ParseErrors::from(ParseError::from(err))
+    }
+}
+
 /// Concrete, recursive type for a Nickel type.
 #[derive(Clone, PartialEq, Debug)]
 pub struct Types(pub AbsType<Box<Types>>);
@@ -156,7 +180,7 @@ pub struct Types(pub AbsType<Box<Types>>);
 impl Types {
     /// Return the contract corresponding to a type, either as a function or a record. Said
     /// contract must then be applied using the `Assume` primitive operation.
-    pub fn contract(&self) -> RichTerm {
+    pub fn contract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
         let mut sy = 0;
         self.subcontract(HashMap::new(), true, &mut sy)
     }
@@ -176,30 +200,40 @@ impl Types {
         mut h: HashMap<Ident, (RichTerm, RichTerm)>,
         pol: bool,
         sy: &mut i32,
-    ) -> RichTerm {
+    ) -> Result<RichTerm, UnboundTypeVariableError> {
         use crate::stdlib::contracts;
 
-        match self.0 {
+        fn get_var(
+            vars: &HashMap<Ident, (RichTerm, RichTerm)>,
+            id: &Ident,
+            pol: bool,
+        ) -> Result<RichTerm, UnboundTypeVariableError> {
+            let (pos, neg) = vars
+                .get(id)
+                .ok_or_else(|| UnboundTypeVariableError(id.clone()))?;
+            if pol {
+                Ok(pos.clone())
+            } else {
+                Ok(neg.clone())
+            }
+        }
+
+        let ctr = match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
             AbsType::Str() => contracts::string(),
             //TODO: optimization: have a specialized contract for `List Dyn`, to avoid mapping an
             //always successful contract on each element.
-            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.subcontract(h, pol, sy)),
+            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.subcontract(h, pol, sy)?),
             AbsType::Sym() => panic!("Are you trying to check a Sym at runtime?"),
             AbsType::Arrow(ref s, ref t) => mk_app!(
                 contracts::func(),
-                s.subcontract(h.clone(), !pol, sy),
-                t.subcontract(h, pol, sy)
+                s.subcontract(h.clone(), !pol, sy)?,
+                t.subcontract(h, pol, sy)?
             ),
             AbsType::Flat(ref t) => t.clone(),
-            AbsType::Var(ref i) => {
-                let (rt, _) = h
-                    .get(i)
-                    .unwrap_or_else(|| panic!("Unbound type variable {:?}", i));
-                rt.clone()
-            }
+            AbsType::Var(ref id) => get_var(&h, id, true)?,
             AbsType::Forall(ref i, ref t) => {
                 let inst_var = mk_app!(contracts::forall_var(), Term::Sym(*sy), Term::Bool(pol));
 
@@ -207,18 +241,21 @@ impl Types {
 
                 h.insert(i.clone(), (inst_var, inst_tail));
                 *sy += 1;
-                t.subcontract(h, pol, sy)
+                t.subcontract(h, pol, sy)?
             }
             AbsType::RowEmpty() | AbsType::RowExtend(..) => contracts::fail(),
             AbsType::Enum(ref r) => {
-                fn form(ty: Types, h: HashMap<Ident, (RichTerm, RichTerm)>) -> RichTerm {
-                    match ty.0 {
+                fn form(
+                    ty: Types,
+                    h: HashMap<Ident, (RichTerm, RichTerm)>,
+                ) -> Result<RichTerm, UnboundTypeVariableError> {
+                    let ctr = match ty.0 {
                         AbsType::RowEmpty() => contracts::fail(),
                         AbsType::RowExtend(_, Some(_), _) => {
                             panic!("It should be a row without type")
                         }
                         AbsType::RowExtend(id, None, rest) => {
-                            let rest_contract = form(*rest, h);
+                            let rest_contract = form(*rest, h)?;
                             let mut map = HashMap::new();
                             map.insert(id, Term::Bool(true).into());
 
@@ -235,17 +272,14 @@ impl Types {
                                 )
                             )
                         }
-                        AbsType::Var(ref i) => {
-                            let (rt, _) = h
-                                .get(i)
-                                .unwrap_or_else(|| panic!("Unbound type variable {:?}", i));
-                            rt.clone()
-                        }
+                        AbsType::Var(ref id) => get_var(&h, id, true)?,
                         not_row => panic!("It should be a row!! {:?}", not_row),
-                    }
+                    };
+
+                    Ok(ctr)
                 }
 
-                form(*r.clone(), h)
+                form(*r.clone(), h)?
             }
             AbsType::StaticRecord(ref ty) => {
                 fn form(
@@ -253,19 +287,14 @@ impl Types {
                     pol: bool,
                     ty: &Types,
                     h: HashMap<Ident, (RichTerm, RichTerm)>,
-                ) -> RichTerm {
-                    match &ty.0 {
+                ) -> Result<RichTerm, UnboundTypeVariableError> {
+                    let ctr = match &ty.0 {
                         AbsType::RowEmpty() => contracts::empty_tail(),
                         AbsType::Dyn() => contracts::dyn_tail(),
-                        AbsType::Var(id) => {
-                            let (_, rt) = h
-                                .get(id)
-                                .unwrap_or_else(|| panic!("Unbound type variable {:?}", id));
-                            rt.clone()
-                        }
+                        AbsType::Var(id) => get_var(&h, id, false)?,
                         AbsType::RowExtend(id, Some(ty), rest) => {
-                            let cont = form(sy, pol, rest.as_ref(), h.clone());
-                            let row_contr = ty.subcontract(h, pol, sy);
+                            let cont = form(sy, pol, rest.as_ref(), h.clone())?;
+                            let row_contr = ty.subcontract(h, pol, sy)?;
                             mk_app!(
                                 contracts::record_extend(),
                                 mk_term::string(format!("{}", id)),
@@ -277,15 +306,19 @@ impl Types {
                             "types::contract_open(): invalid row type {}",
                             Types(ty.clone())
                         ),
-                    }
+                    };
+
+                    Ok(ctr)
                 }
 
-                mk_app!(contracts::record(), form(sy, pol, ty, h))
+                mk_app!(contracts::record(), form(sy, pol, ty, h)?)
             }
             AbsType::DynRecord(ref ty) => {
-                mk_app!(contracts::dyn_record(), ty.subcontract(h, pol, sy))
+                mk_app!(contracts::dyn_record(), ty.subcontract(h, pol, sy)?)
             }
-        }
+        };
+
+        Ok(ctr)
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type
@@ -380,8 +413,8 @@ impl fmt::Display for Types {
 
                 match tail.0 {
                     AbsType::RowEmpty() => write!(f, "{}", tail),
-                    AbsType::Var(_) => write!(f, " | {}", tail),
-                    AbsType::Dyn() => write!(f, " | Dyn"),
+                    AbsType::Var(_) => write!(f, " ; {}", tail),
+                    AbsType::Dyn() => write!(f, " ; Dyn"),
                     _ => write!(f, ", {}", tail),
                 }
             }
@@ -444,11 +477,11 @@ mod test {
         assert_format_eq("{_: (Str -> Str) -> Str}");
 
         assert_format_eq("{x: (Bool -> Bool) -> Bool, y: Bool}");
-        assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool | r}");
+        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/records.ncl b/stdlib/records.ncl
index 309790b8..dac0ad86 100644
--- a/stdlib/records.ncl
+++ b/stdlib/records.ncl
@@ -15,7 +15,7 @@
       "#m
     = fun f r => %record_map% r f,
 
-    fields | { | Dyn} -> List Str
+    fields | { ; Dyn} -> List Str
     | doc m#"
       Given a record, results in a list of the string representation of all fields in the record.
 
@@ -26,7 +26,7 @@
       "#m
     = fun r => %fields% r,
 
-    values | { | Dyn} -> List
+    values | { ; Dyn} -> List
     | doc m#"
       Given a record, results in a list containing all the values in that record.
 


Test patch:
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index 792d979c..7035b71e 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -374,30 +374,3 @@ fn line_comments() {
         parse_without_pos("{field = foo}")
     );
 }
-
-#[test]
-fn unbound_type_variables() {
-    // should fail, "a" is unbound
-    assert_matches!(
-        parse("1 | a"),
-        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("a")) && unbound_vars.len() == 1)
-    );
-
-    // should fail, "d" is unbound
-    assert_matches!(
-        parse("null: forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: b | Dyn}"),
-        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("d")) && unbound_vars.len() == 1)
-    );
-
-    // should fail, "e" is unbound
-    assert_matches!(
-        parse("null: forall a b c. a -> (b -> List c) -> {foo : List {_ : a}, bar: b | e}"),
-        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("e")) && unbound_vars.len() == 1)
-    );
-
-    // should fail, "a" is unbound
-    assert_matches!(
-        parse("null: a -> (forall a. a -> a)"),
-        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("a")) && unbound_vars.len() == 1)
-    );
-}
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 473c5876..5ae5316c 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -98,13 +98,13 @@ fn records_contracts_poly() {
     // but this is not yet the case.
     // eval_string(&format!("{} {{foo = 2}}", extd)).unwrap_err();
 
-    let remv = "let f | forall a. {foo: Num | a} -> { | a} = fun x => x -$ \"foo\" in f";
+    let remv = "let f | forall a. {foo: Num ; a} -> { ; a} = fun x => x -$ \"foo\" in f";
     assert_raise_blame!(&format!("{} {{}}", remv));
 
-    let bad_cst = "let f | forall a. { | a} -> { | a} = fun x => {a=1} in f";
-    let bad_acc = "let f | forall a. { | a} -> { | a} = fun x => %seq% x.a x in f";
-    let bad_extd = "let f | forall a. { | a} -> {foo: Num | a} = fun x => x -$ \"foo\" in f";
-    let bad_rmv = "let f | forall a. {foo: Num | a} -> { | a} = fun x => x$[\"foo\"=1] in f";
+    let bad_cst = "let f | forall a. { ; a} -> { ; a} = fun x => {a=1} in f";
+    let bad_acc = "let f | forall a. { ; a} -> { ; a} = fun x => %seq% x.a x in f";
+    let bad_extd = "let f | forall a. { ; a} -> {foo: Num ; a} = fun x => x -$ \"foo\" in f";
+    let bad_rmv = "let f | forall a. {foo: Num ; a} -> { ; a} = fun x => x$[\"foo\"=1] in f";
 
     assert_raise_blame!(&format!("{} {{}}", bad_cst));
     // The polymorphic parts is protected by hiding it. Thus, trying to access the protected field
@@ -121,9 +121,9 @@ fn records_contracts_poly() {
     assert_raise_blame!(
         "let f |
             forall a.
-                (forall b. {a: Num, b: Num | b} -> { a: Num | b})
-                -> {a: Num | a}
-                -> { | a}
+                (forall b. {a: Num, b: Num ; b} -> { a: Num ; b})
+                -> {a: Num ; a}
+                -> { ; a}
             = fun f rec => (f rec) -$ \"a\" -$ \"b\" in
         f (fun x => x) {a = 1, b = true, c = 3}"
     );
@@ -172,8 +172,8 @@ fn lists_contracts() {
 
 #[test]
 fn records_contracts_closed() {
-    assert_raise_blame!("{a=1} | #{}");
-    assert_raise_blame!("{a=1, b=2} | #{a | Num}");
+    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)");
 }
 
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 532b819c..60d6833a 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -61,10 +61,10 @@ let Assert = fun l x => x || %blame% l in
     %deep_seq% x x == {a = 1, s = { foo = true}},
 
   // polymorphism
-  (let id | forall a. { | a} -> { | a} = fun x => x in
-    let extend | forall a. { | a} -> {foo: Num | a} = fun x =>
+  (let id | forall a. { ; a} -> { ; a} = fun x => x in
+    let extend | forall a. { ; a} -> {foo: Num ; a} = fun x =>
       x & {foo = 1} in
-    let remove | forall a. {foo: Num | a} -> { | a} = fun x =>
+    let remove | forall a. {foo: Num ; a} -> { ; a} = fun x =>
       x -$ "foo" in
 
     (id {} == {} | #Assert) &&
@@ -75,7 +75,7 @@ let Assert = fun l x => x || %blame% l in
     (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 =
+    (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"
@@ -83,10 +83,10 @@ let Assert = fun l x => x || %blame% l in
   ),
 
   // records_dynamic_tail
-  ({a = 1, b = "b"} | {a: Num, b: Str | Dyn}) == {a = 1, b = "b"},
-  ({a = 1, b = "b", c = false} | {a: Num, b: Str | Dyn})
+  ({a = 1, b = "b"} | {a: Num, b: Str ; Dyn}) == {a = 1, b = "b"},
+  ({a = 1, b = "b", c = false} | {a: Num, b: Str ; Dyn})
   == {a = 1, b = "b", c = false},
-  ((fun r => r.b) | {a: Num | Dyn} -> Dyn) {a = 1, b = 2} == 2,
+  ((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},
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 85a47dd0..8d476f8b 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -82,7 +82,7 @@ let typecheck = [
   let r : {bla : Bool, blo : Num} = {blo = 1, bla = true} in
     ((if r.bla then r.blo else 2) : Num),
 
-  let f : forall a r. {bla : Bool, blo : a, ble : a | r} -> a =
+  let f : forall a r. {bla : Bool, blo : a, ble : a ; r} -> a =
       fun r => if r.bla then r.blo else r.ble in
     (if (f {bla = true, blo = false, ble = true, blip = 1, }) then
       (f {bla = true, blo = 1, ble = 2, blip = `blip, })
@@ -130,12 +130,12 @@ let typecheck = [
     : {f : Num -> Num},
 
   // polymorphic_row_constraints
-  let extend | forall c. { | c} -> {a: Str | c} = 0 in
-    let remove | forall c. {a: Str | c} -> { | c} = 0 in
+  let extend | forall c. { ; c} -> {a: Str ; c} = 0 in
+    let remove | forall c. {a: Str ; c} -> { ; c} = 0 in
     (let good = remove (extend {}) in 0) : Num,
 
-  let r | {a: Num | Dyn} = {a = 1, b = 2} in (r.a : Num),
-  ({a = 1, b = 2} | {a: Num | Dyn}) : {a: Num | Dyn},
+  let r | {a: Num ; Dyn} = {a = 1, b = 2} in (r.a : Num),
+  ({a = 1, b = 2} | {a: Num ; Dyn}) : {a: Num ; Dyn},
 
   //Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
   //unifying a variable with itself doesn't introduce a loop. The failure of this test results
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 0468c9e8..2e82d86d 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -114,12 +114,12 @@ fn static_record_simple() {
     assert_typecheck_fails!("{blo = 1}.blo : Bool");
 
     assert_typecheck_fails!(
-        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
+        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
             fun r => if r.bla then r.blo else r.ble in
          (f {bla = true, blo = 1, ble = true, blip = `blip} : Num)"
     );
     assert_typecheck_fails!(
-        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
+        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
             fun r => if r.bla then (r.blo + 1) else r.ble in
          (f {bla = true, blo = 1, ble = 2, blip = `blip} : Num)"
     );
@@ -185,13 +185,13 @@ fn polymorphic_row_constraints() {
     }
 
     let mut res = type_check_expr(
-        "let extend | forall c. { | c} -> {a: Str | c} = null in
+        "let extend | forall c. { ; c} -> {a: Str ; c} = null in
            (let bad = extend {a = 1} in 0) : Num",
     );
     assert_row_conflict(res);
 
     res = type_check_expr(
-        "let remove | forall c. {a: Str | c} -> { | c} = nul in
+        "let remove | forall c. {a: Str ; c} -> { ; c} = nul in
            (let bad = remove (remove {a = \"a\"}) in 0) : Num",
     );
     assert_row_conflict(res);
@@ -201,10 +201,10 @@ fn polymorphic_row_constraints() {
 fn dynamic_row_tail() {
     // Currently, typechecking is conservative wrt the dynamic row type, meaning it can't
     // convert to a less precise type with a dynamic tail.
-    assert_typecheck_fails!("{a = 1, b = 2} : {a: Num | Dyn}");
-    assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");
-    assert_typecheck_fails!("({a = 1} | {a: Num | Dyn}) : {a: Num}");
-    assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");
+    assert_typecheck_fails!("{a = 1, b = 2} : {a: Num ; Dyn}");
+    assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
+    assert_typecheck_fails!("({a = 1} | {a: Num ; Dyn}) : {a: Num}");
+    assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
 }
 
 #[test]
diff --git a/tests/unbound_type_variables.rs b/tests/unbound_type_variables.rs
new file mode 100644
index 00000000..ffb871b0
--- /dev/null
+++ b/tests/unbound_type_variables.rs
@@ -0,0 +1,35 @@
+use assert_matches::assert_matches;
+use nickel::{
+    error::{Error, ParseError, ParseErrors},
+    identifier::Ident,
+};
+
+use utilities::eval;
+
+macro_rules! assert_unbound {
+    ( $term:expr, $var:expr ) => {
+        let res = eval($term);
+        assert_matches!(res, Err(Error::ParseErrors(_)));
+
+        match res {
+            Err(Error::ParseErrors(ParseErrors {errors})) => {
+                assert_matches!(errors.as_slice(), [ParseError::UnboundTypeVariables(vars, _)] if vars.contains(&Ident::from($var)) && vars.len() == 1)
+            }
+            _ => unreachable!(),
+        };
+    }
+}
+
+#[test]
+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}",
+        "d"
+    );
+    assert_unbound!(
+        "null | forall a b c. a -> (b -> List c) -> {foo : List {_ : a}, bar: b; e}",
+        "e"
+    );
+    assert_unbound!("null | a -> (forall a. a -> a)", "a");
+}