diff --git a/error.rs b/error.rs
new file mode 100644
index 00000000..e69de29b
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/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 69174329..a0fa6222 100644
--- a/src/ty_check/error.rs
+++ b/src/ty_check/error.rs
@@ -1,7 +1,10 @@
 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, BinOp, DataTy, DataTyKind, DimCompo, ExecTy, ExecTyKind, Expr, FnTy, Ident, Memory,
+    NatEvalError, Ownership, PlaceExpr, RefDty, TyKind,
+};
 use crate::error;
 use crate::error::{default_format, ErrorReported};
 use crate::parser::SourceCode;
@@ -36,6 +39,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
@@ -50,7 +54,9 @@ 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
     IllegalDimension,
     UnifyError(UnifyError),
@@ -60,14 +66,103 @@ pub enum TyError {
     UnsafeRequired,
     // TODO remove as soon as possible
     String(String),
+
+    // Newly added errors
+    // Index, Array/Tuplegit Length
+    IndexOutOfBounds(usize, usize),
+    // The indexed expression is not an array or a tuple
+    CannotIndex,
+    // 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),
+    ExecError(ExecError),
+    SyncError(SyncError),
+    InvalidIterable(RefDty),
+    NotCopyable,
+    Moved(PlaceExpr, Moved),
+    LoopError(LoopError),
+    IfElseError(IfElseError),
+    ArrayError(ArrayError),
+    BinOpError(BinOp, Ty, Ty),
+    // Cannot cast from [0] to [1]
+    CastError(CastError),
 }
 
-impl<'a> FromIterator<TyError> for TyError {
-    fn from_iter<T: IntoIterator<Item = TyError>>(iter: T) -> Self {
-        TyError::MultiError(iter.into_iter().collect())
-    }
+#[derive(Debug)]
+pub enum Moved {
+    Partially,
+    Entirely,
+}
+
+#[derive(Debug)]
+pub enum SyncError {
+    InvalidResourceType,
+    SplitResource,
+    NothingToSync,
+}
+
+#[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)]
+pub enum DereferenceError {
+    // Trying to dereference a function (that is the only case).
+    InvalidTyKind(TyKind),
+    // Trying to dereference something that is not a reference
+    InvalidDataTyKind(DataTyKind),
+    // Trying to dereference a shrd reference
+    InvalidOwnership,
+    // Trying to dereference something that is not in the current resource
+    NotInExecRes(Memory, ExecTyKind),
+}
+
+#[derive(Debug)]
+pub enum LoopError {
+    InvalidBlockType(DataTy),
+    InvalidConditionType(Ty),
+    ScopeError,
+}
+
+#[derive(Debug)]
+pub enum IfElseError {
+    InvalidConditionType(Ty),
+    InvalidIfBlockType(Ty),
+    InvalidElseBlockType(Ty),
 }
 
+#[derive(Debug)]
+pub enum ArrayError {
+    DifferentTypes(Ty, Ty),
+}
+
+#[derive(Debug)]
+pub enum CastError {
+    FromTo(Ty, DataTy),
+    From(Ty),
+}
+
+// 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 {
         match &self {
@@ -181,7 +276,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 +413,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/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/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) {
diff --git a/src/ty_check/mod.rs b/src/ty_check/mod.rs
index 09511b08..c21c5059 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(
-                    "tyring 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))
     }
 }
 
@@ -308,26 +308,33 @@ 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::LoopError(LoopError::ScopeError));
             }
         } else {
-            return Err(TyError::UnexpectedType);
+            let body_type = body.ty.as_ref().unwrap().dty().clone();
+            return Err(TyError::LoopError(LoopError::InvalidBlockType(body_type)));
         }
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
@@ -335,6 +342,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 +350,9 @@ 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(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
 
     let ident_dty = match &collec_dty.dty {
@@ -368,18 +372,12 @@ 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((**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()
-            )));
+            return Err(TyError::UnexpectedDataType((*collec_dty).clone()));
         }
     };
     let compare_ty_ctx = ctx.ty_ctx.clone();
@@ -394,9 +392,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::LoopError(LoopError::ScopeError));
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
         DataTyKind::Scalar(ScalarTy::Unit),
@@ -412,17 +408,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();
@@ -435,9 +427,8 @@ 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(),
         )));
     }
     if !matches_dty!(
@@ -447,10 +438,16 @@ 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(
+                    (**dty).clone(),
+                )))
+            }
+            TyKind::FnTy(_) => {
+                unreachable!("while body is a function")
+            }
+        }
     }
     Ok(Ty::new(TyKind::Data(Box::new(DataTy::new(
         DataTyKind::Scalar(ScalarTy::Unit),
@@ -493,9 +490,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!(
@@ -505,9 +501,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!(
@@ -517,9 +512,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(),
         )));
     }
 
@@ -545,9 +539,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!(
@@ -557,9 +550,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(),
         )));
     }
 
@@ -728,7 +720,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)
@@ -738,7 +730,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 {
@@ -808,12 +800,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),
@@ -825,9 +814,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
@@ -843,11 +830,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(
@@ -860,10 +843,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),
@@ -914,80 +897,62 @@ 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(),
+            )),
+        },
     }
 }
 
 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)
@@ -996,10 +961,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())),
     }
 }
 
@@ -1012,34 +974,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()))),
     }
 }
 
@@ -1395,7 +1352,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?))))
@@ -1412,18 +1369,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 {
@@ -1450,7 +1410,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), _) => {
@@ -1567,7 +1527,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 +1536,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 +1583,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 +1603,7 @@ fn ty_check_borrow(
                 },
             ),
         },
-        TyKind::FnTy(_) => return Err(TyError::String("Trying to borrow a function.".to_string())),
+        TyKind::FnTy(fnty) => return Err(TyError::UnexpectedFnTy((**fnty).clone())),
     };
     if rmem == Memory::GpuLocal {
         return Err(TyError::String(
@@ -1686,9 +1641,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 +1848,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::IndexOutOfBounds(i, dtys.len())),
         },
-        _ => Err(TyError::String(
-            "Cannot project from non tuple type.".to_string(),
-        )),
+        _ => Err(TyError::CannotIndex),
     }
 }
diff --git a/src/ty_check/pl_expr.rs b/src/ty_check/pl_expr.rs
index 3739792e..7f9f7c0b 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,7 @@ fn ty_check_proj(
                     passed_prvs,
                 ))
             } else {
-                Err(TyError::String(
-                    "Trying to access non existing tuple element.".to_string(),
-                ))
+                Err(TyError::IndexOutOfBounds(n, elem_dtys.len()))
             }
         }
         dty_kind => Err(TyError::ExpectedTupleType(
@@ -275,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(),
             ));
@@ -291,9 +291,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(
@@ -311,15 +309,19 @@ 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,
                 ));
             }
             passed_prvs.push(reff.rgn.clone());
@@ -331,15 +333,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()),
         )),
     }
 }
@@ -376,12 +378,14 @@ 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;
         }
         _ => {
-            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))
@@ -396,9 +400,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 +408,18 @@ 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(),
-        ));
+    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))