From 3c7663cd3c1363340fe4b548671a5b4f4f242364 Mon Sep 17 00:00:00 2001
From: KtorZ <matthias.benkort@gmail.com>
Date: Sat, 11 Feb 2023 16:20:28 +0100
Subject: [PATCH] Basic exhaustivness check on list patterns

  Before that commit, the type-checker would allow unsafe list patterns
  such as:

  ```
  let [x] = xs

  when xs is {
    [x] -> ...
    [x, ..] ->  ...
  }
  ```

  This is quite unsafe and can lead to confusing situations. Now at
  least the compiler warns about this. It isn't perfect though,
  especially in the presence of clause guards. But that's a start.
---
 crates/aiken-lang/src/tipo/environment.rs | 73 +++++++++++++++++++++++
 1 file changed, 73 insertions(+)

diff --git a/crates/aiken-lang/src/tipo/environment.rs b/crates/aiken-lang/src/tipo/environment.rs
index 8b2f265a..6bcea04f 100644
--- a/crates/aiken-lang/src/tipo/environment.rs
+++ b/crates/aiken-lang/src/tipo/environment.rs
@@ -1386,6 +1386,10 @@ impl<'a> Environment<'a> {
                     Some(module.clone())
                 };
 
+                if type_name == "List" && module.is_empty() {
+                    return self.check_list_pattern_exhaustiveness(patterns);
+                }
+
                 if let Ok(constructors) = self.get_constructors_for_type(&m, type_name, location) {
                     let mut unmatched_constructors: HashSet<String> =
                         constructors.iter().cloned().collect();
@@ -1426,6 +1430,75 @@ impl<'a> Environment<'a> {
         }
     }
 
+    pub fn check_list_pattern_exhaustiveness(
+        &mut self,
+        patterns: Vec<Pattern<PatternConstructor, Arc<Type>>>,
+    ) -> Result<(), Vec<String>> {
+        let mut cover_empty = false;
+        let mut cover_tail = false;
+
+        let patterns = patterns.iter().map(|p| match p {
+            Pattern::Assign { pattern, .. } => pattern,
+            _ => p,
+        });
+
+        // TODO: We could also warn on redundant patterns. As soon as we've matched the entire
+        // list, any new pattern is redundant. For example:
+        //
+        // when xs is {
+        //   [] => ...
+        //   [x, ..] => ...
+        //   [y] => ...
+        // }
+        //
+        // That last pattern is actually redundant / unreachable.
+        for p in patterns {
+            match p {
+                Pattern::Var { .. } => {
+                    cover_empty = true;
+                    cover_tail = true;
+                }
+                Pattern::Discard { .. } => {
+                    cover_empty = true;
+                    cover_tail = true;
+                }
+                Pattern::List { elements, tail, .. } => {
+                    if elements.is_empty() {
+                        cover_empty = true;
+                    }
+                    match tail {
+                        None => {}
+                        Some(p) => match **p {
+                            Pattern::Discard { .. } => {
+                                cover_tail = true;
+                            }
+                            Pattern::Var { .. } => {
+                                cover_tail = true;
+                            }
+                            _ => {
+                                unreachable!()
+                            }
+                        },
+                    }
+                }
+                _ => {}
+            }
+        }
+
+        if cover_empty && cover_tail {
+            Ok(())
+        } else {
+            let mut missing = vec![];
+            if !cover_empty {
+                missing.push("[]".to_owned());
+            }
+            if !cover_tail {
+                missing.push("[_, ..]".to_owned());
+            }
+            Err(missing)
+        }
+    }
+
     /// Lookup constructors for type in the current scope.
     ///
     pub fn get_constructors_for_type(