fix: Nonempty returns require nonempty bodies

Functions that return a non-unit value require bodies with a final
expression that is not terminated via semicolon (that would be a
statement). Blocks that are empty or that consist exclusively out of
statements are not allowed.

Assert correctness in a unit test.

Author: uncomputable

src/ast.rs

@@ -667,10 +667,17 @@ impl AbstractSyntaxTree for Expression {
                     .iter()
                     .map(|s| Statement::analyze(s, &ResolvedType::unit(), scope))
                     .collect::<Result<Arc<[Statement]>, RichError>>()?;
-                let ast_expression = expression
-                    .as_ref()
-                    .map(|expr| Expression::analyze(expr, ty, scope).map(Arc::new))
-                    .transpose()?;
+                let ast_expression = match expression {
+                    Some(expression) => Expression::analyze(expression, ty, scope)
+                        .map(Arc::new)
+                        .map(Some),
+                    None if ty.is_unit() => Ok(None),
+                    None => Err(Error::ExpressionTypeMismatch(
+                        ty.clone(),
+                        ResolvedType::unit(),
+                    ))
+                    .with_span(from),
+                }?;
                 scope.pop_scope();
 
                 Ok(Self {

src/lib.rs

@@ -136,6 +136,18 @@ mod tests {
         assert_success(prog_text, &witness)
     }
 
+    fn assert_satisfy_error_empty_witness(prog_text: &str, expected_error: &str) {
+        let witness = WitnessValues::empty();
+        match satisfy(prog_text, &witness) {
+            Ok(_) => panic!("Accepted faulty program"),
+            Err(error) => {
+                if !error.contains(expected_error) {
+                    panic!("Unexpected error: {error}")
+                }
+            }
+        }
+    }
+
     #[test]
     fn redefined_variable() {
         let prog_text = r#"fn main() {
@@ -145,4 +157,20 @@ mod tests {
 "#;
         assert_success_empty_witness(prog_text);
     }
+
+    #[test]
+    fn empty_function_body_nonempty_return() {
+        let prog_text = r#"fn my_true() -> bool {
+    // function body is empty, although function must return `bool`
+}
+
+fn main() {
+    jet_verify(my_true());
+}
+"#;
+        assert_satisfy_error_empty_witness(
+            prog_text,
+            "Expected expression of type `bool`, found type `()`",
+        );
+    }
 }