From eac681bf7ee000a7aa678e25b8c4181cc5242035 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Tue, 1 Apr 2025 18:03:53 +0200
Subject: [PATCH 01/24] Deref Error and others

---
 src/ty_check/error.rs   | 29 ++++++++++++++++++---
 src/ty_check/pl_expr.rs | 57 ++++++++++++++++++++---------------------
 2 files changed, 54 insertions(+), 32 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 69174329..fde70e64 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -1,7 +1,9 @@
+use std::borrow::Borrow;
+
 use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;
-use crate::ast::{BaseExec, DataTy, Expr, Ident, NatEvalError, Ownership, PlaceExpr, TyKind};
+use crate::ast::{BaseExec, DataTy, DataTyKind, Expr, Ident, NatEvalError, Ownership, PlaceExpr, TyKind};
 use crate::error;
 use crate::error::{default_format, ErrorReported};
 use crate::parser::SourceCode;
@@ -60,6 +62,26 @@ pub enum TyError {
     UnsafeRequired,
     // TODO remove as soon as possible
     String(String),
+
+    // Newly added errors
+    IndexOutOfBounds,
+    TupleIndexOutOfBounds,
+    // The indexed expression is not an array
+    CannotIndex,
+    // The expression is not a reference
+    // TODO
+    NotAReference,
+    CannotDereference(DereferenceError),
+}
+
+#[derive(Debug)]
+pub enum DereferenceError {
+    // Trying to dereference a function (that is the only case).
+    InvalidTyKind(TyKind),
+    // Trying to dreference 
+    InvalidDataTyKind(DataTyKind),
+    // Trying to dereference a shrd reference
+    InvalidOwnership,
 }
 
 impl<'a> FromIterator<TyError> for TyError {
@@ -181,7 +203,8 @@ impl TyError {
                             eprintln!("{:?}", conflict)
                         }
                         BorrowingError::ConflictingOwnership => eprintln!("{:?}", conflict),
-                        BorrowingError::ConflictingAccess => eprintln!("{:?}", conflict),
+                        // TODO: better error message for conflicting access
+                        BorrowingError::ConflictingAccess(_, _) => eprintln!("{:?}", conflict),
                         BorrowingError::CtxError(ctx_err) => eprintln!("{:?}", ctx_err),
                         BorrowingError::WrongDevice(under, from) => {
                             eprintln!("error: wrong device\nunder:{:?}\nfrom:{:?}", under, from)
@@ -317,7 +340,7 @@ pub enum BorrowingError {
     //     loan with {} capability.",
     // checked_own, ref_own
     ConflictingOwnership,
-    ConflictingAccess,
+    ConflictingAccess(Ownership, Ownership),
     // The borrowing place is not in the reborrow list
     BorrowNotInReborrowList(Place),
     TemporaryConflictingBorrow(String),
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index 3739792e..5f45ad65 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -1,5 +1,5 @@
 use super::borrow_check::BorrowCheckCtx;
-use super::error::TyError;
+use super::error::{BorrowingError, DereferenceError, TyError};
 use super::TyResult;
 use crate::ast::{
     utils, DataTy, DataTyKind, ExecExpr, ExecTyKind, FnTy, Ident, IdentExec, Memory, Nat, NatCtx,
@@ -191,10 +191,11 @@ fn ty_check_ident(
     // if let Ok(tty) = ctx.ty_ctx.ty_of_ident(ident) {
     let tty = ctx.ty_ctx.ty_of_ident(ident)?;
     if !&tty.is_fully_alive() {
-        return Err(TyError::String(format!(
-            "The value in `{}` has been moved out.",
-            ident
-        )));
+        // return Err(TyError::String(format!(
+        //     "The value in `{}` has been moved out.",
+        //     ident
+        // )));
+        return Err(TyError::DeadTy);
     }
     // FIXME Should throw an error if thread local memory is accessed by a block
     //  for example.
@@ -254,9 +255,10 @@ fn ty_check_proj(
                     passed_prvs,
                 ))
             } else {
-                Err(TyError::String(
-                    "Trying to access non existing tuple element.".to_string(),
-                ))
+                // Err(TyError::String(
+                //     "Trying to access non existing tuple element.".to_string(),
+                // ))
+                Err(TyError::TupleIndexOutOfBounds)
             }
         }
         dty_kind => Err(TyError::ExpectedTupleType(
@@ -311,16 +313,21 @@ fn ty_check_deref(
     let borr_dty = if let TyKind::Data(dty) = &borr_expr.ty.as_ref().unwrap().ty {
         dty
     } else {
-        return Err(TyError::String(
-            "Trying to dereference non reference type.".to_string(),
-        ));
+        // return Err(TyError::String(
+        //     "Trying to dereference a function.".to_string(),
+        // ));
+        return Err(TyError::CannotDereference(DereferenceError::InvalidTyKind(
+            (&borr_expr).ty.as_ref().unwrap().ty.to_owned(),
+        )));
     };
     match &borr_dty.dty {
         DataTyKind::Ref(reff) => {
             if reff.own < ctx.own {
-                return Err(TyError::String(
-                    "Trying to dereference and mutably use a shrd reference.".to_string(),
-                ));
+                // if the expression dereferences a shared reference
+                return Err(
+                    TyError::CannotDereference(DereferenceError::InvalidOwnership), // TyError::String(
+                                                                                    // "Trying to dereference and mutably use a shrd reference.".to_string(),
+                );
             }
             passed_prvs.push(reff.rgn.clone());
             inner_mem.push(reff.mem.clone());
@@ -331,15 +338,15 @@ fn ty_check_deref(
             ))
         }
         DataTyKind::RawPtr(dty) => {
-            // TODO is anything of this correct?
+            // TODO is any of this correct?
             Ok((
                 Ty::new(TyKind::Data(Box::new(dty.as_ref().clone()))),
                 inner_mem,
                 passed_prvs,
             ))
         }
-        _ => Err(TyError::String(
-            "Trying to dereference non reference type.".to_string(),
+        invalid_type => Err(TyError::CannotDereference(
+            DereferenceError::InvalidDataTyKind(invalid_type.clone()),
         )),
     }
 }
@@ -396,9 +403,7 @@ fn ty_check_index(
     let pl_expr_dty = if let TyKind::Data(dty) = &pl_expr.ty.as_ref().unwrap().ty {
         dty
     } else {
-        return Err(TyError::String(
-            "Trying to index into non array type.".to_string(),
-        ));
+        return Err(TyError::CannotIndex);
     };
     let (elem_dty, n) = match pl_expr_dty.dty.clone() {
         DataTyKind::Array(elem_dty, n) | DataTyKind::ArrayShape(elem_dty, n) => (*elem_dty, n),
@@ -406,22 +411,16 @@ fn ty_check_index(
             if let DataTyKind::Array(elem_ty, n) = &arr_dty.dty {
                 (elem_ty.as_ref().clone(), n.clone())
             } else {
-                return Err(TyError::String(
-                    "Trying to index into non array type.".to_string(),
-                ));
+                return Err(TyError::CannotIndex);
             }
         }
         _ => {
-            return Err(TyError::String(
-                "Trying to index into non array type.".to_string(),
-            ))
+            return Err(TyError::CannotIndex);
         }
     };
 
     if n.eval(ctx.nat_ctx)? <= idx.eval(ctx.nat_ctx)? {
-        return Err(TyError::String(
-            "Trying to access array out-of-bounds.".to_string(),
-        ));
+        return Err(TyError::IndexOutOfBounds);
     }
 
     Ok((Ty::new(TyKind::Data(Box::new(elem_dty))), mems, passed_prvs))

From d7c8d0ca923af9f183b4755594fb1cff2747c168 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Wed, 2 Apr 2025 22:28:24 +0200
Subject: [PATCH 02/24] remove all TyError::String from pl_expr.rs

---
 src/ty_check/error.rs   | 12 ++++++++----
 src/ty_check/pl_expr.rs | 15 +++++++--------
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index fde70e64..3c959247 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -3,7 +3,9 @@ use std::borrow::Borrow;
 use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;
-use crate::ast::{BaseExec, DataTy, DataTyKind, Expr, Ident, NatEvalError, Ownership, PlaceExpr, TyKind};
+use crate::ast::{
+    BaseExec, DataTy, DataTyKind, Expr, Ident, NatEvalError, Ownership, PlaceExpr, TyKind,
+};
 use crate::error;
 use crate::error::{default_format, ErrorReported};
 use crate::parser::SourceCode;
@@ -69,16 +71,18 @@ pub enum TyError {
     // The indexed expression is not an array
     CannotIndex,
     // The expression is not a reference
-    // TODO
-    NotAReference,
     CannotDereference(DereferenceError),
+    // Struct does not have given field
+    FieldProjError(Ident),
+    // Select must be applied to an array or a view.
+    SelectError(PlaceExpr),
 }
 
 #[derive(Debug)]
 pub enum DereferenceError {
     // Trying to dereference a function (that is the only case).
     InvalidTyKind(TyKind),
-    // Trying to dreference 
+    // Trying to dereference something that is not a reference
     InvalidDataTyKind(DataTyKind),
     // Trying to dereference a shrd reference
     InvalidOwnership,
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index 5f45ad65..d62f5b3c 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -293,9 +293,7 @@ fn ty_check_field_proj(
                     passed_prvs,
                 ))
             } else {
-                Err(TyError::String(
-                    "Trying to access non existing struct field.".to_string(),
-                ))
+                Err(TyError::FieldProjError(ident.clone()))
             }
         }
         dty_kind => Err(TyError::ExpectedTupleType(
@@ -324,10 +322,9 @@ fn ty_check_deref(
         DataTyKind::Ref(reff) => {
             if reff.own < ctx.own {
                 // if the expression dereferences a shared reference
-                return Err(
-                    TyError::CannotDereference(DereferenceError::InvalidOwnership), // TyError::String(
-                                                                                    // "Trying to dereference and mutably use a shrd reference.".to_string(),
-                );
+                return Err(TyError::CannotDereference(
+                    DereferenceError::InvalidOwnership,
+                ));
             }
             passed_prvs.push(reff.rgn.clone());
             inner_mem.push(reff.mem.clone());
@@ -388,7 +385,9 @@ fn ty_check_select(
             p_dty = *elem_dty;
         }
         _ => {
-            return Err(TyError::String("Expected an array or view.".to_string()));
+            // Select distributes ownership for an array or a view.
+            // return Err(TyError::String("Expected an array or view.".to_string()));
+            return Err(TyError::SelectError(p.clone()));
         }
     }
     Ok((Ty::new(TyKind::Data(Box::new(p_dty))), mems, prvs))

From 4a26df3f14694229cdee48b6dd0d9a4085cee734 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Sat, 5 Apr 2025 18:50:01 +0200
Subject: [PATCH 03/24] Remove all errors from exec.rs

---
 src/ast/mod.rs          |  1 +
 src/ty_check/error.rs   | 20 +++++++++++++++-
 src/ty_check/exec.rs    | 52 ++++++++++++++++++++---------------------
 src/ty_check/pl_expr.rs |  2 +-
 4 files changed, 47 insertions(+), 28 deletions(-)

diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index 0d095fab..e97ccf25 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -1216,6 +1216,7 @@ impl Dim {
 }
 
 #[derive(PartialEq, Eq, PartialOrd, Hash, Debug, Copy, Clone)]
+// Dimension Component
 pub enum DimCompo {
     X,
     Y,
diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 3c959247..7ed19d00 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -4,7 +4,8 @@ use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;
 use crate::ast::{
-    BaseExec, DataTy, DataTyKind, Expr, Ident, NatEvalError, Ownership, PlaceExpr, TyKind,
+    BaseExec, DataTy, DataTyKind, DimCompo, ExecTyKind, Expr, Ident, NatEvalError, Ownership,
+    PlaceExpr, TyKind,
 };
 use crate::error;
 use crate::error::{default_format, ErrorReported};
@@ -76,6 +77,23 @@ pub enum TyError {
     FieldProjError(Ident),
     // Select must be applied to an array or a view.
     SelectError(PlaceExpr),
+    // Errors from exec.rs
+    ExecError(ExecError),
+}
+
+#[derive(Debug)]
+pub enum ExecError {
+    UnexpectedResourceType(ExecTyKind),
+    DimensionNotFound(DimCompo, ExecTyKind),
+    ExecToWarpError(ExecToWarpError),
+    InvalidSplit(ExecTyKind)
+}
+
+#[derive(Debug)]
+pub enum ExecToWarpError {
+    MultipleDimensions(ExecTyKind),
+    DimNotDivBy32(ExecTyKind),
+    InvalidResourceType(ExecTyKind),
 }
 
 #[derive(Debug)]
diff --git a/src/ty_check/exec.rs b/src/ty_check/exec.rs
index cb031d39..3bca0184 100644
--- a/src/ty_check/exec.rs
+++ b/src/ty_check/exec.rs
@@ -1,6 +1,6 @@
 use super::{
-    BaseExec, BinOpNat, Dim, Dim1d, Dim2d, DimCompo, ExecExpr, ExecPathElem, ExecTy, ExecTyKind,
-    IdentExec, Nat, TyCtx, TyError, TyResult,
+    error::ExecError, BaseExec, BinOpNat, Dim, Dim1d, Dim2d, DimCompo, ExecExpr, ExecPathElem,
+    ExecTy, ExecTyKind, IdentExec, Nat, TyCtx, TyError, TyResult,
 };
 use crate::ast::{LeftOrRight, NatCtx};
 
@@ -71,10 +71,10 @@ fn ty_check_exec_to_threads(d: DimCompo, exec_ty: &ExecTyKind) -> TyResult<ExecT
                 Box::new(b.0),
             )))),
             _ => {
-                return Err(TyError::String(format!(
-                    "Provided dimension {} does not exist",
-                    d
-                )))
+                return Err(TyError::ExecError(ExecError::DimensionNotFound(
+                    d,
+                    exec_ty.clone(),
+                )));
             }
         };
         match (rest_gdim, rest_bdim) {
@@ -85,19 +85,22 @@ fn ty_check_exec_to_threads(d: DimCompo, exec_ty: &ExecTyKind) -> TyResult<ExecT
             _ => unimplemented!(),
         }
     } else {
-        Err(TyError::UnexpectedType)
+        Err(TyError::ExecError(ExecError::UnexpectedResourceType(
+            exec_ty.clone(),
+        )))
     }
 }
 
 fn ty_check_exec_to_warps(nat_ctx: &NatCtx, exec_ty: &ExecTyKind) -> TyResult<ExecTyKind> {
+    use super::ExecToWarpError::*;
+    use ExecError::*;
     match exec_ty {
         ExecTyKind::GpuBlock(dim) => match dim.clone() {
             Dim::X(d) => {
                 if d.0.eval(nat_ctx)? % 32 != 0 {
-                    Err(TyError::String(format!(
-                        "Size of GpuBlock needs to be evenly divisible by 32 to create warps, instead got: {:?}",
-                        exec_ty
-                    )))
+                    Err(TyError::ExecError(ExecToWarpError(DimNotDivBy32(
+                        exec_ty.clone(),
+                    ))))
                 } else {
                     Ok(ExecTyKind::GpuWarpGrp(Nat::BinOp(
                         BinOpNat::Div,
@@ -106,15 +109,13 @@ fn ty_check_exec_to_warps(nat_ctx: &NatCtx, exec_ty: &ExecTyKind) -> TyResult<Ex
                     )))
                 }
             }
-            _ => Err(TyError::String(format!(
-                "GpuBlock needs to be one-dimensional to create warps, instead got: {:?}",
-                exec_ty
-            ))),
+            _ => Err(TyError::ExecError(ExecToWarpError(MultipleDimensions(
+                exec_ty.clone(),
+            )))),
         },
-        _ => Err(TyError::String(format!(
-            "Trying to create warps from {:?}",
-            exec_ty
-        ))),
+        _ => Err(TyError::ExecError(ExecToWarpError(InvalidResourceType(
+            exec_ty.clone(),
+        )))),
     }
 }
 
@@ -159,13 +160,17 @@ fn ty_check_exec_forall(d: DimCompo, exec_ty: &ExecTyKind) -> TyResult<ExecTyKin
             }
         }
         ex @ ExecTyKind::CpuThread | ex @ ExecTyKind::GpuThread | ex @ ExecTyKind::Any => {
-            return Err(TyError::String(format!("Cannot schedule over {:?}", ex)))
+            return Err(TyError::ExecError(ExecError::UnexpectedResourceType(
+                ex.clone(),
+            )))
         }
     };
     Ok(res_ty)
 }
 
 pub fn remove_dim(dim: &Dim, dim_compo: DimCompo) -> TyResult<(Option<Dim>, Dim)> {
+    // given (dimension, dimension component)
+    // return (left over dimension, dimension from removing the specific dimension component)
     match (dim, dim_compo) {
         (Dim::XYZ(dim3d), DimCompo::X) => Ok((
             Some(Dim::YZ(Box::new(Dim2d(
@@ -264,12 +269,7 @@ fn ty_check_exec_take_range(
                 panic!("GpuToThreads is not well-formed.")
             }
         }
-        ex => {
-            return Err(TyError::String(format!(
-                "Trying to split non-splittable execution resource: {:?}",
-                ex
-            )))
-        }
+        ex => return Err(TyError::ExecError(ExecError::InvalidSplit(ex.clone()))),
     };
     Ok(if proj == LeftOrRight::Left {
         lexec_ty
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index d62f5b3c..b779a8e5 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -380,7 +380,7 @@ fn ty_check_select(
             // TODO check sizes
             // if n != distrib_exec.active_distrib_size() {
             //     return Err(TyError::String("There must be as many elements in the view
-            //  as there exist execution resources that select from it.".to_string()));
+            //  as there exist execution rces that select from it.".to_string()));
             // }
             p_dty = *elem_dty;
         }

From 79e9871da517695afe8405fa354651351622a158 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Sat, 5 Apr 2025 18:52:07 +0200
Subject: [PATCH 04/24] fix simple typo

---
 src/ty_check/mod.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 09511b08..a6e7be05 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -265,7 +265,7 @@ fn syncable_under_exec(synced: &ExecExpr, under: &ExecExpr) -> TyResult<()> {
         for ep in &under.exec.path[synced.exec.path.len()..] {
             if matches!(ep, ExecPathElem::TakeRange(_)) {
                 return Err(TyError::String(
-                    "tyring to synchronize on split execution resource".to_string(),
+                    "trying to synchronize on split execution resource".to_string(),
                 ));
             }
         }

From fc5faa105f2902ac5704201d65c2c85439756027 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Sun, 6 Apr 2025 18:38:57 +0200
Subject: [PATCH 05/24] remove more string errors

---
 src/ty_check/error.rs   | 41 +++++++++++++++++++---
 src/ty_check/mod.rs     | 78 ++++++++++++++++++-----------------------
 src/ty_check/pl_expr.rs |  5 +--
 3 files changed, 71 insertions(+), 53 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 7ed19d00..fba52aa9 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -4,8 +4,8 @@ use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;
 use crate::ast::{
-    BaseExec, DataTy, DataTyKind, DimCompo, ExecTyKind, Expr, Ident, NatEvalError, Ownership,
-    PlaceExpr, TyKind,
+    BaseExec, DataTy, DataTyKind, DimCompo, ExecTy, ExecTyKind, Expr, FnTy, Ident, Memory,
+    NatEvalError, Ownership, PlaceExpr, RefDty, TyKind,
 };
 use crate::error;
 use crate::error::{default_format, ErrorReported};
@@ -68,17 +68,46 @@ pub enum TyError {
 
     // Newly added errors
     IndexOutOfBounds,
-    TupleIndexOutOfBounds,
+    // Index, Array Length
+    TupleIndexOutOfBounds(usize, usize),
     // The indexed expression is not an array
     CannotIndex,
+    // The projected expression is not a tuple
+    CannotTupleIndex,
     // The expression is not a reference
     CannotDereference(DereferenceError),
     // Struct does not have given field
     FieldProjError(Ident),
     // Select must be applied to an array or a view.
     SelectError(PlaceExpr),
-    // Errors from exec.rs
     ExecError(ExecError),
+    SyncError(SyncError),
+    InvalidIterable(InvalidIterable),
+    NotCopyable,
+    Moved(PlaceExpr, Moved),
+}
+
+#[derive(Debug)]
+pub enum Moved {
+    Partially,
+    Entirely,
+}
+
+#[derive(Debug)]
+pub enum InvalidIterable {
+    // Do I need to contain the Expr so that the span is known?
+    // Should I just return the span and the DataTyKind?
+    InvalidIterable(Expr, DataTyKind),
+    // It's obvious when it's a function.
+    UnexpectedFunction(Expr),
+    NotArrayRef(Expr, RefDty),
+}
+
+#[derive(Debug)]
+pub enum SyncError {
+    InvalidResourceType,
+    SplitResource,
+    NothingToSync,
 }
 
 #[derive(Debug)]
@@ -86,7 +115,7 @@ pub enum ExecError {
     UnexpectedResourceType(ExecTyKind),
     DimensionNotFound(DimCompo, ExecTyKind),
     ExecToWarpError(ExecToWarpError),
-    InvalidSplit(ExecTyKind)
+    InvalidSplit(ExecTyKind),
 }
 
 #[derive(Debug)]
@@ -104,6 +133,8 @@ pub enum DereferenceError {
     InvalidDataTyKind(DataTyKind),
     // Trying to dereference a shrd reference
     InvalidOwnership,
+    // Trying to dereference something that is not in the current resource
+    NotInExecRes(Memory, ExecTyKind),
 }
 
 impl<'a> FromIterator<TyError> for TyError {
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index a6e7be05..5f4576e3 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -255,25 +255,25 @@ fn ty_check_sync(ctx: &mut ExprTyCtx, exec: &mut Option<ExecExpr>) -> TyResult<T
 }
 
 // assumes fully typed ExecExpr as input
+// T-Sync
 fn syncable_under_exec(synced: &ExecExpr, under: &ExecExpr) -> TyResult<()> {
+    // y : ε ⊢ e′ : ε′
     if !syncable_exec_ty(synced.ty.as_ref().unwrap()) {
-        return Err(TyError::String(
-            "trying to synchronize non-synchronizable execution resource".to_string(),
-        ));
+        // ε′∉{ gpu.Block d, gpu.Warp }
+        return Err(TyError::SyncError(SyncError::InvalidResourceType));
     }
     if under.is_sub_exec_of(synced) || under == synced {
         for ep in &under.exec.path[synced.exec.path.len()..] {
             if matches!(ep, ExecPathElem::TakeRange(_)) {
-                return Err(TyError::String(
-                    "trying to synchronize on split execution resource".to_string(),
-                ));
+                // return Err(TyError::String(
+                //     "trying to synchronize on split execution resource".to_string(),
+                // ));
+                return Err(TyError::SyncError(SyncError::SplitResource));
             }
         }
         Ok(())
     } else {
-        Err(TyError::String(
-            "cannot call sync from this execution resource".to_string(),
-        ))
+        Err(TyError::SyncError(SyncError::NothingToSync))
     }
 }
 
@@ -335,6 +335,7 @@ fn ty_check_for_nat(
     )))))
 }
 
+// TODO This doesn't exist in the type formalization.
 fn ty_check_for(
     ctx: &mut ExprTyCtx,
     ident: &Ident,
@@ -342,13 +343,13 @@ fn ty_check_for(
     body: &mut Expr,
 ) -> TyResult<Ty> {
     ty_check_expr(ctx, collec)?;
-    let collec_dty = if let TyKind::Data(collec_dty) = &collec.ty.as_ref().unwrap().ty {
-        collec_dty.as_ref()
-    } else {
-        return Err(TyError::String(format!(
-            "Expected array data type or reference to array data type, but found {:?}",
-            collec.ty.as_ref().unwrap()
-        )));
+    let collec_dty = match &collec.ty.as_ref().unwrap().ty {
+        TyKind::Data(collec_dty) => collec_dty.as_ref(),
+        TyKind::FnTy(_) => {
+            return Err(TyError::InvalidIterable(
+                InvalidIterable::UnexpectedFunction(collec.clone()),
+            ))
+        }
     };
 
     let ident_dty = match &collec_dty.dty {
@@ -368,17 +369,17 @@ fn ty_check_for(
                 elem_dty.as_ref().clone(),
             ))),
             _ => {
-                return Err(TyError::String(format!(
-                    "Expected reference to array data type, but found {:?}",
-                    reff.dty.as_ref(),
+                return Err(TyError::InvalidIterable(InvalidIterable::NotArrayRef(
+                    collec.clone(),
+                    (**reff).clone(),
                 )))
             }
         },
         // DataTyKind::Range => DataTyKind::Scalar(ScalarTy::I32),
-        _ => {
-            return Err(TyError::String(format!(
-                "Expected array data type or reference to array data type, but found {:?}",
-                collec.ty.as_ref().unwrap()
+        dty => {
+            return Err(TyError::InvalidIterable(InvalidIterable::InvalidIterable(
+                collec.clone(),
+                dty.clone(),
             )));
         }
     };
@@ -1567,7 +1568,7 @@ fn ty_check_non_place(ctx: &mut ExprTyCtx, pl_expr: &mut PlaceExpr) -> TyResult<
     if pl_expr.ty.as_ref().unwrap().copyable() {
         Ok(pl_expr.ty.as_ref().unwrap().as_ref().clone())
     } else {
-        Err(TyError::String("Data type is not copyable.".to_string()))
+        Err(TyError::NotCopyable)
     }
 }
 
@@ -1576,10 +1577,7 @@ fn ty_check_place(ctx: &mut ExprTyCtx, pl_expr: &mut PlaceExpr) -> TyResult<Ty>
     let place = pl_expr.clone().to_place().unwrap();
     let pl_ty = ctx.ty_ctx.place_dty(&place)?;
     if !pl_ty.is_fully_alive() {
-        return Err(TyError::String(format!(
-            "Part of Place {:?} was moved before.",
-            pl_expr
-        )));
+        return Err(TyError::Moved(pl_expr.clone(), Moved::Partially));
     }
     if pl_ty.copyable() {
         // TODO refactor
@@ -1626,13 +1624,11 @@ fn ty_check_borrow(
         .try_for_each(|mem| accessible_memory(ctx.exec.ty.as_ref().unwrap().as_ref(), mem))?;
     let pl_expr_ty = pl_expr.ty.as_ref().unwrap();
     if !pl_expr_ty.is_fully_alive() {
-        return Err(TyError::String(
-            "The place was at least partially moved before.".to_string(),
-        ));
+        return Err(TyError::Moved(pl_expr.clone(), Moved::Partially));
     }
     let (reffed_ty, rmem) = match &pl_expr_ty.ty {
         TyKind::Data(dty) => match &dty.dty {
-            DataTyKind::Dead(_) => panic!("Cannot happen because of the alive check."),
+            DataTyKind::Dead(_) => return Err(TyError::DeadTy),
             DataTyKind::At(inner_ty, m) => (inner_ty.as_ref().clone(), m.clone()),
             _ => (
                 dty.as_ref().clone(),
@@ -1648,7 +1644,7 @@ fn ty_check_borrow(
                 },
             ),
         },
-        TyKind::FnTy(_) => return Err(TyError::String("Trying to borrow a function.".to_string())),
+        TyKind::FnTy(_) => return Err(TyError::UnexpectedType),
     };
     if rmem == Memory::GpuLocal {
         return Err(TyError::String(
@@ -1686,9 +1682,9 @@ pub fn accessible_memory(exec_ty: &ExecTy, mem: &Memory) -> TyResult<()> {
     if allowed_mem_for_exec(&exec_ty.ty).contains(mem) {
         Ok(())
     } else {
-        Err(TyError::String(format!(
-            "Trying to dereference pointer to `{:?}` from execution resource `{:?}`",
-            mem, &exec_ty.ty
+        Err(TyError::CannotDereference(DereferenceError::NotInExecRes(
+            mem.clone(),
+            exec_ty.ty.clone(),
         )))
     }
 }
@@ -1893,14 +1889,8 @@ pub fn proj_elem_dty(dty: &DataTy, i: usize) -> TyResult<DataTy> {
     match &dty.dty {
         DataTyKind::Tuple(dtys) => match dtys.get(i) {
             Some(dty) => Ok(dty.clone()),
-            None => Err(TyError::String(format!(
-                "Cannot project element `{}` from tuple with {} elements.",
-                i,
-                dtys.len()
-            ))),
+            None => Err(TyError::TupleIndexOutOfBounds(i, dtys.len())),
         },
-        _ => Err(TyError::String(
-            "Cannot project from non tuple type.".to_string(),
-        )),
+        _ => Err(TyError::CannotTupleIndex),
     }
 }
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index b779a8e5..bcb5077d 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -255,10 +255,7 @@ fn ty_check_proj(
                     passed_prvs,
                 ))
             } else {
-                // Err(TyError::String(
-                //     "Trying to access non existing tuple element.".to_string(),
-                // ))
-                Err(TyError::TupleIndexOutOfBounds)
+                Err(TyError::TupleIndexOutOfBounds(n, elem_dtys.len()))
             }
         }
         dty_kind => Err(TyError::ExpectedTupleType(

From 47c5ec2f69a4a37b1839afc133ccc8c4f9b0065a Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Wed, 9 Apr 2025 20:00:27 +0200
Subject: [PATCH 06/24] Add errors for struct field access

---
 src/ty_check/error.rs   | 1 +
 src/ty_check/pl_expr.rs | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index fba52aa9..430b24ac 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -41,6 +41,7 @@ pub enum TyError {
     SplittingNonViewArray,
     // Expected a different type
     ExpectedTupleType(TyKind, PlaceExpr),
+    ExpectedStructType(TyKind, PlaceExpr),
     // Trying to borrow uniquely but place is not mutable
     ConstBorrow(PlaceExpr),
     // The borrowed view type is at least paritally dead
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index bcb5077d..07efe035 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -274,7 +274,8 @@ fn ty_check_field_proj(
     let struct_dty = match &struct_expr.ty.as_ref().unwrap().ty {
         TyKind::Data(dty) => dty,
         ty_kind => {
-            return Err(TyError::ExpectedTupleType(
+            // FUCK
+            return Err(TyError::ExpectedStructType(
                 ty_kind.clone(),
                 struct_expr.clone(),
             ));

From 12b0388ff313535005fb67d78cac7398e2b6e880 Mon Sep 17 00:00:00 2001
From: "a0+1@berkeley.edu" <mj9012159@gmail.com>
Date: Thu, 10 Apr 2025 15:16:40 +0200
Subject: [PATCH 07/24] small typo

---
 src/ty_check/infer_kinded_args.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ty_check/infer_kinded_args.rs b/src/ty_check/infer_kinded_args.rs
index 94bb916c..6caf90b0 100644
--- a/src/ty_check/infer_kinded_args.rs
+++ b/src/ty_check/infer_kinded_args.rs
@@ -12,7 +12,7 @@ use std::collections::HashMap;
 //  instantiation of a bound identifier
 pub fn infer_kinded_args(poly_fn_ty: &FnTy, mono_fn_ty: &FnTy) -> TyResult<Vec<ArgKinded>> {
     if poly_fn_ty.param_sigs.len() != mono_fn_ty.param_sigs.len() {
-        panic!("Unexpected difference in amount of paramters.")
+        panic!("Unexpected difference in amount of parameters.")
     }
     let mut res_map = HashMap::new();
     for (subst_ty, mono_ty) in poly_fn_ty.param_sigs.iter().zip(&mono_fn_ty.param_sigs) {

From 324f8591653b5ba29514ba21da6405ce54ef7f08 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 12:58:35 +0200
Subject: [PATCH 08/24] Add error enums for for loops

---
 src/ty_check/error.rs |  7 +++++++
 src/ty_check/mod.rs   | 23 +++++++++++++++--------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 430b24ac..d8ed2e1d 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -86,6 +86,7 @@ pub enum TyError {
     InvalidIterable(InvalidIterable),
     NotCopyable,
     Moved(PlaceExpr, Moved),
+    ForLoopError(ForLoopError),
 }
 
 #[derive(Debug)]
@@ -138,6 +139,12 @@ pub enum DereferenceError {
     NotInExecRes(Memory, ExecTyKind),
 }
 
+#[derive(Debug)]
+pub enum ForLoopError {
+    InvalidBlockType(DataTy),
+    ScopeError,
+}
+
 impl<'a> FromIterator<TyError> for TyError {
     fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
         TyError::MultiError(iter.into_iter().collect())
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 5f4576e3..7c309de6 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -308,26 +308,35 @@ fn ty_check_for_nat(
     // TODO make this a block
     body: &mut Expr,
 ) -> TyResult<Ty> {
+    // We probably can remove this vec clone.
     let compare_ty_ctx = ctx.ty_ctx.clone();
     let lifted_range = range.lift(ctx.nat_ctx)?;
 
     for i in lifted_range {
+        // Attach a new context frame and add the loop variable for the type checking within the loop.
         ctx.ty_ctx.push_empty_frame();
         ctx.nat_ctx.push_empty_frame();
-        ctx.nat_ctx.append(&ident.name, i);
 
+        // Add the loop variable to the body context and typecheck
+        ctx.nat_ctx.append(&ident.name, i);
         ty_check_expr(ctx, body)?;
 
+        // Remove the context frames used within the body.
         ctx.nat_ctx.pop_frame();
         ctx.ty_ctx.pop_frame();
+
         if let DataTyKind::Scalar(ScalarTy::Unit) = &body.ty.as_ref().unwrap().dty().dty {
             if ctx.ty_ctx != &compare_ty_ctx {
-                return Err(TyError::String(
-                    "Using a data type in loop that can only be used once.".to_string(),
-                ));
+                // At this point, the type context outside of the loop was mutated while type checking the for body.
+                // Using a data type in loop body that can only be used once.
+                // TODO: actually track exactly where it happens.
+                return Err(TyError::ForLoopError(ForLoopError::ScopeError));
             }
         } else {
-            return Err(TyError::UnexpectedType);
+            let body_type = body.ty.as_ref().unwrap().dty().clone();
+            return Err(TyError::ForLoopError(ForLoopError::InvalidBlockType(
+                body_type,
+            )));
         }
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
@@ -395,9 +404,7 @@ fn ty_check_for(
     ty_check_expr(ctx, body)?;
     ctx.ty_ctx.pop_frame();
     if ctx.ty_ctx != &compare_ty_ctx {
-        return Err(TyError::String(
-            "Using a data type in loop that can only be used once.".to_string(),
-        ));
+        return Err(TyError::ForLoopError(ForLoopError::ScopeError));
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
         DataTyKind::Scalar(ScalarTy::Unit),

From 13dba07f00c63c8e053b2205189bd18810b8168f Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 16:48:24 +0200
Subject: [PATCH 09/24] remove string errors for while loops

---
 src/ty_check/error.rs |  5 +++--
 src/ty_check/mod.rs   | 43 +++++++++++++++++++++++++------------------
 2 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index d8ed2e1d..a226d8e1 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -86,7 +86,7 @@ pub enum TyError {
     InvalidIterable(InvalidIterable),
     NotCopyable,
     Moved(PlaceExpr, Moved),
-    ForLoopError(ForLoopError),
+    LoopError(LoopError),
 }
 
 #[derive(Debug)]
@@ -140,8 +140,9 @@ pub enum DereferenceError {
 }
 
 #[derive(Debug)]
-pub enum ForLoopError {
+pub enum LoopError {
     InvalidBlockType(DataTy),
+    InvalidConditionType(Ty),
     ScopeError,
 }
 
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 7c309de6..53d96159 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -330,13 +330,11 @@ fn ty_check_for_nat(
                 // At this point, the type context outside of the loop was mutated while type checking the for body.
                 // Using a data type in loop body that can only be used once.
                 // TODO: actually track exactly where it happens.
-                return Err(TyError::ForLoopError(ForLoopError::ScopeError));
+                return Err(TyError::LoopError(LoopError::ScopeError));
             }
         } else {
             let body_type = body.ty.as_ref().unwrap().dty().clone();
-            return Err(TyError::ForLoopError(ForLoopError::InvalidBlockType(
-                body_type,
-            )));
+            return Err(TyError::LoopError(LoopError::InvalidBlockType(body_type)));
         }
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
@@ -404,7 +402,7 @@ fn ty_check_for(
     ty_check_expr(ctx, body)?;
     ctx.ty_ctx.pop_frame();
     if ctx.ty_ctx != &compare_ty_ctx {
-        return Err(TyError::ForLoopError(ForLoopError::ScopeError));
+        return Err(TyError::LoopError(LoopError::ScopeError));
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
         DataTyKind::Scalar(ScalarTy::Unit),
@@ -420,17 +418,13 @@ fn ty_check_while(ctx: &mut ExprTyCtx, cond: &mut Expr, body: &mut Expr) -> TyRe
     // Is it better/more correct to push and pop scope around this as well?
     ty_check_expr(ctx, cond)?;
     if ctx.ty_ctx != &compare_ty_ctx {
-        return Err(TyError::String(
-            "Context should have stayed the same".to_string(),
-        ));
+        return Err(TyError::LoopError(LoopError::ScopeError));
     }
     ctx.ty_ctx.push_empty_frame();
     ty_check_expr(ctx, body)?;
     ctx.ty_ctx.pop_frame();
     if ctx.ty_ctx != &compare_ty_ctx {
-        return Err(TyError::String(
-            "Context should have stayed the same".to_string(),
-        ));
+        return Err(TyError::LoopError(LoopError::ScopeError));
     }
 
     let cond_ty = cond.ty.as_ref().unwrap();
@@ -443,9 +437,12 @@ fn ty_check_while(ctx: &mut ExprTyCtx, cond: &mut Expr, body: &mut Expr) -> TyRe
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Expected condition in while loop, instead got {:?}",
-            cond_ty
+        // return Err(TyError::String(format!(
+        //     "Expected condition in while loop, instead got {:?}",
+        //     cond_ty
+        // )));
+        return Err(TyError::LoopError(LoopError::InvalidConditionType(
+            (**cond_ty).clone(),
         )));
     }
     if !matches_dty!(
@@ -455,10 +452,20 @@ fn ty_check_while(ctx: &mut ExprTyCtx, cond: &mut Expr, body: &mut Expr) -> TyRe
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Body of while loop is not of unit type, instead got {:?}",
-            body_ty
-        )));
+        // return Err(TyError::String(format!(
+        //     "Body of while loop is not of unit type, instead got {:?}",
+        //     body_ty
+        // )));
+        match &body_ty.ty {
+            TyKind::Data(dty) => {
+                return Err(TyError::LoopError(LoopError::InvalidBlockType(
+                    (**dty).clone(),
+                )))
+            }
+            TyKind::FnTy(_) => {
+                unreachable!("while body is a function")
+            }
+        }
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
         DataTyKind::Scalar(ScalarTy::Unit),

From 0856b2ec2a0c9224626584573e666950c8fbd6c6 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 16:55:09 +0200
Subject: [PATCH 10/24] add proper errors to if/else block

---
 src/ty_check/error.rs |  8 ++++++++
 src/ty_check/mod.rs   | 15 ++++++---------
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index a226d8e1..33de2077 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -87,6 +87,7 @@ pub enum TyError {
     NotCopyable,
     Moved(PlaceExpr, Moved),
     LoopError(LoopError),
+    IfElseError(IfElseError),
 }
 
 #[derive(Debug)]
@@ -146,6 +147,13 @@ pub enum LoopError {
     ScopeError,
 }
 
+#[derive(Debug)]
+pub enum IfElseError {
+    InvalidConditionType(Ty),
+    InvalidIfBlockType(Ty),
+    InvalidElseBlockType(Ty),
+}
+
 impl<'a> FromIterator<TyError> for TyError {
     fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
         TyError::MultiError(iter.into_iter().collect())
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 53d96159..30798138 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -508,9 +508,8 @@ fn ty_check_if_else(
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Expected condition in if case, instead got {:?}",
-            cond_ty
+        return Err(TyError::IfElseError(IfElseError::InvalidConditionType(
+            (**cond_ty).clone(),
         )));
     }
     if !matches_dty!(
@@ -520,9 +519,8 @@ fn ty_check_if_else(
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Body of the true case is not of unit type, instead got {:?}",
-            case_true_ty
+        return Err(TyError::IfElseError(IfElseError::InvalidIfBlockType(
+            (**case_true_ty).clone(),
         )));
     }
     if !matches_dty!(
@@ -532,9 +530,8 @@ fn ty_check_if_else(
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Body of the false case is not of unit type, instead got {:?}",
-            case_false_ty
+        return Err(TyError::IfElseError(IfElseError::InvalidElseBlockType(
+            (**case_false_ty).clone(),
         )));
     }
 

From 5fda437ba0f463150cecf04b1fb2d38c3a4880f8 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 16:57:04 +0200
Subject: [PATCH 11/24] proper errors for if block

---
 src/ty_check/mod.rs | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 30798138..23ea115a 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -437,10 +437,6 @@ fn ty_check_while(ctx: &mut ExprTyCtx, cond: &mut Expr, body: &mut Expr) -> TyRe
             ..
         }
     ) {
-        // return Err(TyError::String(format!(
-        //     "Expected condition in while loop, instead got {:?}",
-        //     cond_ty
-        // )));
         return Err(TyError::LoopError(LoopError::InvalidConditionType(
             (**cond_ty).clone(),
         )));
@@ -452,10 +448,6 @@ fn ty_check_while(ctx: &mut ExprTyCtx, cond: &mut Expr, body: &mut Expr) -> TyRe
             ..
         }
     ) {
-        // return Err(TyError::String(format!(
-        //     "Body of while loop is not of unit type, instead got {:?}",
-        //     body_ty
-        // )));
         match &body_ty.ty {
             TyKind::Data(dty) => {
                 return Err(TyError::LoopError(LoopError::InvalidBlockType(
@@ -557,9 +549,8 @@ fn ty_check_if(ctx: &mut ExprTyCtx, cond: &mut Expr, case_true: &mut Expr) -> Ty
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Expected condition in if case, instead got {:?}",
-            cond_ty
+        return Err(TyError::IfElseError(IfElseError::InvalidConditionType(
+            (**cond_ty).clone(),
         )));
     }
     if !matches_dty!(
@@ -569,9 +560,8 @@ fn ty_check_if(ctx: &mut ExprTyCtx, cond: &mut Expr, case_true: &mut Expr) -> Ty
             ..
         }
     ) {
-        return Err(TyError::String(format!(
-            "Body of the true case is not of unit type, instead got {:?}",
-            case_true_ty
+        return Err(TyError::IfElseError(IfElseError::InvalidIfBlockType(
+            (**case_true_ty).clone(),
         )));
     }
 

From c60253fdeef5e43387c90337e86b336cc6ee3ade Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 19:07:48 +0200
Subject: [PATCH 12/24] Unary Operation Error

---
 src/ty_check/error.rs | 1 +
 src/ty_check/mod.rs   | 5 +----
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 33de2077..32e10e35 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -57,6 +57,7 @@ pub enum TyError {
     // The annotated or inferred type of the pattern does not fit the pattern.
     PatternAndTypeDoNotMatch,
     UnexpectedType,
+    UnexpectedDataType(DataTy),
     // The thread hierarchy dimension referred to does not exist
     IllegalDimension,
     UnifyError(UnifyError),
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 23ea115a..504943cd 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -998,10 +998,7 @@ fn ty_check_unary_op(ctx: &mut ExprTyCtx, un_op: &UnOp, e: &mut Expr) -> TyResul
         | DataTyKind::Scalar(ScalarTy::U8)
         | DataTyKind::Scalar(ScalarTy::U32)
         | DataTyKind::Scalar(ScalarTy::U64) => Ok(e_ty.as_ref().clone()),
-        _ => Err(TyError::String(format!(
-            "Exected a number type (i.e., f32 or i32), but found {:?}",
-            e_ty
-        ))),
+        _ => Err(TyError::UnexpectedDataType((*e_dty).clone())),
     }
 }
 

From 199451c89479f2b09b3957e97c8da55de5ad5370 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 21:30:34 +0200
Subject: [PATCH 13/24] Remove unnecessary error enums

---
 src/ty_check/error.rs |  8 ++------
 src/ty_check/mod.rs   | 23 ++++++-----------------
 2 files changed, 8 insertions(+), 23 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 32e10e35..bac2d5df 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -57,6 +57,7 @@ pub enum TyError {
     // The annotated or inferred type of the pattern does not fit the pattern.
     PatternAndTypeDoNotMatch,
     UnexpectedType,
+    UnexpectedFnTy(FnTy),
     UnexpectedDataType(DataTy),
     // The thread hierarchy dimension referred to does not exist
     IllegalDimension,
@@ -99,12 +100,7 @@ pub enum Moved {
 
 #[derive(Debug)]
 pub enum InvalidIterable {
-    // Do I need to contain the Expr so that the span is known?
-    // Should I just return the span and the DataTyKind?
-    InvalidIterable(Expr, DataTyKind),
-    // It's obvious when it's a function.
-    UnexpectedFunction(Expr),
-    NotArrayRef(Expr, RefDty),
+    NotArrayRef(RefDty),
 }
 
 #[derive(Debug)]
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 504943cd..1bd4d727 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -352,11 +352,7 @@ fn ty_check_for(
     ty_check_expr(ctx, collec)?;
     let collec_dty = match &collec.ty.as_ref().unwrap().ty {
         TyKind::Data(collec_dty) => collec_dty.as_ref(),
-        TyKind::FnTy(_) => {
-            return Err(TyError::InvalidIterable(
-                InvalidIterable::UnexpectedFunction(collec.clone()),
-            ))
-        }
+        TyKind::FnTy(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
 
     let ident_dty = match &collec_dty.dty {
@@ -377,17 +373,13 @@ fn ty_check_for(
             ))),
             _ => {
                 return Err(TyError::InvalidIterable(InvalidIterable::NotArrayRef(
-                    collec.clone(),
                     (**reff).clone(),
                 )))
             }
         },
         // DataTyKind::Range => DataTyKind::Scalar(ScalarTy::I32),
-        dty => {
-            return Err(TyError::InvalidIterable(InvalidIterable::InvalidIterable(
-                collec.clone(),
-                dty.clone(),
-            )));
+        _ => {
+            return Err(TyError::UnexpectedDataType((*collec_dty).clone()));
         }
     };
     let compare_ty_ctx = ctx.ty_ctx.clone();
@@ -810,12 +802,9 @@ fn ty_check_idx_assign(
 ) -> TyResult<Ty> {
     ty_check_expr(ctx, e)?;
     pl_expr::ty_check(&PlExprTyCtx::new(ctx, Ownership::Uniq), pl_expr)?;
-    let pl_expr_dty = if let TyKind::Data(dty) = &pl_expr.ty.as_ref().unwrap().ty {
-        dty
-    } else {
-        return Err(TyError::String(
-            "Trying to index into non array type.".to_string(),
-        ));
+    let pl_expr_dty = match &pl_expr.ty.as_ref().unwrap().ty {
+        TyKind::Data(dty) => dty,
+        TyKind::FnTy(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
     let (n, own, mem, dty) = match &pl_expr_dty.dty {
         DataTyKind::Array(elem_dty, n) => unimplemented!(), //(Ty::Data(*elem_ty), n),

From b3510c488c98b58c4d1bcef60e90ba974c91b4d2 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 22:19:14 +0200
Subject: [PATCH 14/24] Array errors and cargo fmt

---
 src/parser/mod.rs     | 11 ++++++++---
 src/ty_check/error.rs |  6 ++++++
 src/ty_check/mod.rs   | 27 +++++++++++++++------------
 3 files changed, 29 insertions(+), 15 deletions(-)

diff --git a/src/parser/mod.rs b/src/parser/mod.rs
index b2297a3c..935fef89 100644
--- a/src/parser/mod.rs
+++ b/src/parser/mod.rs
@@ -1063,7 +1063,6 @@ peg::parser! {
 mod tests {
     use super::*;
 
-
     #[test]
     fn nat_literal() {
         assert_eq!(descend::nat("0"), Ok(Nat::Lit(0)), "cannot parse 0");
@@ -2471,12 +2470,18 @@ mod tests {
     #[test]
     fn empty_annotate_snippet() {
         let source = SourceCode::new("fn\n".to_string());
-        assert!(parse(&source).is_err(), "Expected a parsing error and specifically not a panic!");
+        assert!(
+            parse(&source).is_err(),
+            "Expected a parsing error and specifically not a panic!"
+        );
     }
 
     #[test]
     fn empty_annotate_snippet2() {
         let source = SourceCode::new("fn ".to_string());
-        assert!(parse(&source).is_err(),  "Expected a parsing error and specifically not a panic!");
+        assert!(
+            parse(&source).is_err(),
+            "Expected a parsing error and specifically not a panic!"
+        );
     }
 }
diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index bac2d5df..ac1db62f 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -90,6 +90,7 @@ pub enum TyError {
     Moved(PlaceExpr, Moved),
     LoopError(LoopError),
     IfElseError(IfElseError),
+    ArrayError(ArrayError),
 }
 
 #[derive(Debug)]
@@ -151,6 +152,11 @@ pub enum IfElseError {
     InvalidElseBlockType(Ty),
 }
 
+#[derive(Debug)]
+pub enum ArrayError {
+    DifferentTypes(Ty, Ty),
+}
+
 impl<'a> FromIterator<TyError> for TyError {
     fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
         TyError::MultiError(iter.into_iter().collect())
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 1bd4d727..53358732 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -722,7 +722,7 @@ fn ty_check_assign_place(
     check_mutable(ctx.ty_ctx, &pl)?;
 
     // If the place is not dead, check that it is safe to use, otherwise it is safe to use anyway.
-    if !matches!(&place_ty.dty, DataTyKind::Dead(_),) {
+    if !matches!(&place_ty.dty, DataTyKind::Dead(_)) {
         borrow_check::borrow_check(&BorrowCheckCtx::new(ctx, vec![], Ownership::Uniq), pl_expr)
             .map_err(|err| {
                 TyError::ConflictingBorrow(Box::new(pl_expr.clone()), Ownership::Uniq, err)
@@ -1400,18 +1400,21 @@ fn ty_check_array(ctx: &mut ExprTyCtx, elems: &mut Vec<Expr>) -> TyResult<Ty> {
             "Array elements cannot be views.".to_string(),
         ));
     }
-    if elems.iter().any(|elem| ty != elem.ty.as_ref()) {
-        Err(TyError::String(
-            "Not all provided elements have the same type.".to_string(),
-        ))
-    } else {
-        Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
-            DataTyKind::Array(
-                Box::new(ty.as_ref().unwrap().dty().clone()),
-                Nat::Lit(elems.len()),
-            ),
-        )))))
+    for elem in elems.iter() {
+        if ty != elem.ty.as_ref() {
+            return Err(TyError::ArrayError(ArrayError::DifferentTypes(
+                (**ty.unwrap()).clone(),
+                *elem.ty.clone().unwrap(),
+            )));
+        }
     }
+
+    Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
+        DataTyKind::Array(
+            Box::new(ty.as_ref().unwrap().dty().clone()),
+            Nat::Lit(elems.len()),
+        ),
+    )))))
 }
 
 fn ty_check_literal(l: &mut Lit) -> Ty {

From 723502c81774420156c4695f0347abb4b5b71cf8 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 22:44:01 +0200
Subject: [PATCH 15/24] bin op errors

---
 src/ty_check/error.rs |  3 +-
 src/ty_check/mod.rs   | 87 +++++++++++++++++--------------------------
 2 files changed, 37 insertions(+), 53 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index ac1db62f..0f804217 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -4,7 +4,7 @@ use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;
 use crate::ast::{
-    BaseExec, DataTy, DataTyKind, DimCompo, ExecTy, ExecTyKind, Expr, FnTy, Ident, Memory,
+    BaseExec, BinOp, DataTy, DataTyKind, DimCompo, ExecTy, ExecTyKind, Expr, FnTy, Ident, Memory,
     NatEvalError, Ownership, PlaceExpr, RefDty, TyKind,
 };
 use crate::error;
@@ -91,6 +91,7 @@ pub enum TyError {
     LoopError(LoopError),
     IfElseError(IfElseError),
     ArrayError(ArrayError),
+    BinOpError(BinOp, Ty, Ty),
 }
 
 #[derive(Debug)]
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 53358732..c0390e01 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -905,70 +905,53 @@ fn ty_check_binary_op(
     };
     match bin_op {
         // Shift operators only allow integer values (lhs_ty and rhs_ty can differ!)
-        BinOp::Shl
-        | BinOp::Shr => match (&lhs_ty.ty, &rhs_ty.ty) {
+        BinOp::Shl | BinOp::Shr => match (&lhs_ty.ty, &rhs_ty.ty) {
             (TyKind::Data(dty1), TyKind::Data(dty2)) => match (&dty1.dty, &dty2.dty) {
                 (
                     DataTyKind::Scalar(ScalarTy::U8)
                     | DataTyKind::Scalar(ScalarTy::U32)
                     | DataTyKind::Scalar(ScalarTy::U64)
-                    | DataTyKind::Scalar(ScalarTy::I32)
-                    ,
+                    | DataTyKind::Scalar(ScalarTy::I32),
                     DataTyKind::Scalar(ScalarTy::U8)
                     | DataTyKind::Scalar(ScalarTy::U32)
                     | DataTyKind::Scalar(ScalarTy::U64)
                     | DataTyKind::Scalar(ScalarTy::I32),
                 ) => Ok(ret_dty),
-                _ => Err(TyError::String(format!(
-                    "Expected integer types for operator {}, instead got\n Lhs: {:?}\n Rhs: {:?}",
-                    bin_op, lhs, rhs
-                )))
-            }
-            _ => Err(TyError::String(format!(
-                "Expected integer types for operator {}, instead got\n Lhs: {:?}\n Rhs: {:?}",
-                bin_op, lhs, rhs
-            ))),
-        }
+                _ => Err(TyError::BinOpError(
+                    *bin_op,
+                    (**lhs_ty).clone(),
+                    (**rhs_ty).clone(),
+                )),
+            },
+            _ => Err(TyError::BinOpError(
+                *bin_op,
+                (**lhs_ty).clone(),
+                (**rhs_ty).clone(),
+            )),
+        },
         _ => match (&lhs_ty.ty, &rhs_ty.ty) {
             (TyKind::Data(dty1), TyKind::Data(dty2)) => match (&dty1.dty, &dty2.dty) {
-                (
-                    DataTyKind::Scalar(ScalarTy::F32),
-                    DataTyKind::Scalar(ScalarTy::F32),
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::U8),
-                    DataTyKind::Scalar(ScalarTy::U8),
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::U32),
-                    DataTyKind::Scalar(ScalarTy::U32),
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::U64),
-                    DataTyKind::Scalar(ScalarTy::U64),
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::F64),
-                    DataTyKind::Scalar(ScalarTy::F64)
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::I32),
-                    DataTyKind::Scalar(ScalarTy::I32),
-                ) |
-                (
-                    DataTyKind::Scalar(ScalarTy::Bool),
-                    DataTyKind::Scalar(ScalarTy::Bool),
-                ) => Ok(ret_dty),
-                _ => Err(TyError::String(format!(
-                    "Expected the same number types for operator {}, instead got\n Lhs: {:?}\n Rhs: {:?}",
-                    bin_op, dty1, dty2
-                )))
-            }
-            _ => Err(TyError::String(format!(
-                "Expected the same number types for operator {}, instead got\n Lhs: {:?}\n Rhs: {:?}",
-                bin_op, lhs, rhs
-            ))),
-        }
+                (DataTyKind::Scalar(ScalarTy::F32), DataTyKind::Scalar(ScalarTy::F32))
+                | (DataTyKind::Scalar(ScalarTy::U8), DataTyKind::Scalar(ScalarTy::U8))
+                | (DataTyKind::Scalar(ScalarTy::U32), DataTyKind::Scalar(ScalarTy::U32))
+                | (DataTyKind::Scalar(ScalarTy::U64), DataTyKind::Scalar(ScalarTy::U64))
+                | (DataTyKind::Scalar(ScalarTy::F64), DataTyKind::Scalar(ScalarTy::F64))
+                | (DataTyKind::Scalar(ScalarTy::I32), DataTyKind::Scalar(ScalarTy::I32))
+                | (DataTyKind::Scalar(ScalarTy::Bool), DataTyKind::Scalar(ScalarTy::Bool)) => {
+                    Ok(ret_dty)
+                }
+                _ => Err(TyError::BinOpError(
+                    *bin_op,
+                    (**lhs_ty).clone(),
+                    (**rhs_ty).clone(),
+                )),
+            },
+            _ => Err(TyError::BinOpError(
+                *bin_op,
+                (**lhs_ty).clone(),
+                (**rhs_ty).clone(),
+            )),
+        },
     }
 }
 

From e9233c7ca5e54bcfe457f221d94d70fa8167b2a7 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 22:49:59 +0200
Subject: [PATCH 16/24] remove unused import

---
 src/ty_check/error.rs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 0f804217..2d2e7be4 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -1,5 +1,3 @@
-use std::borrow::Borrow;
-
 use super::Ty;
 use crate::ast::internal::Place;
 use crate::ast::printer::PrintState;

From 915b2be441440a2d4b19d5d871b884f7bd0b463e Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 23:01:47 +0200
Subject: [PATCH 17/24] UnexpectedType error enum takes Ty now

---
 src/ty_check/error.rs | 2 +-
 src/ty_check/mod.rs   | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 2d2e7be4..89e7abd3 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -54,7 +54,7 @@ pub enum TyError {
     CouldNotInferProvenance,
     // The annotated or inferred type of the pattern does not fit the pattern.
     PatternAndTypeDoNotMatch,
-    UnexpectedType,
+    UnexpectedType(Ty),
     UnexpectedFnTy(FnTy),
     UnexpectedDataType(DataTy),
     // The thread hierarchy dimension referred to does not exist
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index c0390e01..ffa18fd5 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -732,7 +732,7 @@ fn ty_check_assign_place(
     let e_dty = if let TyKind::Data(dty) = &mut e.ty.as_mut().unwrap().as_mut().ty {
         dty.as_mut()
     } else {
-        return Err(TyError::UnexpectedType);
+        return Err(TyError::UnexpectedType((**e.ty.as_ref().unwrap()).clone()));
     };
     let err = unify::sub_unify(ctx.kind_ctx, ctx.ty_ctx, e_dty, &mut place_ty);
     if let Err(err) = err {
@@ -1366,7 +1366,7 @@ fn ty_check_proj(ctx: &mut ExprTyCtx, e: &mut Expr, i: usize) -> TyResult<Ty> {
     let e_dty = if let TyKind::Data(dty) = &e.ty.as_ref().unwrap().ty {
         dty.as_ref()
     } else {
-        return Err(TyError::UnexpectedType);
+        return Err(TyError::UnexpectedType((**e.ty.as_ref().unwrap()).clone()));
     };
     let elem_ty = proj_elem_dty(e_dty, i);
     Ok(Ty::new(TyKind::Data(Box::new(elem_ty?))))
@@ -1424,7 +1424,7 @@ fn infer_pattern_ident_tys(
     let pattern_dty = if let TyKind::Data(dty) = &pattern_ty.ty {
         dty.as_ref()
     } else {
-        return Err(TyError::UnexpectedType);
+        return Err(TyError::UnexpectedType((*pattern_ty).clone()));
     };
     match (pattern, &pattern_dty.dty) {
         (Pattern::Ident(mutbl, ident), _) => {
@@ -1617,7 +1617,7 @@ fn ty_check_borrow(
                 },
             ),
         },
-        TyKind::FnTy(_) => return Err(TyError::UnexpectedType),
+        TyKind::FnTy(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
     if rmem == Memory::GpuLocal {
         return Err(TyError::String(

From a1c314eeb1159d18eba071093857e5e64621b46e Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 23:05:23 +0200
Subject: [PATCH 18/24] deal with UnaryOp error

---
 src/ty_check/mod.rs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index ffa18fd5..7d21f1ae 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -958,10 +958,9 @@ fn ty_check_binary_op(
 fn ty_check_unary_op(ctx: &mut ExprTyCtx, un_op: &UnOp, e: &mut Expr) -> TyResult<Ty> {
     ty_check_expr(ctx, e)?;
     let e_ty = e.ty.as_ref().unwrap();
-    let e_dty = if let TyKind::Data(dty) = &e_ty.ty {
-        dty.as_ref()
-    } else {
-        return Err(TyError::String("expected data type, but found".to_string()));
+    let e_dty = match &e_ty.ty {
+        TyKind::Data(dty) => dty.as_ref(),
+        TyKind::FnTy(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
     match &e_dty.dty {
         DataTyKind::Scalar(ScalarTy::F32)

From 83c2535684669e52bf0a2e66d8a18b52a2e5dc9a Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Tue, 20 May 2025 23:28:59 +0200
Subject: [PATCH 19/24] add cast error

---
 src/ty_check/error.rs |  8 ++++++++
 src/ty_check/mod.rs   | 23 +++++++++--------------
 2 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 89e7abd3..282c4407 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -90,6 +90,8 @@ pub enum TyError {
     IfElseError(IfElseError),
     ArrayError(ArrayError),
     BinOpError(BinOp, Ty, Ty),
+    // Cannot cast from [0] to [1]
+    CastError(CastError),
 }
 
 #[derive(Debug)]
@@ -156,6 +158,12 @@ pub enum ArrayError {
     DifferentTypes(Ty, Ty),
 }
 
+#[derive(Debug)]
+pub enum CastError {
+    FromTo(Ty, DataTy),
+    From(Ty),
+}
+
 impl<'a> FromIterator<TyError> for TyError {
     fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
         TyError::MultiError(iter.into_iter().collect())
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 7d21f1ae..7734b6b6 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -982,34 +982,29 @@ fn ty_check_cast(ctx: &mut ExprTyCtx, e: &mut Expr, dty: &DataTy) -> TyResult<Ty
         | DataTyKind::Scalar(ScalarTy::I32)
         | DataTyKind::Scalar(ScalarTy::U8)
         | DataTyKind::Scalar(ScalarTy::U32)
-        | DataTyKind::Scalar(ScalarTy::U64)
-        => match dty.dty {
+        | DataTyKind::Scalar(ScalarTy::U64) => match dty.dty {
             DataTyKind::Scalar(ScalarTy::I32)
             | DataTyKind::Scalar(ScalarTy::U8)
             | DataTyKind::Scalar(ScalarTy::U32)
             | DataTyKind::Scalar(ScalarTy::U64)
             | DataTyKind::Scalar(ScalarTy::F32)
             | DataTyKind::Scalar(ScalarTy::F64) => Ok(Ty::new(TyKind::Data(Box::new(dty.clone())))),
-            _ => Err(TyError::String(format!(
-                "Exected a number type (i.e. i32 or f32) to cast to from {:?}, but found {:?}",
-                e_ty, dty
+            _ => Err(TyError::CastError(CastError::FromTo(
+                (**e_ty).clone(),
+                (*dty).clone(),
             ))),
         },
-        DataTyKind::Scalar(ScalarTy::Bool)
-        => match dty.dty {
+        DataTyKind::Scalar(ScalarTy::Bool) => match dty.dty {
             DataTyKind::Scalar(ScalarTy::I32)
             | DataTyKind::Scalar(ScalarTy::U8)
             | DataTyKind::Scalar(ScalarTy::U32)
             | DataTyKind::Scalar(ScalarTy::U64) => Ok(Ty::new(TyKind::Data(Box::new(dty.clone())))),
-            _ => Err(TyError::String(format!(
-                "Exected an integer type (i.e. i32 or u32) to cast to from a bool, but found {:?}",
-                dty
+            _ => Err(TyError::CastError(CastError::FromTo(
+                (**e_ty).clone(),
+                (*dty).clone(),
             ))),
         },
-        _ => Err(TyError::String(format!(
-            "Exected a number type (i.e. f32 or i32) or bool as a type to cast from, but found {:?}",
-            e_ty
-        ))),
+        _ => Err(TyError::CastError(CastError::From((**e_ty).clone()))),
     }
 }
 

From 565989d043cb7d669f6a5582c429f94721262c6b Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Wed, 28 May 2025 11:00:02 +0200
Subject: [PATCH 20/24] some array errors

---
 src/ty_check/error.rs   |  3 ++-
 src/ty_check/mod.rs     | 18 ++++++------------
 src/ty_check/pl_expr.rs |  6 ++++--
 3 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 282c4407..06a71c42 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -68,8 +68,9 @@ pub enum TyError {
     String(String),
 
     // Newly added errors
-    IndexOutOfBounds,
     // Index, Array Length
+    IndexOutOfBounds(usize, usize),
+    // Index, Tuple Length
     TupleIndexOutOfBounds(usize, usize),
     // The indexed expression is not an array
     CannotIndex,
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 7734b6b6..9535d74f 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -816,9 +816,7 @@ fn ty_check_idx_assign(
             {
                 unimplemented!() //(Ty::Data(*elem_ty), n)
             } else {
-                return Err(TyError::String(
-                    "Trying to index into non array type.".to_string(),
-                ));
+                return Err(TyError::UnexpectedDataType((**arr_dty).clone()));
             }
         }
         // FIXME is this allowed? There is no reborrow but this leaks the lifetime and does not
@@ -834,11 +832,7 @@ fn ty_check_idx_assign(
                 ))
             }
         },
-        _ => {
-            return Err(TyError::String(
-                "Trying to index into non array type.".to_string(),
-            ))
-        }
+        _ => return Err(TyError::CannotIndex),
     };
     if !dty.is_fully_alive() {
         return Err(TyError::String(
@@ -851,10 +845,10 @@ fn ty_check_idx_assign(
             "Cannot assign through shared references.".to_string(),
         ));
     }
-    if n.eval(ctx.nat_ctx)? <= idx.eval(ctx.nat_ctx)? {
-        return Err(TyError::String(
-            "Trying to access array out-of-bounds.".to_string(),
-        ));
+    let n_val = n.eval(ctx.nat_ctx)?;
+    let idx_val = idx.eval(ctx.nat_ctx)?;
+    if n_val <= idx_val {
+        return Err(TyError::IndexOutOfBounds(idx_val, n_val));
     }
     let potential_accesses = borrow_check::access_safety_check(
         &BorrowCheckCtx::new(ctx, vec![], Ownership::Uniq),
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index 07efe035..ace891d8 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -416,8 +416,10 @@ fn ty_check_index(
         }
     };
 
-    if n.eval(ctx.nat_ctx)? <= idx.eval(ctx.nat_ctx)? {
-        return Err(TyError::IndexOutOfBounds);
+    let n_val = n.eval(ctx.nat_ctx)?;
+    let idx_val = idx.eval(ctx.nat_ctx)?;
+    if n_val <= idx_val {
+        return Err(TyError::IndexOutOfBounds(idx_val, n_val));
     }
 
     Ok((Ty::new(TyKind::Data(Box::new(elem_dty))), mems, passed_prvs))

From a655c199d7fb2a221ab3c9f449634b8f3a74b3f4 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Fri, 6 Jun 2025 12:14:28 +0200
Subject: [PATCH 21/24] todo: use multierror

---
 error.rs              |  0
 src/ty_check/error.rs | 11 ++++++-----
 2 files changed, 6 insertions(+), 5 deletions(-)
 create mode 100644 error.rs

diff --git a/error.rs b/error.rs
new file mode 100644
index 00000000..e69de29b
diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 06a71c42..0c3c3678 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -165,11 +165,12 @@ pub enum CastError {
     From(Ty),
 }
 
-impl<'a> FromIterator<TyError> for TyError {
-    fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
-        TyError::MultiError(iter.into_iter().collect())
-    }
-}
+// TODO: use this
+// impl<'a> FromIterator<TyError> for TyError {
+//     fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
+//         TyError::MultiError(iter.into_iter().collect())
+//     }
+// }
 
 impl TyError {
     pub fn emit(&self, source: &SourceCode) -> ErrorReported {

From a52e314ea159b62bf84d2aded6eb1f9cfb18ab77 Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Fri, 6 Jun 2025 13:58:19 +0200
Subject: [PATCH 22/24] merge index errors for list and tuple

---
 src/ty_check/error.rs   | 4 +---
 src/ty_check/mod.rs     | 2 +-
 src/ty_check/pl_expr.rs | 2 +-
 3 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 0c3c3678..95577fff 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -68,10 +68,8 @@ pub enum TyError {
     String(String),
 
     // Newly added errors
-    // Index, Array Length
+    // Index, Array/Tuple Length
     IndexOutOfBounds(usize, usize),
-    // Index, Tuple Length
-    TupleIndexOutOfBounds(usize, usize),
     // The indexed expression is not an array
     CannotIndex,
     // The projected expression is not a tuple
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 9535d74f..a1145332 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -1850,7 +1850,7 @@ pub fn proj_elem_dty(dty: &DataTy, i: usize) -> TyResult<DataTy> {
     match &dty.dty {
         DataTyKind::Tuple(dtys) => match dtys.get(i) {
             Some(dty) => Ok(dty.clone()),
-            None => Err(TyError::TupleIndexOutOfBounds(i, dtys.len())),
+            None => Err(TyError::IndexOutOfBounds(i, dtys.len())),
         },
         _ => Err(TyError::CannotTupleIndex),
     }
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index ace891d8..7f9f7c0b 100644
--- a/src/ty_check/pl_expr.rs
+++ b/src/ty_check/pl_expr.rs
@@ -255,7 +255,7 @@ fn ty_check_proj(
                     passed_prvs,
                 ))
             } else {
-                Err(TyError::TupleIndexOutOfBounds(n, elem_dtys.len()))
+                Err(TyError::IndexOutOfBounds(n, elem_dtys.len()))
             }
         }
         dty_kind => Err(TyError::ExpectedTupleType(

From 188cfeb0b221dc8a37b2d0920cfa691552d39aff Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Fri, 6 Jun 2025 14:03:53 +0200
Subject: [PATCH 23/24] merge index errors

---
 src/ty_check/error.rs | 6 ++----
 src/ty_check/mod.rs   | 2 +-
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 95577fff..99b2a867 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -68,12 +68,10 @@ pub enum TyError {
     String(String),
 
     // Newly added errors
-    // Index, Array/Tuple Length
+    // Index, Array/Tuplegit Length
     IndexOutOfBounds(usize, usize),
-    // The indexed expression is not an array
+    // The indexed expression is not an array or a tuple
     CannotIndex,
-    // The projected expression is not a tuple
-    CannotTupleIndex,
     // The expression is not a reference
     CannotDereference(DereferenceError),
     // Struct does not have given field
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index a1145332..bb4902fc 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -1852,6 +1852,6 @@ pub fn proj_elem_dty(dty: &DataTy, i: usize) -> TyResult<DataTy> {
             Some(dty) => Ok(dty.clone()),
             None => Err(TyError::IndexOutOfBounds(i, dtys.len())),
         },
-        _ => Err(TyError::CannotTupleIndex),
+        _ => Err(TyError::CannotIndex),
     }
 }

From a7c88728c5ea09cdbb9530b0ff15706984dcba5f Mon Sep 17 00:00:00 2001
From: migraine-user <mj9012159@gmail.com>
Date: Fri, 6 Jun 2025 15:46:38 +0200
Subject: [PATCH 24/24] simplify invalid iterable error

---
 src/ty_check/error.rs | 7 +------
 src/ty_check/mod.rs   | 4 +---
 2 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/src/ty_check/error.rs b/src/ty_check/error.rs
index 99b2a867..a0fa6222 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -80,7 +80,7 @@ pub enum TyError {
     SelectError(PlaceExpr),
     ExecError(ExecError),
     SyncError(SyncError),
-    InvalidIterable(InvalidIterable),
+    InvalidIterable(RefDty),
     NotCopyable,
     Moved(PlaceExpr, Moved),
     LoopError(LoopError),
@@ -97,11 +97,6 @@ pub enum Moved {
     Entirely,
 }
 
-#[derive(Debug)]
-pub enum InvalidIterable {
-    NotArrayRef(RefDty),
-}
-
 #[derive(Debug)]
 pub enum SyncError {
     InvalidResourceType,
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index bb4902fc..c21c5059 100644
--- a/src/ty_check/mod.rs
+++ b/src/ty_check/mod.rs
@@ -372,9 +372,7 @@ fn ty_check_for(
                 elem_dty.as_ref().clone(),
             ))),
             _ => {
-                return Err(TyError::InvalidIterable(InvalidIterable::NotArrayRef(
-                    (**reff).clone(),
-                )))
+                return Err(TyError::InvalidIterable((**reff).clone()));
             }
         },
         // DataTyKind::Range => DataTyKind::Scalar(ScalarTy::I32),