Repository: tweag/nickel
Pull request #1099 (2023-02-03 11:29:25)

Correctly type identifiers introduced in destructuring patterns
Previously identifiers introduced via record destructuring were always typed as `Dyn`. This PR improves the situation by correctly inferring the type of these identifiers. The expressions in `tests/integration/destructuring/pass/preserves_types.ncl` should give reasonable guidance as to how this behaves.

One notable omission is that type annotations within the pattern are not enforced during typechecking (though they _are_ converted to contracts & applied during evaluation). I decided to hold off on implementing that until after the RFC005 PR gets merged to avoid dealing with whatever merge conflicts might arise.

I also took the opportunity to remove the `Destruct::Array` variant, which was never used in the codebase.


Patch:
diff --git a/src/destruct.rs b/src/destruct.rs
index 25beccba..7f0aa73b 100644
--- a/src/destruct.rs
+++ b/src/destruct.rs
@@ -45,8 +45,6 @@ pub enum Destruct {
         rest: Option<Ident>,
         span: RawSpan,
     },
-    /// An array destructuring. Not implemented.
-    Array { matches: Vec<Match>, span: RawSpan },
     /// An empty destructuring. In this case, the pattern is a classical `let var = something in
     /// body` form.
     Empty,
@@ -78,7 +76,7 @@ impl Destruct {
     /// Get the inner vector of `Matches` of the pattern. If `Empty` return a empty vector.
     pub fn inner(self) -> Vec<Match> {
         match self {
-            Destruct::Record { matches, .. } | Destruct::Array { matches, .. } => matches,
+            Destruct::Record { matches, .. } => matches,
             Destruct::Empty => vec![],
         }
     }
@@ -86,7 +84,7 @@ impl Destruct {
     // Generate a label for this `Destruct`. if `Empty`, return default label.
     fn label(&self) -> Label {
         match *self {
-            Destruct::Record { span, .. } | Destruct::Array { span, .. } => Label {
+            Destruct::Record { span, .. } => Label {
                 span,
                 ..Default::default()
             },
@@ -130,7 +128,6 @@ impl Match {
 
                 (id, field)
             }
-            Match::Assign(_id, _m, (_, _d @ Destruct::Array { .. })) => unimplemented!(),
         }
     }
 }
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 2d0f5179..1f052863 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -561,7 +561,7 @@ pub fn mk_let(
     span: RawSpan,
 ) -> Result<RichTerm, ParseError> {
     let result = match pat {
-        d @ (Destruct::Record { .. } | Destruct::Array { .. }) => {
+        d @ Destruct::Record { .. } => {
             if rec {
                 return Err(ParseError::RecursiveLetPattern(span));
             }
diff --git a/src/pretty.rs b/src/pretty.rs
index c30e0e9e..fd1b2944 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -417,7 +417,6 @@ where
                 })
                 .braces(),
             Destruct::Empty => allocator.nil(),
-            _ => unimplemented!(),
         }
     }
 }
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index d7f43078..b8536c95 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -240,11 +240,6 @@ fn bind_pattern(dest_pat: &Destruct, free_vars: &mut HashSet<Ident>) {
                 free_vars.remove(rest);
             }
         }
-        Destruct::Array { matches, .. } => {
-            for m in matches {
-                bind_match(m, free_vars);
-            }
-        }
         Destruct::Empty => {}
     }
 }
diff --git a/src/typecheck/destructuring.rs b/src/typecheck/destructuring.rs
new file mode 100644
index 00000000..4e6ad075
--- /dev/null
+++ b/src/typecheck/destructuring.rs
@@ -0,0 +1,198 @@
+use std::collections::HashMap;
+
+use crate::{
+    destruct::{Destruct, Match},
+    identifier::Ident,
+    types::{RecordRowF, RecordRowsF, TypeF},
+};
+
+use super::{
+    mk_uniftype, Environment, GenericUnifRecordRowsIteratorItem, GenericUnifType, State,
+    UnifRecordRows, UnifType,
+};
+
+/// Build a `UnifType` from a `Destruct` pattern, creating fresh unification
+/// variables wherever specific types are unknown.
+pub fn build_pattern_type(state: &mut State, pat: &Destruct) -> UnifType {
+    match pat {
+        Destruct::Record { matches, open, .. } => {
+            let tail = if *open {
+                state.table.fresh_rrows_uvar()
+            } else {
+                UnifRecordRows::Concrete(RecordRowsF::Empty)
+            };
+
+            let rows = matches.iter().map(|m| match m {
+                Match::Simple(id, _) => RecordRowF {
+                    id: *id,
+                    types: Box::new(state.table.fresh_type_uvar()),
+                },
+                Match::Assign(id, _, (_, Destruct::Empty)) => RecordRowF {
+                    id: *id,
+                    types: Box::new(state.table.fresh_type_uvar()),
+                },
+                Match::Assign(id, _, (_, r_pat @ Destruct::Record { .. })) => {
+                    let ty = build_pattern_type(state, r_pat);
+                    RecordRowF {
+                        id: *id,
+                        types: Box::new(ty),
+                    }
+                }
+            });
+
+            let rrows = rows.fold(tail, |tail, row| {
+                UnifRecordRows::Concrete(RecordRowsF::Extend {
+                    row,
+                    tail: Box::new(tail),
+                })
+            });
+
+            UnifType::Concrete(TypeF::Record(rrows))
+        }
+        Destruct::Empty => state.table.fresh_type_uvar(),
+    }
+}
+
+/// Extend `env` with any new bindings brought into scope in `pat`. The
+/// types of these bindings will be inferred from `pat_ty`.
+///
+/// For example, if `pat` represents the pattern `{ a, ..rest }` and
+/// `pat_ty` is `{ a : Num, b : Str }` then the `env` will be extended
+/// with `a : Num` and `rest : { b : Str }`.
+pub fn inject_pattern_variables(
+    state: &State,
+    env: &mut Environment,
+    pat: &Destruct,
+    pat_ty: UnifType,
+) {
+    let pat_ty = pat_ty.into_root(state.table);
+
+    match pat {
+        Destruct::Record { matches, rest, .. } => {
+            let mut type_map = RecordTypes::from(&pat_ty);
+
+            matches.iter().for_each(|m| match m {
+                Match::Simple(id, ..) => {
+                    let ty = type_map.get_type(id);
+                    env.insert(*id, ty);
+                }
+                Match::Assign(id, _, (bind_id, 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:
+                    //
+                    // ```
+                    //   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-empty `pat` here means we have a nested destructuring,
+                    // so we recursively call this function.
+                    if !pat.is_empty() {
+                        inject_pattern_variables(state, env, pat, ty)
+                    }
+                }
+            });
+
+            if let Some(id) = rest {
+                let rest_ty = type_map.rest();
+                env.insert(*id, rest_ty);
+            }
+        }
+        Destruct::Empty => (),
+    }
+}
+
+/// A map of identifiers in a destructured record to their types.
+///
+/// This allows us to be resilient to ordering differences between the
+/// pattern and its type. As well as keeping track of which identifiers
+/// have already been "used" in the pattern, to ensure that we can
+/// correctly construct the type of a `..rest` match, if it exists.
+enum RecordTypes {
+    Rows {
+        known_types: HashMap<Ident, UnifType>,
+        tail: UnifRecordRows,
+    },
+    Dyn,
+}
+
+impl From<&UnifType> for RecordTypes {
+    fn from(u: &UnifType) -> Self {
+        match u {
+            GenericUnifType::Concrete(TypeF::Record(t)) => {
+                let (tys, tail) =
+                    t.iter()
+                        .fold((HashMap::new(), None), |(mut m, _), ty| match ty {
+                            GenericUnifRecordRowsIteratorItem::Row(rt) => {
+                                m.insert(rt.id, rt.types.clone());
+                                (m, None)
+                            }
+                            GenericUnifRecordRowsIteratorItem::TailDyn => {
+                                (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailDyn)))
+                            }
+                            GenericUnifRecordRowsIteratorItem::TailVar(v) => {
+                                (m, Some(UnifRecordRows::Concrete(RecordRowsF::TailVar(*v))))
+                            }
+                            GenericUnifRecordRowsIteratorItem::TailUnifVar(n) => {
+                                (m, Some(UnifRecordRows::UnifVar(n)))
+                            }
+                            GenericUnifRecordRowsIteratorItem::TailConstant(n) => {
+                                (m, Some(UnifRecordRows::Constant(n)))
+                            }
+                        });
+                RecordTypes::Rows {
+                    known_types: tys,
+                    tail: tail.unwrap_or(UnifRecordRows::Concrete(RecordRowsF::Empty)),
+                }
+            }
+            _ => RecordTypes::Dyn,
+        }
+    }
+}
+
+impl RecordTypes {
+    /// Returns the type of the identifier `id` in the record.
+    ///
+    /// In the case of `RecordTypes::Rows`, `id` is also removed from the
+    /// map, so that it won't be considered as part of the "tail type"
+    /// when `rest` is called.
+    fn get_type(&mut self, id: &Ident) -> UnifType {
+        match self {
+            Self::Rows {
+                known_types: h,
+                tail: _,
+            } => h
+                .remove(id)
+                .expect("Scopes of identifiers in destruct patterns should be checked already"),
+            Self::Dyn => mk_uniftype::dynamic(),
+        }
+    }
+
+    /// Returns the "tail type" of the record. I.e., the record's tail
+    /// plus any "unused" matches from `known_types`.
+    fn rest(self) -> UnifType {
+        match self {
+            Self::Rows { known_types, tail } => {
+                let rows = known_types.iter().map(|(id, ty)| RecordRowF {
+                    id: *id,
+                    types: Box::new(ty.clone()),
+                });
+                let rrows = rows.fold(tail, |tail, row| {
+                    UnifRecordRows::Concrete(RecordRowsF::Extend {
+                        row,
+                        tail: Box::new(tail),
+                    })
+                });
+                UnifType::Concrete(TypeF::Record(rrows))
+            }
+            Self::Dyn => mk_uniftype::dyn_record(mk_uniftype::dynamic()),
+        }
+    }
+}
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 65bd4855..3c461373 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -47,7 +47,6 @@
 //! [`apparent_type`]).
 use crate::{
     cache::ImportResolver,
-    destruct::*,
     environment::Environment as GenericEnvironment,
     error::TypecheckError,
     identifier::Ident,
@@ -70,6 +69,7 @@ use std::{
 
 use self::linearization::{Linearization, Linearizer, StubHost};
 
+mod destructuring;
 pub mod error;
 pub mod linearization;
 pub mod operation;
@@ -835,7 +835,8 @@ fn walk<L: Linearizer>(
                 ctxt.type_env.insert(*id, binding_type(state, t.as_ref(), &ctxt, false));
             }
 
-            inject_pat_vars(pat, &mut ctxt.type_env);
+            let pattern_ty = destructuring::build_pattern_type(state, pat);
+            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
             walk(state, ctxt, lin, linearizer, t)
         }
         Term::Array(terms, _) => terms
@@ -877,7 +878,8 @@ fn walk<L: Linearizer>(
                 ctxt.type_env.insert(*x, ty_let);
             }
 
-            inject_pat_vars(pat, &mut ctxt.type_env);
+            let pattern_ty = destructuring::build_pattern_type(state, pat);
+            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, pattern_ty);
 
             walk(state, ctxt, lin, linearizer, rt)
         }
@@ -1068,26 +1070,6 @@ fn walk_with_annot<L: Linearizer>(
     }
 }
 
-// TODO: The insertion of values in the type environment is done but everything is
-// typed as `Dyn`.
-fn inject_pat_vars(pat: &Destruct, env: &mut Environment) {
-    if let Destruct::Record { matches, rest, .. } = pat {
-        if let Some(id) = rest {
-            env.insert(*id, UnifType::Concrete(TypeF::Dyn));
-        }
-        matches.iter().for_each(|m| match m {
-            Match::Simple(id, ..) => env.insert(*id, UnifType::Concrete(TypeF::Dyn)),
-            Match::Assign(id, _, (bind_id, pat)) => {
-                let id = bind_id.as_ref().unwrap_or(id);
-                env.insert(*id, UnifType::Concrete(TypeF::Dyn));
-                if !pat.is_empty() {
-                    inject_pat_vars(pat, env);
-                }
-            }
-        });
-    }
-}
-
 /// Typecheck a term against a specific type.
 ///
 /// # Arguments
@@ -1158,16 +1140,17 @@ fn type_check_<L: Linearizer>(
             type_check_(state, ctxt, lin, linearizer, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
-            let src = state.table.fresh_type_uvar();
+            let src = destructuring::build_pattern_type(state, pat);
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
             // behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
             let trg = state.table.fresh_type_uvar();
             let arr = mk_uty_arrow!(src.clone(), trg.clone());
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, src.clone());
-                ctxt.type_env.insert(*x, src);
+                ctxt.type_env.insert(*x, src.clone());
             }
-            inject_pat_vars(pat, &mut ctxt.type_env);
+
+            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, src);
             unify(state, &ctxt, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
             type_check_(state, ctxt, lin, linearizer, t, trg)
         }
@@ -1224,7 +1207,14 @@ fn type_check_<L: Linearizer>(
             type_check_(state, ctxt, lin, linearizer, rt, ty)
         }
         Term::LetPattern(x, pat, re, rt) => {
+            // The inferred type of the pattern w/ unification vars
+            let pattern_type = destructuring::build_pattern_type(state, pat);
+            // The inferred type of the expr being bound
             let ty_let = binding_type(state, re.as_ref(), &ctxt, true);
+
+            unify(state, &ctxt, ty_let.clone(), pattern_type)
+                .map_err(|e| e.into_typecheck_err(state, re.pos))?;
+
             type_check_(
                 state,
                 ctxt.clone(),
@@ -1236,9 +1226,11 @@ fn type_check_<L: Linearizer>(
 
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, ty_let.clone());
-                ctxt.type_env.insert(*x, ty_let);
+                ctxt.type_env.insert(*x, ty_let.clone());
             }
-            inject_pat_vars(pat, &mut ctxt.type_env);
+
+            destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, ty_let);
+
             type_check_(state, ctxt, lin, linearizer, rt, ty)
         }
         Term::App(e, t) => {


Test patch:
diff --git a/tests/integration/destructuring.rs b/tests/integration/destructuring.rs
index 5f870f53..76eaaf99 100644
--- a/tests/integration/destructuring.rs
+++ b/tests/integration/destructuring.rs
@@ -1,55 +1,27 @@
+use std::ffi::OsString;
+use std::path::PathBuf;
+
 use assert_matches::assert_matches;
 use nickel_lang::error::{Error, EvalError, TypecheckError};
 use nickel_lang::term::Term;
 
-use nickel_lang_utilities::eval_file;
-
-#[test]
-fn simple() {
-    assert_eq!(eval_file("destructuring/simple.ncl"), Ok(Term::Bool(true)));
-}
-
-#[test]
-fn assign() {
-    assert_eq!(eval_file("destructuring/assign.ncl"), Ok(Term::Bool(true)));
-}
-
-#[test]
-fn atbind() {
-    assert_eq!(eval_file("destructuring/atbind.ncl"), Ok(Term::Bool(true)));
-}
-
-#[test]
-fn open() {
-    assert_eq!(eval_file("destructuring/open.ncl"), Ok(Term::Bool(true)));
-}
+use nickel_lang_utilities::{eval_file, TestProgram};
+use test_generator::test_resources;
 
-#[test]
-fn nested() {
-    assert_eq!(eval_file("destructuring/nested.ncl"), Ok(Term::Bool(true)));
-}
+#[test_resources("tests/integration/destructuring/pass/*.ncl")]
+fn pass(file: &str) {
+    let mut path = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    path.push(file);
 
-#[test]
-fn rest() {
-    assert_eq!(eval_file("destructuring/rest.ncl"), Ok(Term::Bool(true)));
-}
+    let path: OsString = path.into();
 
-#[test]
-fn default() {
-    assert_eq!(eval_file("destructuring/default.ncl"), Ok(Term::Bool(true)));
-}
-
-#[test]
-fn typecontract() {
+    let mut p = TestProgram::new_from_file(path.clone()).expect("could not load file as program");
     assert_eq!(
-        eval_file("destructuring/typecontract.ncl"),
-        Ok(Term::Bool(true))
-    );
-}
-
-#[test]
-fn mixed() {
-    assert_eq!(eval_file("destructuring/mixed.ncl"), Ok(Term::Bool(true)));
+        p.eval().map(Term::from),
+        Ok(Term::Bool(true)),
+        "error evaluating {}",
+        path.to_string_lossy()
+    )
 }
 
 #[test]
@@ -85,6 +57,33 @@ fn typecontract_fail() {
 }
 
 #[test]
-fn fun() {
-    assert_eq!(eval_file("destructuring/fun.ncl"), Ok(Term::Bool(true)));
+fn type_mismatch_fail() {
+    assert_matches!(
+        eval_file("destructuring/type_mismatch_fail.ncl"),
+        // Note: ideally this would be a typechecker error, but currently
+        //       annotated types in destructuring patterns are just converted
+        //       into contracts. This should be revisted once the metadata
+        //       rework from RFC005 is implemented
+        Err(Error::EvalError(EvalError::BlameError { .. }))
+    )
+}
+
+#[test]
+fn repeated_ident() {
+    assert_matches!(
+        eval_file("destructuring/repeated_ident.ncl"),
+        // Note: currently a repeated identifier in a pattern isn't caught
+        //       unless we're explicitly typechecking. There's an open issue
+        //       (#1098) to handle this when we compile the pattern at which
+        //       point this error will likely change.
+        Err(Error::TypecheckError(TypecheckError::MissingRow(..)))
+    )
+}
+
+#[test]
+fn nonexistent_idents() {
+    assert_matches!(
+        eval_file("destructuring/nonexistent_idents.ncl"),
+        Err(Error::TypecheckError(TypecheckError::MissingRow(..)))
+    )
 }
diff --git a/tests/integration/destructuring/nonexistent_idents.ncl b/tests/integration/destructuring/nonexistent_idents.ncl
new file mode 100644
index 00000000..adc2cffe
--- /dev/null
+++ b/tests/integration/destructuring/nonexistent_idents.ncl
@@ -0,0 +1,4 @@
+(
+  let { a, b } = { a = 1, c = 2 } in
+  a: Num
+): _
diff --git a/tests/integration/destructuring/assign.ncl b/tests/integration/destructuring/pass/assign.ncl
similarity index 100%
rename from tests/integration/destructuring/assign.ncl
rename to tests/integration/destructuring/pass/assign.ncl
diff --git a/tests/integration/destructuring/atbind.ncl b/tests/integration/destructuring/pass/atbind.ncl
similarity index 100%
rename from tests/integration/destructuring/atbind.ncl
rename to tests/integration/destructuring/pass/atbind.ncl
diff --git a/tests/integration/destructuring/default.ncl b/tests/integration/destructuring/pass/default.ncl
similarity index 100%
rename from tests/integration/destructuring/default.ncl
rename to tests/integration/destructuring/pass/default.ncl
diff --git a/tests/integration/destructuring/fun.ncl b/tests/integration/destructuring/pass/fun.ncl
similarity index 100%
rename from tests/integration/destructuring/fun.ncl
rename to tests/integration/destructuring/pass/fun.ncl
diff --git a/tests/integration/destructuring/mixed.ncl b/tests/integration/destructuring/pass/mixed.ncl
similarity index 100%
rename from tests/integration/destructuring/mixed.ncl
rename to tests/integration/destructuring/pass/mixed.ncl
diff --git a/tests/integration/destructuring/nested.ncl b/tests/integration/destructuring/pass/nested.ncl
similarity index 100%
rename from tests/integration/destructuring/nested.ncl
rename to tests/integration/destructuring/pass/nested.ncl
diff --git a/tests/integration/destructuring/open.ncl b/tests/integration/destructuring/pass/open.ncl
similarity index 100%
rename from tests/integration/destructuring/open.ncl
rename to tests/integration/destructuring/pass/open.ncl
diff --git a/tests/integration/destructuring/pass/preserves_types.ncl b/tests/integration/destructuring/pass/preserves_types.ncl
new file mode 100644
index 00000000..1bf8fa9a
--- /dev/null
+++ b/tests/integration/destructuring/pass/preserves_types.ncl
@@ -0,0 +1,63 @@
+let test_cases : _ = {
+  "destructuring let binding preserves types" =
+    let some_record: { a : Num, b : Str, c : Num -> Num } = { a = 1, b = "test", c = fun n => n } in
+    let { a, b, c } = some_record in
+    { a_num = a, a_str = b, the_id_fn = c } : { a_num : Num, a_str : Str, the_id_fn : Num -> Num },
+
+  "destructuring let binding infers types" =
+    let some_record = { a = 1, b = "test", c = fun n => n } in
+    let { a, b, c } = some_record in
+    { a_num = a, a_str = b, the_id_fn = c } : { a_num : Num, a_str : Str, the_id_fn : Num -> Num },
+
+  "destructuring function args preserves types" =
+    let dstrct : { a : Num, b : Str } -> { num : Num, str : Str } =
+      fun { a, b } => { num = a, str = b }
+    in
+    let r :  { a : Num, b : Str } = { a = 1, b = "" } in
+    dstrct r : { num : Num, str : Str },
+
+  "destructuring function args infers types" =
+    let dstrct = fun { a, b } => { num = a, str = b } in
+    let r = { a = 1, b = "" } in
+    dstrct r : { num : Num, str: Str },
+
+  "nested destructuring preserves types" =
+    let { a = { b, c }} = { a = { b : Num = 1, c : Str = "" }} in
+    { num = b, str = c } : { num : Num, str : Str },
+
+  "nested destructuring infers types" =
+    (let { a = { b, c }} = { a = { b = 1, c = "" }} in
+    { num = b, str = c }) : { num : Num, str : Str },
+
+  "destructuring rest pattern removes matched rows" =
+    let some_record : { a : Num, b : Str, c : Bool } = { a = 1, b = "", c = true } in
+    let { b, ..ac } = some_record in
+    ac : { a: Num, c: Bool },
+
+  "destructuring rest pattern infers correct type" =
+    let some_record = { a = 1, b = "", c = fun x => x + 1 } in
+    let { b, ..ac } = some_record in
+    ac : { a : Num, c : Num -> Num },
+
+  "destructuring rest pattern preserves tail type" =
+    let f : forall z. { x: Num, y: Num; z } -> { y: Num; z } = fun { x, ..rest } => rest in
+    (f { x = 1, y = 2, z = 3 }): { y : Num, z: Num },
+
+  "destructuring rest pattern infers tail type" =
+    let f = fun { x, ..rest } => rest in
+    (f { x = "a", y = "b", z = 105}) : { y : Str, z : Num },
+
+  # Note: we need to annotate `a` on the right-hand side of the binding
+  #       because we don't currently have a subtyping rule like:
+  #         `{ f_1: T, ..., f_N: T } <: {_ : T}`
+  #       If you're reading this and we _do_ have such a subtyping rule
+  #       (e.g. after RFC003 has been implemented) then it should be
+  #       safe to remove that type annotation from this test case.
+  "destructuring with explicit types" =
+    let { a : { _ : Num } } = { a: { _ : Num } = { b = 1 } } in
+    a : { _ : Num },
+
+  "destructuring with contracts" =
+    let { a | { _ : Num } } = { a = 1 } in
+    a : Num,
+} in true
diff --git a/tests/integration/destructuring/rest.ncl b/tests/integration/destructuring/pass/rest.ncl
similarity index 100%
rename from tests/integration/destructuring/rest.ncl
rename to tests/integration/destructuring/pass/rest.ncl
diff --git a/tests/integration/destructuring/simple.ncl b/tests/integration/destructuring/pass/simple.ncl
similarity index 100%
rename from tests/integration/destructuring/simple.ncl
rename to tests/integration/destructuring/pass/simple.ncl
diff --git a/tests/integration/destructuring/typecontract.ncl b/tests/integration/destructuring/pass/typecontract.ncl
similarity index 100%
rename from tests/integration/destructuring/typecontract.ncl
rename to tests/integration/destructuring/pass/typecontract.ncl
diff --git a/tests/integration/destructuring/repeated_ident.ncl b/tests/integration/destructuring/repeated_ident.ncl
new file mode 100644
index 00000000..c7370fe9
--- /dev/null
+++ b/tests/integration/destructuring/repeated_ident.ncl
@@ -0,0 +1,6 @@
+# Note: currently repeated identifiers in patterns aren't caught unless
+#       we're in typechecking mode. there's an open issue for this (#1098)
+(
+  let { a, a, .. } = { a = 1, b = 2 } in
+  a : Num
+): _
diff --git a/tests/integration/destructuring/type_mismatch_fail.ncl b/tests/integration/destructuring/type_mismatch_fail.ncl
new file mode 100644
index 00000000..25f7833b
--- /dev/null
+++ b/tests/integration/destructuring/type_mismatch_fail.ncl
@@ -0,0 +1,2 @@
+let { a : Num } = { a = "hi" } in
+a : _
\ No newline at end of file