diff --git a/core/src/bytecode/ast/compat.rs b/core/src/bytecode/ast/compat.rs
index 00d152b7d6..75158575eb 100644
--- a/core/src/bytecode/ast/compat.rs
+++ b/core/src/bytecode/ast/compat.rs
@@ -1042,6 +1042,7 @@ impl<'ast> FromAst<RecordRow<'ast>> for mline_type::RecordRow {
     fn from_ast(rrow: &RecordRow<'ast>) -> Self {
         mline_type::RecordRowF {
             id: rrow.id,
+            opt: false,
             typ: Box::new(rrow.typ.to_mainline()),
         }
     }
diff --git a/core/src/bytecode/ast/mod.rs b/core/src/bytecode/ast/mod.rs
index 64e5b40520..35a0497c60 100644
--- a/core/src/bytecode/ast/mod.rs
+++ b/core/src/bytecode/ast/mod.rs
@@ -271,7 +271,7 @@ pub struct Annotation<'ast> {
     pub contracts: &'ast [Type<'ast>],
 }
 
-impl Annotation<'_> {
+impl<'ast> Annotation<'ast> {
     /// Returns a string representation of the contracts (without the static type annotation) as a
     /// comma-separated list.
     pub fn contracts_to_string(&self) -> Option<String> {
@@ -290,6 +290,18 @@ impl Annotation<'_> {
     pub fn is_empty(&self) -> bool {
         self.typ.is_none() && self.contracts.is_empty()
     }
+
+    /// If this annotation represents a single type (and not a user-defined contract), return it.
+    ///
+    /// This returns `Some(Number)` for either `| Number` or `: Number`, although it currently
+    /// returns `None` for `: Number | Number`. Should it?
+    pub fn simple_type(&self) -> Option<&Type<'ast>> {
+        match (&self.typ, self.contracts) {
+            (None, [ctr]) if !matches!(&ctr.typ, TypeF::Contract(_)) => Some(ctr),
+            (Some(ty), []) => Some(ty),
+            _ => None,
+        }
+    }
 }
 
 /// Specifies where something should be imported from.
diff --git a/core/src/bytecode/typecheck/eq.rs b/core/src/bytecode/typecheck/eq.rs
index 5f289ea8e0..c2d9527837 100644
--- a/core/src/bytecode/typecheck/eq.rs
+++ b/core/src/bytecode/typecheck/eq.rs
@@ -373,6 +373,35 @@ where
     }
 }
 
+impl<'ast, S, T> TypeEqBounded<'ast> for (S, T)
+where
+    S: TypeEqBounded<'ast>,
+    T: TypeEqBounded<'ast>,
+{
+    fn type_eq_bounded(
+        &self,
+        other: &Self,
+        state: &mut State,
+        env1: &TermEnv<'ast>,
+        env2: &TermEnv<'ast>,
+    ) -> bool {
+        self.0.type_eq_bounded(&other.0, state, env1, env2)
+            && self.1.type_eq_bounded(&other.1, state, env1, env2)
+    }
+}
+
+impl<'ast> TypeEqBounded<'ast> for bool {
+    fn type_eq_bounded(
+        &self,
+        other: &Self,
+        _state: &mut State,
+        _env1: &TermEnv<'ast>,
+        _env2: &TermEnv<'ast>,
+    ) -> bool {
+        *self == *other
+    }
+}
+
 impl<'ast> TypeEqBounded<'ast> for UnifEnumRows<'ast> {
     fn type_eq_bounded(
         &self,
@@ -416,7 +445,11 @@ impl<'ast> TypeEqBounded<'ast> for UnifRecordRows<'ast> {
         let map_self: Option<IndexMap<LocIdent, _>> = self
             .iter()
             .map(|item| match item {
-                RecordRowsElt::Row(RecordRowF { id, typ: types }) => Some((id, types)),
+                RecordRowsElt::Row(RecordRowF {
+                    id,
+                    opt,
+                    typ: types,
+                }) => Some((id, (opt, types))),
                 _ => None,
             })
             .collect();
@@ -424,7 +457,11 @@ impl<'ast> TypeEqBounded<'ast> for UnifRecordRows<'ast> {
         let map_other: Option<IndexMap<LocIdent, _>> = other
             .iter()
             .map(|item| match item {
-                RecordRowsElt::Row(RecordRowF { id, typ: types }) => Some((id, types)),
+                RecordRowsElt::Row(RecordRowF {
+                    id,
+                    opt,
+                    typ: types,
+                }) => Some((id, (opt, types))),
                 _ => None,
             })
             .collect();
diff --git a/core/src/bytecode/typecheck/mk_uniftype.rs b/core/src/bytecode/typecheck/mk_uniftype.rs
index a315f4cb33..1323cd21cb 100644
--- a/core/src/bytecode/typecheck/mk_uniftype.rs
+++ b/core/src/bytecode/typecheck/mk_uniftype.rs
@@ -77,6 +77,7 @@ macro_rules! mk_buty_record_row {
             $crate::typ::RecordRowsF::Extend {
                 row: $crate::typ::RecordRowF {
                     id: $crate::identifier::LocIdent::from($id),
+                    opt: false,
                     typ: Box::new($ty.into()),
                 },
                 tail: Box::new($crate::mk_buty_record_row!($(($ids, $tys)),* $(; $tail)?)),
diff --git a/core/src/bytecode/typecheck/mod.rs b/core/src/bytecode/typecheck/mod.rs
index 4bda62f8e1..411d697e10 100644
--- a/core/src/bytecode/typecheck/mod.rs
+++ b/core/src/bytecode/typecheck/mod.rs
@@ -335,7 +335,7 @@ impl VarLevelUpperBound for UnifRecordRowsUnr<'_> {
             // A var that hasn't be instantiated yet isn't a unification variable
             RecordRowsF::Empty | RecordRowsF::TailVar(_) | RecordRowsF::TailDyn => VarLevel::NO_VAR,
             RecordRowsF::Extend {
-                row: RecordRowF { id: _, typ },
+                row: RecordRowF { id: _, opt: _, typ },
                 tail,
             } => max(tail.var_level_upper_bound(), typ.var_level_upper_bound()),
         }
@@ -1155,6 +1155,7 @@ impl<'a, 'ast> Iterator for RecordRowsIterator<'a, UnifType<'ast>, UnifRecordRow
                     self.rrows = Some(tail);
                     Some(RecordRowsElt::Row(RecordRowF {
                         id: row.id,
+                        opt: row.opt,
                         typ: row.typ.as_ref(),
                     }))
                 }
@@ -3072,6 +3073,7 @@ pub fn infer_record_type<'ast>(
                         RecordRowsF::Extend {
                             row: UnifRecordRow {
                                 id,
+                                opt: false,
                                 typ: Box::new(uty),
                             },
                             tail: Box::new(rtype.into()),
diff --git a/core/src/bytecode/typecheck/pattern.rs b/core/src/bytecode/typecheck/pattern.rs
index 4ac10afc49..7cf57f63e2 100644
--- a/core/src/bytecode/typecheck/pattern.rs
+++ b/core/src/bytecode/typecheck/pattern.rs
@@ -492,6 +492,7 @@ impl<'ast> PatternTypes<'ast> for FieldPattern<'ast> {
 
         Ok(UnifRecordRow {
             id: self.matched_id,
+            opt: false,
             typ: Box::new(ty_row),
         })
     }
diff --git a/core/src/bytecode/typecheck/reporting.rs b/core/src/bytecode/typecheck/reporting.rs
index 4d31497802..b766744c94 100644
--- a/core/src/bytecode/typecheck/reporting.rs
+++ b/core/src/bytecode/typecheck/reporting.rs
@@ -263,6 +263,7 @@ impl<'ast> ToType<'ast> for UnifRecordRow<'ast> {
     ) -> Self::Target {
         RecordRow {
             id: self.id,
+            opt: self.opt,
             typ: alloc.alloc(self.typ.to_type(alloc, reg, table)),
         }
     }
diff --git a/core/src/bytecode/typecheck/unif.rs b/core/src/bytecode/typecheck/unif.rs
index fbdb57b09e..0258accac6 100644
--- a/core/src/bytecode/typecheck/unif.rs
+++ b/core/src/bytecode/typecheck/unif.rs
@@ -1734,6 +1734,7 @@ impl<'ast> RemoveRow<'ast> for UnifRecordRows<'ast> {
 
                 let row_to_insert = UnifRecordRow {
                     id: *target,
+                    opt: false,
                     typ: Box::new(target_content.clone()),
                 };
 
diff --git a/core/src/eval/contract_eq.rs b/core/src/eval/contract_eq.rs
index ec03319490..4e3a44c9f9 100644
--- a/core/src/eval/contract_eq.rs
+++ b/core/src/eval/contract_eq.rs
@@ -348,11 +348,11 @@ where
 ///
 /// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
 /// returned. `None` is returned as well if a type encountered is not row, or if it is a enum row.
-fn rrows_as_map(erows: &RecordRows) -> Option<IndexMap<LocIdent, &Type>> {
+fn rrows_as_map(erows: &RecordRows) -> Option<IndexMap<LocIdent, (bool, &Type)>> {
     let map: Option<IndexMap<LocIdent, _>> = erows
         .iter()
         .map(|item| match item {
-            RecordRowsIteratorItem::Row(RecordRowF { id, typ }) => Some((id, typ)),
+            RecordRowsIteratorItem::Row(RecordRowF { id, opt, typ }) => Some((id, (opt, typ))),
             _ => None,
         })
         .collect();
@@ -493,12 +493,12 @@ fn type_eq_bounded(
         (TypeF::Record(uty1), TypeF::Record(uty2)) => {
             fn type_eq_bounded_wrapper(
                 state: &mut State,
-                uty1: &&Type,
+                (opt1, uty1): &(bool, &Type),
                 env1: &Environment,
-                uty2: &&Type,
+                (opt2, uty2): &(bool, &Type),
                 env2: &Environment,
             ) -> bool {
-                type_eq_bounded(state, uty1, env1, uty2, env2)
+                opt1 == opt2 && type_eq_bounded(state, uty1, env1, uty2, env2)
             }
 
             let map1 = rrows_as_map(uty1);
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 4d513af953..82d98f67bb 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -3026,11 +3026,18 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 };
 
                 let split::SplitResult {
-                    left,
+                    mut left,
                     center,
                     right,
                 } = split::split(record1.fields, record2.fields);
 
+                // This doesn't seem very... principled. But at least it's sort of reasonable
+                // current usages of %record/split_pair%? $record_type wants this behavior
+                // because the contract is on the left and we allow optional fields to be
+                // ignored. The other user is std.contract.Equal, and ignoring of optionals
+                // means that `{ } | std.contract.Equal { foo | optional = 1 }` will succeed.
+                left.retain(|_name, value| !value.metadata.opt);
+
                 let left_only = Term::Record(RecordData {
                     fields: left,
                     sealed_tail: record1.sealed_tail,
diff --git a/core/src/label.rs b/core/src/label.rs
index 2956e89d8b..4d47d965f1 100644
--- a/core/src/label.rs
+++ b/core/src/label.rs
@@ -177,7 +177,11 @@ pub mod ty_path {
             (TypeF::Record(rows), next @ Some(Elem::Field(ident))) => {
                 for row_item in rows.iter() {
                     match row_item {
-                        RecordRowsIteratorItem::Row(RecordRowF { id, typ: ty }) if id == *ident => {
+                        RecordRowsIteratorItem::Row(RecordRowF {
+                            id,
+                            typ: ty,
+                            opt: _,
+                        }) if id == *ident => {
                             let path_span = span(path_it, ty)?;
 
                             return Some(PathSpan {
diff --git a/core/src/parser/uniterm.rs b/core/src/parser/uniterm.rs
index ed3fffffb8..9c80a8d47d 100644
--- a/core/src/parser/uniterm.rs
+++ b/core/src/parser/uniterm.rs
@@ -198,7 +198,7 @@ where
 }
 
 /// A record in the `UniTerm` syntax.
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 pub struct UniRecord<'ast> {
     pub fields: Vec<FieldDef<'ast>>,
     pub tail: Option<(RecordRows<'ast>, TermPos)>,
@@ -334,17 +334,13 @@ impl<'ast> UniRecord<'ast> {
                     metadata:
                         FieldMetadata {
                             doc: None,
-                            annotation:
-                                Annotation {
-                                    typ: Some(_),
-                                    contracts,
-                                },
-                            opt: false,
+                            annotation,
+                            opt: _,
                             not_exported: false,
                             priority: MergePriority::Neutral,
                         },
                     ..
-                } if contracts.is_empty())
+                } if annotation.simple_type().is_some())
         })
     }
 
@@ -370,23 +366,26 @@ impl<'ast> UniRecord<'ast> {
                     metadata:
                         FieldMetadata {
                             doc: None,
-                            annotation:
-                                Annotation {
-                                    typ: Some(typ),
-                                    contracts: [],
-                                },
-                            opt: false,
+                            annotation,
+                            opt,
                             not_exported: false,
                             priority: MergePriority::Neutral,
                         },
                     pos: _,
-                } => Ok(RecordRows(RecordRowsF::Extend {
-                    row: RecordRow {
-                        id,
-                        typ: alloc.type_data(typ.typ, typ.pos),
-                    },
-                    tail: alloc.record_rows(tail.0),
-                })),
+                } => match annotation.simple_type() {
+                    Some(typ) => Ok(RecordRows(RecordRowsF::Extend {
+                        row: RecordRow {
+                            id,
+                            opt,
+                            typ: alloc.type_data(typ.typ.clone(), typ.pos),
+                        },
+                        tail: alloc.record_rows(tail.0),
+                    })),
+                    None => Err(InvalidRecordTypeError::InvalidField(
+                        // Position of identifiers must always be set at this stage (parsing)
+                        id.pos.fuse(field_def.pos).unwrap(),
+                    )),
+                },
                 _ => {
                     Err(InvalidRecordTypeError::InvalidField(
                         // Position of identifiers must always be set at this stage (parsing)
@@ -943,6 +942,7 @@ impl<'ast> FixTypeVars<'ast> for RecordRow<'ast> {
             .fix_type_vars_env(alloc, bound_vars, span)?
             .map(|typ| RecordRow {
                 id: self.id,
+                opt: self.opt,
                 typ: alloc.alloc(typ),
             }))
     }
diff --git a/core/src/pretty.rs b/core/src/pretty.rs
index d0d78bb444..8d13e89507 100644
--- a/core/src/pretty.rs
+++ b/core/src/pretty.rs
@@ -1218,7 +1218,8 @@ where
         docs![
             allocator,
             ident_quoted(&self.id),
-            " : ",
+            // FIXME: we don't actually have a surface syntax for optional fields in types
+            if self.opt { " ?: " } else { " : " },
             allocator.type_part(self.typ.deref()),
         ]
     }
diff --git a/core/src/typ.rs b/core/src/typ.rs
index 5b58f9ef10..7ff9448e61 100644
--- a/core/src/typ.rs
+++ b/core/src/typ.rs
@@ -51,10 +51,13 @@ use crate::{
     position::TermPos,
     pretty::PrettyPrintCap,
     stdlib::internals,
-    term::pattern::compile::Compile,
     term::{
-        array::Array, make as mk_term, record::RecordData, string::NickelString, IndexMap,
-        MatchBranch, MatchData, RichTerm, Term,
+        array::Array,
+        make as mk_term,
+        pattern::compile::Compile,
+        record::{Field, RecordData},
+        string::NickelString,
+        IndexMap, MatchBranch, MatchData, RichTerm, Term,
     },
     traverse::*,
 };
@@ -72,6 +75,7 @@ use std::{collections::HashSet, convert::Infallible};
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct RecordRowF<Ty> {
     pub id: LocIdent,
+    pub opt: bool,
     pub typ: Ty,
 }
 
@@ -359,11 +363,12 @@ impl<Ty, RRows> RecordRowsF<Ty, RRows> {
         match self {
             RecordRowsF::Empty => Ok(RecordRowsF::Empty),
             RecordRowsF::Extend {
-                row: RecordRowF { id, typ },
+                row: RecordRowF { id, opt, typ },
                 tail,
             } => Ok(RecordRowsF::Extend {
                 row: RecordRowF {
                     id,
+                    opt,
                     typ: f_ty(typ, state)?,
                 },
                 tail: f_rrows(tail, state)?,
@@ -773,6 +778,7 @@ impl<'a> Iterator for RecordRowsIterator<'a, Type, RecordRows> {
                 self.rrows = Some(tail);
                 Some(RecordRowsIteratorItem::Row(RecordRowF {
                     id: row.id,
+                    opt: row.opt,
                     typ: row.typ.as_ref(),
                 }))
             }
@@ -1228,6 +1234,7 @@ impl RecordRows {
 
         find_path_ref(self, path).map(|row| RecordRow {
             id: row.id,
+            opt: row.opt,
             typ: Box::new(row.typ.clone()),
         })
     }
@@ -1385,6 +1392,7 @@ impl RecordRows {
 
                     let row = RecordRow {
                         id: row.id,
+                        opt: row.opt,
                         typ: Box::new(typ_simplified),
                     };
 
@@ -1485,14 +1493,16 @@ impl Subcontract for RecordRows {
         // We begin by building a record whose arguments are contracts
         // derived from the types of the statically known fields.
         let mut rrows = self;
-        let mut fcs = IndexMap::new();
+        let mut fields = IndexMap::new();
 
         while let RecordRowsF::Extend {
-            row: RecordRowF { id, typ: ty },
+            row: RecordRowF { id, opt, typ: ty },
             tail,
         } = &rrows.0
         {
-            fcs.insert(*id, ty.subcontract(vars.clone(), pol, sy)?);
+            let mut field = Field::from(ty.subcontract(vars.clone(), pol, sy)?);
+            field.metadata.opt = *opt;
+            fields.insert(*id, field);
             rrows = tail
         }
 
@@ -1507,7 +1517,10 @@ impl Subcontract for RecordRows {
             RecordRowsF::Extend { .. } => unreachable!(),
         };
 
-        let rec = RichTerm::from(Term::Record(RecordData::with_field_values(fcs)));
+        let rec = RichTerm::from(Term::Record(RecordData {
+            fields,
+            ..Default::default()
+        }));
 
         Ok(mk_app!(
             internals::record_type(),
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 42092946d1..3296a81e47 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -513,13 +513,15 @@ where
 /// returned. `None` is returned as well if a type encountered is not row, or if it is a enum row.
 fn rrows_as_map<E: TermEnvironment>(
     erows: &GenericUnifRecordRows<E>,
-) -> Option<IndexMap<LocIdent, &GenericUnifType<E>>> {
+) -> Option<IndexMap<LocIdent, (bool, &GenericUnifType<E>)>> {
     let map: Option<IndexMap<LocIdent, _>> = erows
         .iter()
         .map(|item| match item {
-            GenericUnifRecordRowsIteratorItem::Row(RecordRowF { id, typ: types }) => {
-                Some((id, types))
-            }
+            GenericUnifRecordRowsIteratorItem::Row(RecordRowF {
+                id,
+                typ: types,
+                opt,
+            }) => Some((id, (opt, types))),
             _ => None,
         })
         .collect();
@@ -685,12 +687,12 @@ fn type_eq_bounded<E: TermEnvironment>(
                 (TypeF::Record(uty1), TypeF::Record(uty2)) => {
                     fn type_eq_bounded_wrapper<E: TermEnvironment>(
                         state: &mut State,
-                        uty1: &&GenericUnifType<E>,
+                        (opt1, uty1): &(bool, &GenericUnifType<E>),
                         env1: &E,
-                        uty2: &&GenericUnifType<E>,
+                        (opt2, uty2): &(bool, &GenericUnifType<E>),
                         env2: &E,
                     ) -> bool {
-                        type_eq_bounded(state, *uty1, env1, *uty2, env2)
+                        opt1 == opt2 && type_eq_bounded(state, *uty1, env1, *uty2, env2)
                     }
 
                     let map1 = rrows_as_map(uty1);
diff --git a/core/src/typecheck/mk_uniftype.rs b/core/src/typecheck/mk_uniftype.rs
index f031f05e16..87692d78b1 100644
--- a/core/src/typecheck/mk_uniftype.rs
+++ b/core/src/typecheck/mk_uniftype.rs
@@ -77,6 +77,7 @@ macro_rules! mk_uty_record_row {
             $crate::typ::RecordRowsF::Extend {
                 row: $crate::typ::RecordRowF {
                     id: $crate::identifier::LocIdent::from($id),
+                    opt: false,
                     typ: Box::new($ty.into()),
                 },
                 tail: Box::new($crate::mk_uty_record_row!($(($ids, $tys)),* $(; $tail)?)),
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index df9bd80955..5401ec4146 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -297,7 +297,7 @@ impl<E: TermEnvironment> VarLevelUpperBound for GenericUnifRecordRowsUnrolling<E
             // A var that hasn't be instantiated yet isn't a unification variable
             RecordRowsF::Empty | RecordRowsF::TailVar(_) | RecordRowsF::TailDyn => VarLevel::NO_VAR,
             RecordRowsF::Extend {
-                row: RecordRowF { id: _, typ },
+                row: RecordRowF { id: _, opt: _, typ },
                 tail,
             } => max(tail.var_level_upper_bound(), typ.var_level_upper_bound()),
         }
@@ -1125,6 +1125,7 @@ impl<'a, E: TermEnvironment> Iterator
                     self.rrows = Some(tail);
                     Some(GenericUnifRecordRowsIteratorItem::Row(RecordRowF {
                         id: row.id,
+                        opt: row.opt,
                         typ: row.typ.as_ref(),
                     }))
                 }
@@ -2942,6 +2943,7 @@ pub fn infer_record_type(
                     RecordRowsF::Extend {
                         row: UnifRecordRow {
                             id: *id,
+                            opt: false,
                             typ: Box::new(uty),
                         },
                         tail: Box::new(r.into()),
diff --git a/core/src/typecheck/pattern.rs b/core/src/typecheck/pattern.rs
index 5dbfd54439..30458f8727 100644
--- a/core/src/typecheck/pattern.rs
+++ b/core/src/typecheck/pattern.rs
@@ -484,6 +484,7 @@ impl PatternTypes for FieldPattern {
 
         Ok(UnifRecordRow {
             id: self.matched_id,
+            opt: false,
             typ: Box::new(ty_row),
         })
     }
diff --git a/core/src/typecheck/reporting.rs b/core/src/typecheck/reporting.rs
index e95f7599c5..574c98f57e 100644
--- a/core/src/typecheck/reporting.rs
+++ b/core/src/typecheck/reporting.rs
@@ -232,6 +232,7 @@ impl ToType for UnifRecordRow {
     fn to_type(self, reg: &mut NameReg, table: &UnifTable) -> Self::Target {
         RecordRow {
             id: self.id,
+            opt: self.opt,
             typ: Box::new(self.typ.to_type(reg, table)),
         }
     }
diff --git a/core/src/typecheck/subtyping.rs b/core/src/typecheck/subtyping.rs
index bbcaa86669..1aceb2cd18 100644
--- a/core/src/typecheck/subtyping.rs
+++ b/core/src/typecheck/subtyping.rs
@@ -121,7 +121,7 @@ impl SubsumedBy for UnifType {
                     ..
                 },
             ) => a.subsumed_by(*b, state, ctxt),
-            // {a1 : T1,...,an : Tn} <: {b1 : U1,...,bn : Un} if for every n `Tn <: Un`
+            // {a1 : T1,...,an : Tn} <: {b1 : U1,...,bn : Un} if for every n `Tn <: Un` or `an` is optional and `bn` is missing
             (
                 UnifType::Concrete {
                     typ: TypeF::Record(rrows1),
@@ -145,7 +145,7 @@ impl SubsumedBy for UnifRecordRows {
     type Error = RowUnifError;
 
     fn subsumed_by(self, t2: Self, state: &mut State, ctxt: Context) -> Result<(), Self::Error> {
-        // This code is almost taken verbatim fro `unify`, but where some recursive calls are
+        // This code is almost taken verbatim from `unify`, but where some recursive calls are
         // changed to be `subsumed_by` instead of `unify`. We can surely factorize both into a
         // generic function, but this is left for future work.
         let inferred = self.into_root(state.table);
@@ -189,34 +189,13 @@ impl SubsumedBy for UnifRecordRows {
                 | (RecordRowsF::TailDyn, RecordRowsF::TailDyn) => Ok(()),
                 (RecordRowsF::Empty, RecordRowsF::TailDyn)
                 | (RecordRowsF::TailDyn, RecordRowsF::Empty) => Err(RowUnifError::ExtraDynTail),
-                (
-                    RecordRowsF::Empty,
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                )
-                | (
-                    RecordRowsF::TailDyn,
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                ) => Err(RowUnifError::MissingRow(id)),
-                (
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                    RecordRowsF::TailDyn,
-                )
-                | (
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                    RecordRowsF::Empty,
-                ) => Err(RowUnifError::ExtraRow(id)),
+                (RecordRowsF::Empty | RecordRowsF::TailDyn, RecordRowsF::Extend { row, .. }) => {
+                    // TODO: shouldn't we need to handle optional rows here too?
+                    Err(RowUnifError::MissingRow(row.id))
+                }
+                (RecordRowsF::Extend { row, .. }, RecordRowsF::TailDyn | RecordRowsF::Empty) => {
+                    Err(RowUnifError::ExtraRow(row.id))
+                }
             },
             (UnifRecordRows::UnifVar { id, .. }, urrows)
             | (urrows, UnifRecordRows::UnifVar { id, .. }) => {
diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs
index 2f2b2ad41c..95466cbec3 100644
--- a/core/src/typecheck/unif.rs
+++ b/core/src/typecheck/unif.rs
@@ -1490,34 +1490,23 @@ impl Unify for UnifRecordRows {
                 | (RecordRowsF::TailDyn, RecordRowsF::TailDyn) => Ok(()),
                 (RecordRowsF::Empty, RecordRowsF::TailDyn) => Err(RowUnifError::ExtraDynTail),
                 (RecordRowsF::TailDyn, RecordRowsF::Empty) => Err(RowUnifError::MissingDynTail),
+                (RecordRowsF::Empty | RecordRowsF::TailDyn, RecordRowsF::Extend { row, .. }) => {
+                    Err(RowUnifError::ExtraRow(row.id))
+                }
                 (
-                    RecordRowsF::Empty,
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                )
-                | (
-                    RecordRowsF::TailDyn,
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                ) => Err(RowUnifError::ExtraRow(id)),
-                (
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                    RecordRowsF::TailDyn,
-                )
-                | (
-                    RecordRowsF::Extend {
-                        row: UnifRecordRow { id, .. },
-                        ..
-                    },
-                    RecordRowsF::Empty,
-                ) => Err(RowUnifError::MissingRow(id)),
+                    RecordRowsF::Extend { row, tail },
+                    rrows2 @ (RecordRowsF::Empty | RecordRowsF::TailDyn),
+                ) => {
+                    if row.opt {
+                        let urrows2 = UnifRecordRows::Concrete {
+                            rrows: rrows2,
+                            var_levels_data: var_levels2,
+                        };
+                        tail.unify(urrows2, state, ctxt)
+                    } else {
+                        Err(RowUnifError::MissingRow(row.id))
+                    }
+                }
                 (RecordRowsF::Extend { row, tail }, rrows2 @ RecordRowsF::Extend { .. }) => {
                     let urrows2 = UnifRecordRows::Concrete {
                         rrows: rrows2,
@@ -1708,6 +1697,7 @@ impl RemoveRow for UnifRecordRows {
 
                 let row_to_insert = UnifRecordRow {
                     id: *target,
+                    opt: false,
                     typ: Box::new(target_content.clone()),
                 };