From 656e3163e5d169b81cc3a212ed930da9af3685cd Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 2 Jul 2025 10:22:29 +0200
Subject: [PATCH 01/42] Make it build successfully

---
 crates/formality-check/src/fns.rs             |  6 ++---
 crates/formality-check/src/lib.rs             |  4 +---
 crates/formality-check/src/mini_rust_check.rs | 24 +++++++++++--------
 src/lib.rs                                    |  2 --
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs
index bb42c3e1..b09949d2 100644
--- a/crates/formality-check/src/fns.rs
+++ b/crates/formality-check/src/fns.rs
@@ -5,7 +5,7 @@ use formality_rust::{
 };
 use formality_types::grammar::{Fallible, Wcs};
 
-use crate::{mini_rust_check, Check};
+use crate::Check;
 
 impl Check<'_> {
     /// A "free function" is a free-standing function that is not part of an impl.
@@ -59,7 +59,7 @@ impl Check<'_> {
         for input_ty in &input_tys {
             self.prove_goal(&env, &fn_assumptions, input_ty.well_formed())?;
         }
-        self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?;
+        self.prove_goal(&env, &fn_assumptions, &output_ty.well_formed())?;
 
         // Type-check the function body, if present.
         match body {
@@ -71,7 +71,7 @@ impl Check<'_> {
                     // A trusted function body is assumed to be valid, all set.
                 }
                 formality_rust::grammar::FnBody::MiniRust(body) => {
-                    mini_rust_check::check_body(&env, &fn_assumptions, body)?;
+                    self.check_body(&env, &output_ty, &fn_assumptions, body)?;
                 }
             }
         }
diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs
index cee76cef..80f16980 100644
--- a/crates/formality-check/src/lib.rs
+++ b/crates/formality-check/src/lib.rs
@@ -1,7 +1,5 @@
 #![allow(dead_code)]
 
-use formality_types::rust::FormalityLang;
-
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
@@ -13,7 +11,7 @@ use formality_rust::{
 };
 use formality_types::grammar::{Fallible, Wcs};
 
-mod mini_rust_check;;
+mod mini_rust_check;
 
 /// Check all crates in the program. The crates must be in dependency order
 /// such that any prefix of the crates is a complete program.
diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index d3d6075c..3d9b1a01 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,4 +1,4 @@
-use formality_core::{term, Fallible, Map, Upcast};
+use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
 use formality_rust::grammar::minirust::{self, LocalId};
 use formality_types::grammar::{Ty, Wcs, Relation};
@@ -39,7 +39,7 @@ impl Check<'_> {
         )?;
 
         let env = TypeckEnv {
-            env,
+            env: env.clone(),
             output_ty,
             local_variables,
         };
@@ -57,43 +57,47 @@ impl Check<'_> {
             self.check_statement(env, statement)?;
         }
 
-        self.check_terminator(&block.terminator)?;
+        self.check_terminator(env, &block.terminator)?;
 
         Ok(())
     }
 
-    fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(&self, _env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
         match statement {
-            minirust::Statement::Assign(place_expression, value_expression) => {
+            minirust::Statement::Assign(_place_expression, _value_expression) => {
                 // FIXME: check that the place and value are well-formed
                 // FIXME: check that the type of the value is a subtype of the place's type
+                todo!();
             }
-            minirust::Statement::PlaceMention(place_expression) => {
+            minirust::Statement::PlaceMention(_place_expression) => {
                 // FIXME: check that the place is well-formed
                 // FIXME: check that access the place is allowed per borrowck rules
+                todo!();
             }
         }
     }
 
-    fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
+    fn check_terminator(&self, _env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
         match terminator {
-            minirust::Terminator::Goto(bb_id) => {
+            minirust::Terminator::Goto(_bb_id) => {
                 // FIXME: Check that the basic block `bb_id` exists
+                todo!();
             }
-            minirust::Terminator::Call { callee, arguments, ret, next_block } => {
+            minirust::Terminator::Call { callee:_, generic_arguments:_, arguments:_, ret:_, next_block:_ } => {
                 // FIXME: check that the callee is something callable
                 // FIXME: check that the arguments are well formed and their types are subtypes of the expected argument types
                 // FIXME: check that the next block is valid
                 // FIXME: check that the fn's declared return type is a subtype of the type of the local variable `ret`
+                todo!();
             }
             minirust::Terminator::Return => {
                 // FIXME: Check that the return local variable has been initialized
+                todo!();
             }
         }
     }
 }
 
-#[term]
 struct TypeckEnv {
     env: Env,
 
diff --git a/src/lib.rs b/src/lib.rs
index c71cfac1..1442d53b 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,5 +1,3 @@
-#![feature(control_flow_enum)]
-
 use std::{path::PathBuf, sync::Arc};
 
 use clap::Parser;

From 829d15bcda85adf68813778f2dd43292e233212d Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 2 Jul 2025 11:48:24 +0200
Subject: [PATCH 02/42] Add some comments

---
 crates/formality-rust/src/grammar/minirust.rs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 69ff1cfe..9b2fe94a 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -63,6 +63,7 @@ pub enum Statement {
     #[grammar($v0 = $v1;)]
     Assign(PlaceExpression, ValueExpression),
 
+    // Represent let _ = place;
     #[grammar($v0;)]
     PlaceMention(PlaceExpression),
 
@@ -89,14 +90,19 @@ pub enum Terminator {
     //    call foo.add<u32>(x, y)
     #[grammar(call $callee $<?generic_arguments> $(arguments) -> $ret $:goto $next_block)]
     Call {
+        /// What function or method to call.
         callee: ValueExpression,
         // cc: CallingConvention,
         generic_arguments: Vec<Parameter>,
+        /// The function arguments to pass.
         arguments: Vec<ArgumentExpression>,
+        /// The place to put the return value into.
         ret: PlaceExpression,
+        /// The block to jump to when this call returns.
         next_block: Option<BbId>,
     },
 
+    /// Return from the current function.
     #[grammar(return)]
     Return,
 }

From 8f6e5f57db5285b8b22fcab0ffb13132eee0678a Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 2 Jul 2025 12:11:48 +0200
Subject: [PATCH 03/42] Check if the place expression is well-formed

---
 crates/formality-check/src/mini_rust_check.rs | 32 ++++++++++++++-----
 1 file changed, 24 insertions(+), 8 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 3d9b1a01..52d4915a 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,8 +1,10 @@
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
-use formality_rust::grammar::minirust::{self, LocalId};
+use formality_rust::grammar::minirust::{self, LocalId, PlaceExpression};
+use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_types::grammar::{Ty, Wcs, Relation};
 
+use anyhow::bail;
 use crate::Check;
 
 impl Check<'_> {
@@ -62,19 +64,19 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_statement(&self, _env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
         match statement {
-            minirust::Statement::Assign(_place_expression, _value_expression) => {
-                // FIXME: check that the place and value are well-formed
+            minirust::Statement::Assign(place_expression, _value_expression) => {
+                self.check_place(env, place_expression)?;
+                // FIXME: check that the value are well-formed
                 // FIXME: check that the type of the value is a subtype of the place's type
-                todo!();
             }
-            minirust::Statement::PlaceMention(_place_expression) => {
-                // FIXME: check that the place is well-formed
+            minirust::Statement::PlaceMention(place_expression) => {
+                self.check_place(env, place_expression)?;
                 // FIXME: check that access the place is allowed per borrowck rules
-                todo!();
             }
         }
+        Ok(())
     }
 
     fn check_terminator(&self, _env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
@@ -96,6 +98,20 @@ impl Check<'_> {
             }
         }
     }
+
+    // Check if the place expression is well-formed.
+    // FIXME: there might be a way to use prove_goal for this.
+    fn check_place(&self, env: &TypeckEnv, place: &PlaceExpression) -> Fallible<()> {
+        match place {
+            Local(local_id) => {
+                if !env.local_variables.iter().any(|(declared_local_id, _)| declared_local_id == local_id) {
+                    bail!("PlaceExpression::Local: unknown local name") 
+                }
+            }
+        }
+        Ok(())
+
+    }
 }
 
 struct TypeckEnv {

From 93b4a79c34c3f2f75506ac0d4bb29651f9b1ac3c Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 2 Jul 2025 13:40:45 +0200
Subject: [PATCH 04/42] Check if the value expression is well-formed

---
 crates/formality-check/src/mini_rust_check.rs | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 52d4915a..39100462 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,7 +1,8 @@
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
-use formality_rust::grammar::minirust::{self, LocalId, PlaceExpression};
+use formality_rust::grammar::minirust::{self, LocalId, PlaceExpression, ValueExpression};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
+use formality_rust::grammar::minirust::ValueExpression::Load;
 use formality_types::grammar::{Ty, Wcs, Relation};
 
 use anyhow::bail;
@@ -66,9 +67,9 @@ impl Check<'_> {
 
     fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
         match statement {
-            minirust::Statement::Assign(place_expression, _value_expression) => {
+            minirust::Statement::Assign(place_expression, value_expression) => {
                 self.check_place(env, place_expression)?;
-                // FIXME: check that the value are well-formed
+                self.check_value(env, value_expression)?;
                 // FIXME: check that the type of the value is a subtype of the place's type
             }
             minirust::Statement::PlaceMention(place_expression) => {
@@ -110,7 +111,17 @@ impl Check<'_> {
             }
         }
         Ok(())
+    }
 
+    // Check if the value expression is well-formed.
+    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<()> {
+        match value {
+            Load(place_expression) => {
+                self.check_place(env, place_expression)?;
+                // FIXME(tiif): minirust checks if the type of the value is sized, maybe we should do that.
+            }
+        }
+        Ok(())
     }
 }
 

From e187afbb29079240b4c6e545e11ab61471f0e8fc Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 2 Jul 2025 14:13:40 +0200
Subject: [PATCH 05/42] Check if the value type is the subtype of place type

---
 crates/formality-check/src/mini_rust_check.rs | 45 ++++++++++++-------
 1 file changed, 28 insertions(+), 17 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 39100462..1cfe11d1 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -49,15 +49,15 @@ impl Check<'_> {
 
         // (3) Check statements in body are valid
         for block in &body.blocks {
-            self.check_block(&env, block)?;
+            self.check_block(&env, fn_assumptions, block)?;
         }
 
         Ok(())
     }
     
-    fn check_block(&self, env: &TypeckEnv, block: &minirust::BasicBlock) -> Fallible<()> {
+    fn check_block(&self, env: &TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock) -> Fallible<()> {
         for statement in  &block.statements {
-            self.check_statement(env, statement)?;
+            self.check_statement(env, fn_assumptions, statement)?;
         }
 
         self.check_terminator(env, &block.terminator)?;
@@ -65,15 +65,23 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement) -> Fallible<()> {
         match statement {
             minirust::Statement::Assign(place_expression, value_expression) => {
-                self.check_place(env, place_expression)?;
-                self.check_value(env, value_expression)?;
-                // FIXME: check that the type of the value is a subtype of the place's type
+                // Check if the place expression is well-formed.
+                let place_ty = self.check_place(typeck_env, place_expression)?;
+                // Check if the value expression is well-formed.
+                let value_ty = self.check_value(typeck_env, value_expression)?;
+                // Check that the type of the value is a subtype of the place's type
+                self.prove_goal(
+                    &typeck_env.env,
+                    fn_assumptions,
+                    Relation::sub(value_ty, place_ty),
+                )?;
             }
             minirust::Statement::PlaceMention(place_expression) => {
-                self.check_place(env, place_expression)?;
+                // Check if the place expression is well-formed.
+                self.check_place(typeck_env, place_expression)?;
                 // FIXME: check that access the place is allowed per borrowck rules
             }
         }
@@ -100,28 +108,31 @@ impl Check<'_> {
         }
     }
 
-    // Check if the place expression is well-formed.
+    // Check if the place expression is well-formed, and return the type of the place expression.
     // FIXME: there might be a way to use prove_goal for this.
-    fn check_place(&self, env: &TypeckEnv, place: &PlaceExpression) -> Fallible<()> {
+    fn check_place(&self, env: &TypeckEnv, place: &PlaceExpression) -> Fallible<Ty> {
+        let place_ty;
         match place {
             Local(local_id) => {
-                if !env.local_variables.iter().any(|(declared_local_id, _)| declared_local_id == local_id) {
+                let Some((_, ty)) = env.local_variables.iter().find(|(declared_local_id, _)| *declared_local_id == local_id) else {
                     bail!("PlaceExpression::Local: unknown local name") 
-                }
+                };
+                place_ty = ty;
             }
         }
-        Ok(())
+        Ok(place_ty.clone())
     }
 
-    // Check if the value expression is well-formed.
-    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<()> {
+    // Check if the value expression is well-formed, and return the type of the value expression.
+    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
+        let value_ty;
         match value {
             Load(place_expression) => {
-                self.check_place(env, place_expression)?;
+                value_ty = self.check_place(env, place_expression)?;
                 // FIXME(tiif): minirust checks if the type of the value is sized, maybe we should do that.
             }
         }
-        Ok(())
+        Ok(value_ty)
     }
 }
 

From f6e80ec2a2be35d14778b5ee8712f354c276c058 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 3 Jul 2025 11:53:16 +0200
Subject: [PATCH 06/42] Pass down the function information in a crate (try to
 improve this later)

---
 crates/formality-check/src/fns.rs             |  8 +++--
 crates/formality-check/src/impls.rs           | 11 ++++---
 crates/formality-check/src/lib.rs             | 12 ++++----
 crates/formality-check/src/mini_rust_check.rs | 29 ++++++++++++-------
 crates/formality-check/src/traits.rs          | 12 ++++----
 crates/formality-rust/src/grammar/minirust.rs |  6 ++--
 6 files changed, 47 insertions(+), 31 deletions(-)

diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs
index b09949d2..bd498c42 100644
--- a/crates/formality-check/src/fns.rs
+++ b/crates/formality-check/src/fns.rs
@@ -6,11 +6,12 @@ use formality_rust::{
 use formality_types::grammar::{Fallible, Wcs};
 
 use crate::Check;
+use crate::CrateItem;
 
 impl Check<'_> {
     /// A "free function" is a free-standing function that is not part of an impl.
-    pub(crate) fn check_free_fn(&self, f: &Fn) -> Fallible<()> {
-        self.check_fn(&Env::default(), Wcs::t(), f)
+    pub(crate) fn check_free_fn(&self, f: &Fn, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+        self.check_fn(&Env::default(), Wcs::t(), f, all_fn)
     }
 
     /// Invoked for both free functions and methods.
@@ -25,6 +26,7 @@ impl Check<'_> {
         in_env: &Env,
         in_assumptions: impl ToWcs,
         f: &Fn,
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         let in_assumptions = in_assumptions.to_wcs();
 
@@ -71,7 +73,7 @@ impl Check<'_> {
                     // A trusted function body is assumed to be valid, all set.
                 }
                 formality_rust::grammar::FnBody::MiniRust(body) => {
-                    self.check_body(&env, &output_ty, &fn_assumptions, body)?;
+                    self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn)?;
                 }
             }
         }
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index a6241140..ae7f70dc 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -15,10 +15,11 @@ use formality_types::{
     grammar::{Binder, Fallible, Relation, Substitution, Wcs},
     rust::Term,
 };
+use crate::CrateItem;
 
 impl super::Check<'_> {
     #[context("check_trait_impl({trait_impl:?})")]
-    pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> {
+    pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         let TraitImpl { binder, safety: _ } = trait_impl;
 
         let mut env = Env::default();
@@ -48,7 +49,7 @@ impl super::Check<'_> {
         self.check_safety_matches(trait_decl, trait_impl)?;
 
         for impl_item in &impl_items {
-            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
+            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, all_fn)?;
         }
 
         Ok(())
@@ -101,6 +102,7 @@ impl super::Check<'_> {
         assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
+        all_fn: &Vec<CrateItem>
     ) -> Fallible<()> {
         let assumptions: Wcs = assumptions.to_wcs();
         assert!(
@@ -108,7 +110,7 @@ impl super::Check<'_> {
         );
 
         match impl_item {
-            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v),
+            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v, all_fn),
             ImplItem::AssociatedTyValue(v) => {
                 self.check_associated_ty_value(env, assumptions, trait_items, v)
             }
@@ -121,6 +123,7 @@ impl super::Check<'_> {
         impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
+        all_fn: &Vec<CrateItem>
     ) -> Fallible<()> {
         let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
@@ -139,7 +142,7 @@ impl super::Check<'_> {
 
         tracing::debug!(?ti_fn);
 
-        self.check_fn(env, &impl_assumptions, ii_fn)?;
+        self.check_fn(env, &impl_assumptions, ii_fn, all_fn)?;
 
         let mut env = env.clone();
         let (
diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs
index 80f16980..a71171ba 100644
--- a/crates/formality-check/src/lib.rs
+++ b/crates/formality-check/src/lib.rs
@@ -61,11 +61,13 @@ impl Check<'_> {
 
     fn check_current_crate(&self, c: &Crate) -> Fallible<()> {
         let Crate { id: _, items } = c;
+        // Collect all fn informatiion from current crate.
+        let all_fn: Vec<CrateItem> = c.items.clone().into_iter().filter(|item,| matches!(item, CrateItem::Fn(_))).collect();
 
         self.check_for_duplicate_items()?;
 
         for item in items {
-            self.check_crate_item(item)?;
+            self.check_crate_item(item, &all_fn)?;
         }
 
         self.check_coherence(c)?;
@@ -109,13 +111,13 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_crate_item(&self, c: &CrateItem) -> Fallible<()> {
+    fn check_crate_item(&self, c: &CrateItem, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match c {
-            CrateItem::Trait(v) => self.check_trait(v),
-            CrateItem::TraitImpl(v) => self.check_trait_impl(v),
+            CrateItem::Trait(v) => self.check_trait(v, all_fn),
+            CrateItem::TraitImpl(v) => self.check_trait_impl(v, all_fn),
             CrateItem::Struct(s) => self.check_adt(&s.to_adt()),
             CrateItem::Enum(e) => self.check_adt(&e.to_adt()),
-            CrateItem::Fn(f) => self.check_free_fn(f),
+            CrateItem::Fn(f) => self.check_free_fn(f, all_fn),
             CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),
             CrateItem::Test(t) => self.check_test(t),
         }
diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 1cfe11d1..1d95d88d 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -2,11 +2,12 @@ use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
 use formality_rust::grammar::minirust::{self, LocalId, PlaceExpression, ValueExpression};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
-use formality_rust::grammar::minirust::ValueExpression::Load;
+use formality_rust::grammar::minirust::ValueExpression::{Load, Fn};
 use formality_types::grammar::{Ty, Wcs, Relation};
 
 use anyhow::bail;
 use crate::Check;
+use crate::CrateItem;
 
 impl Check<'_> {
     pub(crate) fn check_body(
@@ -15,6 +16,7 @@ impl Check<'_> {
         output_ty: impl Upcast<Ty>,
         fn_assumptions: &Wcs,
         body: minirust::Body,
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         // Type-check:
         //
@@ -49,29 +51,29 @@ impl Check<'_> {
 
         // (3) Check statements in body are valid
         for block in &body.blocks {
-            self.check_block(&env, fn_assumptions, block)?;
+            self.check_block(&env, fn_assumptions, block, all_fn)?;
         }
 
         Ok(())
     }
     
-    fn check_block(&self, env: &TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock) -> Fallible<()> {
+    fn check_block(&self, env: &TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         for statement in  &block.statements {
-            self.check_statement(env, fn_assumptions, statement)?;
+            self.check_statement(env, fn_assumptions, statement, all_fn)?;
         }
 
-        self.check_terminator(env, &block.terminator)?;
+        self.check_terminator(env, &block.terminator, all_fn)?;
 
         Ok(())
     }
 
-    fn check_statement(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match statement {
             minirust::Statement::Assign(place_expression, value_expression) => {
                 // Check if the place expression is well-formed.
                 let place_ty = self.check_place(typeck_env, place_expression)?;
                 // Check if the value expression is well-formed.
-                let value_ty = self.check_value(typeck_env, value_expression)?;
+                let value_ty = self.check_value(typeck_env, value_expression, all_fn)?;
                 // Check that the type of the value is a subtype of the place's type
                 self.prove_goal(
                     &typeck_env.env,
@@ -88,14 +90,15 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_terminator(&self, _env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
+    fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match terminator {
             minirust::Terminator::Goto(_bb_id) => {
                 // FIXME: Check that the basic block `bb_id` exists
                 todo!();
             }
-            minirust::Terminator::Call { callee:_, generic_arguments:_, arguments:_, ret:_, next_block:_ } => {
-                // FIXME: check that the callee is something callable
+            minirust::Terminator::Call { callee, generic_arguments:_, arguments:_, ret:_, next_block:_ } => {
+                // Function is part of the value expression, so we will check if the function exists in check_value.
+                self.check_value(env, callee, all_fn)?;
                 // FIXME: check that the arguments are well formed and their types are subtypes of the expected argument types
                 // FIXME: check that the next block is valid
                 // FIXME: check that the fn's declared return type is a subtype of the type of the local variable `ret`
@@ -124,13 +127,17 @@ impl Check<'_> {
     }
 
     // Check if the value expression is well-formed, and return the type of the value expression.
-    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
+    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression, _all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
         let value_ty;
         match value {
             Load(place_expression) => {
                 value_ty = self.check_place(env, place_expression)?;
                 // FIXME(tiif): minirust checks if the type of the value is sized, maybe we should do that.
             }
+            Fn(_fn_value) => {
+                // Check if the function is in the crate
+                todo!() 
+            }
         }
         Ok(value_ty)
     }
diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs
index d319f652..6f2f27c1 100644
--- a/crates/formality-check/src/traits.rs
+++ b/crates/formality-check/src/traits.rs
@@ -6,10 +6,11 @@ use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, Fn, Trait, TraitBoundData, TraitItem, WhereClause,
 };
 use formality_types::grammar::Fallible;
+use crate::CrateItem;
 
 impl super::Check<'_> {
     #[context("check_trait({:?})", t.id)]
-    pub(super) fn check_trait(&self, t: &Trait) -> Fallible<()> {
+    pub(super) fn check_trait(&self, t: &Trait, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         let Trait {
             safety: _,
             id: _,
@@ -27,7 +28,7 @@ impl super::Check<'_> {
         self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
         for trait_item in &trait_items {
-            self.check_trait_item(&env, &where_clauses, trait_item)?;
+            self.check_trait_item(&env, &where_clauses, trait_item, all_fn)?;
         }
 
         Ok(())
@@ -62,15 +63,16 @@ impl super::Check<'_> {
         env: &Env,
         where_clauses: &[WhereClause],
         trait_item: &TraitItem,
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         match trait_item {
-            TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v),
+            TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v, all_fn),
             TraitItem::AssociatedTy(v) => self.check_associated_ty(env, where_clauses, v),
         }
     }
 
-    fn check_fn_in_trait(&self, env: &Env, where_clauses: &[WhereClause], f: &Fn) -> Fallible<()> {
-        self.check_fn(env, where_clauses, f)
+    fn check_fn_in_trait(&self, env: &Env, where_clauses: &[WhereClause], f: &Fn, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+        self.check_fn(env, where_clauses, f, all_fn)
     }
 
     fn check_associated_ty(
diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 9b2fe94a..0f3c9dc5 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -3,6 +3,8 @@ use formality_core::id;
 use formality_macros::term;
 use formality_types::grammar::{Parameter, Ty};
 
+use crate::grammar::Fn;
+
 // This definition is based on [MiniRust](https://github.com/minirust/minirust/blob/master/spec/lang/syntax.md).
 
 id!(BbId);
@@ -115,7 +117,7 @@ pub enum ArgumentExpression {
 
 #[term]
 pub enum ValueExpression {
-    // Const
+    Fn(Fn),
     // #[grammar($(v0) as $v1)]
     // Tuple(Vec<ValueExpression>, Ty),
     // Union
@@ -136,5 +138,3 @@ pub enum PlaceExpression {
     // Index
     // Downcast
 }
-
-

From b3e15aafe188c67b566cc19533f5e911a24b7674 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 3 Jul 2025 13:12:48 +0200
Subject: [PATCH 07/42] Check if the function called is in current crate

---
 crates/formality-check/src/mini_rust_check.rs | 24 +++++++++++++++----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 1d95d88d..f4edb9dd 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -127,19 +127,33 @@ impl Check<'_> {
     }
 
     // Check if the value expression is well-formed, and return the type of the value expression.
-    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression, _all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
+    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression, all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
         let value_ty;
         match value {
             Load(place_expression) => {
                 value_ty = self.check_place(env, place_expression)?;
+                Ok(value_ty)
                 // FIXME(tiif): minirust checks if the type of the value is sized, maybe we should do that.
             }
-            Fn(_fn_value) => {
-                // Check if the function is in the crate
-                todo!() 
+            // Check if the function called is in declared in current crate.
+            // FIXME (tiif): tidy up the code here
+            Fn(fn_called) => {
+                for item in all_fn {
+                    match item {
+                        CrateItem::Fn(fn_declared) => {
+                            if fn_called == fn_declared {
+                                value_ty = env.output_ty.clone();
+                                return Ok(value_ty);
+                            }
+                        }
+                        _ => {
+                            bail!("only CrateItem::Function should be here")
+                        }
+                    }
+                }
+               bail!("The function called is not declared in current crate")
             }
         }
-        Ok(value_ty)
     }
 }
 

From 4593f35e337f7e58d9718dddfc6c9397b6d1705a Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 3 Jul 2025 13:38:49 +0200
Subject: [PATCH 08/42] Check argument expression

---
 crates/formality-check/src/mini_rust_check.rs | 42 +++++++++++++++----
 1 file changed, 34 insertions(+), 8 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index f4edb9dd..b8ad7115 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,8 +1,9 @@
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
-use formality_rust::grammar::minirust::{self, LocalId, PlaceExpression, ValueExpression};
+use formality_rust::grammar::minirust::{self, ArgumentExpression, LocalId, PlaceExpression, ValueExpression};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_rust::grammar::minirust::ValueExpression::{Load, Fn};
+use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
 use formality_types::grammar::{Ty, Wcs, Relation};
 
 use anyhow::bail;
@@ -62,7 +63,7 @@ impl Check<'_> {
             self.check_statement(env, fn_assumptions, statement, all_fn)?;
         }
 
-        self.check_terminator(env, &block.terminator, all_fn)?;
+        self.check_terminator(env, fn_assumptions, &block.terminator, all_fn)?;
 
         Ok(())
     }
@@ -90,25 +91,37 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_terminator(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs, terminator: &minirust::Terminator, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match terminator {
             minirust::Terminator::Goto(_bb_id) => {
                 // FIXME: Check that the basic block `bb_id` exists
                 todo!();
             }
-            minirust::Terminator::Call { callee, generic_arguments:_, arguments:_, ret:_, next_block:_ } => {
+            minirust::Terminator::Call { callee, generic_arguments:_, arguments, ret, next_block:_ } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
-                self.check_value(env, callee, all_fn)?;
-                // FIXME: check that the arguments are well formed and their types are subtypes of the expected argument types
+                self.check_value(typeck_env, callee, all_fn)?;
+                // FIXME: Check that the arguments are well formed and their types are subtypes of the expected argument types
+                for argument in arguments {
+                    let _actual_ty = self.check_argument_expression(typeck_env, argument, all_fn);
+                    // FIXME(tiif): we don't have the expected argument type information yet?
+                    let _expect_ty:Ty = todo!();
+                }
+                // Check if ret is well-formed. 
+                let actual_return_ty = self.check_place(typeck_env, ret)?;
+                // Check that the fn's declared return type is a subtype of the type of the local variable `ret`
+                self.prove_goal(
+                    &typeck_env.env,
+                    fn_assumptions,
+                    Relation::sub( &typeck_env.output_ty, &actual_return_ty),
+                )?;
                 // FIXME: check that the next block is valid
-                // FIXME: check that the fn's declared return type is a subtype of the type of the local variable `ret`
-                todo!();
             }
             minirust::Terminator::Return => {
                 // FIXME: Check that the return local variable has been initialized
                 todo!();
             }
         }
+        Ok(())
     }
 
     // Check if the place expression is well-formed, and return the type of the place expression.
@@ -155,6 +168,19 @@ impl Check<'_> {
             }
         }
     }
+
+    fn check_argument_expression(&self, env: &TypeckEnv, arg_expr: &ArgumentExpression, all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
+        let ty;
+        match arg_expr {
+            ByValue(val_expr) => {
+                ty = self.check_value(env, val_expr, all_fn)?;
+            },
+            InPlace(place_expr) => {
+                ty = self.check_place(env, place_expr)?;
+            }
+        }
+        Ok(ty)
+    }
 }
 
 struct TypeckEnv {

From d1b93634f1f1d76ec19f44ccb90f88dc12acbc2d Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 3 Jul 2025 13:45:53 +0200
Subject: [PATCH 09/42] Add some comments

---
 crates/formality-check/src/mini_rust_check.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index b8ad7115..475d814c 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -103,8 +103,9 @@ impl Check<'_> {
                 // FIXME: Check that the arguments are well formed and their types are subtypes of the expected argument types
                 for argument in arguments {
                     let _actual_ty = self.check_argument_expression(typeck_env, argument, all_fn);
-                    // FIXME(tiif): we don't have the expected argument type information yet?
+                    // FIXME(tiif): we don't have the expected argument type information yet, need to take it from the declared function. 
                     let _expect_ty:Ty = todo!();
+                    // TODO: check subtyping
                 }
                 // Check if ret is well-formed. 
                 let actual_return_ty = self.check_place(typeck_env, ret)?;

From 0ae046d51df0e7c2a15ee313fdb22b52ab979350 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Fri, 4 Jul 2025 10:20:25 +0200
Subject: [PATCH 10/42] Typeck for basic blocks

---
 crates/formality-check/src/mini_rust_check.rs | 34 ++++++++++++++-----
 1 file changed, 26 insertions(+), 8 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 475d814c..1db8811e 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,6 +1,6 @@
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
-use formality_rust::grammar::minirust::{self, ArgumentExpression, LocalId, PlaceExpression, ValueExpression};
+use formality_rust::grammar::minirust::{self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_rust::grammar::minirust::ValueExpression::{Load, Fn};
 use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
@@ -48,11 +48,12 @@ impl Check<'_> {
             env: env.clone(),
             output_ty,
             local_variables,
+            blocks: body.blocks.clone(),
         };
 
         // (3) Check statements in body are valid
-        for block in &body.blocks {
-            self.check_block(&env, fn_assumptions, block, all_fn)?;
+        for block in body.blocks {
+            self.check_block(&env, fn_assumptions, &block, all_fn)?;
         }
 
         Ok(())
@@ -93,11 +94,11 @@ impl Check<'_> {
 
     fn check_terminator(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs, terminator: &minirust::Terminator, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match terminator {
-            minirust::Terminator::Goto(_bb_id) => {
-                // FIXME: Check that the basic block `bb_id` exists
-                todo!();
+            minirust::Terminator::Goto(bb_id) => {
+                // Check that the basic block `bb_id` exists.
+                self.check_block_exist(typeck_env, bb_id)?;
             }
-            minirust::Terminator::Call { callee, generic_arguments:_, arguments, ret, next_block:_ } => {
+            minirust::Terminator::Call { callee, generic_arguments:_, arguments, ret, next_block } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
                 self.check_value(typeck_env, callee, all_fn)?;
                 // FIXME: Check that the arguments are well formed and their types are subtypes of the expected argument types
@@ -115,7 +116,12 @@ impl Check<'_> {
                     fn_assumptions,
                     Relation::sub( &typeck_env.output_ty, &actual_return_ty),
                 )?;
-                // FIXME: check that the next block is valid
+
+                // Check that the next block is valid.
+                let Some(bb_id) = next_block else {
+                    bail!("There should be next block for Terminator::Call, but it does not exist!");
+                };
+                self.check_block_exist(typeck_env, bb_id)?;
             }
             minirust::Terminator::Return => {
                 // FIXME: Check that the return local variable has been initialized
@@ -182,6 +188,15 @@ impl Check<'_> {
         }
         Ok(ty)
     }
+
+    fn check_block_exist(&self, env: &TypeckEnv, id: &BbId) -> Fallible<()> {
+        for block in env.blocks.iter() {
+            if *id == block.id {
+                return Ok(())
+            }
+        }
+        bail!("Basic block {:?} does not exist", id)
+    }
 }
 
 struct TypeckEnv {
@@ -192,4 +207,7 @@ struct TypeckEnv {
 
     /// Type of each local variable, as declared.
     local_variables: Map<LocalId, Ty>,
+
+    /// All basic blocks of current body.
+    blocks: Vec<BasicBlock>,
 }

From 44d64e0169365ac0828b2539cf76db6842044355 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Fri, 4 Jul 2025 10:49:26 +0200
Subject: [PATCH 11/42] Check if the return place has been initialised

---
 crates/formality-check/src/mini_rust_check.rs | 26 ++++++++++++++-----
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 1db8811e..3ba6f759 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -44,22 +44,24 @@ impl Check<'_> {
             Relation::sub(&local_variables[&body.ret], &output_ty),
         )?;
 
-        let env = TypeckEnv {
+        let mut env = TypeckEnv {
             env: env.clone(),
             output_ty,
             local_variables,
             blocks: body.blocks.clone(),
+            ret_id: body.ret,
+            ret_place_is_initialised: false,
         };
 
         // (3) Check statements in body are valid
         for block in body.blocks {
-            self.check_block(&env, fn_assumptions, &block, all_fn)?;
+            self.check_block(&mut env, fn_assumptions, &block, all_fn)?;
         }
 
         Ok(())
     }
     
-    fn check_block(&self, env: &TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_block(&self, env: &mut TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         for statement in  &block.statements {
             self.check_statement(env, fn_assumptions, statement, all_fn)?;
         }
@@ -69,7 +71,7 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_statement(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_statement(&self, typeck_env: &mut TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match statement {
             minirust::Statement::Assign(place_expression, value_expression) => {
                 // Check if the place expression is well-formed.
@@ -82,6 +84,10 @@ impl Check<'_> {
                     fn_assumptions,
                     Relation::sub(value_ty, place_ty),
                 )?;
+                // Record if the return place has been initialised.
+                if *place_expression == PlaceExpression::Local(typeck_env.ret_id.clone()) {
+                        typeck_env.ret_place_is_initialised = true;
+                }
             }
             minirust::Statement::PlaceMention(place_expression) => {
                 // Check if the place expression is well-formed.
@@ -124,8 +130,10 @@ impl Check<'_> {
                 self.check_block_exist(typeck_env, bb_id)?;
             }
             minirust::Terminator::Return => {
-                // FIXME: Check that the return local variable has been initialized
-                todo!();
+                // Check that the return local variable has been initialized
+                if !typeck_env.ret_place_is_initialised {
+                    bail!("The return local variable has not been initialized.")
+                }
             }
         }
         Ok(())
@@ -210,4 +218,10 @@ struct TypeckEnv {
 
     /// All basic blocks of current body.
     blocks: Vec<BasicBlock>,
+
+    /// local_id of return place,
+    ret_id: LocalId,
+
+    /// Record if the return place has been initialised.
+    ret_place_is_initialised: bool,
 }

From bfa12dbabbebd43c4298e4a27f48642249a848a1 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Fri, 4 Jul 2025 11:20:47 +0200
Subject: [PATCH 12/42] Complete typeck for function arguments

---
 crates/formality-check/src/fns.rs             |  2 +-
 crates/formality-check/src/mini_rust_check.rs | 30 +++++++++++++++++--
 2 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs
index bd498c42..1f3ca059 100644
--- a/crates/formality-check/src/fns.rs
+++ b/crates/formality-check/src/fns.rs
@@ -73,7 +73,7 @@ impl Check<'_> {
                     // A trusted function body is assumed to be valid, all set.
                 }
                 formality_rust::grammar::FnBody::MiniRust(body) => {
-                    self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn)?;
+                    self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn, input_tys)?;
                 }
             }
         }
diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 3ba6f759..72d53acb 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -1,3 +1,5 @@
+use std::iter::zip;
+
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
 use formality_rust::grammar::minirust::{self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression};
@@ -18,6 +20,7 @@ impl Check<'_> {
         fn_assumptions: &Wcs,
         body: minirust::Body,
         all_fn: &Vec<CrateItem>,
+        declared_input_tys: Vec<Ty>,
     ) -> Fallible<()> {
         // Type-check:
         //
@@ -51,6 +54,7 @@ impl Check<'_> {
             blocks: body.blocks.clone(),
             ret_id: body.ret,
             ret_place_is_initialised: false,
+            declared_input_tys,
         };
 
         // (3) Check statements in body are valid
@@ -104,11 +108,28 @@ impl Check<'_> {
                 // Check that the basic block `bb_id` exists.
                 self.check_block_exist(typeck_env, bb_id)?;
             }
-            minirust::Terminator::Call { callee, generic_arguments:_, arguments, ret, next_block } => {
+            minirust::Terminator::Call { callee, generic_arguments:_, arguments: actual_arguments, ret, next_block } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
                 self.check_value(typeck_env, callee, all_fn)?;
-                // FIXME: Check that the arguments are well formed and their types are subtypes of the expected argument types
-                for argument in arguments {
+                // Check if the numbers of arguments passed equals to number of arguments declared.
+                let actual_arg_num = actual_arguments.len();
+                let declared_arg_num = typeck_env.declared_input_tys.len();
+                if actual_arg_num != declared_arg_num {
+                    bail!("The numbers of arguments passed to Terminator::Call is {actual_arg_num}, but the declared function argument number is {declared_arg_num}");
+                }
+                let arguments = zip(typeck_env.declared_input_tys.clone(), actual_arguments);
+                for (declared_ty, actual_argument) in arguments {
+                    // Check if the arguments are well formed.
+                    let actual_ty = self.check_argument_expression(typeck_env, actual_argument, all_fn)?;
+                    // Check if the actual argument type passed in is the subtype of expect argument type.
+                    self.prove_goal(
+                        &typeck_env.env,
+                        fn_assumptions,
+                        Relation::sub( &actual_ty, &declared_ty),
+                    )?;
+
+                }
+                for argument in actual_arguments {
                     let _actual_ty = self.check_argument_expression(typeck_env, argument, all_fn);
                     // FIXME(tiif): we don't have the expected argument type information yet, need to take it from the declared function. 
                     let _expect_ty:Ty = todo!();
@@ -224,4 +245,7 @@ struct TypeckEnv {
 
     /// Record if the return place has been initialised.
     ret_place_is_initialised: bool,
+
+    /// All declared argument type of the function.
+    declared_input_tys: Vec<Ty>,
 }

From b22ac9391bd203e979d84866979186a0a6d3a332 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Fri, 4 Jul 2025 11:25:36 +0200
Subject: [PATCH 13/42] Remove unused code

---
 crates/formality-check/src/mini_rust_check.rs | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 72d53acb..82f17034 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -129,12 +129,6 @@ impl Check<'_> {
                     )?;
 
                 }
-                for argument in actual_arguments {
-                    let _actual_ty = self.check_argument_expression(typeck_env, argument, all_fn);
-                    // FIXME(tiif): we don't have the expected argument type information yet, need to take it from the declared function. 
-                    let _expect_ty:Ty = todo!();
-                    // TODO: check subtyping
-                }
                 // Check if ret is well-formed. 
                 let actual_return_ty = self.check_place(typeck_env, ret)?;
                 // Check that the fn's declared return type is a subtype of the type of the local variable `ret`

From 4a5215879f852ecf3f27687eac59d27b0bf72c84 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 10:47:17 +0200
Subject: [PATCH 14/42] Clean up some code

---
 crates/formality-check/src/mini_rust_check.rs | 53 ++++++++-----------
 1 file changed, 23 insertions(+), 30 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 82f17034..9c5bf15d 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -19,7 +19,7 @@ impl Check<'_> {
         output_ty: impl Upcast<Ty>,
         fn_assumptions: &Wcs,
         body: minirust::Body,
-        all_fn: &Vec<CrateItem>,
+        declared_fn: &Vec<CrateItem>,
         declared_input_tys: Vec<Ty>,
     ) -> Fallible<()> {
         // Type-check:
@@ -55,33 +55,34 @@ impl Check<'_> {
             ret_id: body.ret,
             ret_place_is_initialised: false,
             declared_input_tys,
+            declared_fn: declared_fn.to_vec(),
         };
 
         // (3) Check statements in body are valid
         for block in body.blocks {
-            self.check_block(&mut env, fn_assumptions, &block, all_fn)?;
+            self.check_block(&mut env, fn_assumptions, &block)?;
         }
 
         Ok(())
     }
     
-    fn check_block(&self, env: &mut TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_block(&self, env: &mut TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock) -> Fallible<()> {
         for statement in  &block.statements {
-            self.check_statement(env, fn_assumptions, statement, all_fn)?;
+            self.check_statement(env, fn_assumptions, statement)?;
         }
 
-        self.check_terminator(env, fn_assumptions, &block.terminator, all_fn)?;
+        self.check_terminator(env, fn_assumptions, &block.terminator)?;
 
         Ok(())
     }
 
-    fn check_statement(&self, typeck_env: &mut TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_statement(&self, typeck_env: &mut TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement) -> Fallible<()> {
         match statement {
             minirust::Statement::Assign(place_expression, value_expression) => {
                 // Check if the place expression is well-formed.
                 let place_ty = self.check_place(typeck_env, place_expression)?;
                 // Check if the value expression is well-formed.
-                let value_ty = self.check_value(typeck_env, value_expression, all_fn)?;
+                let value_ty = self.check_value(typeck_env, value_expression)?;
                 // Check that the type of the value is a subtype of the place's type
                 self.prove_goal(
                     &typeck_env.env,
@@ -102,7 +103,7 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_terminator(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs, terminator: &minirust::Terminator, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_terminator(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs, terminator: &minirust::Terminator) -> Fallible<()> {
         match terminator {
             minirust::Terminator::Goto(bb_id) => {
                 // Check that the basic block `bb_id` exists.
@@ -110,7 +111,7 @@ impl Check<'_> {
             }
             minirust::Terminator::Call { callee, generic_arguments:_, arguments: actual_arguments, ret, next_block } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
-                self.check_value(typeck_env, callee, all_fn)?;
+                self.check_value(typeck_env, callee)?;
                 // Check if the numbers of arguments passed equals to number of arguments declared.
                 let actual_arg_num = actual_arguments.len();
                 let declared_arg_num = typeck_env.declared_input_tys.len();
@@ -120,7 +121,7 @@ impl Check<'_> {
                 let arguments = zip(typeck_env.declared_input_tys.clone(), actual_arguments);
                 for (declared_ty, actual_argument) in arguments {
                     // Check if the arguments are well formed.
-                    let actual_ty = self.check_argument_expression(typeck_env, actual_argument, all_fn)?;
+                    let actual_ty = self.check_argument_expression(typeck_env, actual_argument)?;
                     // Check if the actual argument type passed in is the subtype of expect argument type.
                     self.prove_goal(
                         &typeck_env.env,
@@ -155,11 +156,11 @@ impl Check<'_> {
     }
 
     // Check if the place expression is well-formed, and return the type of the place expression.
-    // FIXME: there might be a way to use prove_goal for this.
     fn check_place(&self, env: &TypeckEnv, place: &PlaceExpression) -> Fallible<Ty> {
         let place_ty;
         match place {
             Local(local_id) => {
+                // Check if place id is a valid local id. 
                 let Some((_, ty)) = env.local_variables.iter().find(|(declared_local_id, _)| *declared_local_id == local_id) else {
                     bail!("PlaceExpression::Local: unknown local name") 
                 };
@@ -170,40 +171,29 @@ impl Check<'_> {
     }
 
     // Check if the value expression is well-formed, and return the type of the value expression.
-    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression, all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
+    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
         let value_ty;
         match value {
             Load(place_expression) => {
                 value_ty = self.check_place(env, place_expression)?;
                 Ok(value_ty)
-                // FIXME(tiif): minirust checks if the type of the value is sized, maybe we should do that.
             }
-            // Check if the function called is in declared in current crate.
-            // FIXME (tiif): tidy up the code here
             Fn(fn_called) => {
-                for item in all_fn {
-                    match item {
-                        CrateItem::Fn(fn_declared) => {
-                            if fn_called == fn_declared {
-                                value_ty = env.output_ty.clone();
-                                return Ok(value_ty);
-                            }
-                        }
-                        _ => {
-                            bail!("only CrateItem::Function should be here")
-                        }
-                    }
+                // Check if the function called is in declared in current crate.
+                if let None = env.declared_fn.iter().find(|&item| *item == CrateItem::Fn(fn_called.clone())) {
+                    bail!("The function called is not declared in current crate")
                 }
-               bail!("The function called is not declared in current crate")
+                value_ty = env.output_ty.clone();
+                Ok(value_ty)
             }
         }
     }
 
-    fn check_argument_expression(&self, env: &TypeckEnv, arg_expr: &ArgumentExpression, all_fn: &Vec<CrateItem>) -> Fallible<Ty> {
+    fn check_argument_expression(&self, env: &TypeckEnv, arg_expr: &ArgumentExpression) -> Fallible<Ty> {
         let ty;
         match arg_expr {
             ByValue(val_expr) => {
-                ty = self.check_value(env, val_expr, all_fn)?;
+                ty = self.check_value(env, val_expr)?;
             },
             InPlace(place_expr) => {
                 ty = self.check_place(env, place_expr)?;
@@ -242,4 +232,7 @@ struct TypeckEnv {
 
     /// All declared argument type of the function.
     declared_input_tys: Vec<Ty>,
+
+    /// All declared fn in current crate.
+    declared_fn: Vec<CrateItem>,
 }

From 11c89626fc8a8322077fa35cad1029e79e17a7ba Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 10:58:41 +0200
Subject: [PATCH 15/42] fmt

---
 crates/formality-check/src/fns.rs             |  6 +-
 crates/formality-check/src/impls.rs           | 12 ++-
 crates/formality-check/src/lib.rs             |  7 +-
 crates/formality-check/src/mini_rust_check.rs | 84 +++++++++++++------
 crates/formality-check/src/traits.rs          | 10 ++-
 crates/formality-rust/src/grammar/minirust.rs |  2 -
 6 files changed, 85 insertions(+), 36 deletions(-)

diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs
index 1f3ca059..2f913fc5 100644
--- a/crates/formality-check/src/fns.rs
+++ b/crates/formality-check/src/fns.rs
@@ -15,9 +15,9 @@ impl Check<'_> {
     }
 
     /// Invoked for both free functions and methods.
-    /// 
+    ///
     /// # Parameters
-    /// 
+    ///
     /// * `in_env` -- the environment from the enclosing impl (if any)
     /// * `in_assumptions` -- where-clauses from the enclosing impl (if any)
     /// * `f` -- the function definition
@@ -75,7 +75,7 @@ impl Check<'_> {
                 formality_rust::grammar::FnBody::MiniRust(body) => {
                     self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn, input_tys)?;
                 }
-            }
+            },
         }
 
         Ok(())
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index ae7f70dc..c2beff5f 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -1,5 +1,6 @@
 use anyhow::bail;
 
+use crate::CrateItem;
 use fn_error_context::context;
 use formality_core::Downcasted;
 use formality_prove::{Env, Safety};
@@ -15,11 +16,14 @@ use formality_types::{
     grammar::{Binder, Fallible, Relation, Substitution, Wcs},
     rust::Term,
 };
-use crate::CrateItem;
 
 impl super::Check<'_> {
     #[context("check_trait_impl({trait_impl:?})")]
-    pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    pub(super) fn check_trait_impl(
+        &self,
+        trait_impl: &TraitImpl,
+        all_fn: &Vec<CrateItem>,
+    ) -> Fallible<()> {
         let TraitImpl { binder, safety: _ } = trait_impl;
 
         let mut env = Env::default();
@@ -102,7 +106,7 @@ impl super::Check<'_> {
         assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
-        all_fn: &Vec<CrateItem>
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         let assumptions: Wcs = assumptions.to_wcs();
         assert!(
@@ -123,7 +127,7 @@ impl super::Check<'_> {
         impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
-        all_fn: &Vec<CrateItem>
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs
index a71171ba..adf52257 100644
--- a/crates/formality-check/src/lib.rs
+++ b/crates/formality-check/src/lib.rs
@@ -62,7 +62,12 @@ impl Check<'_> {
     fn check_current_crate(&self, c: &Crate) -> Fallible<()> {
         let Crate { id: _, items } = c;
         // Collect all fn informatiion from current crate.
-        let all_fn: Vec<CrateItem> = c.items.clone().into_iter().filter(|item,| matches!(item, CrateItem::Fn(_))).collect();
+        let all_fn: Vec<CrateItem> = c
+            .items
+            .clone()
+            .into_iter()
+            .filter(|item| matches!(item, CrateItem::Fn(_)))
+            .collect();
 
         self.check_for_duplicate_items()?;
 
diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 9c5bf15d..399d5c27 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -2,15 +2,17 @@ use std::iter::zip;
 
 use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
-use formality_rust::grammar::minirust::{self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression};
-use formality_rust::grammar::minirust::PlaceExpression::Local;
-use formality_rust::grammar::minirust::ValueExpression::{Load, Fn};
 use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
-use formality_types::grammar::{Ty, Wcs, Relation};
+use formality_rust::grammar::minirust::PlaceExpression::Local;
+use formality_rust::grammar::minirust::ValueExpression::{Fn, Load};
+use formality_rust::grammar::minirust::{
+    self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
+};
+use formality_types::grammar::{Relation, Ty, Wcs};
 
-use anyhow::bail;
 use crate::Check;
 use crate::CrateItem;
+use anyhow::bail;
 
 impl Check<'_> {
     pub(crate) fn check_body(
@@ -65,9 +67,14 @@ impl Check<'_> {
 
         Ok(())
     }
-    
-    fn check_block(&self, env: &mut TypeckEnv, fn_assumptions: &Wcs, block: &minirust::BasicBlock) -> Fallible<()> {
-        for statement in  &block.statements {
+
+    fn check_block(
+        &self,
+        env: &mut TypeckEnv,
+        fn_assumptions: &Wcs,
+        block: &minirust::BasicBlock,
+    ) -> Fallible<()> {
+        for statement in &block.statements {
             self.check_statement(env, fn_assumptions, statement)?;
         }
 
@@ -76,7 +83,12 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_statement(&self, typeck_env: &mut TypeckEnv, fn_assumptions: &Wcs,statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(
+        &self,
+        typeck_env: &mut TypeckEnv,
+        fn_assumptions: &Wcs,
+        statement: &minirust::Statement,
+    ) -> Fallible<()> {
         match statement {
             minirust::Statement::Assign(place_expression, value_expression) => {
                 // Check if the place expression is well-formed.
@@ -91,7 +103,7 @@ impl Check<'_> {
                 )?;
                 // Record if the return place has been initialised.
                 if *place_expression == PlaceExpression::Local(typeck_env.ret_id.clone()) {
-                        typeck_env.ret_place_is_initialised = true;
+                    typeck_env.ret_place_is_initialised = true;
                 }
             }
             minirust::Statement::PlaceMention(place_expression) => {
@@ -103,13 +115,24 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_terminator(&self, typeck_env: &TypeckEnv, fn_assumptions: &Wcs, terminator: &minirust::Terminator) -> Fallible<()> {
+    fn check_terminator(
+        &self,
+        typeck_env: &TypeckEnv,
+        fn_assumptions: &Wcs,
+        terminator: &minirust::Terminator,
+    ) -> Fallible<()> {
         match terminator {
             minirust::Terminator::Goto(bb_id) => {
                 // Check that the basic block `bb_id` exists.
                 self.check_block_exist(typeck_env, bb_id)?;
             }
-            minirust::Terminator::Call { callee, generic_arguments:_, arguments: actual_arguments, ret, next_block } => {
+            minirust::Terminator::Call {
+                callee,
+                generic_arguments: _,
+                arguments: actual_arguments,
+                ret,
+                next_block,
+            } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
                 self.check_value(typeck_env, callee)?;
                 // Check if the numbers of arguments passed equals to number of arguments declared.
@@ -126,22 +149,23 @@ impl Check<'_> {
                     self.prove_goal(
                         &typeck_env.env,
                         fn_assumptions,
-                        Relation::sub( &actual_ty, &declared_ty),
+                        Relation::sub(&actual_ty, &declared_ty),
                     )?;
-
                 }
-                // Check if ret is well-formed. 
+                // Check if ret is well-formed.
                 let actual_return_ty = self.check_place(typeck_env, ret)?;
                 // Check that the fn's declared return type is a subtype of the type of the local variable `ret`
                 self.prove_goal(
                     &typeck_env.env,
                     fn_assumptions,
-                    Relation::sub( &typeck_env.output_ty, &actual_return_ty),
+                    Relation::sub(&typeck_env.output_ty, &actual_return_ty),
                 )?;
 
                 // Check that the next block is valid.
                 let Some(bb_id) = next_block else {
-                    bail!("There should be next block for Terminator::Call, but it does not exist!");
+                    bail!(
+                        "There should be next block for Terminator::Call, but it does not exist!"
+                    );
                 };
                 self.check_block_exist(typeck_env, bb_id)?;
             }
@@ -160,9 +184,13 @@ impl Check<'_> {
         let place_ty;
         match place {
             Local(local_id) => {
-                // Check if place id is a valid local id. 
-                let Some((_, ty)) = env.local_variables.iter().find(|(declared_local_id, _)| *declared_local_id == local_id) else {
-                    bail!("PlaceExpression::Local: unknown local name") 
+                // Check if place id is a valid local id.
+                let Some((_, ty)) = env
+                    .local_variables
+                    .iter()
+                    .find(|(declared_local_id, _)| *declared_local_id == local_id)
+                else {
+                    bail!("PlaceExpression::Local: unknown local name")
                 };
                 place_ty = ty;
             }
@@ -180,7 +208,11 @@ impl Check<'_> {
             }
             Fn(fn_called) => {
                 // Check if the function called is in declared in current crate.
-                if let None = env.declared_fn.iter().find(|&item| *item == CrateItem::Fn(fn_called.clone())) {
+                if let None = env
+                    .declared_fn
+                    .iter()
+                    .find(|&item| *item == CrateItem::Fn(fn_called.clone()))
+                {
                     bail!("The function called is not declared in current crate")
                 }
                 value_ty = env.output_ty.clone();
@@ -189,12 +221,16 @@ impl Check<'_> {
         }
     }
 
-    fn check_argument_expression(&self, env: &TypeckEnv, arg_expr: &ArgumentExpression) -> Fallible<Ty> {
+    fn check_argument_expression(
+        &self,
+        env: &TypeckEnv,
+        arg_expr: &ArgumentExpression,
+    ) -> Fallible<Ty> {
         let ty;
         match arg_expr {
             ByValue(val_expr) => {
                 ty = self.check_value(env, val_expr)?;
-            },
+            }
             InPlace(place_expr) => {
                 ty = self.check_place(env, place_expr)?;
             }
@@ -205,7 +241,7 @@ impl Check<'_> {
     fn check_block_exist(&self, env: &TypeckEnv, id: &BbId) -> Fallible<()> {
         for block in env.blocks.iter() {
             if *id == block.id {
-                return Ok(())
+                return Ok(());
             }
         }
         bail!("Basic block {:?} does not exist", id)
diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs
index 6f2f27c1..9a9a49d6 100644
--- a/crates/formality-check/src/traits.rs
+++ b/crates/formality-check/src/traits.rs
@@ -1,3 +1,4 @@
+use crate::CrateItem;
 use anyhow::bail;
 use fn_error_context::context;
 use formality_core::Set;
@@ -6,7 +7,6 @@ use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, Fn, Trait, TraitBoundData, TraitItem, WhereClause,
 };
 use formality_types::grammar::Fallible;
-use crate::CrateItem;
 
 impl super::Check<'_> {
     #[context("check_trait({:?})", t.id)]
@@ -71,7 +71,13 @@ impl super::Check<'_> {
         }
     }
 
-    fn check_fn_in_trait(&self, env: &Env, where_clauses: &[WhereClause], f: &Fn, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_fn_in_trait(
+        &self,
+        env: &Env,
+        where_clauses: &[WhereClause],
+        f: &Fn,
+        all_fn: &Vec<CrateItem>,
+    ) -> Fallible<()> {
         self.check_fn(env, where_clauses, f, all_fn)
     }
 
diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 0f3c9dc5..6e2f7e9a 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -1,4 +1,3 @@
-
 use formality_core::id;
 use formality_macros::term;
 use formality_types::grammar::{Parameter, Ty};
@@ -68,7 +67,6 @@ pub enum Statement {
     // Represent let _ = place;
     #[grammar($v0;)]
     PlaceMention(PlaceExpression),
-
     // SetDiscriminant
     // Validate
     // Deinit

From eb8173232ac796aa4b43d2388a599e3a95db4fce Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 13:47:55 +0200
Subject: [PATCH 16/42] Use FnId for calling function

---
 crates/formality-check/src/mini_rust_check.rs | 14 +++++++++++---
 crates/formality-rust/src/grammar/minirust.rs |  5 +++--
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 399d5c27..98fba7d0 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -206,12 +206,20 @@ impl Check<'_> {
                 value_ty = self.check_place(env, place_expression)?;
                 Ok(value_ty)
             }
-            Fn(fn_called) => {
+            Fn(fn_id) => {
                 // Check if the function called is in declared in current crate.
-                if let None = env
+                let item = env
                     .declared_fn
                     .iter()
-                    .find(|&item| *item == CrateItem::Fn(fn_called.clone()))
+                    .find(|&item| {
+                        match item {
+                            CrateItem::Fn(fn_declared) => {
+                                return fn_declared.id == *fn_id;
+                            }
+                            _ => false
+                        }
+                    });
+                if item == None
                 {
                     bail!("The function called is not declared in current crate")
                 }
diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 6e2f7e9a..4e8ae6ce 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -2,7 +2,7 @@ use formality_core::id;
 use formality_macros::term;
 use formality_types::grammar::{Parameter, Ty};
 
-use crate::grammar::Fn;
+use crate::grammar::FnId;
 
 // This definition is based on [MiniRust](https://github.com/minirust/minirust/blob/master/spec/lang/syntax.md).
 
@@ -115,7 +115,8 @@ pub enum ArgumentExpression {
 
 #[term]
 pub enum ValueExpression {
-    Fn(Fn),
+    #[grammar(fn $v0)]
+    Fn(FnId),
     // #[grammar($(v0) as $v1)]
     // Tuple(Vec<ValueExpression>, Ty),
     // Union

From 0d2fd54f32c3f3696dc7d7c4c1c41b5acb7a1884 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 14:19:34 +0200
Subject: [PATCH 17/42] Fix some rules

---
 crates/formality-rust/src/grammar/minirust.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 4e8ae6ce..944ba4de 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -51,6 +51,7 @@ pub struct LocalDecl {
 }
 
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
+// FIXME(tiif): for some reason statements is always not required
 #[term($id: ${statements} $terminator;)]
 pub struct BasicBlock {
     pub id: BbId,
@@ -115,7 +116,7 @@ pub enum ArgumentExpression {
 
 #[term]
 pub enum ValueExpression {
-    #[grammar(fn $v0)]
+    #[grammar($v0)]
     Fn(FnId),
     // #[grammar($(v0) as $v1)]
     // Tuple(Vec<ValueExpression>, Ty),
@@ -131,6 +132,8 @@ pub enum ValueExpression {
 
 #[term]
 pub enum PlaceExpression {
+    // FIXME(tiif): if we remove the local keyword, call bar () -> v1 goto bb1; won't work
+    #[grammar(local($v0))]
     Local(LocalId),
     // Deref(Arc<ValueExpression>),
     // Field(Arc<PlaceExpression>, FieldId),

From 45df6fb1c0c1127adcef16ff34929365266422ec Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 14:19:44 +0200
Subject: [PATCH 18/42] Add some tests

---
 src/test/mir_fn_bodies.rs | 100 ++++++++++++++++++++++++++++++++++++++
 src/test/mod.rs           |   1 +
 2 files changed, 101 insertions(+)
 create mode 100644 src/test/mir_fn_bodies.rs

diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
new file mode 100644
index 00000000..7ec2a638
--- /dev/null
+++ b/src/test/mir_fn_bodies.rs
@@ -0,0 +1,100 @@
+
+
+// All the tests are still failing because the parser cannot accept any statement for some reason?
+#[test]
+fn test_assign_statement() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        v1 = v0;
+                    }
+                    return;
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+}
+
+// TODO: we need to add a rule for () <: ()
+#[test]
+fn test_place_mention_statement() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        v0;
+                    }
+                    return;
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+}
+
+
+#[test]
+fn test_goto_terminator() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                    }
+                    goto bb1;
+
+                    bb1: {
+                        v1 = v0;
+                    }
+                    return;
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+    
+}
+
+#[test]
+fn test_call_terminator() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo () -> () = minirust() -> v0 {
+                    let v0: ();
+                    let v1: ();
+                    
+                    bb0: {
+                    }
+                    call bar() -> local(v1) goto bb1;
+
+                    bb1: {}
+                    return;
+                };
+
+                fn bar() -> () = minirust() -> v0 {
+                    let v0: ();
+                    
+                    bb0: {
+                    }
+                    return;
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+
+}
diff --git a/src/test/mod.rs b/src/test/mod.rs
index 327f7d0a..77b14096 100644
--- a/src/test/mod.rs
+++ b/src/test/mod.rs
@@ -6,6 +6,7 @@ mod consts;
 mod decl_safety;
 mod functions;
 mod well_formed_trait_ref;
+mod mir_fn_bodies;
 
 #[test]
 fn parser() {

From fa5fef10ed5a0b2279254654c6db36c5aff04c9e Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 14:43:25 +0200
Subject: [PATCH 19/42] Some hack in the grammar to make grammar works

---
 crates/formality-rust/src/grammar/minirust.rs |  2 +-
 src/test/mir_fn_bodies.rs                     | 48 +++++++++++++------
 2 files changed, 35 insertions(+), 15 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 944ba4de..530f3b7e 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -52,7 +52,7 @@ pub struct LocalDecl {
 
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
 // FIXME(tiif): for some reason statements is always not required
-#[term($id: ${statements} $terminator;)]
+#[term($id: {statement ${statements} $terminator;})]
 pub struct BasicBlock {
     pub id: BbId,
     pub statements: Vec<Statement>,
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 7ec2a638..d3304d0d 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -1,5 +1,4 @@
 
-
 // All the tests are still failing because the parser cannot accept any statement for some reason?
 #[test]
 fn test_assign_statement() {
@@ -11,9 +10,12 @@ fn test_assign_statement() {
                     let v1: u32;
                     
                     bb0: {
-                        v1 = v0;
+                        statement { 
+                            local(v1) = v0;
+                        }
+                        return;
                     }
-                    return;
+                    
                 };
             }
         ]
@@ -32,9 +34,12 @@ fn test_place_mention_statement() {
                     let v1: u32;
                     
                     bb0: {
-                        v0;
+                        statement {
+                            local(v0);
+                        }
+                        return;
                     }
-                    return;
+                    
                 };
             }
         ]
@@ -53,13 +58,17 @@ fn test_goto_terminator() {
                     let v1: u32;
                     
                     bb0: {
+                        statement {}
+                        goto bb1;
                     }
-                    goto bb1;
 
                     bb1: {
-                        v1 = v0;
+                        statement {
+                            local(v1) = v0;
+                        }
+                        return;
                     }
-                    return;
+                    
                 };
             }
         ]
@@ -73,24 +82,35 @@ fn test_call_terminator() {
     crate::assert_ok!(
         [
             crate Foo {
-                fn foo () -> () = minirust() -> v0 {
+                fn foo () -> () = minirust(v1) -> v0 {
                     let v0: ();
                     let v1: ();
                     
                     bb0: {
+                        statement {
+                            local(v0) = v1;
+                        }
+                        call bar() -> local(v1) goto bb1;
                     }
-                    call bar() -> local(v1) goto bb1;
 
-                    bb1: {}
-                    return;
+                    bb1: {
+                        statement {}
+                        return;
+                    }
+                    
                 };
 
-                fn bar() -> () = minirust() -> v0 {
+                fn bar() -> () = minirust(v1) -> v0 {
                     let v0: ();
+                    let v1: ();
                     
                     bb0: {
+                        statement {
+                            local(v0) = v1;
+                        } 
+                        return;
                     }
-                    return;
+                    
                 };
             }
         ]

From 758e04641502b7e8128dc0c1eb791cbfb983281f Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 15:02:01 +0200
Subject: [PATCH 20/42] Apply more hacks to make the syntax works

---
 crates/formality-rust/src/grammar/minirust.rs |  2 ++
 src/test/mir_fn_bodies.rs                     | 30 ++++++++-----------
 2 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 530f3b7e..a88df9c3 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -110,7 +110,9 @@ pub enum Terminator {
 
 #[term]
 pub enum ArgumentExpression {
+    #[grammar(value($v0))]
     ByValue(ValueExpression),
+    #[grammar(place($v0))]
     InPlace(PlaceExpression),
 }
 
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index d3304d0d..dad8b101 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -82,35 +82,31 @@ fn test_call_terminator() {
     crate::assert_ok!(
         [
             crate Foo {
-                fn foo () -> () = minirust(v1) -> v0 {
-                    let v0: ();
-                    let v1: ();
+                fn foo(u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
                     
                     bb0: {
                         statement {
                             local(v0) = v1;
                         }
-                        call bar() -> local(v1) goto bb1;
-                    }
-
-                    bb1: {
-                        statement {}
                         return;
                     }
-                    
                 };
 
-                fn bar() -> () = minirust(v1) -> v0 {
-                    let v0: ();
-                    let v1: ();
-                    
+                fn bar() -> u32 = minirust() -> v0 {
+                    let v0: u32;
+                    let v1: u32; // FIXME(tiif): This might not work because this is not initialised?
+
                     bb0: {
-                        statement {
-                            local(v0) = v1;
-                        } 
-                        return;
+                        statement {}
+                        call foo(place(local(v1))) -> local(v0) goto bb1;
                     }
                     
+                    bb1: {
+                        statement {}
+                        return;
+                    }
                 };
             }
         ]

From ff340382bc9462202860fd1a7718297ac0526083 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 7 Jul 2025 15:02:38 +0200
Subject: [PATCH 21/42] Remove comment

---
 src/test/mir_fn_bodies.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index dad8b101..5e5a293b 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -1,5 +1,4 @@
 
-// All the tests are still failing because the parser cannot accept any statement for some reason?
 #[test]
 fn test_assign_statement() {
     crate::assert_ok!(

From 3ac1659f14bd230c532f63ddfb882f0f65a0b735 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 14:47:00 +0200
Subject: [PATCH 22/42] Change keyword to statements

---
 crates/formality-rust/src/grammar/minirust.rs |  2 +-
 src/test/mir_fn_bodies.rs                     | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index a88df9c3..fc7bce2a 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -52,7 +52,7 @@ pub struct LocalDecl {
 
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
 // FIXME(tiif): for some reason statements is always not required
-#[term($id: {statement ${statements} $terminator;})]
+#[term($id: {statements ${statements} $terminator;})]
 pub struct BasicBlock {
     pub id: BbId,
     pub statements: Vec<Statement>,
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 5e5a293b..a5dba077 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -9,8 +9,8 @@ fn test_assign_statement() {
                     let v1: u32;
                     
                     bb0: {
-                        statement { 
-                            local(v1) = v0;
+                        statements { 
+                            local(v1) = v0; // load(local(v0))
                         }
                         return;
                     }
@@ -33,7 +33,7 @@ fn test_place_mention_statement() {
                     let v1: u32;
                     
                     bb0: {
-                        statement {
+                        statements {
                             local(v0);
                         }
                         return;
@@ -57,13 +57,13 @@ fn test_goto_terminator() {
                     let v1: u32;
                     
                     bb0: {
-                        statement {}
+                        statements {}
                         goto bb1;
                     }
 
                     bb1: {
-                        statement {
-                            local(v1) = v0;
+                        statements {
+                            local(v1) = v0; // load(local(v0))
                         }
                         return;
                     }
@@ -86,7 +86,7 @@ fn test_call_terminator() {
                     let v1: u32;
                     
                     bb0: {
-                        statement {
+                        statements {
                             local(v0) = v1;
                         }
                         return;
@@ -98,12 +98,12 @@ fn test_call_terminator() {
                     let v1: u32; // FIXME(tiif): This might not work because this is not initialised?
 
                     bb0: {
-                        statement {}
+                        statements {} //statements for this.  
                         call foo(place(local(v1))) -> local(v0) goto bb1;
                     }
                     
                     bb1: {
-                        statement {}
+                        statements {}
                         return;
                     }
                 };

From 3582f16aae7803a00fa074bee8810b96ca24ad91 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 15:00:20 +0200
Subject: [PATCH 23/42] Change some syntax to make it work correctly

---
 crates/formality-rust/src/grammar/minirust.rs |  6 +++---
 src/test/mir_fn_bodies.rs                     | 10 +++++-----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index fc7bce2a..fd329396 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -112,13 +112,13 @@ pub enum Terminator {
 pub enum ArgumentExpression {
     #[grammar(value($v0))]
     ByValue(ValueExpression),
-    #[grammar(place($v0))]
+    #[grammar(arg_place($v0))]
     InPlace(PlaceExpression),
 }
 
 #[term]
 pub enum ValueExpression {
-    #[grammar($v0)]
+    #[grammar(fn_id $v0)]
     Fn(FnId),
     // #[grammar($(v0) as $v1)]
     // Tuple(Vec<ValueExpression>, Ty),
@@ -135,7 +135,7 @@ pub enum ValueExpression {
 #[term]
 pub enum PlaceExpression {
     // FIXME(tiif): if we remove the local keyword, call bar () -> v1 goto bb1; won't work
-    #[grammar(local($v0))]
+    #[grammar(placeexpr_local($v0))]
     Local(LocalId),
     // Deref(Arc<ValueExpression>),
     // Field(Arc<PlaceExpression>, FieldId),
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index a5dba077..1b850eb2 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -10,7 +10,7 @@ fn test_assign_statement() {
                     
                     bb0: {
                         statements { 
-                            local(v1) = v0; // load(local(v0))
+                            placeexpr_local(v1) = load(placeexpr_local(v0)); // load(local(v0))
                         }
                         return;
                     }
@@ -34,7 +34,7 @@ fn test_place_mention_statement() {
                     
                     bb0: {
                         statements {
-                            local(v0);
+                            placeexpr_local(v0);
                         }
                         return;
                     }
@@ -63,7 +63,7 @@ fn test_goto_terminator() {
 
                     bb1: {
                         statements {
-                            local(v1) = v0; // load(local(v0))
+                            placeexpr_local(v1) = load(placeexpr_local(v0)); // load(local(v0))
                         }
                         return;
                     }
@@ -87,7 +87,7 @@ fn test_call_terminator() {
                     
                     bb0: {
                         statements {
-                            local(v0) = v1;
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;
                     }
@@ -99,7 +99,7 @@ fn test_call_terminator() {
 
                     bb0: {
                         statements {} //statements for this.  
-                        call foo(place(local(v1))) -> local(v0) goto bb1;
+                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
                     }
                     
                     bb1: {

From 1cb5d7635d09137bec7cbc7091b7bb7762ab3360 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 15:36:57 +0200
Subject: [PATCH 24/42] Add reflexive rules for type

---
 crates/formality-prove/src/prove/prove_via.rs | 2 +-
 crates/formality-prove/src/prove/prove_wc.rs  | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs
index 4ddbd463..81bb9a40 100644
--- a/crates/formality-prove/src/prove/prove_via.rs
+++ b/crates/formality-prove/src/prove/prove_via.rs
@@ -37,7 +37,7 @@ judgment_fn! {
             (let (skel_c, parameters_c) = rel_1.debone())
             (let (skel_g, parameters_g) = rel_2.debone())
             (if skel_c == skel_g)
-            (if parameters_c == parameters_g)! // for relations, we require 100% match
+            (if parameters_c == parameters_g) // for relations, we require 100% match
             ----------------------------- ("relation-axiom")
             (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env))
         )
diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
index 1f4f8f25..d44d5cb4 100644
--- a/crates/formality-prove/src/prove/prove_wc.rs
+++ b/crates/formality-prove/src/prove/prove_wc.rs
@@ -16,6 +16,7 @@ use crate::{
 };
 
 use super::constraints::Constraints;
+use formality_types::grammar::Parameter::Ty;
 
 judgment_fn! {
     pub fn prove_wc(
@@ -53,6 +54,14 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c)
         )
 
+        (
+            (if let Ty(_) = param1.clone())!
+            (if let Ty(_) = param2.clone())!
+            (if param1 == param2)
+                ----------------------------- ("subtype - reflexive")
+            (prove_wc(_decls, env, _assumptions, WcData::Relation(Relation::Sub(param1, param2))) => Constraints::none(env))
+        )
+
         (
             (decls.impl_decls(&trait_ref.trait_id) => i)!
             (let (env, subst) = env.existential_substitution(&i.binder))

From 65d5c8ff0eab6f2d7daf2ac05fdd3caf43725567 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 15:40:04 +0200
Subject: [PATCH 25/42] Fix some tests to make them pass

---
 src/test/mir_fn_bodies.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 1b850eb2..5d4e5399 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -10,7 +10,7 @@ fn test_assign_statement() {
                     
                     bb0: {
                         statements { 
-                            placeexpr_local(v1) = load(placeexpr_local(v0)); // load(local(v0))
+                            placeexpr_local(v0) = load(placeexpr_local(v1)); // load(local(v0))
                         }
                         return;
                     }
@@ -34,6 +34,7 @@ fn test_place_mention_statement() {
                     
                     bb0: {
                         statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
                             placeexpr_local(v0);
                         }
                         return;
@@ -63,7 +64,7 @@ fn test_goto_terminator() {
 
                     bb1: {
                         statements {
-                            placeexpr_local(v1) = load(placeexpr_local(v0)); // load(local(v0))
+                            placeexpr_local(v0) = load(placeexpr_local(v1)); // load(local(v0))
                         }
                         return;
                     }

From ffadeb01337bde853d51ded716089e2efa8ac654 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 15:52:49 +0200
Subject: [PATCH 26/42] Skip the function arg number check for now, it's wrong

---
 crates/formality-check/src/mini_rust_check.rs |  7 +------
 src/test/mir_fn_bodies.rs                     | 10 ++++++----
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 98fba7d0..4fdb10eb 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -136,11 +136,6 @@ impl Check<'_> {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
                 self.check_value(typeck_env, callee)?;
                 // Check if the numbers of arguments passed equals to number of arguments declared.
-                let actual_arg_num = actual_arguments.len();
-                let declared_arg_num = typeck_env.declared_input_tys.len();
-                if actual_arg_num != declared_arg_num {
-                    bail!("The numbers of arguments passed to Terminator::Call is {actual_arg_num}, but the declared function argument number is {declared_arg_num}");
-                }
                 let arguments = zip(typeck_env.declared_input_tys.clone(), actual_arguments);
                 for (declared_ty, actual_argument) in arguments {
                     // Check if the arguments are well formed.
@@ -274,7 +269,7 @@ struct TypeckEnv {
     /// Record if the return place has been initialised.
     ret_place_is_initialised: bool,
 
-    /// All declared argument type of the function.
+    /// All declared argument type of current function.
     declared_input_tys: Vec<Ty>,
 
     /// All declared fn in current crate.
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 5d4e5399..fc5fe359 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -10,7 +10,7 @@ fn test_assign_statement() {
                     
                     bb0: {
                         statements { 
-                            placeexpr_local(v0) = load(placeexpr_local(v1)); // load(local(v0))
+                            placeexpr_local(v0) = load(placeexpr_local(v1)); 
                         }
                         return;
                     }
@@ -64,7 +64,7 @@ fn test_goto_terminator() {
 
                     bb1: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1)); // load(local(v0))
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;
                     }
@@ -96,10 +96,12 @@ fn test_call_terminator() {
 
                 fn bar() -> u32 = minirust() -> v0 {
                     let v0: u32;
-                    let v1: u32; // FIXME(tiif): This might not work because this is not initialised?
+                    let v1: u32;
 
                     bb0: {
-                        statements {} //statements for this.  
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        } 
                         call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
                     }
                     

From 7ec2414c9aed8f307bbf2ae7c52b79d15f72009a Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 16:14:34 +0200
Subject: [PATCH 27/42] Make place mention test pass

---
 crates/formality-rust/src/grammar/minirust.rs |  2 +-
 src/test/mir_fn_bodies.rs                     | 48 +++++++++----------
 2 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index fd329396..7ec1d01e 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -66,7 +66,7 @@ pub enum Statement {
     Assign(PlaceExpression, ValueExpression),
 
     // Represent let _ = place;
-    #[grammar($v0;)]
+    #[grammar(place_mention($v0);)]
     PlaceMention(PlaceExpression),
     // SetDiscriminant
     // Validate
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index fc5fe359..3418f920 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -22,30 +22,6 @@ fn test_assign_statement() {
     )
 }
 
-// TODO: we need to add a rule for () <: ()
-#[test]
-fn test_place_mention_statement() {
-    crate::assert_ok!(
-        [
-            crate Foo {
-                fn foo (u32) -> u32 = minirust(v1) -> v0 {
-                    let v0: u32;
-                    let v1: u32;
-                    
-                    bb0: {
-                        statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
-                            placeexpr_local(v0);
-                        }
-                        return;
-                    }
-                    
-                };
-            }
-        ]
-        expect_test::expect![["()"]]
-    )
-}
 
 
 #[test]
@@ -116,3 +92,27 @@ fn test_call_terminator() {
     )
 
 }
+
+#[test]
+fn test_place_mention_statement() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements {
+                            place_mention(placeexpr_local(v0));,
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        }
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+}

From e4b2effb351ffb1f79f744ada397b374075f38a3 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 16:15:54 +0200
Subject: [PATCH 28/42] Make the place_mention test syntax better

---
 crates/formality-rust/src/grammar/minirust.rs | 2 +-
 src/test/mir_fn_bodies.rs                     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 7ec1d01e..83413b35 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -52,7 +52,7 @@ pub struct LocalDecl {
 
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
 // FIXME(tiif): for some reason statements is always not required
-#[term($id: {statements ${statements} $terminator;})]
+#[term($id: {statements {$*statements} $terminator;})]
 pub struct BasicBlock {
     pub id: BbId,
     pub statements: Vec<Statement>,
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 3418f920..4a8ff82b 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -104,7 +104,7 @@ fn test_place_mention_statement() {
                     
                     bb0: {
                         statements {
-                            place_mention(placeexpr_local(v0));,
+                            place_mention(placeexpr_local(v0));
                             placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;

From ddf51a4a07e851ec1394f0c409c7a190b980bdae Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Thu, 10 Jul 2025 17:00:48 +0200
Subject: [PATCH 29/42] WIP: add some fail tests

---
 src/test/mir_fn_bodies.rs | 822 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 822 insertions(+)

diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 4a8ff82b..5d1ca414 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -116,3 +116,825 @@ fn test_place_mention_statement() {
         expect_test::expect![["()"]]
     )
 }
+
+
+// Test the behaviour of assigning value that is not subtype of the place. 
+#[test]
+fn test_invalid_assign_statement() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo (u32) -> () = minirust(v1) -> v0 {
+                    let v0: ();
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements { 
+                            placeexpr_local(v0) = load(placeexpr_local(v1)); 
+                        }
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#"
+            judgment `prove { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
+              failed at (src/file.rs:LL:CC) because
+                judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                  the rule "some" failed at step #0 (src/file.rs:LL:CC) because
+                    judgment `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
+                        condition evaluted to false: `param1 == param2`
+                          param1 = u32
+                          param2 = ()
+
+            Stack backtrace:
+               0: anyhow::error::<impl core::convert::From<E> for anyhow::Error>::from
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: <core::result::Result<T,F> as core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible,E>>>::from_residual
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs:2079:27
+               2: formality_check::Check::prove_goal
+                         at ./crates/formality-check/src/lib.rs:150:18
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_statement
+                         at ./crates/formality-check/src/mini_rust_check.rs:99:22
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:78:18
+               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               6: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               8: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               9: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+              10: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              11: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              12: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              13: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              14: a_mir_formality::test::mir_fn_bodies::test_invalid_assign_statement
+                         at ./src/lib.rs:58:9
+              15: a_mir_formality::test::mir_fn_bodies::test_invalid_assign_statement::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:123:35
+              16: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              17: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              18: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              19: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              21: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              22: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              23: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              24: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              26: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              27: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              30: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              31: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              32: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              33: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              37: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              38: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              39: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+}
+
+// Test the behaviour of having invalid local name in place mention.
+#[test]
+fn test_invalid_local_in_place_mention() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements {
+                            place_mention(placeexpr_local(v2));
+                        }
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#"
+            PlaceExpression::Local: unknown local name
+
+            Stack backtrace:
+               0: anyhow::error::<impl anyhow::Error>::msg
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: anyhow::__private::format_err
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
+               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_place
+                         at ./crates/formality-check/src/mini_rust_check.rs:188:21
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_statement
+                         at ./crates/formality-check/src/mini_rust_check.rs:111:22
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:78:18
+               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               6: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               8: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               9: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+              10: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              11: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              12: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              13: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              14: a_mir_formality::test::mir_fn_bodies::test_invalid_local_in_place_mention
+                         at ./src/lib.rs:58:9
+              15: a_mir_formality::test::mir_fn_bodies::test_invalid_local_in_place_mention::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:239:41
+              16: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              17: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              18: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              19: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              21: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              22: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              23: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              24: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              26: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              27: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              30: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              31: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              32: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              33: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              37: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              38: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              39: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+}
+
+
+// Test the behaviour of having invalid bb_id in goto. 
+#[test]
+fn test_invalid_goto_bbid() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements {}
+                        goto bb1;
+                    }
+
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#"
+            Basic block bb1 does not exist
+
+            Stack backtrace:
+               0: anyhow::error::<impl anyhow::Error>::msg
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: formality_check::mini_rust_check::<impl formality_check::Check>::check_block_exist
+                         at ./crates/formality-check/src/mini_rust_check.rs:250:9
+               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
+                         at ./crates/formality-check/src/mini_rust_check.rs:127:22
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               5: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               7: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               8: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+               9: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              10: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              11: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              12: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              13: a_mir_formality::test::mir_fn_bodies::test_invalid_goto_bbid
+                         at ./src/lib.rs:58:9
+              14: a_mir_formality::test::mir_fn_bodies::test_invalid_goto_bbid::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:348:28
+              15: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              16: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              17: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              18: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              20: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              21: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              22: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              23: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              24: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              26: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              29: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              30: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              31: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              32: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              37: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              38: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+    
+}
+
+// Test what will happen if we call a function that does not exist .
+#[test]
+fn test_call_invalid_fn() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn bar() -> u32 = minirust() -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+
+                    bb0: {
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        } 
+                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
+                    }
+                    
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#"
+            The function called is not declared in current crate
+
+            Stack backtrace:
+               0: anyhow::error::<impl anyhow::Error>::msg
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: anyhow::__private::format_err
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
+               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_value
+                         at ./crates/formality-check/src/mini_rust_check.rs:219:21
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
+                         at ./crates/formality-check/src/mini_rust_check.rs:137:22
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
+               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               6: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               8: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               9: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+              10: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              11: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              12: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              13: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              14: a_mir_formality::test::mir_fn_bodies::test_call_invalid_fn
+                         at ./src/lib.rs:58:9
+              15: a_mir_formality::test::mir_fn_bodies::test_call_invalid_fn::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:453:26
+              16: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              17: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              18: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              19: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              21: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              22: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              23: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              24: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              26: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              27: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              30: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              31: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              32: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              33: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              37: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              38: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              39: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+}
+
+#[test]
+// Test what will happen if the type of argument passed in is not subtype of what is expected.
+// FIXME(tiif): figure out why this test passed.
+fn test_pass_non_subtype_arg() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo(u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        }
+                        return;
+                    }
+                };
+
+                fn bar() -> () = minirust(v1) -> v0 {
+                    let v0: ();
+                    let v1: ();
+
+                    bb0: {
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        } 
+                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
+                    }
+
+                    bb1: {
+                        statements {}
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#""#]]
+    )
+}
+
+// Test what will happen if the next block does not exist for Terminator::Call
+// FIXME: we might want to allow this?
+#[test]
+fn test_no_next_bb_for_call_terminator() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo(u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        }
+                        return;
+                    }
+                };
+
+                fn bar() -> u32 = minirust() -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+
+                    bb0: {
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        } 
+                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
+                    }
+                    
+                };
+            }
+        ]
+        []
+        expect_test::expect![[r#"
+            There should be next block for Terminator::Call, but it does not exist!
+
+            Stack backtrace:
+               0: anyhow::error::<impl anyhow::Error>::msg
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: anyhow::__private::format_err
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
+               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
+                         at ./crates/formality-check/src/mini_rust_check.rs:161:21
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               5: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               7: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               8: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+               9: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              10: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              11: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              12: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              13: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator
+                         at ./src/lib.rs:58:9
+              14: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:134:41
+              15: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              16: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              17: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              18: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              20: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              21: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              22: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              23: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              24: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              26: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              29: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              30: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              31: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              32: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              37: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              38: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+
+}
+
+// Test what will happen if the fn's declared return type is not subtype of the local variable ret. 
+#[test]
+fn test_uncompatible_return_type() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo () -> () = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+                    
+                    bb0: {
+                        statements { 
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                        }
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+
+        []
+
+        expect_test::expect![[r#"
+            judgment `prove { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
+              failed at (src/file.rs:LL:CC) because
+                judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                  the rule "some" failed at step #0 (src/file.rs:LL:CC) because
+                    judgment `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
+                        condition evaluted to false: `param1 == param2`
+                          param1 = u32
+                          param2 = ()
+
+            Stack backtrace:
+               0: anyhow::error::<impl core::convert::From<E> for anyhow::Error>::from
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: <core::result::Result<T,F> as core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible,E>>>::from_residual
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs:2079:27
+               2: formality_check::Check::prove_goal
+                         at ./crates/formality-check/src/lib.rs:150:18
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:46:14
+               4: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               5: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               6: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               7: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+               8: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+               9: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              10: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              11: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              12: a_mir_formality::test::mir_fn_bodies::test_uncompatible_return_type
+                         at ./src/lib.rs:58:9
+              13: a_mir_formality::test::mir_fn_bodies::test_uncompatible_return_type::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:135:35
+              14: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              15: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              16: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              17: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              18: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              19: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              20: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              21: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              22: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              23: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              24: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              25: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              26: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              27: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              28: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              29: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              30: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              31: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              32: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              33: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              35: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              36: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              37: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+}
+
+// Test the behaviour of having unitialised return local variable.  
+#[test]
+fn test_uninitialised_return_type() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo () -> u32 = minirust() -> v0 {
+                    let v0: u32;
+                    
+                    bb0: {
+                        statements { 
+                        }
+                        return;
+                    }
+                    
+                };
+            }
+        ]
+
+        []
+
+        expect_test::expect![[r#"
+            The return local variable has not been initialized.
+
+            Stack backtrace:
+               0: anyhow::error::<impl anyhow::Error>::msg
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
+               1: anyhow::__private::format_err
+                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
+               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
+                         at ./crates/formality-check/src/mini_rust_check.rs:170:21
+               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
+                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
+               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
+                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+               5: formality_check::fns::<impl formality_check::Check>::check_fn
+                         at ./crates/formality-check/src/fns.rs:76:26
+               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
+                         at ./crates/formality-check/src/fns.rs:14:14
+               7: formality_check::Check::check_crate_item
+                         at ./crates/formality-check/src/lib.rs:125:38
+               8: formality_check::Check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:75:18
+               9: formality_check::Check::check
+                         at ./crates/formality-check/src/lib.rs:57:18
+              10: formality_check::check_current_crate
+                         at ./crates/formality-check/src/lib.rs:38:6
+              11: formality_check::check_all_crates
+                         at ./crates/formality-check/src/lib.rs:25:9
+              12: a_mir_formality::test_program_ok
+                         at ./src/lib.rs:64:5
+              13: a_mir_formality::test::mir_fn_bodies::test_uninitialised_return_type
+                         at ./src/lib.rs:58:9
+              14: a_mir_formality::test::mir_fn_bodies::test_uninitialised_return_type::{{closure}}
+                         at ./src/test/mir_fn_bodies.rs:137:36
+              15: core::ops::function::FnOnce::call_once
+                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
+              16: core::ops::function::FnOnce::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              17: test::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
+              18: test::run_test_in_process::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
+              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              20: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              21: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              22: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              23: test::run_test_in_process
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
+              24: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
+              25: test::run_test::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
+              26: std::sys::backtrace::__rust_begin_short_backtrace
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
+              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
+              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
+              29: std::panicking::catch_unwind::do_call
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
+              30: std::panicking::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
+              31: std::panic::catch_unwind
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
+              32: std::thread::Builder::spawn_unchecked_::{{closure}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
+              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
+              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
+              36: std::sys::pal::unix::thread::Thread::new::thread_start
+                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
+              37: start_thread
+                         at ./nptl/pthread_create.c:442:8
+              38: __GI___clone3
+                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+    )
+}
\ No newline at end of file

From 7c1de68fcdfd413b6c2813095d7465c85b27d74b Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 11:36:19 +0200
Subject: [PATCH 30/42] Fix function argument type checking

---
 crates/formality-check/src/mini_rust_check.rs | 35 ++++++++++++++-----
 src/test/mir_fn_bodies.rs                     | 13 ++++---
 2 files changed, 33 insertions(+), 15 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 4fdb10eb..999bbe08 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -5,6 +5,8 @@ use formality_prove::Env;
 use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_rust::grammar::minirust::ValueExpression::{Fn, Load};
+use formality_rust::grammar::FnBoundData;
+use formality_types::grammar::FnId;
 use formality_rust::grammar::minirust::{
     self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
 };
@@ -58,6 +60,7 @@ impl Check<'_> {
             ret_place_is_initialised: false,
             declared_input_tys,
             declared_fn: declared_fn.to_vec(),
+            callee_input_tys: Map::new(),
         };
 
         // (3) Check statements in body are valid
@@ -117,7 +120,7 @@ impl Check<'_> {
 
     fn check_terminator(
         &self,
-        typeck_env: &TypeckEnv,
+        typeck_env: &mut TypeckEnv,
         fn_assumptions: &Wcs,
         terminator: &minirust::Terminator,
     ) -> Fallible<()> {
@@ -135,8 +138,14 @@ impl Check<'_> {
             } => {
                 // Function is part of the value expression, so we will check if the function exists in check_value.
                 self.check_value(typeck_env, callee)?;
+                // Get argument information from the callee.
+                let Fn(callee_fn_id) = callee else {
+                    unreachable!("Callee must exists in Terminator::Call");
+                };
+                let callee_fn_bound_data = typeck_env.callee_input_tys.get(callee_fn_id).unwrap();
+                let callee_declared_input_tys = callee_fn_bound_data.input_tys.clone();
                 // Check if the numbers of arguments passed equals to number of arguments declared.
-                let arguments = zip(typeck_env.declared_input_tys.clone(), actual_arguments);
+                let arguments = zip(callee_declared_input_tys, actual_arguments);
                 for (declared_ty, actual_argument) in arguments {
                     // Check if the arguments are well formed.
                     let actual_ty = self.check_argument_expression(typeck_env, actual_argument)?;
@@ -194,22 +203,28 @@ impl Check<'_> {
     }
 
     // Check if the value expression is well-formed, and return the type of the value expression.
-    fn check_value(&self, env: &TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
+    fn check_value(&self, typeck_env: &mut TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
         let value_ty;
         match value {
             Load(place_expression) => {
-                value_ty = self.check_place(env, place_expression)?;
+                value_ty = self.check_place(typeck_env, place_expression)?;
                 Ok(value_ty)
             }
             Fn(fn_id) => {
                 // Check if the function called is in declared in current crate.
-                let item = env
+                let item = typeck_env
                     .declared_fn
                     .iter()
                     .find(|&item| {
                         match item {
                             CrateItem::Fn(fn_declared) => {
-                                return fn_declared.id == *fn_id;
+                                if fn_declared.id == *fn_id {
+                                    let fn_bound_data = typeck_env.env.instantiate_universally(&fn_declared.binder);
+                                    // Store the callee information in typeck_env, we will need this when type checking Terminator::Call. 
+                                    typeck_env.callee_input_tys.insert(fn_declared.id.clone(), fn_bound_data);
+                                    return true;
+                                }
+                                false
                             }
                             _ => false
                         }
@@ -218,7 +233,7 @@ impl Check<'_> {
                 {
                     bail!("The function called is not declared in current crate")
                 }
-                value_ty = env.output_ty.clone();
+                value_ty = typeck_env.output_ty.clone();
                 Ok(value_ty)
             }
         }
@@ -226,7 +241,7 @@ impl Check<'_> {
 
     fn check_argument_expression(
         &self,
-        env: &TypeckEnv,
+        env: &mut TypeckEnv,
         arg_expr: &ArgumentExpression,
     ) -> Fallible<Ty> {
         let ty;
@@ -274,4 +289,8 @@ struct TypeckEnv {
 
     /// All declared fn in current crate.
     declared_fn: Vec<CrateItem>,
+
+    /// All information of callee.
+    callee_input_tys: Map<FnId, FnBoundData>,
+
 }
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 5d1ca414..c3dfca36 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -558,7 +558,6 @@ fn test_call_invalid_fn() {
 
 #[test]
 // Test what will happen if the type of argument passed in is not subtype of what is expected.
-// FIXME(tiif): figure out why this test passed.
 fn test_pass_non_subtype_arg() {
     crate::assert_err!(
         [
@@ -575,7 +574,7 @@ fn test_pass_non_subtype_arg() {
                     }
                 };
 
-                fn bar() -> () = minirust(v1) -> v0 {
+                fn bar(()) -> () = minirust(v1) -> v0 {
                     let v0: ();
                     let v1: ();
 
@@ -595,7 +594,7 @@ fn test_pass_non_subtype_arg() {
             }
         ]
         []
-        expect_test::expect![[r#""#]]
+        expect_test::expect!["()"]
     )
 }
 
@@ -642,11 +641,11 @@ fn test_no_next_bb_for_call_terminator() {
                1: anyhow::__private::format_err
                          at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
                2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
-                         at ./crates/formality-check/src/mini_rust_check.rs:161:21
+                         at ./crates/formality-check/src/mini_rust_check.rs:170:21
                3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
+                         at ./crates/formality-check/src/mini_rust_check.rs:84:14
                4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
+                         at ./crates/formality-check/src/mini_rust_check.rs:68:18
                5: formality_check::fns::<impl formality_check::Check>::check_fn
                          at ./crates/formality-check/src/fns.rs:76:26
                6: formality_check::fns::<impl formality_check::Check>::check_free_fn
@@ -666,7 +665,7 @@ fn test_no_next_bb_for_call_terminator() {
               13: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator
                          at ./src/lib.rs:58:9
               14: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:134:41
+                         at ./src/test/mir_fn_bodies.rs:604:41
               15: core::ops::function::FnOnce::call_once
                          at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
               16: core::ops::function::FnOnce::call_once

From 42c017c70dd4e3addeb28585609cdc602df338ec Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 12:12:31 +0200
Subject: [PATCH 31/42] Clean up the trace

---
 src/test/mir_fn_bodies.rs | 589 ++------------------------------------
 1 file changed, 17 insertions(+), 572 deletions(-)

diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index c3dfca36..eccbc9ec 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -148,89 +148,7 @@ fn test_invalid_assign_statement() {
                       the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
                         condition evaluted to false: `param1 == param2`
                           param1 = u32
-                          param2 = ()
-
-            Stack backtrace:
-               0: anyhow::error::<impl core::convert::From<E> for anyhow::Error>::from
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: <core::result::Result<T,F> as core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible,E>>>::from_residual
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs:2079:27
-               2: formality_check::Check::prove_goal
-                         at ./crates/formality-check/src/lib.rs:150:18
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_statement
-                         at ./crates/formality-check/src/mini_rust_check.rs:99:22
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:78:18
-               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
-               6: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               8: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               9: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-              10: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              11: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              12: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              13: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              14: a_mir_formality::test::mir_fn_bodies::test_invalid_assign_statement
-                         at ./src/lib.rs:58:9
-              15: a_mir_formality::test::mir_fn_bodies::test_invalid_assign_statement::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:123:35
-              16: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              17: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              18: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              19: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              21: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              22: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              23: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              24: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              26: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              27: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              30: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              31: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              32: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              33: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              37: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              38: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              39: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+                          param2 = ()"#]]
     )
 }
 
@@ -256,89 +174,7 @@ fn test_invalid_local_in_place_mention() {
         ]
         []
         expect_test::expect![[r#"
-            PlaceExpression::Local: unknown local name
-
-            Stack backtrace:
-               0: anyhow::error::<impl anyhow::Error>::msg
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: anyhow::__private::format_err
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
-               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_place
-                         at ./crates/formality-check/src/mini_rust_check.rs:188:21
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_statement
-                         at ./crates/formality-check/src/mini_rust_check.rs:111:22
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:78:18
-               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
-               6: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               8: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               9: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-              10: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              11: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              12: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              13: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              14: a_mir_formality::test::mir_fn_bodies::test_invalid_local_in_place_mention
-                         at ./src/lib.rs:58:9
-              15: a_mir_formality::test::mir_fn_bodies::test_invalid_local_in_place_mention::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:239:41
-              16: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              17: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              18: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              19: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              21: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              22: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              23: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              24: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              26: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              27: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              30: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              31: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              32: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              33: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              37: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              38: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              39: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+            PlaceExpression::Local: unknown local name"#]]
     )
 }
 
@@ -363,87 +199,7 @@ fn test_invalid_goto_bbid() {
         ]
         []
         expect_test::expect![[r#"
-            Basic block bb1 does not exist
-
-            Stack backtrace:
-               0: anyhow::error::<impl anyhow::Error>::msg
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: formality_check::mini_rust_check::<impl formality_check::Check>::check_block_exist
-                         at ./crates/formality-check/src/mini_rust_check.rs:250:9
-               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
-                         at ./crates/formality-check/src/mini_rust_check.rs:127:22
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
-               5: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               7: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               8: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-               9: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              10: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              11: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              12: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              13: a_mir_formality::test::mir_fn_bodies::test_invalid_goto_bbid
-                         at ./src/lib.rs:58:9
-              14: a_mir_formality::test::mir_fn_bodies::test_invalid_goto_bbid::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:348:28
-              15: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              16: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              17: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              18: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              20: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              21: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              22: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              23: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              24: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              26: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              29: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              30: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              31: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              32: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              37: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              38: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+            Basic block bb1 does not exist"#]]
     )
     
 }
@@ -470,89 +226,7 @@ fn test_call_invalid_fn() {
         ]
         []
         expect_test::expect![[r#"
-            The function called is not declared in current crate
-
-            Stack backtrace:
-               0: anyhow::error::<impl anyhow::Error>::msg
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: anyhow::__private::format_err
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
-               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_value
-                         at ./crates/formality-check/src/mini_rust_check.rs:219:21
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
-                         at ./crates/formality-check/src/mini_rust_check.rs:137:22
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
-               5: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
-               6: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               7: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               8: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               9: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-              10: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              11: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              12: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              13: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              14: a_mir_formality::test::mir_fn_bodies::test_call_invalid_fn
-                         at ./src/lib.rs:58:9
-              15: a_mir_formality::test::mir_fn_bodies::test_call_invalid_fn::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:453:26
-              16: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              17: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              18: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              19: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              20: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              21: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              22: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              23: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              24: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              26: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              27: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              28: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              29: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              30: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              31: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              32: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              33: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              34: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              37: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              38: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              39: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+            The function called is not declared in current crate"#]]
     )
 }
 
@@ -594,7 +268,16 @@ fn test_pass_non_subtype_arg() {
             }
         ]
         []
-        expect_test::expect!["()"]
+        expect_test::expect![[r#"
+            judgment `prove { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
+              failed at (src/file.rs:LL:CC) because
+                judgment `prove_wc_list { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                  the rule "some" failed at step #0 (src/file.rs:LL:CC) because
+                    judgment `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
+                        condition evaluted to false: `param1 == param2`
+                          param1 = ()
+                          param2 = u32"#]]
     )
 }
 
@@ -633,87 +316,7 @@ fn test_no_next_bb_for_call_terminator() {
         ]
         []
         expect_test::expect![[r#"
-            There should be next block for Terminator::Call, but it does not exist!
-
-            Stack backtrace:
-               0: anyhow::error::<impl anyhow::Error>::msg
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: anyhow::__private::format_err
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
-               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
-                         at ./crates/formality-check/src/mini_rust_check.rs:170:21
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:84:14
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:68:18
-               5: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               7: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               8: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-               9: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              10: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              11: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              12: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              13: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator
-                         at ./src/lib.rs:58:9
-              14: a_mir_formality::test::mir_fn_bodies::test_no_next_bb_for_call_terminator::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:604:41
-              15: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              16: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              17: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              18: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              20: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              21: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              22: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              23: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              24: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              26: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              29: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              30: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              31: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              32: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              37: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              38: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+            There should be next block for Terminator::Call, but it does not exist!"#]]
     )
 
 }
@@ -750,85 +353,7 @@ fn test_uncompatible_return_type() {
                       the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
                         condition evaluted to false: `param1 == param2`
                           param1 = u32
-                          param2 = ()
-
-            Stack backtrace:
-               0: anyhow::error::<impl core::convert::From<E> for anyhow::Error>::from
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: <core::result::Result<T,F> as core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible,E>>>::from_residual
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs:2079:27
-               2: formality_check::Check::prove_goal
-                         at ./crates/formality-check/src/lib.rs:150:18
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:46:14
-               4: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               5: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               6: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               7: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-               8: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-               9: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              10: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              11: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              12: a_mir_formality::test::mir_fn_bodies::test_uncompatible_return_type
-                         at ./src/lib.rs:58:9
-              13: a_mir_formality::test::mir_fn_bodies::test_uncompatible_return_type::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:135:35
-              14: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              15: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              16: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              17: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              18: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              19: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              20: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              21: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              22: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              23: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              24: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              25: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              26: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              27: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              28: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              29: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              30: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              31: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              32: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              33: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              35: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              36: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              37: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+                          param2 = ()"#]]
     )
 }
 
@@ -854,86 +379,6 @@ fn test_uninitialised_return_type() {
         []
 
         expect_test::expect![[r#"
-            The return local variable has not been initialized.
-
-            Stack backtrace:
-               0: anyhow::error::<impl anyhow::Error>::msg
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/backtrace.rs:27:14
-               1: anyhow::__private::format_err
-                         at /home/tiif/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/anyhow-1.0.75/src/lib.rs:675:13
-               2: formality_check::mini_rust_check::<impl formality_check::Check>::check_terminator
-                         at ./crates/formality-check/src/mini_rust_check.rs:170:21
-               3: formality_check::mini_rust_check::<impl formality_check::Check>::check_block
-                         at ./crates/formality-check/src/mini_rust_check.rs:81:14
-               4: formality_check::mini_rust_check::<impl formality_check::Check>::check_body
-                         at ./crates/formality-check/src/mini_rust_check.rs:65:18
-               5: formality_check::fns::<impl formality_check::Check>::check_fn
-                         at ./crates/formality-check/src/fns.rs:76:26
-               6: formality_check::fns::<impl formality_check::Check>::check_free_fn
-                         at ./crates/formality-check/src/fns.rs:14:14
-               7: formality_check::Check::check_crate_item
-                         at ./crates/formality-check/src/lib.rs:125:38
-               8: formality_check::Check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:75:18
-               9: formality_check::Check::check
-                         at ./crates/formality-check/src/lib.rs:57:18
-              10: formality_check::check_current_crate
-                         at ./crates/formality-check/src/lib.rs:38:6
-              11: formality_check::check_all_crates
-                         at ./crates/formality-check/src/lib.rs:25:9
-              12: a_mir_formality::test_program_ok
-                         at ./src/lib.rs:64:5
-              13: a_mir_formality::test::mir_fn_bodies::test_uninitialised_return_type
-                         at ./src/lib.rs:58:9
-              14: a_mir_formality::test::mir_fn_bodies::test_uninitialised_return_type::{{closure}}
-                         at ./src/test/mir_fn_bodies.rs:137:36
-              15: core::ops::function::FnOnce::call_once
-                         at /home/tiif/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
-              16: core::ops::function::FnOnce::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              17: test::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:648:18
-              18: test::run_test_in_process::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:74
-              19: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              20: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              21: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              22: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              23: test::run_test_in_process
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:671:27
-              24: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:592:43
-              25: test::run_test::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/test/src/lib.rs:622:41
-              26: std::sys::backtrace::__rust_begin_short_backtrace
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/backtrace.rs:152:18
-              27: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:559:17
-              28: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/panic/unwind_safe.rs:272:9
-              29: std::panicking::catch_unwind::do_call
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:589:40
-              30: std::panicking::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panicking.rs:552:19
-              31: std::panic::catch_unwind
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/panic.rs:359:14
-              32: std::thread::Builder::spawn_unchecked_::{{closure}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/thread/mod.rs:557:30
-              33: core::ops::function::FnOnce::call_once{{vtable.shim}}
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/core/src/ops/function.rs:250:5
-              34: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              35: <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/alloc/src/boxed.rs:1966:9
-              36: std::sys::pal::unix::thread::Thread::new::thread_start
-                         at /rustc/71e4c005caa812a16fcb08d0bf1e6f1eda7c8381/library/std/src/sys/pal/unix/thread.rs:97:17
-              37: start_thread
-                         at ./nptl/pthread_create.c:442:8
-              38: __GI___clone3
-                         at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81:0"#]]
+            The return local variable has not been initialized."#]]
     )
 }
\ No newline at end of file

From 2cb9d5da19c52a8f4268b960172f03a490c555d4 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 12:15:50 +0200
Subject: [PATCH 32/42] Remove spurious change

---
 crates/formality-prove/src/prove/prove_via.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs
index 81bb9a40..4ddbd463 100644
--- a/crates/formality-prove/src/prove/prove_via.rs
+++ b/crates/formality-prove/src/prove/prove_via.rs
@@ -37,7 +37,7 @@ judgment_fn! {
             (let (skel_c, parameters_c) = rel_1.debone())
             (let (skel_g, parameters_g) = rel_2.debone())
             (if skel_c == skel_g)
-            (if parameters_c == parameters_g) // for relations, we require 100% match
+            (if parameters_c == parameters_g)! // for relations, we require 100% match
             ----------------------------- ("relation-axiom")
             (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env))
         )

From f9cf30736a550186b2421201c933470d5fd43d77 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 12:18:21 +0200
Subject: [PATCH 33/42] fmt

---
 crates/formality-check/src/mini_rust_check.rs | 38 ++++-----
 src/test/mir_fn_bodies.rs                     | 83 +++++++++----------
 src/test/mod.rs                               |  2 +-
 3 files changed, 56 insertions(+), 67 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 999bbe08..0adbb7fc 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -5,11 +5,11 @@ use formality_prove::Env;
 use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_rust::grammar::minirust::ValueExpression::{Fn, Load};
-use formality_rust::grammar::FnBoundData;
-use formality_types::grammar::FnId;
 use formality_rust::grammar::minirust::{
     self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
 };
+use formality_rust::grammar::FnBoundData;
+use formality_types::grammar::FnId;
 use formality_types::grammar::{Relation, Ty, Wcs};
 
 use crate::Check;
@@ -212,25 +212,24 @@ impl Check<'_> {
             }
             Fn(fn_id) => {
                 // Check if the function called is in declared in current crate.
-                let item = typeck_env
-                    .declared_fn
-                    .iter()
-                    .find(|&item| {
-                        match item {
-                            CrateItem::Fn(fn_declared) => {
-                                if fn_declared.id == *fn_id {
-                                    let fn_bound_data = typeck_env.env.instantiate_universally(&fn_declared.binder);
-                                    // Store the callee information in typeck_env, we will need this when type checking Terminator::Call. 
-                                    typeck_env.callee_input_tys.insert(fn_declared.id.clone(), fn_bound_data);
-                                    return true;
-                                }
-                                false
+                let item = typeck_env.declared_fn.iter().find(|&item| {
+                    match item {
+                        CrateItem::Fn(fn_declared) => {
+                            if fn_declared.id == *fn_id {
+                                let fn_bound_data =
+                                    typeck_env.env.instantiate_universally(&fn_declared.binder);
+                                // Store the callee information in typeck_env, we will need this when type checking Terminator::Call.
+                                typeck_env
+                                    .callee_input_tys
+                                    .insert(fn_declared.id.clone(), fn_bound_data);
+                                return true;
                             }
-                            _ => false
+                            false
                         }
-                    });
-                if item == None
-                {
+                        _ => false,
+                    }
+                });
+                if item == None {
                     bail!("The function called is not declared in current crate")
                 }
                 value_ty = typeck_env.output_ty.clone();
@@ -292,5 +291,4 @@ struct TypeckEnv {
 
     /// All information of callee.
     callee_input_tys: Map<FnId, FnBoundData>,
-
 }
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index eccbc9ec..42939473 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -1,4 +1,3 @@
-
 #[test]
 fn test_assign_statement() {
     crate::assert_ok!(
@@ -7,14 +6,14 @@ fn test_assign_statement() {
                 fn foo (u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
-                        statements { 
-                            placeexpr_local(v0) = load(placeexpr_local(v1)); 
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -22,8 +21,6 @@ fn test_assign_statement() {
     )
 }
 
-
-
 #[test]
 fn test_goto_terminator() {
     crate::assert_ok!(
@@ -32,7 +29,7 @@ fn test_goto_terminator() {
                 fn foo (u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {}
                         goto bb1;
@@ -44,13 +41,12 @@ fn test_goto_terminator() {
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
         expect_test::expect![["()"]]
     )
-    
 }
 
 #[test]
@@ -61,7 +57,7 @@ fn test_call_terminator() {
                 fn foo(u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
@@ -77,10 +73,10 @@ fn test_call_terminator() {
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
-                        } 
+                        }
                         call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
                     }
-                    
+
                     bb1: {
                         statements {}
                         return;
@@ -90,7 +86,6 @@ fn test_call_terminator() {
         ]
         expect_test::expect![["()"]]
     )
-
 }
 
 #[test]
@@ -101,7 +96,7 @@ fn test_place_mention_statement() {
                 fn foo (u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {
                             place_mention(placeexpr_local(v0));
@@ -109,7 +104,7 @@ fn test_place_mention_statement() {
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -117,8 +112,7 @@ fn test_place_mention_statement() {
     )
 }
 
-
-// Test the behaviour of assigning value that is not subtype of the place. 
+// Test the behaviour of assigning value that is not subtype of the place.
 #[test]
 fn test_invalid_assign_statement() {
     crate::assert_err!(
@@ -127,14 +121,14 @@ fn test_invalid_assign_statement() {
                 fn foo (u32) -> () = minirust(v1) -> v0 {
                     let v0: ();
                     let v1: u32;
-                    
+
                     bb0: {
-                        statements { 
-                            placeexpr_local(v0) = load(placeexpr_local(v1)); 
+                        statements {
+                            placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -161,14 +155,14 @@ fn test_invalid_local_in_place_mention() {
                 fn foo (u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {
                             place_mention(placeexpr_local(v2));
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -178,8 +172,7 @@ fn test_invalid_local_in_place_mention() {
     )
 }
 
-
-// Test the behaviour of having invalid bb_id in goto. 
+// Test the behaviour of having invalid bb_id in goto.
 #[test]
 fn test_invalid_goto_bbid() {
     crate::assert_err!(
@@ -188,7 +181,7 @@ fn test_invalid_goto_bbid() {
                 fn foo (u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {}
                         goto bb1;
@@ -201,7 +194,6 @@ fn test_invalid_goto_bbid() {
         expect_test::expect![[r#"
             Basic block bb1 does not exist"#]]
     )
-    
 }
 
 // Test what will happen if we call a function that does not exist .
@@ -217,10 +209,10 @@ fn test_call_invalid_fn() {
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
-                        } 
+                        }
                         call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
                     }
-                    
+
                 };
             }
         ]
@@ -239,7 +231,7 @@ fn test_pass_non_subtype_arg() {
                 fn foo(u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
@@ -255,7 +247,7 @@ fn test_pass_non_subtype_arg() {
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
-                        } 
+                        }
                         call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
                     }
 
@@ -263,7 +255,7 @@ fn test_pass_non_subtype_arg() {
                         statements {}
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -291,7 +283,7 @@ fn test_no_next_bb_for_call_terminator() {
                 fn foo(u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
@@ -307,10 +299,10 @@ fn test_no_next_bb_for_call_terminator() {
                     bb0: {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
-                        } 
+                        }
                         call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
                     }
-                    
+
                 };
             }
         ]
@@ -318,10 +310,9 @@ fn test_no_next_bb_for_call_terminator() {
         expect_test::expect![[r#"
             There should be next block for Terminator::Call, but it does not exist!"#]]
     )
-
 }
 
-// Test what will happen if the fn's declared return type is not subtype of the local variable ret. 
+// Test what will happen if the fn's declared return type is not subtype of the local variable ret.
 #[test]
 fn test_uncompatible_return_type() {
     crate::assert_err!(
@@ -330,14 +321,14 @@ fn test_uncompatible_return_type() {
                 fn foo () -> () = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
-                    
+
                     bb0: {
-                        statements { 
+                        statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -357,7 +348,7 @@ fn test_uncompatible_return_type() {
     )
 }
 
-// Test the behaviour of having unitialised return local variable.  
+// Test the behaviour of having unitialised return local variable.
 #[test]
 fn test_uninitialised_return_type() {
     crate::assert_err!(
@@ -365,13 +356,13 @@ fn test_uninitialised_return_type() {
             crate Foo {
                 fn foo () -> u32 = minirust() -> v0 {
                     let v0: u32;
-                    
+
                     bb0: {
-                        statements { 
+                        statements {
                         }
                         return;
                     }
-                    
+
                 };
             }
         ]
@@ -381,4 +372,4 @@ fn test_uninitialised_return_type() {
         expect_test::expect![[r#"
             The return local variable has not been initialized."#]]
     )
-}
\ No newline at end of file
+}
diff --git a/src/test/mod.rs b/src/test/mod.rs
index 77b14096..ced577b2 100644
--- a/src/test/mod.rs
+++ b/src/test/mod.rs
@@ -5,8 +5,8 @@ mod coherence_overlap;
 mod consts;
 mod decl_safety;
 mod functions;
-mod well_formed_trait_ref;
 mod mir_fn_bodies;
+mod well_formed_trait_ref;
 
 #[test]
 fn parser() {

From 649e671825b13f9fcaa3643215adfd771675d7ae Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 12:28:17 +0200
Subject: [PATCH 34/42] Update on the rule

---
 crates/formality-prove/src/prove/prove_wc.rs |  2 +-
 src/test/mir_fn_bodies.rs                    | 18 +++---------------
 2 files changed, 4 insertions(+), 16 deletions(-)

diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
index d44d5cb4..3fac7ccc 100644
--- a/crates/formality-prove/src/prove/prove_wc.rs
+++ b/crates/formality-prove/src/prove/prove_wc.rs
@@ -57,7 +57,7 @@ judgment_fn! {
         (
             (if let Ty(_) = param1.clone())!
             (if let Ty(_) = param2.clone())!
-            (if param1 == param2)
+            (if param1 == param2)!
                 ----------------------------- ("subtype - reflexive")
             (prove_wc(_decls, env, _assumptions, WcData::Relation(Relation::Sub(param1, param2))) => Constraints::none(env))
         )
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 42939473..85eab47f 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -138,11 +138,7 @@ fn test_invalid_assign_statement() {
               failed at (src/file.rs:LL:CC) because
                 judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
-                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
-                        condition evaluted to false: `param1 == param2`
-                          param1 = u32
-                          param2 = ()"#]]
+                    judgment had no applicable rules: `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]
     )
 }
 
@@ -265,11 +261,7 @@ fn test_pass_non_subtype_arg() {
               failed at (src/file.rs:LL:CC) because
                 judgment `prove_wc_list { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
-                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
-                        condition evaluted to false: `param1 == param2`
-                          param1 = ()
-                          param2 = u32"#]]
+                    judgment had no applicable rules: `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]
     )
 }
 
@@ -340,11 +332,7 @@ fn test_uncompatible_return_type() {
               failed at (src/file.rs:LL:CC) because
                 judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
-                      the rule "subtype - reflexive" failed at step #2 (src/file.rs:LL:CC) because
-                        condition evaluted to false: `param1 == param2`
-                          param1 = u32
-                          param2 = ()"#]]
+                    judgment had no applicable rules: `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]
     )
 }
 

From b5f1e03d55317e5b6bc507b876037b33573ccffb Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 17:02:44 +0200
Subject: [PATCH 35/42] Check the number of function arguments

---
 crates/formality-check/src/mini_rust_check.rs | 15 +++-
 src/test/mir_fn_bodies.rs                     | 81 ++++++++++++++++---
 2 files changed, 82 insertions(+), 14 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 0adbb7fc..4be6b1bb 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -29,8 +29,9 @@ impl Check<'_> {
         // Type-check:
         //
         // (1) Check that all the types declared for each local variable are well-formed
-        // (2) Check that the type of the returned local is compatible with the declared return type
-        // (3) Check that the statements in the body are valid
+        // (2) Check whether the number of declared function parameters matches the number of arguments provided.
+        // (3) Check that the type of the returned local is compatible with the declared return type
+        // (4) Check that the statements in the body are valid
 
         let output_ty: Ty = output_ty.upcast();
 
@@ -44,7 +45,13 @@ impl Check<'_> {
             .map(|lv| (lv.id.clone(), lv.ty.clone()))
             .collect();
 
-        // (2) Check if the actual return type is the subtype of the declared return type.
+
+        // (2) Check whether the number of declared function parameters matches the number of arguments provided.
+        if declared_input_tys.len() != body.args.len() {
+            bail!("Function argument number mismatch: expected {} arguments, but found {}", declared_input_tys.len(), body.args.len());
+        }
+
+        // (3) Check if the actual return type is the subtype of the declared return type.
         self.prove_goal(
             &env,
             fn_assumptions,
@@ -63,7 +70,7 @@ impl Check<'_> {
             callee_input_tys: Map::new(),
         };
 
-        // (3) Check statements in body are valid
+        // (4) Check statements in body are valid
         for block in body.blocks {
             self.check_block(&mut env, fn_assumptions, &block)?;
         }
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 85eab47f..0eec1fe7 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -1,3 +1,4 @@
+/// Test valid assign statement.
 #[test]
 fn test_assign_statement() {
     crate::assert_ok!(
@@ -21,6 +22,7 @@ fn test_assign_statement() {
     )
 }
 
+/// Test valid goto terminator.
 #[test]
 fn test_goto_terminator() {
     crate::assert_ok!(
@@ -49,6 +51,21 @@ fn test_goto_terminator() {
     )
 }
 
+/// Test valid call terminator.
+/// This is equivalent to:
+/// ```
+///    fn foo(v1: u32) -> u32 {
+///      let v0: u32;
+///      v0 = v1;
+///      return v0;
+///    }
+///    
+///    fn bar(v1: u32) -> u32 {
+///       v0 = v1;
+///       let v0 = foo(v0);
+///       return v0;
+///    }
+/// ```
 #[test]
 fn test_call_terminator() {
     crate::assert_ok!(
@@ -66,7 +83,7 @@ fn test_call_terminator() {
                     }
                 };
 
-                fn bar() -> u32 = minirust() -> v0 {
+                fn bar(u32) -> u32 = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
 
@@ -74,7 +91,7 @@ fn test_call_terminator() {
                         statements {
                             placeexpr_local(v0) = load(placeexpr_local(v1));
                         }
-                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
+                        call fn_id foo (arg_place(placeexpr_local(v0))) -> placeexpr_local(v0) goto bb1;
                     }
 
                     bb1: {
@@ -88,6 +105,18 @@ fn test_call_terminator() {
     )
 }
 
+
+/// Test valid place mention statement.
+/// This is equivalent to:
+/// ```
+///    fn foo(v1: u32) -> u32 {
+///      let v0: u32;
+///      v0;
+///      v0 = v1;
+///      return v0;
+///    }
+///    
+/// ```
 #[test]
 fn test_place_mention_statement() {
     crate::assert_ok!(
@@ -112,7 +141,16 @@ fn test_place_mention_statement() {
     )
 }
 
-// Test the behaviour of assigning value that is not subtype of the place.
+/// Test the behaviour of assigning value that is not subtype of the place.
+/// This is equivalent to:
+/// ```
+///    fn foo(v1: u32) -> () {
+///      let v0: ();
+///      v0 = v1;
+///      return v0;
+///    }
+///    
+/// ```
 #[test]
 fn test_invalid_assign_statement() {
     crate::assert_err!(
@@ -168,7 +206,7 @@ fn test_invalid_local_in_place_mention() {
     )
 }
 
-// Test the behaviour of having invalid bb_id in goto.
+// Test the behaviour of having invalid bb_id in goto terminator.
 #[test]
 fn test_invalid_goto_bbid() {
     crate::assert_err!(
@@ -192,7 +230,7 @@ fn test_invalid_goto_bbid() {
     )
 }
 
-// Test what will happen if we call a function that does not exist .
+// Test the behaviour of calling a function that does not exist .
 #[test]
 fn test_call_invalid_fn() {
     crate::assert_err!(
@@ -219,7 +257,7 @@ fn test_call_invalid_fn() {
 }
 
 #[test]
-// Test what will happen if the type of argument passed in is not subtype of what is expected.
+// Test what will happen if the type of arguments passed in is not subtype of what is expected.
 fn test_pass_non_subtype_arg() {
     crate::assert_err!(
         [
@@ -265,8 +303,7 @@ fn test_pass_non_subtype_arg() {
     )
 }
 
-// Test what will happen if the next block does not exist for Terminator::Call
-// FIXME: we might want to allow this?
+// Test what will happen if the next block does not exist for Terminator::Call.
 #[test]
 fn test_no_next_bb_for_call_terminator() {
     crate::assert_err!(
@@ -304,13 +341,18 @@ fn test_no_next_bb_for_call_terminator() {
     )
 }
 
-// Test what will happen if the fn's declared return type is not subtype of the local variable ret.
+/// Test what will happen if the fn's declared return type is not subtype of the local variable ret.
+/// This is equivalent to:
+/// ```
+/// fn foo() {
+/// }
+/// ```
 #[test]
 fn test_uncompatible_return_type() {
     crate::assert_err!(
         [
             crate Foo {
-                fn foo () -> () = minirust(v1) -> v0 {
+                fn foo (u32) -> () = minirust(v1) -> v0 {
                     let v0: u32;
                     let v1: u32;
 
@@ -336,6 +378,25 @@ fn test_uncompatible_return_type() {
     )
 }
 
+
+#[test]
+fn test_function_arg_number_mismatch() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo () -> () = minirust(v1) -> v0 {
+                    let v0: ();
+                    let v1: ();
+                };
+            }
+        ]
+
+        []
+
+        expect_test::expect!["Function argument number mismatch: expected 0 arguments, but found 1"]
+    )
+}
+
 // Test the behaviour of having unitialised return local variable.
 #[test]
 fn test_uninitialised_return_type() {

From 1ff76c8171b64fe79d191cf6b6c6c08adf373673 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 17:28:29 +0200
Subject: [PATCH 36/42] Add more comments

---
 crates/formality-check/src/mini_rust_check.rs |  2 +-
 src/test/mir_fn_bodies.rs                     | 21 +++++++++++--------
 2 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 4be6b1bb..58c779a2 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -50,7 +50,7 @@ impl Check<'_> {
         if declared_input_tys.len() != body.args.len() {
             bail!("Function argument number mismatch: expected {} arguments, but found {}", declared_input_tys.len(), body.args.len());
         }
-
+        
         // (3) Check if the actual return type is the subtype of the declared return type.
         self.prove_goal(
             &env,
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 0eec1fe7..73715a9e 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -341,20 +341,23 @@ fn test_no_next_bb_for_call_terminator() {
     )
 }
 
-/// Test what will happen if the fn's declared return type is not subtype of the local variable ret.
+/// Test what will happen if the declared and actual return type are not compatible.
 /// This is equivalent to:
 /// ```
-/// fn foo() {
+/// fn foo(v1: ()) -> u32 {
+///     let v0: ();
+///     v0 = v1;
+///     return v0;
 /// }
 /// ```
 #[test]
-fn test_uncompatible_return_type() {
+fn test_incompatible_return_type() {
     crate::assert_err!(
         [
             crate Foo {
-                fn foo (u32) -> () = minirust(v1) -> v0 {
-                    let v0: u32;
-                    let v1: u32;
+                fn foo (()) -> u32 = minirust(v1) -> v0 {
+                    let v0: ();
+                    let v1: ();
 
                     bb0: {
                         statements {
@@ -370,11 +373,11 @@ fn test_uncompatible_return_type() {
         []
 
         expect_test::expect![[r#"
-            judgment `prove { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
+            judgment `prove { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
               failed at (src/file.rs:LL:CC) because
-                judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                judgment `prove_wc_list { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment had no applicable rules: `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]
+                    judgment had no applicable rules: `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]
     )
 }
 

From ada095237290a44e10effa3b064d2386b45c76eb Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Mon, 14 Jul 2025 17:28:40 +0200
Subject: [PATCH 37/42] fmt

---
 crates/formality-check/src/mini_rust_check.rs | 9 ++++++---
 src/test/mir_fn_bodies.rs                     | 2 --
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 58c779a2..5e6cb6a7 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -45,12 +45,15 @@ impl Check<'_> {
             .map(|lv| (lv.id.clone(), lv.ty.clone()))
             .collect();
 
-
         // (2) Check whether the number of declared function parameters matches the number of arguments provided.
         if declared_input_tys.len() != body.args.len() {
-            bail!("Function argument number mismatch: expected {} arguments, but found {}", declared_input_tys.len(), body.args.len());
+            bail!(
+                "Function argument number mismatch: expected {} arguments, but found {}",
+                declared_input_tys.len(),
+                body.args.len()
+            );
         }
-        
+
         // (3) Check if the actual return type is the subtype of the declared return type.
         self.prove_goal(
             &env,
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 73715a9e..270ace97 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -105,7 +105,6 @@ fn test_call_terminator() {
     )
 }
 
-
 /// Test valid place mention statement.
 /// This is equivalent to:
 /// ```
@@ -381,7 +380,6 @@ fn test_incompatible_return_type() {
     )
 }
 
-
 #[test]
 fn test_function_arg_number_mismatch() {
     crate::assert_err!(

From d0e36782bc2bdc9f83d1c0449f5574309a4af086 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Tue, 15 Jul 2025 23:21:22 +0200
Subject: [PATCH 38/42] Improve some syntax after meeting

---
 crates/formality-rust/src/grammar/minirust.rs |  8 +++--
 src/test/mir_fn_bodies.rs                     | 36 +++++++++----------
 2 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 83413b35..600881ae 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -89,6 +89,7 @@ pub enum Terminator {
     //
     //    call foo(x, y)
     //    call foo.add<u32>(x, y)
+    // FIXME: allow not having next block for goto, and add a comment for it.
     #[grammar(call $callee $<?generic_arguments> $(arguments) -> $ret $:goto $next_block)]
     Call {
         /// What function or method to call.
@@ -110,9 +111,9 @@ pub enum Terminator {
 
 #[term]
 pub enum ArgumentExpression {
-    #[grammar(value($v0))]
+    #[grammar(Copy($v0))]
     ByValue(ValueExpression),
-    #[grammar(arg_place($v0))]
+    #[grammar(Move($v0))]
     InPlace(PlaceExpression),
 }
 
@@ -127,6 +128,7 @@ pub enum ValueExpression {
     // GetDiscriminant
     #[grammar(load($v0))]
     Load(PlaceExpression),
+    // TODO: literals
     // AddrOf
     // UnOp
     // BinOp
@@ -135,7 +137,7 @@ pub enum ValueExpression {
 #[term]
 pub enum PlaceExpression {
     // FIXME(tiif): if we remove the local keyword, call bar () -> v1 goto bb1; won't work
-    #[grammar(placeexpr_local($v0))]
+    #[grammar(local($v0))]
     Local(LocalId),
     // Deref(Arc<ValueExpression>),
     // Field(Arc<PlaceExpression>, FieldId),
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 270ace97..8393d08b 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -10,7 +10,7 @@ fn test_assign_statement() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -39,7 +39,7 @@ fn test_goto_terminator() {
 
                     bb1: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -77,7 +77,7 @@ fn test_call_terminator() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -89,9 +89,9 @@ fn test_call_terminator() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
-                        call fn_id foo (arg_place(placeexpr_local(v0))) -> placeexpr_local(v0) goto bb1;
+                        call fn_id foo (Move(local(v0))) -> local(v0) goto bb1;
                     }
 
                     bb1: {
@@ -127,8 +127,8 @@ fn test_place_mention_statement() {
 
                     bb0: {
                         statements {
-                            place_mention(placeexpr_local(v0));
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            place_mention(local(v0));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -161,7 +161,7 @@ fn test_invalid_assign_statement() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -191,7 +191,7 @@ fn test_invalid_local_in_place_mention() {
 
                     bb0: {
                         statements {
-                            place_mention(placeexpr_local(v2));
+                            place_mention(local(v2));
                         }
                         return;
                     }
@@ -241,9 +241,9 @@ fn test_call_invalid_fn() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
-                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
+                        call fn_id foo (Move(local(v1))) -> local(v0);
                     }
 
                 };
@@ -267,7 +267,7 @@ fn test_pass_non_subtype_arg() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -279,9 +279,9 @@ fn test_pass_non_subtype_arg() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
-                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0) goto bb1;
+                        call fn_id foo (Move(local(v1))) -> local(v0) goto bb1;
                     }
 
                     bb1: {
@@ -314,7 +314,7 @@ fn test_no_next_bb_for_call_terminator() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }
@@ -326,9 +326,9 @@ fn test_no_next_bb_for_call_terminator() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
-                        call fn_id foo (arg_place(placeexpr_local(v1))) -> placeexpr_local(v0);
+                        call fn_id foo (Move(local(v1))) -> local(v0);
                     }
 
                 };
@@ -360,7 +360,7 @@ fn test_incompatible_return_type() {
 
                     bb0: {
                         statements {
-                            placeexpr_local(v0) = load(placeexpr_local(v1));
+                            local(v0) = load(local(v1));
                         }
                         return;
                     }

From 3907b292ae9612b1d69c0a55b9d52f588cedcd05 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Tue, 15 Jul 2025 23:31:43 +0200
Subject: [PATCH 39/42] Add checks for undeclared local_id at function argument
 and return position

---
 crates/formality-check/src/mini_rust_check.rs | 12 +++++
 src/test/mir_fn_bodies.rs                     | 47 +++++++++++++++++++
 2 files changed, 59 insertions(+)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 5e6cb6a7..129ed2f2 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -39,6 +39,18 @@ impl Check<'_> {
         for lv in &body.locals {
             self.prove_goal(&env, &fn_assumptions, lv.ty.well_formed())?;
         }
+
+        // Check if the local_id in function arguments are declared.
+        for function_arg_id in &body.args {
+            if body.locals.iter().find(|declared_decl| declared_decl.id == *function_arg_id).is_none() {
+                bail!("Function argument {:?} is not declared, consider declaring them with `let {:?}: type;`", function_arg_id, function_arg_id);
+            }
+        }
+
+        // Check if the local_id in the return place are declared.
+        if body.locals.iter().find(|declared_decl| declared_decl.id == body.ret).is_none() {
+            bail!("Function return place {:?} is not declared, consider declaring them with `let {:?}: type;`", body.ret, body.ret);
+        }
         let local_variables: Map<LocalId, Ty> = body
             .locals
             .iter()
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 8393d08b..bb3deba2 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -205,6 +205,53 @@ fn test_invalid_local_in_place_mention() {
     )
 }
 
+
+// Test the behavior of having undeclared local_id in function argument.
+#[test]
+fn test_undeclared_local_in_function_arg() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo (u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+
+                    bb0: {
+                        statements {
+                        }
+                        return;
+                    }
+
+                };
+            }
+        ]
+        []
+        expect_test::expect!["Function argument v1 is not declared, consider declaring them with `let v1: type;`"]
+    )
+}
+
+
+// Test the behavior of having undeclared local_id in return place.
+#[test]
+fn test_undeclared_local_in_return_place() {
+    crate::assert_err!(
+        [
+            crate Foo {
+                fn foo () -> u32 = minirust() -> v0 {
+
+                    bb0: {
+                        statements {
+                        }
+                        return;
+                    }
+
+                };
+            }
+        ]
+        []
+        expect_test::expect!["Function return place v0 is not declared, consider declaring them with `let v0: type;`"]
+    )
+}
+
 // Test the behaviour of having invalid bb_id in goto terminator.
 #[test]
 fn test_invalid_goto_bbid() {

From f2c43e869e67da4abb8a4954fa9a27eb6e8eb09c Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Tue, 15 Jul 2025 23:33:03 +0200
Subject: [PATCH 40/42] Improve error messages for unknown local name

---
 crates/formality-check/src/mini_rust_check.rs | 2 +-
 src/test/mir_fn_bodies.rs                     | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 129ed2f2..f00e290f 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -216,7 +216,7 @@ impl Check<'_> {
                     .iter()
                     .find(|(declared_local_id, _)| *declared_local_id == local_id)
                 else {
-                    bail!("PlaceExpression::Local: unknown local name")
+                    bail!("PlaceExpression::Local: unknown local name `{:?}`", local_id)
                 };
                 place_ty = ty;
             }
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index bb3deba2..8844483d 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -200,8 +200,7 @@ fn test_invalid_local_in_place_mention() {
             }
         ]
         []
-        expect_test::expect![[r#"
-            PlaceExpression::Local: unknown local name"#]]
+        expect_test::expect!["PlaceExpression::Local: unknown local name `v2`"]
     )
 }
 

From b95e18411dd4bcf35a669c57371c058256134129 Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Tue, 15 Jul 2025 23:34:29 +0200
Subject: [PATCH 41/42] fmt

---
 crates/formality-check/src/mini_rust_check.rs | 19 ++++++++++++++++---
 src/test/mir_fn_bodies.rs                     |  2 --
 2 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index f00e290f..5cfae449 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -42,13 +42,23 @@ impl Check<'_> {
 
         // Check if the local_id in function arguments are declared.
         for function_arg_id in &body.args {
-            if body.locals.iter().find(|declared_decl| declared_decl.id == *function_arg_id).is_none() {
+            if body
+                .locals
+                .iter()
+                .find(|declared_decl| declared_decl.id == *function_arg_id)
+                .is_none()
+            {
                 bail!("Function argument {:?} is not declared, consider declaring them with `let {:?}: type;`", function_arg_id, function_arg_id);
             }
         }
 
         // Check if the local_id in the return place are declared.
-        if body.locals.iter().find(|declared_decl| declared_decl.id == body.ret).is_none() {
+        if body
+            .locals
+            .iter()
+            .find(|declared_decl| declared_decl.id == body.ret)
+            .is_none()
+        {
             bail!("Function return place {:?} is not declared, consider declaring them with `let {:?}: type;`", body.ret, body.ret);
         }
         let local_variables: Map<LocalId, Ty> = body
@@ -216,7 +226,10 @@ impl Check<'_> {
                     .iter()
                     .find(|(declared_local_id, _)| *declared_local_id == local_id)
                 else {
-                    bail!("PlaceExpression::Local: unknown local name `{:?}`", local_id)
+                    bail!(
+                        "PlaceExpression::Local: unknown local name `{:?}`",
+                        local_id
+                    )
                 };
                 place_ty = ty;
             }
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 8844483d..360da543 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -204,7 +204,6 @@ fn test_invalid_local_in_place_mention() {
     )
 }
 
-
 // Test the behavior of having undeclared local_id in function argument.
 #[test]
 fn test_undeclared_local_in_function_arg() {
@@ -228,7 +227,6 @@ fn test_undeclared_local_in_function_arg() {
     )
 }
 
-
 // Test the behavior of having undeclared local_id in return place.
 #[test]
 fn test_undeclared_local_in_return_place() {

From 3e3b065ee1424b57db24e805beb7f7a092fda58d Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 16 Jul 2025 11:27:19 +0200
Subject: [PATCH 42/42] Improve the check Terminator::Call's next block

---
 crates/formality-check/src/mini_rust_check.rs |  7 +--
 crates/formality-rust/src/grammar/minirust.rs |  3 +-
 src/test/mir_fn_bodies.rs                     | 45 ++++++++++++++++---
 3 files changed, 44 insertions(+), 11 deletions(-)

diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
index 5cfae449..6256dec4 100644
--- a/crates/formality-check/src/mini_rust_check.rs
+++ b/crates/formality-check/src/mini_rust_check.rs
@@ -198,12 +198,9 @@ impl Check<'_> {
                 )?;
 
                 // Check that the next block is valid.
-                let Some(bb_id) = next_block else {
-                    bail!(
-                        "There should be next block for Terminator::Call, but it does not exist!"
-                    );
+                if let Some(bb_id) = next_block {
+                    self.check_block_exist(typeck_env, bb_id)?;
                 };
-                self.check_block_exist(typeck_env, bb_id)?;
             }
             minirust::Terminator::Return => {
                 // Check that the return local variable has been initialized
diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs
index 600881ae..191b9ec9 100644
--- a/crates/formality-rust/src/grammar/minirust.rs
+++ b/crates/formality-rust/src/grammar/minirust.rs
@@ -51,7 +51,6 @@ pub struct LocalDecl {
 }
 
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
-// FIXME(tiif): for some reason statements is always not required
 #[term($id: {statements {$*statements} $terminator;})]
 pub struct BasicBlock {
     pub id: BbId,
@@ -101,6 +100,8 @@ pub enum Terminator {
         /// The place to put the return value into.
         ret: PlaceExpression,
         /// The block to jump to when this call returns.
+        /// In minirust, if this is None, then UB will be raised when the function returns.
+        /// FIXME(tiif): should we have the same behaviour as minirust?
         next_block: Option<BbId>,
     },
 
diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs
index 360da543..d4c79c3f 100644
--- a/src/test/mir_fn_bodies.rs
+++ b/src/test/mir_fn_bodies.rs
@@ -140,6 +140,42 @@ fn test_place_mention_statement() {
     )
 }
 
+// Test what will happen if the next block does not exist for Terminator::Call.
+#[test]
+fn test_no_next_bb_for_call_terminator() {
+    crate::assert_ok!(
+        [
+            crate Foo {
+                fn foo(u32) -> u32 = minirust(v1) -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+
+                    bb0: {
+                        statements {
+                            local(v0) = load(local(v1));
+                        }
+                        return;
+                    }
+                };
+
+                fn bar() -> u32 = minirust() -> v0 {
+                    let v0: u32;
+                    let v1: u32;
+
+                    bb0: {
+                        statements {
+                            local(v0) = load(local(v1));
+                        }
+                        call fn_id foo (Move(local(v1))) -> local(v0);
+                    }
+
+                };
+            }
+        ]
+        expect_test::expect![["()"]]
+    )
+}
+
 /// Test the behaviour of assigning value that is not subtype of the place.
 /// This is equivalent to:
 /// ```
@@ -346,9 +382,9 @@ fn test_pass_non_subtype_arg() {
     )
 }
 
-// Test what will happen if the next block does not exist for Terminator::Call.
+// Test the behaviour of having invalid next bbid Terminator::Call.
 #[test]
-fn test_no_next_bb_for_call_terminator() {
+fn test_invalid_next_bbid_for_call_terminator() {
     crate::assert_err!(
         [
             crate Foo {
@@ -372,15 +408,14 @@ fn test_no_next_bb_for_call_terminator() {
                         statements {
                             local(v0) = load(local(v1));
                         }
-                        call fn_id foo (Move(local(v1))) -> local(v0);
+                        call fn_id foo (Move(local(v1))) -> local(v0) goto bb1;
                     }
 
                 };
             }
         ]
         []
-        expect_test::expect![[r#"
-            There should be next block for Terminator::Call, but it does not exist!"#]]
+        expect_test::expect!["Basic block bb1 does not exist"]
     )
 }