Use all_sub

Author: tiif

crates/formality-check/src/mini_rust_check.rs

@@ -410,24 +410,28 @@ impl Check<'_> {
                     bail!("The length of ValueExpression::Tuple does not match the type of the ADT declared")
                 }
 
-                let expression_ty_pair = zip(value_expressions, struct_field_tys);
+                let mut value_tys: Vec<Ty> = Vec::new();
 
-                // FIXME: we only support const in value expression of struct for now, we can add support
-                // more in future.
-
-                for (value_expression, declared_ty) in expression_ty_pair {
+                for value_expression in value_expressions {
+                    // FIXME: we only support const in value expression of struct for now, we can add support
+                    // more in future.
                     let Constant(_) = value_expression else {
                         bail!("Only Constant is supported in ValueExpression::Struct for now.")
                     };
-                    let ty = self.check_value(typeck_env, fn_assumptions, value_expression)?;
-
-                    // Make sure the type matches the declared adt.
-                    if ty != declared_ty {
-                        bail!(
-                            "The type in ValueExpression::Tuple does not match the struct declared"
-                        )
-                    }
+                    value_tys.push(self.check_value(
+                        typeck_env,
+                        fn_assumptions,
+                        value_expression,
+                    )?);
                 }
+
+                // Make sure all the types supplied are the subtype of declared types.
+                self.prove_goal(
+                    &typeck_env.env,
+                    &fn_assumptions,
+                    Wcs::all_sub(value_tys, struct_field_tys),
+                )?;
+
                 Ok(ty.clone())
             }
         }

src/test/mir_fn_bodies.rs

@@ -889,7 +889,18 @@ fn test_struct_wrong_type_in_initialisation() {
             }
         ]
         []
-        expect_test::expect!["The type in ValueExpression::Tuple does not match the struct declared"]
+        expect_test::expect![[r#"
+            judgment `prove { goal: {bool <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [adt Dummy { struct { value : u32 } }], {}, {Dummy}) }` failed at the following rule(s):
+              failed at (src/file.rs:LL:CC) because
+                judgment `prove_wc_list { goal: {bool <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
+                  the rule "some" failed at step #0 (src/file.rs:LL:CC) because
+                    judgment `prove_wc { goal: bool <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
+                      the rule "subtype" failed at step #0 (src/file.rs:LL:CC) because
+                        judgment `prove_sub { a: bool, b: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
+                          the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
+                            judgment had no applicable rules: `prove_normalize { p: bool, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }`
+                          the rule "normalize-r" failed at step #0 (src/file.rs:LL:CC) because
+                            judgment had no applicable rules: `prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }`"#]]
     )
 }