Repository: tweag/nickel
Pull request #1144 (2023-02-24 16:09:53)

[Refactor] Only represent valid match pattern states
Previously we stored match patterns as
`(Option<Ident>, Option<Pattern>)`, but this
allowed for the invalid state `(None, None)`.

This commit replaces this with an enum which
only allows the three valid states to be
represented, which removes some `panic`s.

matthew-healy: @yannham Apologies, meant to move it out of review once CI passed but I forgot before the weekend. 

Patch:
diff --git a/src/destructuring.rs b/src/destructuring.rs
index 1f46a773..b5dc8735 100644
--- a/src/destructuring.rs
+++ b/src/destructuring.rs
@@ -12,6 +12,19 @@ use crate::{
     types::{TypeF, Types},
 };
 
+#[derive(Debug, PartialEq, Clone)]
+pub enum FieldPattern {
+    /// An assignment match like `{ ..., a = b, ... }`
+    Ident(Ident),
+    /// A nested record pattern like `{ ..., a = { b, c }, ... }`
+    RecordPattern(RecordPattern),
+    /// An aliased nested record pattern like `{ ..., a = b @ { c, d }, ... }`
+    AliasedRecordPattern {
+        alias: Ident,
+        pattern: RecordPattern,
+    },
+}
+
 /// A match field in a `Destruct` pattern. Every field can be annotated with a type, with contracts
 /// or with a default value.
 #[derive(Debug, PartialEq, Clone)]
@@ -19,7 +32,7 @@ pub enum Match {
     /// `{..., a=b, ...}` will bind the field `a` of the record to variable `b`. Here, `a` is the
     /// first field of this variant and `b` the optional one. The last field can actualy be a
     /// nested destruct pattern.
-    Assign(Ident, Field, (Option<Ident>, Option<RecordPattern>)),
+    Assign(Ident, Field, FieldPattern),
     /// Simple binding. the `Ident` is bind to a variable with the same name.
     Simple(Ident, Field),
 }
@@ -91,21 +104,28 @@ impl Match {
     /// contract representing a record pattern destructuring.
     pub fn as_binding(self) -> (Ident, Field) {
         match self {
-            Match::Assign(id, field, (_, None)) | Match::Simple(id, field) => (id, field),
+            Match::Assign(id, field, FieldPattern::Ident(_)) | Match::Simple(id, field) => {
+                (id, field)
+            }
 
             // In this case we fuse spans of the `Ident` (LHS) with the destruct (RHS)
             // because we can have two cases:
             //
             // - extra field on the destructuring `d`
             // - missing field on the `id`
-            Match::Assign(id, mut field, (_, Some(destruct))) => {
-                let mut label = destruct.label();
+            Match::Assign(
+                id,
+                mut field,
+                FieldPattern::RecordPattern(pattern)
+                | FieldPattern::AliasedRecordPattern { pattern, .. },
+            ) => {
+                let mut label = pattern.label();
                 label.span = RawSpan::fuse(id.pos.unwrap(), label.span).unwrap();
                 field
                     .metadata
                     .annotation
                     .contracts
-                    .push(destruct.into_contract_with_lbl(label));
+                    .push(pattern.into_contract_with_lbl(label));
 
                 (id, field)
             }
@@ -116,42 +136,65 @@ impl Match {
     /// It also tells the "path" to the bound variable; this is just the
     /// record field names traversed to get to a pattern.
     pub fn as_flattened_bindings(self) -> Vec<(Vec<Ident>, Option<Ident>, Field)> {
+        fn get_label(id: &Ident, pattern: &RecordPattern) -> Label {
+            let mut label = pattern.label();
+            label.span = RawSpan::fuse(id.pos.unwrap(), label.span).unwrap();
+            label
+        }
+
+        fn flatten_matches(
+            id: &Ident,
+            matches: &[Match],
+        ) -> Vec<(Vec<Ident>, Option<Ident>, Field)> {
+            matches
+                .iter()
+                .flat_map(|m| m.clone().as_flattened_bindings())
+                .map(|(mut path, bind, field)| {
+                    path.push(*id);
+                    (path, bind, field)
+                })
+                .collect()
+        }
+
         match self {
             Match::Simple(id, field) => vec![(vec![id], None, field)],
-            Match::Assign(id, field, (bind_id, None)) => {
-                vec![(vec![id], bind_id, field)]
+            Match::Assign(id, field, FieldPattern::Ident(bind_id)) => {
+                vec![(vec![id], Some(bind_id), field)]
             }
             Match::Assign(
                 id,
                 mut field,
-                (bind_id, Some(ref destruct @ RecordPattern { ref matches, .. })),
+                FieldPattern::RecordPattern(ref pattern @ RecordPattern { ref matches, .. }),
             ) => {
-                let destruct = destruct.clone();
-                let mut label = destruct.label();
-                label.span = RawSpan::fuse(id.pos.unwrap(), label.span).unwrap();
+                let label = get_label(&id, pattern);
+                let pattern = pattern.clone();
                 field
                     .metadata
                     .annotation
                     .contracts
-                    .push(destruct.into_contract_with_lbl(label));
-
-                let inner = matches
-                    .iter()
-                    .flat_map(|m| m.clone().as_flattened_bindings())
-                    .map(|(mut path, bind, field)| {
-                        path.push(id);
-                        (path, bind, field)
-                    });
-
-                // We only want to return the outer if we actually have a variable name
-                // bound to it.
-                let outer = if bind_id.is_some() {
-                    vec![(vec![id], bind_id, field)]
-                } else {
-                    Vec::new()
-                };
-
-                inner.chain(outer).collect()
+                    .push(pattern.into_contract_with_lbl(label));
+
+                flatten_matches(&id, matches)
+            }
+            Match::Assign(
+                id,
+                mut field,
+                FieldPattern::AliasedRecordPattern {
+                    alias: bind_id,
+                    pattern: ref pattern @ RecordPattern { ref matches, .. },
+                },
+            ) => {
+                let label = get_label(&id, pattern);
+                let pattern = pattern.clone();
+                field
+                    .metadata
+                    .annotation
+                    .contracts
+                    .push(pattern.into_contract_with_lbl(label));
+
+                let mut flattened = flatten_matches(&id, matches);
+                flattened.push((vec![id], Some(bind_id), field));
+                flattened
             }
         }
     }
diff --git a/src/error.rs b/src/error.rs
index 0e943d82..f6dc9b93 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -1224,6 +1224,9 @@ mod blame_error {
             // contract for the elements of an array
             (Some(ty_path::Elem::Array), None) => (String::from("expected array element type"), Vec::new()),
             // The type path doesn't contain any arrow, and the failing subcontract is the contract
+            // for the fields of a dictionary
+            (Some(ty_path::Elem::Dict), None) => (String::from("expected dictionary field type"), Vec::new()),
+            // The type path doesn't contain any arrow, and the failing subcontract is the contract
             // for the field of a record
             (Some(ty_path::Elem::Field(_)), None) => (String::from("expected field type"), Vec::new()),
             // The original contract contains an arrow, and the path is only composed of codomains.
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 2d8a9a04..2d5ec0ba 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -25,7 +25,7 @@ use crate::{
     term::{
         array::{Array, ArrayAttrs},
         make as mk_term,
-        record::{self, Field, FieldMetadata, RecordData},
+        record::{self, Field, FieldMetadata, RecordAttrs, RecordData},
         BinaryOp, MergePriority, NAryOp, PendingContract, RecordExtKind, RichTerm, SharedTerm,
         StrChunk, Term, UnaryOp,
     },
@@ -453,6 +453,24 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     ))
                 }
             },
+            UnaryOp::GoDict() => match_sharedterm! {t, with {
+                    Term::Lbl(l) => {
+                        let mut l = l;
+                        l.path.push(ty_path::Elem::Dict);
+                        Ok(Closure::atomic_closure(RichTerm::new(
+                            Term::Lbl(l),
+                            pos_op_inh,
+                        )))
+                    }
+                } else {
+                    Err(EvalError::TypeError(
+                        String::from("Label"),
+                        String::from("go_dict"),
+                        arg_pos,
+                        RichTerm { term: t, pos },
+                    ))
+                }
+            },
             UnaryOp::StaticAccess(id) => {
                 if let Term::Record(record) = &*t {
                     // We have to apply potentially pending contracts. Right now, this
@@ -2477,11 +2495,11 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         Term::Lbl(lbl) => lbl
                     } else return Err(EvalError::TypeError(
                         String::from("Lbl"),
-                        String::from("arrayLazyAssume, 2nd argument"),
+                        String::from("arrayLazyAssume, 1st argument"),
                         fst_pos,
                         RichTerm {
-                            term: t2,
-                            pos: pos2,
+                            term: t1,
+                            pos: pos1,
                         },
                     ))
                 };
@@ -2513,6 +2531,103 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     ))
                 }
             }
+            // This implementation of `%dictionary_assume%` internally creates
+            // essentially a copy of the record that is being checked, albeit
+            // without values for the fields. If the record in question is
+            // particularly huge, this could have performance implications.
+            //
+            // An alternative implementation would be to duplicate some of the
+            // logic from `eval::merge` in here. We decided not to do that for
+            // simplicity and to keep all the magic operations on revertible
+            // thunks contained in their own module.
+            BinaryOp::DictionaryAssume() => {
+                let (
+                    Closure {
+                        body: contract_term,
+                        env: contract_env,
+                    },
+                    _,
+                ) = self.stack.pop_arg(&self.cache).ok_or_else(|| {
+                    EvalError::NotEnoughArgs(3, String::from("dictionary_assume"), pos_op)
+                })?;
+
+                let lbl = match_sharedterm! {t1, with {
+                        Term::Lbl(lbl) => lbl
+                    } else return Err(EvalError::TypeError(
+                        String::from("Lbl"),
+                        String::from("dictionary_assume, 2nd argument"),
+                        fst_pos,
+                        RichTerm {
+                            term: t1,
+                            pos: pos1,
+                        }
+                    ))
+                };
+
+                match_sharedterm! {t2,
+                    with {
+                        Term::Record(record_data) => {
+                            let contract = contract_term.closurize(&mut self.cache, &mut env2, contract_env);
+                            let record_contract = Term::Record(RecordData {
+                                fields: record_data
+                                    .fields
+                                    .iter()
+                                    .map(|(key, value)| {
+                                        (
+                                            *key,
+                                            Field {
+                                                value: None,
+                                                pending_contracts: vec![PendingContract::new(
+                                                    contract.clone(),
+                                                    lbl.clone(),
+                                                )],
+                                                // This is intentionally not written as
+                                                // `{ opt: value.metadata.opt, ..Default::default() }`
+                                                //
+                                                // When `FieldMetadata` is changed in the future, we will need to consider
+                                                // which values should be inherited from `value.metadata`.
+                                                //
+                                                // The `metadata` field here must be chosen such that, upon merging it
+                                                // with `value.metadata`, the result is identical to the original metadata
+                                                // `value.metadata` of the field.
+                                                metadata: FieldMetadata {
+                                                    opt: value.metadata.opt,
+
+                                                    doc: None,
+                                                    annotation: Default::default(),
+                                                    not_exported: false,
+                                                    priority: Default::default(),
+                                                },
+                                            },
+                                        )
+                                    })
+                                    .collect(),
+                                attrs: RecordAttrs { open: true },
+                                ..Default::default()
+                            });
+
+                            let merge_term = Closure {
+                                body: mk_opn!(
+                                    NAryOp::MergeContract(),
+                                    Term::Lbl(lbl),
+                                    Term::Record(record_data),
+                                    record_contract
+                                ),
+                                env: env2,
+                            };
+                            Ok(merge_term)
+                        }
+                    } else Err(EvalError::TypeError(
+                        String::from("Record"),
+                        String::from("dictionary_assume, 2nd argument"),
+                        snd_pos,
+                        RichTerm {
+                            term: t2,
+                            pos: pos2
+                        }
+                    ))
+                }
+            }
         }
     }
 
diff --git a/src/label.rs b/src/label.rs
index 6c56e002..3a19795e 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -58,6 +58,7 @@ pub mod ty_path {
         Codomain,
         Field(Ident),
         Array,
+        Dict,
     }
 
     pub type Path = Vec<Elem>;
@@ -273,6 +274,24 @@ but this field doesn't exist in {}",
                     last_arrow_elem,
                 }
             }
+            (TypeF::Dict(ty), next @ Some(Elem::Dict)) => {
+                // initial "{_: "
+                let start_offset = 4;
+                let paren_offset = usize::from(!ty.fmt_is_atom());
+
+                let PathSpan {
+                    start: sub_start,
+                    end: sub_end,
+                    last,
+                    last_arrow_elem,
+                } = span(path_it, ty);
+                PathSpan {
+                    start: start_offset + paren_offset + sub_start,
+                    end: start_offset + paren_offset + sub_end,
+                    last: last.or_else(|| next.copied()),
+                    last_arrow_elem,
+                }
+            }
             // The type and the path don't match, we stop here.
             _ => {
                 let repr = format!("{ty}");
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 00e7d0d0..87c9d207 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -56,7 +56,7 @@ use crate::{
     mk_opn,
     mk_fun,
     identifier::Ident,
-    destructuring::{Match, LastMatch, RecordPattern},
+    destructuring::{Match, FieldPattern, LastMatch, RecordPattern},
     term::{
         *,
         record::{RecordAttrs, Field, FieldMetadata},
@@ -228,12 +228,12 @@ UniTerm: UniTerm = {
             t1 = ann.annotation.attach_term(t1);
         }
 
-        Ok(UniTerm::from(mk_let(recursive.is_some(), pat.0, pat.1, t1, t2, mk_span(src_id, l, r))?))
+        Ok(UniTerm::from(mk_let(recursive.is_some(), pat, t1, t2, mk_span(src_id, l, r))?))
     },
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
-        let rt = pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
-            term: SharedTerm::new(mk_fun(id, destruct, t)),
+        let rt = pats.into_iter().rev().fold(t, |t, assgn| RichTerm {
+            term: SharedTerm::new(mk_fun(assgn, t)),
             pos,
         });
 
@@ -450,9 +450,15 @@ LastMatch: LastMatch = {
 
 // The right hand side of an `=` inside a destructuring pattern.
 #[inline]
-Pattern: (Option<Ident>, Option<RecordPattern>) = {
-    <id:(<Ident> "@")?> <pat: RecordPattern> => (id, Some(pat)),
-    Ident => (Some(<>), None),
+Pattern: FieldPattern = {
+    <id:(<Ident> "@")?> <pat: RecordPattern> => {
+        if let Some(id) = id {
+            FieldPattern::AliasedRecordPattern { alias: id, pattern: pat }
+        } else {
+            FieldPattern::RecordPattern(pat)
+        }
+    },
+    Ident => FieldPattern::Ident(<>),
 };
 
 // A full pattern at the left-hand side of a destructuring let.
@@ -626,6 +632,7 @@ UOp: UnaryOp = {
     "go_dom" => UnaryOp::GoDom(),
     "go_codom" => UnaryOp::GoCodom(),
     "go_array" => UnaryOp::GoArray(),
+    "go_dict" => UnaryOp::GoDict(),
     "embed" <Ident> => UnaryOp::Embed(<>),
     "map"  => UnaryOp::ArrayMap(),
     "generate" => UnaryOp::ArrayGen(),
@@ -821,6 +828,7 @@ InfixExpr: UniTerm = {
 BOpPre: BinaryOp = {
     "assume" => BinaryOp::Assume(),
     "array_lazy_assume" => BinaryOp::ArrayLazyAssume(),
+    "dictionary_assume" => BinaryOp::DictionaryAssume(),
     "unseal" => BinaryOp::Unseal(),
     "seal" => BinaryOp::Seal(),
     "go_field" => BinaryOp::GoField(),
@@ -973,6 +981,7 @@ extern {
         "typeof" => Token::Normal(NormalToken::Typeof),
         "assume" => Token::Normal(NormalToken::Assume),
         "array_lazy_assume" => Token::Normal(NormalToken::ArrayLazyAssume),
+        "dictionary_assume" => Token::Normal(NormalToken::DictionaryAssume),
         "op force" => Token::Normal(NormalToken::OpForce),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
@@ -980,6 +989,7 @@ extern {
         "go_dom" => Token::Normal(NormalToken::GoDom),
         "go_codom" => Token::Normal(NormalToken::GoCodom),
         "go_array" => Token::Normal(NormalToken::GoArray),
+        "go_dict" => Token::Normal(NormalToken::GoDict),
         "go_field" => Token::Normal(NormalToken::GoField),
         "seal" => Token::Normal(NormalToken::Seal),
         "unseal" => Token::Normal(NormalToken::Unseal),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 75a27bda..f4f64e8b 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -184,6 +184,8 @@ pub enum NormalToken<'input> {
     Assume,
     #[token("%array_lazy_assume%")]
     ArrayLazyAssume,
+    #[token("%dictionary_assume%")]
+    DictionaryAssume,
     #[token("%blame%")]
     Blame,
     #[token("%chng_pol%")]
@@ -198,6 +200,8 @@ pub enum NormalToken<'input> {
     GoField,
     #[token("%go_array%")]
     GoArray,
+    #[token("%go_dict%")]
+    GoDict,
 
     #[token("%seal%")]
     Seal,
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index d34a2005..62c87293 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -10,7 +10,7 @@ use codespan::FileId;
 use super::error::ParseError;
 
 use crate::{
-    destructuring::RecordPattern,
+    destructuring::FieldPattern,
     eval::operation::RecPriority,
     identifier::Ident,
     label::Label,
@@ -558,52 +558,39 @@ pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
     }
 }
 
-/// Generate a `Let` or a `LetPattern` (depending on `pat` being empty or not) from the parsing of
-/// a let definition. This function fails if the definition has both a non-empty pattern and is
-/// recursive (`pat != Destruct::Empty && rec`), because recursive let-patterns are currently not
-/// supported.
+/// Generate a `Let` or a `LetPattern` (depending on whether `assgn` has a record pattern) from
+/// the parsing of a let definition. This function fails if the definition has both a pattern
+/// and is recursive because recursive let-patterns are currently not supported.
 pub fn mk_let(
     rec: bool,
-    id: Option<Ident>,
-    pat: Option<RecordPattern>,
+    assgn: FieldPattern,
     t1: RichTerm,
     t2: RichTerm,
     span: RawSpan,
 ) -> Result<RichTerm, ParseError> {
-    let result = match pat {
-        Some(d) => {
-            if rec {
-                return Err(ParseError::RecursiveLetPattern(span));
-            }
-            mk_term::let_pat(id, d, t1, t2)
+    match assgn {
+        FieldPattern::Ident(id) if rec => Ok(mk_term::let_rec_in(id, t1, t2)),
+        FieldPattern::Ident(id) => Ok(mk_term::let_in(id, t1, t2)),
+        _ if rec => Err(ParseError::RecursiveLetPattern(span)),
+        FieldPattern::RecordPattern(pat) => {
+            let id: Option<Ident> = None;
+            Ok(mk_term::let_pat(id, pat, t1, t2))
         }
-        None => {
-            if let Some(id) = id {
-                if rec {
-                    mk_term::let_rec_in(id, t1, t2)
-                } else {
-                    mk_term::let_in(id, t1, t2)
-                }
-            } else {
-                panic!("unexpected let-binding without pattern or identifier")
-            }
+        FieldPattern::AliasedRecordPattern { alias, pattern } => {
+            Ok(mk_term::let_pat(Some(alias), pattern, t1, t2))
         }
-    };
-
-    Ok(result)
+    }
 }
 
-/// Generate a `Fun` or a `FunPattern` (depending on `pat` being empty or not) from the
-/// parsing of a function definition. This function panics if the definition somehow
-/// has neither an `Ident` nor a non-`Empty` `Destruct` pattern.
-pub fn mk_fun(id: Option<Ident>, pat: Option<RecordPattern>, body: RichTerm) -> Term {
-    match pat {
-        Some(d) => Term::FunPattern(id, d, body),
-        None => {
-            let Some(id) = id else {
-                unreachable!("functions always have either a non-Empty pattern or an ident")
-            };
-            Term::Fun(id, body)
+/// Generate a `Fun` or a `FunPattern` (depending on `assgn` having a pattern or not)
+/// from the parsing of a function definition. This function panics if the definition
+/// somehow has neither an `Ident` nor a non-`Empty` `Destruct` pattern.
+pub fn mk_fun(assgn: FieldPattern, body: RichTerm) -> Term {
+    match assgn {
+        FieldPattern::Ident(id) => Term::Fun(id, body),
+        FieldPattern::RecordPattern(pat) => Term::FunPattern(None, pat, body),
+        FieldPattern::AliasedRecordPattern { alias, pattern } => {
+            Term::FunPattern(Some(alias), pattern, body)
         }
     }
 }
diff --git a/src/term/mod.rs b/src/term/mod.rs
index d17db9d7..b349883f 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -1028,6 +1028,10 @@ pub enum UnaryOp {
     ///
     /// See `GoDom`.
     GoArray(),
+    /// Go to the type ascribed to every field in a dictionary.
+    ///
+    /// See `GoDom`.
+    GoDict(),
 
     /// Force the evaluation of its argument and proceed with the second.
     Seq(),
@@ -1305,6 +1309,16 @@ pub enum BinaryOp {
     /// Lazily apply a contract to an Array.
     /// This simply inserts a contract into the array attributes.
     ArrayLazyAssume(),
+
+    /// Apply a dictionary contract to a record. The arguments are a label
+    /// and the contract contained in the dictionary type. Results in a function from
+    /// records to records that applies the dictionary contract to its argument.
+    ///
+    /// When used with a dictionary contract `{_: C}` and a record `R`,
+    /// synthesizes a record contract whose fields are the fields of `R` with the
+    /// contract `C` attached to each of them. Then uses `NAryOp::MergeContract` to
+    /// apply this record contract to `R`.
+    DictionaryAssume(),
 }
 
 impl BinaryOp {
diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs
index c129df15..86d508c7 100644
--- a/src/transform/desugar_destructuring.rs
+++ b/src/transform/desugar_destructuring.rs
@@ -30,7 +30,7 @@
 //!     <do_something>
 //! ) in ...
 //! ```
-use crate::destructuring::{Match, RecordPattern};
+use crate::destructuring::{FieldPattern, Match, RecordPattern};
 use crate::identifier::Ident;
 use crate::match_sharedterm;
 use crate::term::make::{op1, op2};
@@ -178,11 +178,7 @@ fn destruct_term(x: Ident, pat: &RecordPattern, body: RichTerm) -> RichTerm {
             ),
             pos,
         ),
-        Match::Assign(f, _, (id, Some(pat))) => desugar(RichTerm::new(
-            Term::LetPattern(*id, pat.clone(), op1(StaticAccess(*f), Term::Var(x)), t),
-            pos,
-        )),
-        Match::Assign(f, _, (Some(id), None)) => desugar(RichTerm::new(
+        Match::Assign(f, _, FieldPattern::Ident(id)) => desugar(RichTerm::new(
             Term::Let(
                 *id,
                 op1(StaticAccess(*f), Term::Var(x)),
@@ -194,6 +190,25 @@ fn destruct_term(x: Ident, pat: &RecordPattern, body: RichTerm) -> RichTerm {
             ),
             pos,
         )),
-        _ => unreachable!("Match::Assign always has either an ident or a pattern"),
+        Match::Assign(f, _, FieldPattern::RecordPattern(pattern)) => desugar(RichTerm::new(
+            Term::LetPattern(
+                None,
+                pattern.clone(),
+                op1(StaticAccess(*f), Term::Var(x)),
+                t,
+            ),
+            pos,
+        )),
+        Match::Assign(f, _, FieldPattern::AliasedRecordPattern { alias, pattern }) => {
+            desugar(RichTerm::new(
+                Term::LetPattern(
+                    Some(*alias),
+                    pattern.clone(),
+                    op1(StaticAccess(*f), Term::Var(x)),
+                    t,
+                ),
+                pos,
+            ))
+        }
     })
 }
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index dc861f1c..0d866d4d 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -4,7 +4,7 @@
 //! the recursive fields that actually appear in the definition of each field when computing the
 //! fixpoint.
 use crate::{
-    destructuring::{Match, RecordPattern},
+    destructuring::{FieldPattern, Match, RecordPattern},
     identifier::Ident,
     term::{
         record::{Field, FieldDeps, RecordDeps},
@@ -244,13 +244,22 @@ fn bind_pattern(dest_pat: &RecordPattern, free_vars: &mut HashSet<Ident>) {
 /// a set of free variables.
 fn bind_match(m: &Match, free_vars: &mut HashSet<Ident>) {
     match m {
-        Match::Assign(_, _, (id, sub_pat)) => {
-            if let Some(id) = id {
-                free_vars.remove(id);
-            }
-            if let Some(sub_pat) = sub_pat {
-                bind_pattern(sub_pat, free_vars);
-            }
+        Match::Assign(_, _, FieldPattern::Ident(ident)) => {
+            free_vars.remove(ident);
+        }
+        Match::Assign(_, _, FieldPattern::RecordPattern(sub_pattern)) => {
+            bind_pattern(sub_pattern, free_vars);
+        }
+        Match::Assign(
+            _,
+            _,
+            FieldPattern::AliasedRecordPattern {
+                alias,
+                pattern: sub_pattern,
+            },
+        ) => {
+            free_vars.remove(alias);
+            bind_pattern(sub_pattern, free_vars);
         }
         Match::Simple(id, _) => {
             free_vars.remove(id);
diff --git a/src/typecheck/destructuring.rs b/src/typecheck/destructuring.rs
index 82a0b2c6..92804989 100644
--- a/src/typecheck/destructuring.rs
+++ b/src/typecheck/destructuring.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 
 use crate::{
-    destructuring::{Match, RecordPattern},
+    destructuring::{FieldPattern, Match, RecordPattern},
     identifier::Ident,
     mk_uty_row,
     types::{RecordRowF, RecordRowsF, TypeF},
@@ -58,11 +58,16 @@ fn build_pattern_type(
             id: *id,
             types: Box::new(new_leaf_type(state, leaf_type)),
         },
-        Match::Assign(id, _, (_, None)) => RecordRowF {
+        Match::Assign(id, _, FieldPattern::Ident(_)) => RecordRowF {
             id: *id,
             types: Box::new(new_leaf_type(state, leaf_type)),
         },
-        Match::Assign(id, _, (_, Some(r_pat))) => {
+        Match::Assign(
+            id,
+            _,
+            FieldPattern::RecordPattern(r_pat)
+            | FieldPattern::AliasedRecordPattern { pattern: r_pat, .. },
+        ) => {
             let row_tys = build_pattern_type(state, r_pat, leaf_type);
             let ty = UnifType::Concrete(TypeF::Record(row_tys));
             RecordRowF {
@@ -100,32 +105,42 @@ pub fn inject_pattern_variables(
             let ty = type_map.get_type(id);
             env.insert(*id, ty);
         }
-        Match::Assign(id, _, (bind_id, pat)) => {
+        Match::Assign(id, _, FieldPattern::Ident(bind_id)) => {
+            let ty = type_map.get_type(id);
+            env.insert(*bind_id, ty);
+        }
+        Match::Assign(id, _, FieldPattern::RecordPattern(pat)) => {
             let ty = type_map.get_type(id);
 
-            // If we don't have a `bind_id`, we can infer that `id` is
-            // an intermediate value that isn't accessible from the code.
-            // e.g. the `foo` in a binding like:
+            // Since we don't have a `bind_id` in this branch,
+            // we can infer that `id` is an intermediate value that
+            // isn't accessible from the code. e.g. the `foo` in a
+            // binding like:
             //
             // ```
             //   let { foo = { bar = baz } } = { foo.bar = 1 } in ...
             // ```
             //
             // As such, we don't need to add it to the environment.
-            if let Some(id) = bind_id {
-                env.insert(*id, ty.clone());
-            }
 
-            // A non-None `pat` here means we have a nested destructuring,
-            // so we recursively call this function.
-            if let Some(pat) = pat {
-                let UnifType::Concrete(TypeF::Record(rs)) = ty else {
-                            unreachable!("since this is a destructured record, \
-                                its type was constructed by build_pattern_ty, \
-                                so it must be a concrete record type")
-                        };
-                inject_pattern_variables(state, env, pat, rs)
-            }
+            let UnifType::Concrete(TypeF::Record(rs)) = ty else {
+                unreachable!("since this is a destructured record, \
+                              its type was constructed by build_pattern_ty, \
+                              which means it must be a concrete record type")
+            };
+            inject_pattern_variables(state, env, pat, rs)
+        }
+        Match::Assign(id, _, FieldPattern::AliasedRecordPattern { alias, pattern }) => {
+            let ty = type_map.get_type(id);
+
+            env.insert(*alias, ty.clone());
+
+            let UnifType::Concrete(TypeF::Record(rs)) = ty else {
+                unreachable!("since this is a destructured record, \
+                              its type was constructed by build_pattern_ty, \
+                              which means it must be a concrete record type")
+            };
+            inject_pattern_variables(state, env, pattern, rs)
         }
     });
 
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 972db631..5a857b01 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -56,10 +56,13 @@ pub fn get_uop_type(
         }
         // This should not happen, as a match primop is only produced during evaluation.
         UnaryOp::Match { .. } => panic!("cannot typecheck match primop"),
+        // Morally, Label -> Label
         // Dyn -> Dyn
-        UnaryOp::ChangePolarity() | UnaryOp::GoDom() | UnaryOp::GoCodom() | UnaryOp::GoArray() => {
-            (mk_uniftype::dynamic(), mk_uniftype::dynamic())
-        }
+        UnaryOp::ChangePolarity()
+        | UnaryOp::GoDom()
+        | UnaryOp::GoCodom()
+        | UnaryOp::GoArray()
+        | UnaryOp::GoDict() => (mk_uniftype::dynamic(), mk_uniftype::dynamic()),
         // forall rows a. { id: a | rows} -> a
         UnaryOp::StaticAccess(id) => {
             let rows = state.table.fresh_rrows_uvar();
@@ -391,6 +394,17 @@ pub fn get_bop_type(
                 mk_uty_arrow!(ty_array.clone(), ty_array),
             )
         }
+        // The first argument is a label, the third is a contract.
+        // forall a. Dyn -> {_: a} -> Dyn -> {_: a}
+        BinaryOp::DictionaryAssume() => {
+            let ty_field = UnifType::UnifVar(state.table.fresh_type_var_id());
+            let ty_dict = mk_uniftype::dyn_record(ty_field);
+            (
+                mk_uniftype::dynamic(),
+                ty_dict.clone(),
+                mk_uty_arrow!(mk_uniftype::dynamic(), ty_dict),
+            )
+        }
     })
 }
 
diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl
index 2ee57991..3e4f293c 100644
--- a/stdlib/internals.ncl
+++ b/stdlib/internals.ncl
@@ -85,7 +85,7 @@
 
   "$dyn_record" = fun contr l t =>
       if %typeof% t == `Record then
-          %record_map% t (fun _field value => %assume% contr l value)
+          %dictionary_assume% (%go_dict% l) t contr
       else
           %blame% (%tag% "not a record" l),
 


Test patch:
diff --git a/tests/integration/contracts_fail.rs b/tests/integration/contracts_fail.rs
index 60f98f2a..15bc685e 100644
--- a/tests/integration/contracts_fail.rs
+++ b/tests/integration/contracts_fail.rs
@@ -284,6 +284,25 @@ fn records_contracts_closed() {
     assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | Contract)");
 }
 
+#[test]
+fn dictionary_contracts() {
+    use nickel_lang::label::ty_path::Elem;
+
+    assert_raise_blame!("%force% (({foo} | {_: Num}) & {foo = \"string\"}) true");
+
+    let res = eval("%force% ({foo = 1} | {_: Str}) false");
+    match &res {
+        Err(Error::EvalError(EvalError::BlameError {
+            evaluated_arg: _,
+            ref label,
+            call_stack: _,
+        })) => {
+            assert_matches!(label.path.as_slice(), [Elem::Dict])
+        }
+        err => panic!("expected blame error, got {err:#?}"),
+    }
+}
+
 #[test]
 fn enum_complex() {
     eval(
diff --git a/tests/integration/pass/records.ncl b/tests/integration/pass/records.ncl
index 8469e2a2..ffbdcf36 100644
--- a/tests/integration/pass/records.ncl
+++ b/tests/integration/pass/records.ncl
@@ -115,5 +115,16 @@ let {check, ..} = import "lib/assert.ncl" in
       name = "name",
   } in
   data.name == "hijack",
+
+  # recursive overriding with dictionaries
+  # regression tests for [#892](https://github.com/tweag/nickel/issues/892)
+  (({a = 1, b = a} | {_: Num}) & { a | force = 2}).b == 2,
+
+  ({
+     b = { foo = c.foo },
+     c = {}
+   } | {_: {
+     foo | default = 0
+   } }).b.foo == 0,
 ]
 |> check
diff --git a/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl b/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl
new file mode 100644
index 00000000..3dec3c8c
--- /dev/null
+++ b/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl
@@ -0,0 +1,1 @@
+{ foo = 1, bar = "bar" } | {_: Str}
\ No newline at end of file
diff --git a/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap
new file mode 100644
index 00000000..2dd5274f
--- /dev/null
+++ b/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap
@@ -0,0 +1,22 @@
+---
+source: tests/snapshot/main.rs
+expression: snapshot
+---
+error: contract broken by a value
+  ┌─ :1:5
+  │
+1 │ {_: Str}
+  │     --- expected dictionary field type
+  │
+  ┌─ [INPUTS_PATH]/errors/dictionary_contract_fail.ncl:1:9
+  │
+1 │ { foo = 1, bar = "bar" } | {_: Str}
+  │         ^ applied to this expression
+
+note: 
+  ┌─ [INPUTS_PATH]/errors/dictionary_contract_fail.ncl:1:28
+  │
+1 │ { foo = 1, bar = "bar" } | {_: Str}
+  │                            ^^^^^^^^ bound here
+
+