Allow the type checker to accept empty values

ast/src/parsed/types.rs

@@ -126,6 +126,10 @@ impl<E> Type<E> {
     pub fn contained_type_vars(&self) -> impl Iterator<Item = &String> {
         self.contained_type_vars_with_repetitions().unique()
     }
+
+    pub fn empty_tuple() -> Type<E> {
+        Type::Tuple(TupleType { items: vec![] })
+    }
 }
 impl<E: Clone> Type<E> {
     /// Substitutes all occurrences of the given type variables with the given types.

pil-analyzer/src/condenser.rs

@@ -238,7 +238,14 @@ impl<'a, T: FieldElement> Condenser<'a, T> {
         if identity.kind == IdentityKind::Polynomial {
             let expr = identity.expression_for_poly_id();
             evaluator::evaluate(expr, self)
-                .and_then(|expr| self.add_constraints(expr, identity.source.clone()))
+                .and_then(|expr| {
+                    if let Value::Tuple(items) = expr.as_ref() {
+                        assert!(items.is_empty());
+                        Ok(())
+                    } else {
+                        self.add_constraints(expr, identity.source.clone())
+                    }
+                })
                 .unwrap_or_else(|err| {
                     panic!(
                         "Error reducing expression to constraint:\nExpression: {expr}\nError: {err:?}"

pil-analyzer/src/pil_analyzer.rs

@@ -270,15 +270,18 @@ impl PILAnalyzer {
                 Some((name.clone(), (type_scheme, expr)))
             })
             .collect();
-        // Collect all expressions in identities.
-        let statement_type = ExpectedType {
+        let constr_function_statement_type = ExpectedType {
             ty: Type::NamedType(SymbolPath::from_str("std::prelude::Constr").unwrap(), None),
             allow_array: true,
+            allow_empty: true,
         };
         for id in &mut self.identities {
             if id.kind == IdentityKind::Polynomial {
-                // At statement level, we allow Constr or Constr[].
-                expressions.push((id.expression_for_poly_id_mut(), statement_type.clone()));
+                // At statement level, we allow Constr, Constr[] or ().
+                expressions.push((
+                    id.expression_for_poly_id_mut(),
+                    constr_function_statement_type.clone(),
+                ));
             } else {
                 for part in [&mut id.left, &mut id.right] {
                     if let Some(selector) = &mut part.selector {
@@ -290,15 +293,19 @@ impl PILAnalyzer {
                 }
             }
         }
-        let inferred_types = infer_types(definitions, &mut expressions, &statement_type)
-            .map_err(|mut errors| {
-                eprintln!("\nError during type inference:");
-                for e in &errors {
-                    e.output_to_stderr();
-                }
-                errors.pop().unwrap()
-            })
-            .unwrap();
+        let inferred_types = infer_types(
+            definitions,
+            &mut expressions,
+            &constr_function_statement_type,
+        )
+        .map_err(|mut errors| {
+            eprintln!("\nError during type inference:");
+            for e in &errors {
+                e.output_to_stderr();
+            }
+            errors.pop().unwrap()
+        })
+        .unwrap();
         // Store the inferred types.
         for (name, ty) in inferred_types {
             let Some(FunctionValueDefinition::Expression(TypedExpression {

pil-analyzer/src/side_effect_checker.rs

@@ -62,22 +62,12 @@ impl<'a> SideEffectChecker<'a> {
             }
             Expression::BlockExpression(_, BlockExpression { statements, .. }) => {
                 for s in statements {
-                    match s {
-                        StatementInsideBlock::LetStatement(s) => {
-                            if s.value.is_none() && self.context != FunctionKind::Constr {
-                                return Err(format!(
-                                    "Tried to create a witness column in a {} context: {s}",
-                                    self.context
-                                ));
-                            }
-                        }
-                        StatementInsideBlock::Expression(expr) => {
-                            if self.context != FunctionKind::Constr {
-                                return Err(format!(
-                                    "Tried to add a constraint in a {} context: {expr}",
-                                    self.context
-                                ));
-                            }
+                    if let StatementInsideBlock::LetStatement(ls) = s {
+                        if ls.value.is_none() && self.context != FunctionKind::Constr {
+                            return Err(format!(
+                                "Tried to create a witness column in a {} context: {ls}",
+                                self.context
+                            ));
                         }
                     }
                 }

pil-analyzer/src/type_builtins.rs

@@ -40,10 +40,7 @@ lazy_static! {
         ("std::convert::fe", ("T: FromLiteral", "T -> fe")),
         ("std::convert::int", ("T: FromLiteral", "T -> int")),
         ("std::convert::expr", ("T: FromLiteral", "T -> expr")),
-        (
-            "std::debug::print",
-            ("T: ToString", "T -> std::prelude::Constr[]")
-        ),
+        ("std::debug::print", ("T: ToString", "T -> ()")),
         ("std::field::modulus", ("", "-> int")),
         ("std::prover::challenge", ("", "int, int -> expr")),
         ("std::prover::degree", ("", "-> int")),

pil-analyzer/src/type_inference.rs

@@ -7,7 +7,7 @@ use powdr_ast::{
         display::format_type_scheme_around_name,
         types::{ArrayType, FunctionType, TupleType, Type, TypeBounds, TypeScheme},
         visitor::ExpressionVisitable,
-        ArrayLiteral, BinaryOperation, BlockExpression, FunctionCall, IndexAccess,
+        ArrayLiteral, BinaryOperation, BlockExpression, FunctionCall, FunctionKind, IndexAccess,
         LambdaExpression, LetStatementInsideBlock, MatchArm, MatchExpression, Number, Pattern,
         SourceReference, StatementInsideBlock, UnaryOperation,
     },
@@ -39,21 +39,25 @@ pub fn infer_types(
 #[derive(Clone)]
 pub struct ExpectedType {
     pub ty: Type,
+    /// If true, arrays of `ty` are also allowed.
     pub allow_array: bool,
+    /// If true, the empty tuple is also allowed.
+    pub allow_empty: bool,
 }
 
 impl From<Type> for ExpectedType {
     fn from(ty: Type) -> Self {
         ExpectedType {
             ty,
             allow_array: false,
+            allow_empty: false,
         }
     }
 }
 
 struct TypeChecker<'a> {
-    /// The expected type for expressions at statement level in block expressions.
-    statement_type: &'a ExpectedType,
+    /// The expected type for expressions at statement level in block expressions inside a constr function.
+    constr_function_statement_type: &'a ExpectedType,
     /// Types for local variables, might contain type variables.
     local_var_types: Vec<Type>,
     /// Declared types for all symbols and their source references.
@@ -65,17 +69,20 @@ struct TypeChecker<'a> {
     unifier: Unifier,
     /// Last used type variable index.
     last_type_var: usize,
+    /// Keeps track of the kind of lambda we are currently type-checking.
+    lambda_kind: FunctionKind,
 }
 
 impl<'a> TypeChecker<'a> {
     pub fn new(statement_type: &'a ExpectedType) -> Self {
         Self {
-            statement_type,
+            constr_function_statement_type: statement_type,
             local_var_types: Default::default(),
             declared_types: Default::default(),
             declared_type_vars: Default::default(),
             unifier: Default::default(),
             last_type_var: Default::default(),
+            lambda_kind: FunctionKind::Constr,
         }
     }
 
@@ -441,31 +448,30 @@ impl<'a> TypeChecker<'a> {
         expected_type: &ExpectedType,
         expr: &mut Expression,
     ) -> Result<(), Error> {
-        if expected_type.allow_array {
-            self.infer_type_of_expression(expr).and_then(|ty| {
-                let ty = self.type_into_substituted(ty);
-                let expected_type = if matches!(ty, Type::Array(_)) {
-                    Type::Array(ArrayType {
-                        base: Box::new(expected_type.ty.clone()),
-                        length: None,
-                    })
-                } else {
-                    expected_type.ty.clone()
-                };
+        update_type_if_literal(expr, &expected_type.ty);
 
-                self.unifier
-                    .unify_types(ty.clone(), expected_type.clone())
-                    .map_err(|err| {
-                        expr.source_reference().with_error(format!(
-                            "Expected type {} but got type {}.\n{err}",
-                            self.format_type_with_bounds(expected_type),
-                            self.format_type_with_bounds(ty)
-                        ))
-                    })
+        let ty = self.infer_type_of_expression(expr)?;
+        let ty = self.type_into_substituted(ty);
+        let expected_type = if expected_type.allow_array && matches!(ty, Type::Array(_)) {
+            Type::Array(ArrayType {
+                base: Box::new(expected_type.ty.clone()),
+                length: None,
             })
+        } else if expected_type.allow_empty && (ty == Type::empty_tuple()) {
+            Type::empty_tuple()
         } else {
-            self.expect_type(&expected_type.ty, expr)
-        }
+            expected_type.ty.clone()
+        };
+
+        self.unifier
+            .unify_types(ty.clone(), expected_type.clone())
+            .map_err(|err| {
+                expr.source_reference().with_error(format!(
+                    "Expected type {} but got type {}.\n{err}",
+                    self.format_type_with_bounds(expected_type),
+                    self.format_type_with_bounds(ty),
+                ))
+            })
     }
 
     /// Process an expression and return the type of the expression.
@@ -532,14 +538,7 @@ impl<'a> TypeChecker<'a> {
                     .map(|item| self.infer_type_of_expression(item))
                     .collect::<Result<_, _>>()?,
             }),
-            Expression::LambdaExpression(
-                source_ref,
-                LambdaExpression {
-                    kind: _,
-                    params,
-                    body,
-                },
-            ) => {
+            Expression::LambdaExpression(source_ref, LambdaExpression { kind, params, body }) => {
                 let old_len = self.local_var_types.len();
                 let result = params
                     .iter()
@@ -548,7 +547,11 @@ impl<'a> TypeChecker<'a> {
                     // TODO we need a better source reference
                     .map_err(|err| source_ref.with_error(err))
                     .and_then(|param_types| {
-                        Ok((param_types, self.infer_type_of_expression(body)?))
+                        let old_lambda_kind = self.lambda_kind;
+                        self.lambda_kind = *kind;
+                        let body_type = self.infer_type_of_expression(body);
+                        self.lambda_kind = old_lambda_kind;
+                        Ok((param_types, body_type?))
                     });
                 self.local_var_types.truncate(old_len);
                 let (param_types, body_type) = result?;
@@ -639,6 +642,7 @@ impl<'a> TypeChecker<'a> {
             }
             Expression::BlockExpression(source_ref, BlockExpression { statements, expr }) => {
                 let original_var_count = self.local_var_types.len();
+
                 for statement in statements {
                     match statement {
                         StatementInsideBlock::LetStatement(LetStatementInsideBlock {
@@ -655,7 +659,7 @@ impl<'a> TypeChecker<'a> {
                                 .map_err(|err| source_ref.with_error(err))?;
                         }
                         StatementInsideBlock::Expression(expr) => {
-                            self.expect_type_with_flexibility(self.statement_type, expr)?;
+                            self.expect_type_with_flexibility(&self.statement_type(), expr)?;
                         }
                     }
                 }
@@ -666,6 +670,15 @@ impl<'a> TypeChecker<'a> {
         })
     }
 
+    /// Returns the type expected at statement level, given the current function context.
+    fn statement_type(&self) -> ExpectedType {
+        if self.lambda_kind == FunctionKind::Constr {
+            self.constr_function_statement_type.clone()
+        } else {
+            Type::empty_tuple().into()
+        }
+    }
+
     /// Process a function call and return the type of the expression.
     /// The error message is used to clarify which kind of function call it is
     /// (it might be an operator).
@@ -707,24 +720,8 @@ impl<'a> TypeChecker<'a> {
     /// This function should be preferred over `infer_type_of_expression` if an expected type is known
     /// because we can create better error messages.
     fn expect_type(&mut self, expected_type: &Type, expr: &mut Expression) -> Result<(), Error> {
-        // For literals, we try to store the type here already.
-        // This avoids creating tons of type variables for large arrays.
-        if let Expression::Number(
-            _,
-            Number {
-                type_: annotated_type @ None,
-                ..
-            },
-        ) = expr
-        {
-            match expected_type {
-                Type::Int => *annotated_type = Some(Type::Int),
-                Type::Fe => *annotated_type = Some(Type::Fe),
-                Type::Expr => *annotated_type = Some(Type::Expr),
-                Type::TypeVar(tv) => *annotated_type = Some(Type::TypeVar(tv.clone())),
-                _ => {}
-            };
-        }
+        update_type_if_literal(expr, expected_type);
+
         let inferred_type = self.infer_type_of_expression(expr)?;
         self.unifier
             .unify_types(inferred_type.clone(), expected_type.clone())
@@ -946,3 +943,27 @@ impl<'a> TypeChecker<'a> {
         self.local_var_types[id as usize].clone()
     }
 }
+
+fn update_type_if_literal(
+    expr: &mut powdr_ast::parsed::Expression<Reference>,
+    expected_type: &Type,
+) {
+    // For literals, we try to store the type here already.
+    // This avoids creating tons of type variables for large arrays.
+    if let Expression::Number(
+        _,
+        Number {
+            type_: annotated_type @ None,
+            ..
+        },
+    ) = expr
+    {
+        match expected_type.clone() {
+            Type::Int => *annotated_type = Some(Type::Int),
+            Type::Fe => *annotated_type = Some(Type::Fe),
+            Type::Expr => *annotated_type = Some(Type::Expr),
+            Type::TypeVar(tv) => *annotated_type = Some(Type::TypeVar(tv.clone())),
+            _ => {}
+        };
+    }
+}

pil-analyzer/src/type_unifier.rs

@@ -116,7 +116,6 @@ impl Unifier {
                     .zip(args2)
                     .try_for_each(|(a1, a2)| self.unify_types(a1, a2))
             }
-
             (ty1, ty2) => Err(format!("Cannot unify types {ty1} and {ty2}")),
         }
     }

pil-analyzer/tests/parse_display.rs

@@ -346,7 +346,7 @@ fn expression_but_expected_constraint() {
 }
 
 #[test]
-#[should_panic = "Expected type: expr\\nInferred type: std::prelude::Constr\\n"]
+#[should_panic = "Expected type expr but got type std::prelude::Constr."]
 fn constraint_but_expected_expression() {
     let input = r#"namespace N(16);
     col witness y;

pil-analyzer/tests/side_effects.rs

@@ -12,7 +12,7 @@ fn new_wit_in_pure() {
 }
 
 #[test]
-#[should_panic = "Tried to add a constraint in a pure context: x = 7"]
+#[should_panic = "Expected type () but got type std::prelude::Constr"]
 fn constr_in_pure() {
     let input = r#"namespace N(16);
     let new_col = |x| { x = 7; [] };
@@ -77,7 +77,7 @@ fn constr_lambda_in_pure() {
 }
 
 #[test]
-#[should_panic = "Tried to add a constraint in a pure context: x = 7"]
+#[should_panic = "Expected type () but got type std::prelude::Constr"]
 fn reset_context() {
     let input = r#"namespace N(16);
     let new_col = |x| { x = 7; [] };

pil-analyzer/tests/types.rs

@@ -327,7 +327,7 @@ fn enum_is_not_constr() {
 }
 
 #[test]
-#[should_panic = "Expected type: int -> std::prover::Query"]
+#[should_panic = "Expected type int -> std::prover::Query"]
 fn query_with_wrong_type() {
     let input = "col witness w(i) query i;";
     type_check(input, &[]);