diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 7c5b64133b5..319f1852739 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1173,7 +1173,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
       const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, ns, nil_exprt()),
+        dynamic_object_lower_bound(address, nil_exprt()),
         dynamic_object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
@@ -1189,8 +1189,8 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
       flags.is_static_lifetime())
     {
       const or_exprt object_bounds_violation(
-        object_lower_bound(address, ns, nil_exprt()),
-        object_upper_bound(address, ns, size));
+        object_lower_bound(address, nil_exprt()),
+        object_upper_bound(address, size));
 
       conditions.push_back(conditiont(
         or_exprt(
diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp
index 2da68a84dac..6c00c9ae808 100644
--- a/src/util/allocate_objects.cpp
+++ b/src/util/allocate_objects.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "fresh_symbol.h"
 #include "pointer_offset_size.h"
 #include "string_constant.h"
+#include "type_eq.h"
 
 /// Allocates a new object, either by creating a local variable with automatic
 /// lifetime, a global variable with static lifetime, or by dynamically
@@ -183,7 +184,7 @@ exprt allocate_objectst::allocate_dynamic_object(
   output_code.add(assign);
 
   exprt malloc_symbol_expr =
-    ns.follow(malloc_sym.symbol_expr().type()) != ns.follow(target_expr.type())
+    !type_eq(malloc_sym.symbol_expr().type(), target_expr.type(), ns)
       ? (exprt)typecast_exprt(malloc_sym.symbol_expr(), target_expr.type())
       : malloc_sym.symbol_expr();
 
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index cb981543d0a..994dc3c9ec4 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -263,7 +263,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result = expr_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
-    if(ns.follow(type).id()!=ID_array)
+    if(type.id() != ID_array)
       result.type()=type;
 
     return result;
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index e30d6f36f69..72d0a6d899f 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -104,10 +104,9 @@ exprt is_not_zero(
   // Note that this returns a proper bool_typet(), not a C/C++ boolean.
   // To get a C/C++ boolean, add a further typecast.
 
-  const typet &src_type=
-    src.type().id()==ID_c_enum_tag?
-    ns.follow_tag(to_c_enum_tag_type(src.type())):
-    ns.follow(src.type());
+  const typet &src_type = src.type().id() == ID_c_enum_tag
+                            ? ns.follow_tag(to_c_enum_tag_type(src.type()))
+                            : src.type();
 
   if(src_type.id()==ID_bool) // already there
     return src; // do nothing
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 93fb6f45c34..89d1e4ddf3a 100644
--- a/src/util/pointer_predicates.cpp
+++ b/src/util/pointer_predicates.cpp
@@ -84,16 +84,15 @@ exprt good_pointer_def(
   const exprt &pointer,
   const namespacet &ns)
 {
-  const pointer_typet &pointer_type=to_pointer_type(ns.follow(pointer.type()));
+  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
   const typet &dereference_type=pointer_type.subtype();
 
   const or_exprt good_dynamic_tmp1(
     not_exprt(malloc_object(pointer, ns)),
     and_exprt(
-      not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())),
-      not_exprt(
-        dynamic_object_upper_bound(
-          pointer, ns, size_of_expr(dereference_type, ns)))));
+      not_exprt(dynamic_object_lower_bound(pointer, nil_exprt())),
+      not_exprt(dynamic_object_upper_bound(
+        pointer, ns, size_of_expr(dereference_type, ns)))));
 
   const and_exprt good_dynamic_tmp2(
     not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
@@ -106,9 +105,8 @@ exprt good_pointer_def(
   const not_exprt not_invalid(invalid_pointer(pointer));
 
   const or_exprt bad_other(
-    object_lower_bound(pointer, ns, nil_exprt()),
-    object_upper_bound(
-      pointer, ns, size_of_expr(dereference_type, ns)));
+    object_lower_bound(pointer, nil_exprt()),
+    object_upper_bound(pointer, size_of_expr(dereference_type, ns)));
 
   const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
 
@@ -145,10 +143,9 @@ exprt invalid_pointer(const exprt &pointer)
 
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
-  return object_lower_bound(pointer, ns, offset);
+  return object_lower_bound(pointer, offset);
 }
 
 exprt dynamic_object_upper_bound(
@@ -171,22 +168,17 @@ exprt dynamic_object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(malloc_size.type()))
-    sum.make_typecast(malloc_size.type());
-
-  return binary_relation_exprt(sum, op, malloc_size);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
 }
 
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &access_size)
 {
   // this is
@@ -204,23 +196,19 @@ exprt object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-
-  if(ns.follow(sum.type())!=
-     ns.follow(object_size_expr.type()))
-    sum.make_typecast(object_size_expr.type());
-
-  return binary_relation_exprt(sum, op, object_size_expr);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, object_size_expr.type()),
+    op,
+    object_size_expr);
 }
 
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
   exprt p_offset=pointer_offset(pointer);
@@ -230,11 +218,8 @@ exprt object_lower_bound(
 
   if(offset.is_not_nil())
   {
-    if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
-      p_offset=
-        plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
-    else
-      p_offset=plus_exprt(p_offset, offset);
+    p_offset = plus_exprt(
+      p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
   }
 
   return binary_relation_exprt(p_offset, ID_lt, zero);
diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h
index f83588df8fe..a0c88d1192e 100644
--- a/src/util/pointer_predicates.h
+++ b/src/util/pointer_predicates.h
@@ -33,7 +33,6 @@ exprt integer_address(const exprt &pointer);
 exprt invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
@@ -41,11 +40,9 @@ exprt dynamic_object_upper_bound(
   const exprt &access_size);
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &access_size);
 
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 6c33946460a..8dc39db06da 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -67,7 +67,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -107,7 +107,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -163,8 +163,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  const typet &expr_type=ns.follow(expr.type());
-  const typet &op_type=ns.follow(expr.op0().type());
+  const typet &expr_type = expr.type();
+  const typet &op_type = expr.op0().type();
 
   // eliminate casts of infinity
   if(expr.op0().id()==ID_infinity)
@@ -778,11 +778,12 @@ bool simplify_exprt::simplify_dereference(exprt &expr)
     if(address_of.object().id()==ID_index)
     {
       const index_exprt &old=to_index_expr(address_of.object());
-      if(ns.follow(old.array().type()).id()==ID_array)
+      if(old.array().type().id() == ID_array)
       {
-        index_exprt idx(old.array(),
-                        plus_exprt(old.index(), pointer.op1()),
-                        ns.follow(old.array().type()).subtype());
+        index_exprt idx(
+          old.array(),
+          plus_exprt(old.index(), pointer.op1()),
+          old.array().type().subtype());
         simplify_rec(idx);
         expr.swap(idx);
         return false;
@@ -1347,7 +1348,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
     {
       // kill integers from sum
       Forall_operands(it, expr)
-        if(ns.follow(it->type()).id()==ID_pointer)
+        if(it->type().id() == ID_pointer)
         {
           exprt tmp=*it;
           expr.swap(tmp);
@@ -1359,7 +1360,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
   else if(expr.id()==ID_typecast)
   {
     auto const &typecast_expr = to_typecast_expr(expr);
-    const typet &op_type = ns.follow(typecast_expr.op().type());
+    const typet &op_type = typecast_expr.op().type();
 
     if(op_type.id()==ID_pointer)
     {
@@ -1563,7 +1564,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
   bool little_endian)
 {
   // extract bits from lowest to highest memory address
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   if(expr.id()==ID_constant)
   {
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index fbdfa283595..2ffda22887b 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -21,7 +21,7 @@ bool simplify_exprt::simplify_isinf(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
+  if(expr.op0().type().id() != ID_floatbv)
     return true;
 
   if(expr.op0().is_constant())
@@ -72,7 +72,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -114,7 +114,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -144,8 +144,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
 
   auto const &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
 
-  const typet &dest_type = ns.follow(floatbv_typecast_expr.type());
-  const typet &src_type = ns.follow(floatbv_typecast_expr.op().type());
+  const typet &dest_type = floatbv_typecast_expr.type();
+  const typet &src_type = floatbv_typecast_expr.op().type();
 
   // eliminate redundant casts
   if(dest_type==src_type)
@@ -171,8 +171,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
        casted_expr.op1().id()==ID_typecast &&
        casted_expr.op0().operands().size()==1 &&
        casted_expr.op1().operands().size()==1 &&
-       ns.follow(casted_expr.op0().type())==dest_type &&
-       ns.follow(casted_expr.op1().type())==dest_type)
+       casted_expr.op0().type()==dest_type &&
+       casted_expr.op1().type()==dest_type)
     {
       exprt result(casted_expr.id(), floatbv_typecast_expr.type());
       result.operands().resize(3);
@@ -282,7 +282,7 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
 
 bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 {
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   PRECONDITION(type.id() == ID_floatbv);
   PRECONDITION(
@@ -298,10 +298,10 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
   exprt op2=expr.op2(); // rounding mode
 
   INVARIANT(
-    ns.follow(op0.type()) == type,
+    op0.type() == type,
     "expression type of operand must match type of expression");
   INVARIANT(
-    ns.follow(op1.type()) == type,
+    op1.type() == type,
     "expression type of operand must match type of expression");
 
   // Remember that floating-point addition is _NOT_ associative.
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index b92549780e1..9b968201391 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -447,7 +447,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
   // floating-point addition is _NOT_ associative; thus,
   // there is special case for float
 
-  if(ns.follow(plus_expr.type()).id() == ID_floatbv)
+  if(plus_expr.type().id() == ID_floatbv)
   {
     // we only merge neighboring constants!
     Forall_expr(it, operands)
@@ -660,9 +660,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
     forall_operands(it, expr)
     {
-      if(it->id()==ID_typecast &&
-         it->operands().size()==1 &&
-         ns.follow(it->op0().type()).id()==ID_bool)
+      if(
+        it->id() == ID_typecast && it->operands().size() == 1 &&
+        it->op0().type().id() == ID_bool)
       {
       }
       else if(it->is_zero() || it->is_one())
@@ -1355,9 +1355,6 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
      (expr.id()==ID_equal || expr.id()==ID_notequal))
     return simplify_inequality_pointer_object(expr);
 
-  tmp0.type() = ns.follow(tmp0.type());
-  tmp1.type() = ns.follow(tmp1.type());
-
   if(tmp0.type().id()==ID_c_enum_tag)
     tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
 
@@ -1547,7 +1544,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
   // pretty much all of the simplifications below are unsound
   // for IEEE float because of NaN!
 
-  if(ns.follow(expr.op0().type()).id()==ID_floatbv)
+  if(expr.op0().type().id() == ID_floatbv)
     return true;
 
   // eliminate strict inequalities
@@ -1800,18 +1797,18 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
   // (double)value REL const ---> value rel const
   // if 'const' can be represented exactly.
 
-  if(expr.op0().id()==ID_typecast &&
-     expr.op0().operands().size()==1 &&
-     ns.follow(expr.op0().type()).id()==ID_floatbv &&
-     ns.follow(expr.op0().op0().type()).id()==ID_floatbv)
+  if(
+    expr.op0().id() == ID_typecast && expr.op0().operands().size() == 1 &&
+    expr.op0().type().id() == ID_floatbv &&
+    expr.op0().op0().type().id() == ID_floatbv)
   {
     ieee_floatt const_val(to_constant_expr(expr.op1()));
     ieee_floatt const_val_converted=const_val;
     const_val_converted.change_spec(
-      ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().op0().type()))));
+      ieee_float_spect(to_floatbv_type(expr.op0().op0().type())));
     ieee_floatt const_val_converted_back=const_val_converted;
     const_val_converted_back.change_spec(
-      ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().type()))));
+      ieee_float_spect(to_floatbv_type(expr.op0().type())));
     if(const_val_converted_back==const_val)
     {
       exprt result=expr;
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 671c555dc01..af27c2a89bd 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -177,7 +177,7 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  if(ns.follow(expr.type()).id()!=ID_pointer)
+  if(expr.type().id() != ID_pointer)
     return true;
 
   exprt &object=expr.op0();
@@ -249,7 +249,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     if(ptr.operands().size()!=1)
       return true;
 
-    const typet &op_type=ns.follow(ptr.op0().type());
+    const typet &op_type = ptr.op0().type();
 
     if(op_type.id()==ID_pointer)
     {
@@ -281,7 +281,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
         // We do a bit of special treatment for (TYPE *)(a+(int)&o),
         // which is re-written to 'a'.
 
-        typet type=ns.follow(expr.type());
+        typet type = expr.type();
         exprt tmp=ptr.op0();
         if(tmp.id()==ID_plus && tmp.operands().size()==2)
         {
@@ -289,9 +289,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
              tmp.op0().operands().size()==1 &&
              tmp.op0().op0().id()==ID_address_of)
           {
-            expr=tmp.op1();
-            if(type!=expr.type())
-              expr.make_typecast(type);
+            expr = typecast_exprt::conditional_cast(tmp.op1(), type);
 
             simplify_node(expr);
             return false;
@@ -300,9 +298,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
                   tmp.op1().operands().size()==1 &&
                   tmp.op1().op0().id()==ID_address_of)
           {
-            expr=tmp.op0();
-            if(type!=expr.type())
-              expr.make_typecast(type);
+            expr = typecast_exprt::conditional_cast(tmp.op0(), type);
 
             simplify_node(expr);
             return false;
@@ -664,9 +660,7 @@ bool simplify_exprt::simplify_object_size(exprt &expr)
     if(op.op0().id()==ID_symbol)
     {
       // just get the type
-      const typet &type=ns.follow(op.op0().type());
-
-      exprt size=size_of_expr(type, ns);
+      exprt size = size_of_expr(op.op0().type(), ns);
 
       if(size.is_not_nil())
       {
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 1e162ce03cc..4c94ec00fc0 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -200,7 +200,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
   else if(op.id()==ID_union && op_type.id()==ID_union)
   {
     // trivial?
-    if(ns.follow(to_union_expr(op).op().type())==ns.follow(expr.type()))
+    if(type_eq(to_union_expr(op).op().type(), expr.type(), ns))
     {
       exprt tmp=to_union_expr(op).op();
       expr.swap(tmp);