diff --git a/nac3core/src/top_level.rs b/nac3core/src/top_level.rs
index 8560cfb3..56827cc2 100644
--- a/nac3core/src/top_level.rs
+++ b/nac3core/src/top_level.rs
@@ -15,6 +15,8 @@ pub struct DefinitionId(pub usize);
 
 pub enum TopLevelDef {
     Class {
+        // name for error messages and symbols
+        name: String,
         // object ID used for TypeEnum
         object_id: DefinitionId,
         // type variables bounded to the class.
@@ -135,11 +137,11 @@ impl TopLevelComposer {
         let primitives = Self::make_primitives();
 
         let top_level_def_list = vec![
-            Arc::new(RwLock::new(Self::make_top_level_class_def(0, None))),
-            Arc::new(RwLock::new(Self::make_top_level_class_def(1, None))),
-            Arc::new(RwLock::new(Self::make_top_level_class_def(2, None))),
-            Arc::new(RwLock::new(Self::make_top_level_class_def(3, None))),
-            Arc::new(RwLock::new(Self::make_top_level_class_def(4, None))),
+            Arc::new(RwLock::new(Self::make_top_level_class_def(0, None, "int32"))),
+            Arc::new(RwLock::new(Self::make_top_level_class_def(1, None, "int64"))),
+            Arc::new(RwLock::new(Self::make_top_level_class_def(2, None, "float"))),
+            Arc::new(RwLock::new(Self::make_top_level_class_def(3, None, "bool"))),
+            Arc::new(RwLock::new(Self::make_top_level_class_def(4, None, "none"))),
         ];
 
         let ast_list: Vec<Option<ast::Stmt<()>>> = vec![None, None, None, None, None];
@@ -171,8 +173,10 @@ impl TopLevelComposer {
     pub fn make_top_level_class_def(
         index: usize,
         resolver: Option<Arc<Mutex<dyn SymbolResolver + Send + Sync>>>,
+        name: &str,
     ) -> TopLevelDef {
         TopLevelDef::Class {
+            name: name.to_string(),
             object_id: DefinitionId(index),
             type_vars: Default::default(),
             fields: Default::default(),
@@ -216,6 +220,7 @@ impl TopLevelComposer {
                     Arc::new(RwLock::new(Self::make_top_level_class_def(
                         class_def_id,
                         resolver.clone(),
+                        name.as_str(),
                     ))),
                     None,
                 );
diff --git a/nac3core/src/typecheck/type_inferencer/mod.rs b/nac3core/src/typecheck/type_inferencer/mod.rs
index 72c47f60..0be84d75 100644
--- a/nac3core/src/typecheck/type_inferencer/mod.rs
+++ b/nac3core/src/typecheck/type_inferencer/mod.rs
@@ -77,7 +77,7 @@ impl<'a> fold::Fold<()> for Inferencer<'a> {
                 let target = Box::new(self.fold_expr(*target)?);
                 let value = if let Some(v) = value {
                     let ty = Box::new(self.fold_expr(*v)?);
-                    self.unifier.unify(target.custom.unwrap(), ty.custom.unwrap())?;
+                    self.unify(target.custom.unwrap(), ty.custom.unwrap(), &node.location)?;
                     Some(ty)
                 } else {
                     None
@@ -88,7 +88,7 @@ impl<'a> fold::Fold<()> for Inferencer<'a> {
                     &self.primitives,
                     annotation.as_ref(),
                 )?;
-                self.unifier.unify(annotation_type, target.custom.unwrap())?;
+                self.unify(annotation_type, target.custom.unwrap(), &node.location)?;
                 let annotation = Box::new(NaiveFolder().fold_expr(*annotation)?);
                 Located {
                     location: node.location,
@@ -101,21 +101,21 @@ impl<'a> fold::Fold<()> for Inferencer<'a> {
         match &stmt.node {
             ast::StmtKind::For { target, iter, .. } => {
                 let list = self.unifier.add_ty(TypeEnum::TList { ty: target.custom.unwrap() });
-                self.unifier.unify(list, iter.custom.unwrap())?;
+                self.unify(list, iter.custom.unwrap(), &iter.location)?;
             }
             ast::StmtKind::If { test, .. } | ast::StmtKind::While { test, .. } => {
-                self.unifier.unify(test.custom.unwrap(), self.primitives.bool)?;
+                self.unify(test.custom.unwrap(), self.primitives.bool, &test.location)?;
             }
             ast::StmtKind::Assign { targets, value, .. } => {
                 for target in targets.iter() {
-                    self.unifier.unify(target.custom.unwrap(), value.custom.unwrap())?;
+                    self.unify(target.custom.unwrap(), value.custom.unwrap(), &target.location)?;
                 }
             }
             ast::StmtKind::AnnAssign { .. } | ast::StmtKind::Expr { .. } => {}
             ast::StmtKind::Break | ast::StmtKind::Continue => {}
             ast::StmtKind::Return { value } => match (value, self.function_data.return_type) {
                 (Some(v), Some(v1)) => {
-                    self.unifier.unify(v.custom.unwrap(), v1)?;
+                    self.unify(v.custom.unwrap(), v1, &v.location)?;
                 }
                 (Some(_), None) => {
                     return Err("Unexpected return value".to_string());
@@ -178,8 +178,12 @@ type InferenceResult = Result<Type, String>;
 impl<'a> Inferencer<'a> {
     /// Constrain a <: b
     /// Currently implemented as unification
-    fn constrain(&mut self, a: Type, b: Type) -> Result<(), String> {
-        self.unifier.unify(a, b)
+    fn constrain(&mut self, a: Type, b: Type, location: &Location) -> Result<(), String> {
+        self.unifier.unify(a, b).map_err(|old| format!("{} at {}", old, location))
+    }
+
+    fn unify(&mut self, a: Type, b: Type, location: &Location) -> Result<(), String> {
+        self.unifier.unify(a, b).map_err(|old| format!("{} at {}", old, location))
     }
 
     fn build_method_call(
@@ -200,7 +204,7 @@ impl<'a> Inferencer<'a> {
         let call = self.unifier.add_ty(TypeEnum::TCall(vec![call].into()));
         let fields = once((method, call)).collect();
         let record = self.unifier.add_record(fields);
-        self.constrain(obj, record)?;
+        self.constrain(obj, record, &location)?;
         Ok(ret)
     }
 
@@ -249,7 +253,7 @@ impl<'a> Inferencer<'a> {
             vars: Default::default(),
         };
         let body = new_context.fold_expr(body)?;
-        new_context.unifier.unify(fun.ret, body.custom.unwrap())?;
+        new_context.unify(fun.ret, body.custom.unwrap(), &location)?;
         let mut args = new_context.fold_arguments(args)?;
         for (arg, (name, ty)) in args.args.iter_mut().zip(fn_args.iter()) {
             assert_eq!(&arg.node.arg, name);
@@ -299,10 +303,10 @@ impl<'a> Inferencer<'a> {
         // iter should be a list of targets...
         // actually it should be an iterator of targets, but we don't have iter type for now
         let list = new_context.unifier.add_ty(TypeEnum::TList { ty: target.custom.unwrap() });
-        new_context.unifier.unify(iter.custom.unwrap(), list)?;
+        new_context.unify(iter.custom.unwrap(), list, &iter.location)?;
         // if conditions should be bool
         for v in ifs.iter() {
-            new_context.unifier.unify(v.custom.unwrap(), new_context.primitives.bool)?;
+            new_context.unify(v.custom.unwrap(), new_context.primitives.bool, &v.location)?;
         }
 
         Ok(Located {
@@ -409,7 +413,7 @@ impl<'a> Inferencer<'a> {
         });
         self.calls.insert(location.into(), call);
         let call = self.unifier.add_ty(TypeEnum::TCall(vec![call].into()));
-        self.unifier.unify(func.custom.unwrap(), call)?;
+        self.unify(func.custom.unwrap(), call, &func.location)?;
 
         Ok(Located { location, custom: Some(ret), node: ExprKind::Call { func, args, keywords } })
     }
@@ -454,7 +458,7 @@ impl<'a> Inferencer<'a> {
     fn infer_list(&mut self, elts: &[ast::Expr<Option<Type>>]) -> InferenceResult {
         let (ty, _) = self.unifier.get_fresh_var();
         for t in elts.iter() {
-            self.unifier.unify(ty, t.custom.unwrap())?;
+            self.unify(ty, t.custom.unwrap(), &t.location)?;
         }
         Ok(self.unifier.add_ty(TypeEnum::TList { ty }))
     }
@@ -468,14 +472,14 @@ impl<'a> Inferencer<'a> {
         let (attr_ty, _) = self.unifier.get_fresh_var();
         let fields = once((attr.to_string(), attr_ty)).collect();
         let record = self.unifier.add_record(fields);
-        self.constrain(value.custom.unwrap(), record)?;
+        self.constrain(value.custom.unwrap(), record, &value.location)?;
         Ok(attr_ty)
     }
 
     fn infer_bool_ops(&mut self, values: &[ast::Expr<Option<Type>>]) -> InferenceResult {
         let b = self.primitives.bool;
         for v in values {
-            self.constrain(v.custom.unwrap(), b)?;
+            self.constrain(v.custom.unwrap(), b, &v.location)?;
         }
         Ok(b)
     }
@@ -543,10 +547,10 @@ impl<'a> Inferencer<'a> {
         match &slice.node {
             ast::ExprKind::Slice { lower, upper, step } => {
                 for v in [lower.as_ref(), upper.as_ref(), step.as_ref()].iter().flatten() {
-                    self.constrain(v.custom.unwrap(), self.primitives.int32)?;
+                    self.constrain(v.custom.unwrap(), self.primitives.int32, &v.location)?;
                 }
                 let list = self.unifier.add_ty(TypeEnum::TList { ty });
-                self.constrain(value.custom.unwrap(), list)?;
+                self.constrain(value.custom.unwrap(), list, &value.location)?;
                 Ok(list)
             }
             ast::ExprKind::Constant { value: ast::Constant::Int(val), .. } => {
@@ -554,14 +558,14 @@ impl<'a> Inferencer<'a> {
                 let ind: i32 = val.try_into().map_err(|_| "Index must be int32".to_string())?;
                 let map = once((ind, ty)).collect();
                 let seq = self.unifier.add_sequence(map);
-                self.constrain(value.custom.unwrap(), seq)?;
+                self.constrain(value.custom.unwrap(), seq, &value.location)?;
                 Ok(ty)
             }
             _ => {
                 // the index is not a constant, so value can only be a list
-                self.constrain(slice.custom.unwrap(), self.primitives.int32)?;
+                self.constrain(slice.custom.unwrap(), self.primitives.int32, &slice.location)?;
                 let list = self.unifier.add_ty(TypeEnum::TList { ty });
-                self.constrain(value.custom.unwrap(), list)?;
+                self.constrain(value.custom.unwrap(), list, &value.location)?;
                 Ok(ty)
             }
         }
@@ -573,10 +577,10 @@ impl<'a> Inferencer<'a> {
         body: &ast::Expr<Option<Type>>,
         orelse: &ast::Expr<Option<Type>>,
     ) -> InferenceResult {
-        self.constrain(test.custom.unwrap(), self.primitives.bool)?;
+        self.constrain(test.custom.unwrap(), self.primitives.bool, &test.location)?;
         let ty = self.unifier.get_fresh_var().0;
-        self.constrain(body.custom.unwrap(), ty)?;
-        self.constrain(orelse.custom.unwrap(), ty)?;
+        self.constrain(body.custom.unwrap(), ty, &body.location)?;
+        self.constrain(orelse.custom.unwrap(), ty, &orelse.location)?;
         Ok(ty)
     }
 }
diff --git a/nac3core/src/typecheck/type_inferencer/test.rs b/nac3core/src/typecheck/type_inferencer/test.rs
index 6952ef1e..df986b7a 100644
--- a/nac3core/src/typecheck/type_inferencer/test.rs
+++ b/nac3core/src/typecheck/type_inferencer/test.rs
@@ -145,9 +145,10 @@ impl TestEnvironment {
             params: HashMap::new().into(),
         });
         identifier_mapping.insert("None".into(), none);
-        for i in 0..5 {
+        for (i, name) in ["int32", "int64", "float", "bool", "none"].iter().enumerate() {
             top_level_defs.push(
                 RwLock::new(TopLevelDef::Class {
+                    name: format!("obj{}", i),
                     object_id: DefinitionId(i),
                     type_vars: Default::default(),
                     fields: Default::default(),
@@ -170,6 +171,7 @@ impl TestEnvironment {
         });
         top_level_defs.push(
             RwLock::new(TopLevelDef::Class {
+                name: "Foo".to_string(),
                 object_id: DefinitionId(5),
                 type_vars: vec![v0],
                 fields: [("a".into(), v0)].into(),
@@ -206,6 +208,7 @@ impl TestEnvironment {
         });
         top_level_defs.push(
             RwLock::new(TopLevelDef::Class {
+                name: "Bar".to_string(),
                 object_id: DefinitionId(6),
                 type_vars: Default::default(),
                 fields: [("a".into(), int32), ("b".into(), fun)].into(),
@@ -233,6 +236,7 @@ impl TestEnvironment {
         });
         top_level_defs.push(
             RwLock::new(TopLevelDef::Class {
+                name: "Bar2".to_string(),
                 object_id: DefinitionId(7),
                 type_vars: Default::default(),
                 fields: [("a".into(), bool), ("b".into(), fun)].into(),
diff --git a/nac3core/src/typecheck/typedef/mod.rs b/nac3core/src/typecheck/typedef/mod.rs
index 5ca9a9fd..671b32e5 100644
--- a/nac3core/src/typecheck/typedef/mod.rs
+++ b/nac3core/src/typecheck/typedef/mod.rs
@@ -8,7 +8,7 @@ use std::sync::{Arc, Mutex};
 
 use super::unification_table::{UnificationKey, UnificationTable};
 use crate::symbol_resolver::SymbolValue;
-use crate::top_level::DefinitionId;
+use crate::top_level::{DefinitionId, TopLevelContext, TopLevelDef};
 
 #[cfg(test)]
 mod test;
@@ -99,6 +99,7 @@ pub type SharedUnifier = Arc<Mutex<(UnificationTable<TypeEnum>, u32, Vec<Call>)>
 
 #[derive(Clone)]
 pub struct Unifier {
+    pub top_level: Option<Arc<TopLevelContext>>,
     unification_table: UnificationTable<Rc<TypeEnum>>,
     calls: Vec<Rc<Call>>,
     var_id: u32,
@@ -107,7 +108,12 @@ pub struct Unifier {
 impl Unifier {
     /// Get an empty unifier
     pub fn new() -> Unifier {
-        Unifier { unification_table: UnificationTable::new(), var_id: 0, calls: Vec::new() }
+        Unifier {
+            unification_table: UnificationTable::new(),
+            var_id: 0,
+            calls: Vec::new(),
+            top_level: None,
+        }
     }
 
     /// Determine if the two types are the same
@@ -121,6 +127,7 @@ impl Unifier {
             unification_table: UnificationTable::from_send(&lock.0),
             var_id: lock.1,
             calls: lock.2.iter().map(|v| Rc::new(v.clone())).collect_vec(),
+            top_level: None,
         }
     }
 
@@ -338,7 +345,7 @@ impl Unifier {
                         }
                     }
                     _ => {
-                        return Err("Incompatible".to_string());
+                        return Err("Incompatible type variables".to_string());
                     }
                 }
                 let range1 = range1.borrow();
@@ -464,7 +471,7 @@ impl Unifier {
                 TObj { obj_id: id2, params: params2, .. },
             ) => {
                 if id1 != id2 {
-                    return Err(format!("Cannot unify objects with ID {} and {}", id1.0, id2.0));
+                    self.incompatible_types(a, b)?;
                 }
                 for (x, y) in zip(params1.borrow().values(), params2.borrow().values()) {
                     self.unify(*x, *y)?;
@@ -552,7 +559,7 @@ impl Unifier {
                         return Err("Functions differ in parameter names.".to_string());
                     }
                     if x.default_value != y.default_value {
-                        return Err("Functions differ in optional parameters.".to_string());
+                        return Err("Functions differ in optional parameters value".to_string());
                     }
                     self.unify(x.ty, y.ty)?;
                 }
@@ -561,7 +568,7 @@ impl Unifier {
             }
             _ => {
                 if swapped {
-                    return self.incompatible_types(&*ty_a, &*ty_b);
+                    return self.incompatible_types(a, b);
                 } else {
                     self.unify_impl(b, a, true)?;
                 }
@@ -570,6 +577,28 @@ impl Unifier {
         Ok(())
     }
 
+    fn internal_stringify(&mut self, ty: Type) -> String {
+        let top_level = self.top_level.clone();
+        self.stringify(
+            ty,
+            &mut |id| {
+                top_level.as_ref().map_or_else(
+                    || format!("{}", id),
+                    |top_level| {
+                        if let TopLevelDef::Class { name, .. } =
+                            &*top_level.definitions.read()[id].read()
+                        {
+                            name.clone()
+                        } else {
+                            unreachable!("expected class definition")
+                        }
+                    },
+                )
+            },
+            &mut |id| format!("var{}", id),
+        )
+    }
+
     /// Get string representation of the type
     pub fn stringify<F, G>(&mut self, ty: Type, obj_to_name: &mut F, var_to_name: &mut G) -> String
     where
@@ -642,8 +671,8 @@ impl Unifier {
         table.set_value(a, ty_b)
     }
 
-    fn incompatible_types(&self, a: &TypeEnum, b: &TypeEnum) -> Result<(), String> {
-        Err(format!("Cannot unify {} with {}", a.get_type_name(), b.get_type_name()))
+    fn incompatible_types(&mut self, a: Type, b: Type) -> Result<(), String> {
+        Err(format!("Cannot unify {} with {}", self.internal_stringify(a), self.internal_stringify(b)))
     }
 
     /// Instantiate a function if it hasn't been instantiated.
@@ -949,9 +978,9 @@ impl Unifier {
             }
         }
         return Err(format!(
-            "Cannot unify type variable {} with {} due to incompatible value range",
+            "Cannot unify variable {} with {} due to incompatible value range",
             id,
-            self.get_ty(b).get_type_name()
+            self.internal_stringify(b)
         ));
     }
 }
diff --git a/nac3standalone/mandelbrot.py b/nac3standalone/mandelbrot.py
index 6c8de275..ac222f25 100644
--- a/nac3standalone/mandelbrot.py
+++ b/nac3standalone/mandelbrot.py
@@ -5,6 +5,8 @@ def run() -> int32:
     height = 36.0
     aspectRatio = 2.0
 
+    test = 1.0 + 1
+
     yScale = (maxX-minX)*(height/width)*aspectRatio
 
     y = 0.0
diff --git a/nac3standalone/src/main.rs b/nac3standalone/src/main.rs
index 464d4cf1..4bbc1eb1 100644
--- a/nac3standalone/src/main.rs
+++ b/nac3standalone/src/main.rs
@@ -53,7 +53,8 @@ fn main() {
     let (_, composer) = TopLevelComposer::new();
     let mut unifier = composer.unifier.clone();
     let primitives = composer.primitives.clone();
-    let top_level = composer.to_top_level_context();
+    let top_level = Arc::new(composer.to_top_level_context());
+    unifier.top_level = Some(top_level.clone());
     let fun = unifier.add_ty(TypeEnum::TFunc(RefCell::new(FunSignature {
         args: vec![FuncArg {
             name: "c".into(),