diff --git a/bin/src/main.rs b/bin/src/main.rs
index 6b7f155..f98bdf6 100644
--- a/bin/src/main.rs
+++ b/bin/src/main.rs
@@ -1,7 +1,7 @@
 use ariadne::{sources, Color, Label, Report, ReportKind};
 use chumsky::{Parser, prelude::Input};
 use syntax::parser::{lexer, exprs_parser};
-use typing::infer::infer_exprs;
+use typing::infer::{infer_exprs, InferErrorKind};
 
 pub mod args;
 
@@ -10,6 +10,7 @@ fn main() {
     let filename = args.file.clone();
     let src = std::fs::read_to_string(&args.file).expect("file not found");
 
+    // Lexing & parsing
     let (ts, errs) = lexer().parse(&src).into_output_errors();
 
     let (ast, parse_errs) = if let Some(tokens) = &ts {
@@ -23,19 +24,37 @@ fn main() {
         (None, vec![])
     };
 
-    let (_typed_ast, _type_errs) = if let Some(ast) = ast.filter(|_| errs.len() + parse_errs.len() == 0) {
+    // Typecheck if there are no lexing or parsing errors
+    if let Some(ast) = ast.filter(|_| errs.len() + parse_errs.len() == 0) {
         let (ast, e) = infer_exprs(ast.0);
         if !e.is_empty() {
-            e.iter().for_each(|e| println!("{e:?}"));
+            e.into_iter()
+                .for_each(|e| {
+                    let mut r = Report::build(ReportKind::Error, filename.clone(), e.span.start)
+                        .with_message(e.title.to_string());
+
+                    for (msg, kind, span) in e.labels {
+                        r = r.with_label(
+                            Label::new((filename.clone(), span.into_range()))
+                                .with_message(msg.to_string())
+                                .with_color(match kind {
+                                    InferErrorKind::Error => Color::Red,
+                                    InferErrorKind::Hint => Color::Blue,
+                                }),
+                        );
+                    }
+
+                    r
+                        .finish()
+                        .print(sources([(filename.clone(), src.clone())]))
+                        .unwrap()
+                });
+        } else {
+            ast.iter().for_each(|node| println!("{:?}", node.0));
         }
-        if !ast.is_empty() {
-            ast.iter().for_each(|(e, _)| println!("{e:?}"));
-        }
-        (Some(ast), e)
-    } else {
-        (None, vec![])
     };
 
+    // Report lex & parse errors
     errs.into_iter()
         .map(|e| e.map_token(|c| c.to_string()))
         .chain(
@@ -51,11 +70,6 @@ fn main() {
                         .with_message(e.reason().to_string())
                         .with_color(Color::Red),
                 )
-                // .with_labels(e.contexts().map(|(label, span)| {
-                //     Label::new((filename.clone(), span.into_range()))
-                //         .with_message(format!("while parsing this {}", label))
-                //         .with_color(Color::Yellow)
-                // }))
                 .finish()
                 .print(sources([(filename.clone(), src.clone())]))
                 .unwrap()
diff --git a/simple.hlm b/simple.hlm
new file mode 100644
index 0000000..8686804
--- /dev/null
+++ b/simple.hlm
@@ -0,0 +1,3 @@
+let mk = fn n = fn x = x + n;
+let f = mk(35);
+let res = f(34);
\ No newline at end of file
diff --git a/syntax/src/ty.rs b/syntax/src/ty.rs
index a7300df..5257615 100644
--- a/syntax/src/ty.rs
+++ b/syntax/src/ty.rs
@@ -43,9 +43,9 @@ pub fn itoa(i: usize) -> String {
     let mut i = i;
 
     while i >= 26 {
-        s.push((b'a' + (i % 26) as u8) as char);
+        s.push((b'A' + (i % 26) as u8) as char);
         i /= 26;
     }
-    s.push((b'a' + i as u8) as char);
+    s.push((b'A' + i as u8) as char);
     s
 }
\ No newline at end of file
diff --git a/test2.hlm b/test2.hlm
deleted file mode 100644
index d35dac1..0000000
--- a/test2.hlm
+++ /dev/null
@@ -1,4 +0,0 @@
-let factorial = fn x =
-    if x == 1
-        then x
-        else x * factorial(x - 1);
diff --git a/typing/src/infer.rs b/typing/src/infer.rs
index 0cdfe7c..fb08724 100644
--- a/typing/src/infer.rs
+++ b/typing/src/infer.rs
@@ -8,6 +8,8 @@ use syntax::{
     ty::*,
 };
 
+use crate::rename::{rename_exprs, rename_type};
+
 use super::typed::TExpr;
 
 macro_rules! ok {
@@ -23,12 +25,36 @@ macro_rules! unbox {
 }
 
 #[derive(Clone, Debug)]
-pub enum InferError<'src> {
-    UnboundVariable(&'src str, SimpleSpan),
-    UnboundFunction(&'src str, SimpleSpan),
-    InfiniteType(Type, Type),
-    LengthMismatch(Type, Type),
-    TypeMismatch(Type, Type),
+pub enum InferErrorKind {
+    Error,
+    Hint,
+}
+
+#[derive(Clone, Debug)]
+pub struct InferError {
+    pub title: String,
+    pub labels: Vec<(String, InferErrorKind, SimpleSpan)>,
+    pub span: SimpleSpan,
+}
+
+impl InferError {
+    pub fn new<S: Into<String>>(title: S, span: SimpleSpan) -> Self {
+        Self {
+            title: title.into(),
+            labels: Vec::new(),
+            span,
+        }
+    }
+
+    pub fn add_error<S: Into<String>>(mut self, reason: S, span: SimpleSpan) -> Self {
+        self.labels.push((reason.into(), InferErrorKind::Error, span));
+        self
+    }
+
+    pub fn add_hint<S: Into<String>>(mut self, reason: S, span: SimpleSpan) -> Self {
+        self.labels.push((reason.into(), InferErrorKind::Hint, span));
+        self
+    }
 }
 
 #[derive(Clone, Debug)]
@@ -86,7 +112,7 @@ impl<'src> Infer<'src> {
     }
 
     /// Unify two types
-    fn unify(&mut self, t1: Type, t2: Type) -> Result<(), InferError<'src>> {
+    fn unify(&mut self, t1: Type, t2: Type, s: SimpleSpan) -> Result<(), InferError> {
         use Type::*;
         match (t1, t2) {
             // Literal types
@@ -102,12 +128,15 @@ impl<'src> Infer<'src> {
                 // unify the substitution with t2
                 if let Some(t) = self.subst(i) {
                     if t != Var(i) {
-                        return self.unify(t, t2);
+                        return self.unify(t, t2, s);
                     }
                 }
                 // If the variable occurs in t2
                 if self.occurs(i, t2.clone()) {
-                    return Err(InferError::InfiniteType(Var(i), t2));
+                    return Err(InferError::new("Infinite type", s)
+                        .add_error(format!(
+                            "This type contains itself: {}", rename_type(Var(i))
+                        ), s));
                 }
                 // Set the substitution
                 self.subst[i] = t2;
@@ -116,11 +145,15 @@ impl<'src> Infer<'src> {
             (t1, Var(i)) => {
                 if let Some(t) = self.subst(i) {
                     if t != Var(i) {
-                        return self.unify(t1, t);
+                        return self.unify(t1, t, s);
                     }
                 }
                 if self.occurs(i, t1.clone()) {
-                    return Err(InferError::InfiniteType(Var(i), t1));
+                    return Err(InferError::new("Infinite type", s)
+                        .add_error(format!(
+                            "This type contains itself: {}",
+                            rename_type(Var(i))
+                        ), s));
                 }
                 self.subst[i] = t1;
                 Ok(())
@@ -130,41 +163,53 @@ impl<'src> Infer<'src> {
             (Func(a1, r1), Func(a2, r2)) => {
                 // Check the number of arguments
                 if a1.len() != a2.len() {
-                    return Err(InferError::LengthMismatch(Func(a1, r1), Func(a2, r2)));
+                    return Err(InferError::new("Argument length mismatch", s)
+                        .add_error(format!(
+                            "Expected {} arguments, found {}",
+                            a1.len(), a2.len()
+                        ), s));
                 }
                 // Unify the arguments
                 for (a1, a2) in a1.into_iter().zip(a2.into_iter()) {
-                    self.unify(a1, a2)?;
+                    self.unify(a1, a2, s)?;
                 }
                 // Unify the return types
-                self.unify(*r1, *r2)
+                self.unify(*r1, *r2, s)
             },
 
             // Tuple
             (Tuple(t1), Tuple(t2)) => {
                 // Check the number of elements
                 if t1.len() != t2.len() {
-                    return Err(InferError::LengthMismatch(Tuple(t1), Tuple(t2)));
+                    return Err(InferError::new("Tuple length mismatch", s)
+                        .add_error(format!(
+                            "Expected {} elements, found {}",
+                            t1.len(), t2.len()
+                        ), s));
                 }
                 // Unify the elements
                 for (t1, t2) in t1.into_iter().zip(t2.into_iter()) {
-                    self.unify(t1, t2)?;
+                    self.unify(t1, t2, s)?;
                 }
                 Ok(())
             },
 
             // Array
-            (Array(t1), Array(t2)) => self.unify(*t1, *t2),
+            (Array(t1), Array(t2)) => self.unify(*t1, *t2, s),
 
             // The rest will be type mismatch
-            (t1, t2) => Err(InferError::TypeMismatch(t1, t2)),
+            (t1, t2) => Err(InferError::new("Type mismatch", s)
+                .add_error(format!(
+                    "Expected {}, found {}",
+                    rename_type(t1), rename_type(t2)
+                ), s)),
         }
     }
 
     /// Solve the constraints by unifying them
-    fn solve(&mut self) -> Result<(), InferError<'src>> {
-        for (t1, t2, _span) in self.constraints.clone().into_iter() {
-            self.unify(t1, t2)?;
+    fn solve(&mut self) -> Result<(), InferError> {
+        for (t1, t2, span) in self.constraints.clone().into_iter() {
+            self.unify(t1, t2, span)?;
         }
         Ok(())
     }
@@ -283,7 +328,7 @@ impl<'src> Infer<'src> {
     /// Infer the type of an expression
     fn infer(
         &mut self, e: (Expr<'src>, SimpleSpan), expected: Type
-    ) -> (TExpr<'src>, Vec<InferError<'src>>) {
+    ) -> (TExpr<'src>, Vec<InferError>) {
         let span = e.1;
         match e.0 {
             // Literal values
@@ -315,10 +360,14 @@ impl<'src> Infer<'src> {
                     self.add_constraint(expected, t.clone(), span);
                     ok!(TExpr::Ident(x))
                 } else {
-                    (TExpr::Ident(x), vec![match expected {
-                        Type::Func(_, _) => InferError::UnboundFunction(x, span),
-                        _ => InferError::UnboundVariable(x, span),
-                    }])
+                    let kind = match &expected {
+                        Type::Func(_, _) => "function",
+                        _ => "value",
+                    };
+                    (
+                        TExpr::Ident(x),
+                        vec![InferError::new(format!("Undefined {}", kind), span)]
+                    )
                 }
             }
 
@@ -611,5 +660,5 @@ pub fn infer_exprs(es: Vec<(Expr, SimpleSpan)>) -> (Vec<(TExpr, SimpleSpan)>, Ve
         }
     }
 
-    (typed_exprs, errors)
+    (rename_exprs(typed_exprs), errors)
 }
\ No newline at end of file
diff --git a/typing/src/rename.rs b/typing/src/rename.rs
index e69de29..b77aafa 100644
--- a/typing/src/rename.rs
+++ b/typing/src/rename.rs
@@ -0,0 +1,185 @@
+use chumsky::span::SimpleSpan;
+use syntax::ty::Type;
+
+use crate::typed::TExpr;
+
+/// A renamer to rename type variables to a "minimized" form for more readable output
+pub struct Renamer {
+    // Type variables encountered so far
+    vars: Vec<usize>,
+}
+
+impl<'src> Renamer {
+    pub fn new() -> Self {
+        Self {
+            vars: vec![],
+        }
+    }
+
+    fn rename_var(&self, i: usize) -> Type {
+        let n = self.vars.iter().position(|x| x == &i).unwrap();
+        Type::Var(n)
+    }
+
+    fn add_var(&mut self, i: usize) {
+        if !self.vars.contains(&i) {
+            self.vars.push(i);
+        }
+    }
+
+    fn find_var(&mut self, t: Type) {
+        match t {
+            Type::Var(i) => {
+                self.add_var(i);
+            },
+            Type::Func(args, ret) => {
+                args.into_iter().for_each(|t| self.find_var(t));
+                self.find_var(*ret);
+            },
+            Type::Tuple(tys) => {
+                tys.into_iter().for_each(|t| self.find_var(t));
+            },
+            Type::Array(ty) => {
+                self.find_var(*ty);
+            },
+            _ => {},
+        }
+    }
+
+    fn traverse(&mut self, e: TExpr) {
+        match e {
+            TExpr::Unary { expr, ret_ty, ..} => {
+                self.traverse(*expr.0);
+                self.find_var(ret_ty);
+            },
+            TExpr::Binary { lhs, rhs, ret_ty, ..} => {
+                self.traverse(*lhs.0);
+                self.traverse(*rhs.0);
+                self.find_var(ret_ty);
+            },
+            TExpr::Lambda { params, body, ret_ty } => {
+                for (_, t) in params { self.find_var(t); }
+                self.find_var(ret_ty);
+                self.traverse(*body.0);
+            },
+            TExpr::Call { func, args } => {
+                self.traverse(*func.0);
+                for arg in args {
+                    self.traverse(arg.0);
+                }
+            },
+            TExpr::Let { ty, value, body, .. } => {
+                self.find_var(ty);
+                self.traverse(*value.0);
+                self.traverse(*body.0);
+            },
+            TExpr::Define { ty, value, .. } => {
+                self.find_var(ty);
+                self.traverse(*value.0);
+            },
+            TExpr::Block { exprs, ret_ty, .. } => {
+                for expr in exprs {
+                    self.traverse(expr.0);
+                }
+                self.find_var(ret_ty);
+            },
+            _ => {},
+        }
+    }
+
+    fn rename_type(&self, t: Type) -> Type {
+        match t {
+            Type::Var(i) => self.rename_var(i),
+            Type::Func(args, ret) => {
+                Type::Func(
+                    args.into_iter().map(|x| self.rename_type(x)).collect(),
+                    Box::new(self.rename_type(*ret)),
+                )
+            },
+            Type::Tuple(tys) => {
+                Type::Tuple(tys.into_iter().map(|x| self.rename_type(x)).collect())
+            },
+            Type::Array(ty) => {
+                Type::Array(Box::new(self.rename_type(*ty)))
+            },
+            _ => t,
+        }
+    }
+
+    fn rename_texp(&self, e: TExpr<'src>) -> TExpr<'src> {
+        match e {
+            TExpr::Unary { op, expr, ret_ty } => {
+                TExpr::Unary {
+                    op,
+                    expr: (Box::new(self.rename_texp(*expr.0)), expr.1),
+                    ret_ty: self.rename_type(ret_ty)
+                }
+            },
+            TExpr::Binary { op, lhs, rhs, ret_ty } => {
+                TExpr::Binary {
+                    op,
+                    lhs: (Box::new(self.rename_texp(*lhs.0)), lhs.1),
+                    rhs: (Box::new(self.rename_texp(*rhs.0)), rhs.1),
+                    ret_ty: self.rename_type(ret_ty)
+                }
+            },
+            TExpr::Lambda { params, body, ret_ty } => {
+                TExpr::Lambda {
+                    params: params.into_iter()
+                        .map(|(x, t)| (x, self.rename_type(t)))
+                        .collect(),
+                    body: (Box::new(self.rename_texp(*body.0)), body.1),
+                    ret_ty: self.rename_type(ret_ty)
+                }
+            },
+            TExpr::Call { func, args } => {
+                TExpr::Call {
+                    func: (Box::new(self.rename_texp(*func.0)), func.1),
+                    args: args.into_iter()
+                        .map(|x| (self.rename_texp(x.0), x.1))
+                        .collect()
+                }
+            },
+            TExpr::Let { name, ty, value, body } => {
+                TExpr::Let {
+                    name,
+                    ty: self.rename_type(ty),
+                    value: (Box::new(self.rename_texp(*value.0)), value.1),
+                    body: (Box::new(self.rename_texp(*body.0)), body.1)
+                }
+            },
+            TExpr::Define { name, ty, value } => {
+                TExpr::Define {
+                    name,
+                    ty: self.rename_type(ty),
+                    value: (Box::new(self.rename_texp(*value.0)), value.1)
+                }
+            },
+            TExpr::Block { exprs, void, ret_ty } => {
+                TExpr::Block {
+                    exprs: exprs.into_iter()
+                        .map(|x| (self.rename_texp(x.0), x.1))
+                        .collect(),
+                    void,
+                    ret_ty: self.rename_type(ret_ty)
+                }
+            },
+            _ => e,
+        }
+    }
+}
+
+pub fn rename_type(t: Type) -> Type {
+    let mut renamer = Renamer::new();
+    renamer.find_var(t.clone());
+    renamer.rename_type(t)
+}
+
+pub fn rename_exprs(es: Vec<(TExpr, SimpleSpan)>) -> Vec<(TExpr, SimpleSpan)> {
+    let mut renamer = Renamer::new();
+    es.clone().into_iter()
+        .for_each(|e| renamer.traverse(e.0));
+    es.into_iter()
+        .map(|(e, s)| (renamer.rename_texp(e), s))
+        .collect()
+}
\ No newline at end of file