diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
index 8822e4b6c25..a9e5512d774 100644
--- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp
+++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
@@ -424,7 +424,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
     require_goto_statements::require_declaration_of_name(
       symbol_identifier, entry_point_instructions);
   const typet &component_type =
-    to_pointer_type(component_declaration.symbol().type()).subtype();
+    to_pointer_type(component_declaration.symbol().type()).base_type();
   REQUIRE(component_type.id() == ID_struct_tag);
   const auto &component_struct =
     ns.follow_tag(to_struct_tag_type(component_type));
@@ -480,7 +480,7 @@ require_goto_statements::require_struct_array_component_assignment(
   REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
   REQUIRE(
     to_struct_tag_type(
-      to_pointer_type(component_assignment_rhs.type()).subtype())
+      to_pointer_type(component_assignment_rhs.type()).base_type())
       .get(ID_identifier) == array_type_name);
 
   // Get the tmp_object name and find assignments to it, there should be only
@@ -501,7 +501,8 @@ require_goto_statements::require_struct_array_component_assignment(
   PRECONDITION(
     array_component_reference_assignment_rhs.type().id() == ID_pointer);
   const typet &array =
-    to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
+    to_pointer_type(array_component_reference_assignment_rhs.type())
+      .base_type();
   PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
   REQUIRE(array.get(ID_identifier) == array_type_name);
 
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 89aaa8036d7..c7648675765 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -23,7 +23,7 @@ pointer_typet require_type::require_pointer(
   const pointer_typet &pointer = to_pointer_type(type);
 
   if(subtype)
-    REQUIRE(pointer.subtype() == subtype.value());
+    REQUIRE(pointer.base_type() == subtype.value());
 
   return pointer;
 }
@@ -155,8 +155,8 @@ bool require_java_generic_type_argument_expectation(
   {
     REQUIRE(!is_java_generic_parameter(type_argument));
     REQUIRE(
-      to_struct_tag_type(type_argument.subtype()).get_identifier() ==
-      expected.description);
+      to_struct_tag_type(to_pointer_type(type_argument).base_type())
+        .get_identifier() == expected.description);
     return true;
   }
   }
@@ -248,7 +248,7 @@ const typet &require_type::require_java_non_generic_type(
   REQUIRE(!is_java_generic_parameter(type));
   REQUIRE(!is_java_generic_type(type));
   if(expect_subtype)
-    REQUIRE(type.subtype() == expect_subtype.value());
+    REQUIRE(to_pointer_type(type).base_type() == expect_subtype.value());
   return type;
 }
 
@@ -474,7 +474,7 @@ pointer_typet
 require_type::require_pointer_to_tag(const typet &type, const irep_idt &tag)
 {
   const auto pointer_type = require_type::require_pointer(type, {});
-  require_type::require_struct_tag(pointer_type.subtype(), tag);
+  require_type::require_struct_tag(pointer_type.base_type(), tag);
   return pointer_type;
 }
 
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 40b4aa3c4ed..b53e65e988f 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -687,7 +687,8 @@ bool cpp_typecheckt::standard_conversion_sequence(
 
   // bit fields are converted like their underlying type
   if(type.id()==ID_c_bit_field)
-    return standard_conversion_sequence(expr, type.subtype(), new_expr, rank);
+    return standard_conversion_sequence(
+      expr, to_c_bit_field_type(type).underlying_type(), new_expr, rank);
 
   // we turn bit fields into their underlying type
   if(curr_expr.type().id()==ID_c_bit_field)
@@ -774,7 +775,9 @@ bool cpp_typecheckt::standard_conversion_sequence(
     }
     else if(type.id()==ID_pointer)
     {
-      if(expr.type().subtype().id()==ID_nullptr)
+      if(
+        expr.type().id() == ID_pointer &&
+        to_pointer_type(expr.type()).base_type().id() == ID_nullptr)
       {
         // std::nullptr_t to _any_ pointer type is ok
         new_expr = typecast_exprt::conditional_cast(new_expr, type);
@@ -1132,9 +1135,9 @@ bool cpp_typecheckt::reference_related(
     return subtype_typecast(to_struct_type(from),
                             to_struct_type(to));
 
-  if(from.id()==ID_struct &&
-     type.get_bool(ID_C_this) &&
-     type.subtype().id()==ID_empty)
+  if(
+    from.id() == ID_struct && type.get_bool(ID_C_this) &&
+    to_pointer_type(type).base_type().id() == ID_empty)
   {
     // virtual-call case
     return true;
@@ -1158,14 +1161,14 @@ bool cpp_typecheckt::reference_compatible(
   if(!reference_related(expr, type))
     return false;
 
-  if(expr.type()!=type.subtype())
+  if(expr.type() != to_reference_type(type).base_type())
     rank+=3;
 
   c_qualifierst qual_from;
     qual_from.read(expr.type());
 
   c_qualifierst qual_to;
-    qual_to.read(type.subtype());
+  qual_to.read(to_reference_type(type).base_type());
 
   if(qual_from!=qual_to)
     rank+=1;
@@ -1264,7 +1267,7 @@ bool cpp_typecheckt::reference_binding(
         new_expr.swap(tmp);
       }
 
-      if(expr.type()!=type.subtype())
+      if(expr.type() != to_reference_type(type).base_type())
       {
         c_qualifierst qual_from;
         qual_from.read(expr.type());
@@ -1341,7 +1344,7 @@ bool cpp_typecheckt::reference_binding(
 
           new_expr = to_multi_ary_expr(returned_value).op0();
 
-          if(returned_value.type() != type.subtype())
+          if(returned_value.type() != to_reference_type(type).base_type())
           {
             c_qualifierst qual_from;
             qual_from.read(returned_value.type());
@@ -1359,13 +1362,15 @@ bool cpp_typecheckt::reference_binding(
   if(type.get_bool(ID_C_this))
     return false;
 
-  if(!type.subtype().get_bool(ID_C_constant) ||
-     type.subtype().get_bool(ID_C_volatile))
+  if(
+    !to_reference_type(type).base_type().get_bool(ID_C_constant) ||
+    to_reference_type(type).base_type().get_bool(ID_C_volatile))
     return false;
 
   // TODO: handle the case for implicit parameters
-  if(!type.subtype().get_bool(ID_C_constant) &&
-     !expr.get_bool(ID_C_lvalue))
+  if(
+    !to_reference_type(type).base_type().get_bool(ID_C_constant) &&
+    !expr.get_bool(ID_C_lvalue))
     return false;
 
   exprt arg_expr=expr;
@@ -1376,7 +1381,8 @@ bool cpp_typecheckt::reference_binding(
     arg_expr.set(ID_C_lvalue, true);
   }
 
-  if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
+  if(user_defined_conversion_sequence(
+       arg_expr, to_reference_type(type).base_type(), new_expr, rank))
   {
     address_of_exprt tmp(new_expr, reference_type(new_expr.type()));
     tmp.add_source_location()=new_expr.source_location();
@@ -1385,12 +1391,15 @@ bool cpp_typecheckt::reference_binding(
   }
 
   rank=backup_rank;
-  if(standard_conversion_sequence(expr, type.subtype(), new_expr, rank))
+  if(standard_conversion_sequence(
+       expr, to_reference_type(type).base_type(), new_expr, rank))
   {
     {
       // create temporary object
       side_effect_exprt tmp(
-        ID_temporary_object, type.subtype(), expr.source_location());
+        ID_temporary_object,
+        to_reference_type(type).base_type(),
+        expr.source_location());
       tmp.set(ID_mode, ID_cpp);
       // tmp.set(ID_C_lvalue, true);
       tmp.add_to_operands(std::move(new_expr));
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 10d112a0508..a43e24c7c7d 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -324,12 +324,13 @@ void cpp_typecheckt::typecheck_expr_sizeof(exprt &expr)
     {
       // sizeof(expr[index]) can be parsed as an array type!
 
-      if(type.subtype().id()==ID_cpp_name)
+      if(to_array_type(type).element_type().id() == ID_cpp_name)
       {
         cpp_typecheck_fargst fargs;
 
-        exprt symbol_expr=resolve(
-          to_cpp_name(static_cast<const irept &>(type.subtype())),
+        exprt symbol_expr = resolve(
+          to_cpp_name(
+            static_cast<const irept &>(to_array_type(type).element_type())),
           cpp_typecheck_resolvet::wantt::BOTH,
           fargs);
 
@@ -1652,7 +1653,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
       // look for the right entry
       irep_idt vtentry_component_name =
-        vt_compo.type().subtype().get_string(ID_identifier) +
+        to_pointer_type(vt_compo.type()).base_type().get_string(ID_identifier) +
         "::" + expr.function().type().get_string(ID_C_virtual_name);
 
       exprt vtentry_member(ID_ptrmember);
@@ -1719,14 +1720,14 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
     assert(parameters.size()>=1);
 
-    const typet &this_type=parameters[0].type();
+    const auto &this_type = to_pointer_type(parameters[0].type());
 
     // change type from 'constructor' to object type
-    expr.type()=this_type.subtype();
+    expr.type() = this_type.base_type();
 
     // create temporary object
     side_effect_exprt tmp_object_expr(
-      ID_temporary_object, this_type.subtype(), expr.source_location());
+      ID_temporary_object, this_type.base_type(), expr.source_location());
     tmp_object_expr.set(ID_C_lvalue, true);
     tmp_object_expr.set(ID_mode, ID_cpp);
 
@@ -1808,7 +1809,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
       if(
         operand.type().id() != ID_pointer &&
-        operand.type() == parameter.type().subtype())
+        operand.type() == to_pointer_type(parameter.type()).base_type())
       {
         address_of_exprt tmp(operand, pointer_type(operand.type()));
         tmp.add_source_location()=operand.source_location();
@@ -1869,7 +1870,7 @@ void cpp_typecheckt::typecheck_function_call_arguments(
         exprt temporary;
         new_temporary(
           arg_it->source_location(),
-          parameter.type().subtype(),
+          to_reference_type(parameter.type()).base_type(),
           already_typechecked_exprt{*arg_it},
           temporary);
         arg_it->swap(temporary);
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index de26dd0dc78..12a32023232 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -269,10 +269,14 @@ exprt cpp_typecheck_resolvet::convert_identifier(
       {
         // use this->...
         assert(this_expr.type().id()==ID_pointer);
-        object=exprt(ID_dereference, this_expr.type().subtype());
+        object =
+          exprt(ID_dereference, to_pointer_type(this_expr.type()).base_type());
         object.copy_to_operands(this_expr);
-        object.type().set(ID_C_constant,
-                          this_expr.type().subtype().get_bool(ID_C_constant));
+        object.type().set(
+          ID_C_constant,
+          to_pointer_type(this_expr.type())
+            .base_type()
+            .get_bool(ID_C_constant));
         object.set(ID_C_lvalue, true);
         object.add_source_location()=source_location;
       }
@@ -1838,19 +1842,24 @@ void cpp_typecheck_resolvet::guess_template_args(
   else if(is_reference(template_type) ||
           is_rvalue_reference(template_type))
   {
-    guess_template_args(template_type.subtype(), desired_type);
+    guess_template_args(
+      to_reference_type(template_type).base_type(), desired_type);
   }
   else if(template_type.id()==ID_pointer)
   {
     if(desired_type.id() == ID_pointer)
-      guess_template_args(template_type.subtype(), desired_type.subtype());
+      guess_template_args(
+        to_pointer_type(template_type).base_type(),
+        to_pointer_type(desired_type).base_type());
   }
   else if(template_type.id()==ID_array)
   {
     if(desired_type.id() == ID_array)
     {
       // look at subtype first
-      guess_template_args(template_type.subtype(), desired_type.subtype());
+      guess_template_args(
+        to_array_type(template_type).element_type(),
+        to_array_type(desired_type).element_type());
 
       // size (e.g., buffer size guessing)
       guess_template_args(
@@ -2134,7 +2143,8 @@ bool cpp_typecheck_resolvet::disambiguate_functions(
       if(type.return_type().id() == ID_constructor)
       {
         // it's a constructor
-        const typet &object_type=parameter.type().subtype();
+        const typet &object_type =
+          to_pointer_type(parameter.type()).base_type();
         symbol_exprt object(irep_idt(), object_type);
         object.set(ID_C_lvalue, true);
 
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 4900ca5c336..1f5acc0c285 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -46,7 +46,8 @@ bool string_abstractiont::build_wrap(
   if(
     dest.type() != a_t &&
     !(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
-      dest.type().subtype() == a_t.subtype()))
+      to_array_type(dest.type()).element_type() ==
+        to_pointer_type(a_t).base_type()))
   {
     messaget log{message_handler};
     log.warning() << "warning: inconsistent abstract type for "
@@ -59,7 +60,8 @@ bool string_abstractiont::build_wrap(
 
 bool string_abstractiont::is_ptr_string_struct(const typet &type) const
 {
-  return type.id() == ID_pointer && type.subtype() == string_struct;
+  return type.id() == ID_pointer &&
+         to_pointer_type(type).base_type() == string_struct;
 }
 
 static inline bool is_ptr_argument(const typet &type)
@@ -334,10 +336,16 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
 {
   if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer)
   {
-    const typet &source_subt =
-      is_ptr_string_struct(symbol.type) ? source_type : source_type.subtype();
+    const typet &source_subt = is_ptr_string_struct(symbol.type)
+                                 ? source_type
+                                 : to_type_with_subtype(source_type).subtype();
     symbol_exprt sym_expr = add_dummy_symbol_and_value(
-      dest, ref_instr, symbol, irep_idt(), symbol.type.subtype(), source_subt);
+      dest,
+      ref_instr,
+      symbol,
+      irep_idt(),
+      to_type_with_subtype(symbol.type).subtype(),
+      source_subt);
 
     if(symbol.type.id() == ID_array)
       return array_of_exprt(sym_expr, to_array_type(symbol.type));
@@ -429,7 +437,8 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
 
   // set the value - may be nil
   if(
-    source_type.id() == ID_array && is_char_type(source_type.subtype()) &&
+    source_type.id() == ID_array &&
+    is_char_type(to_array_type(source_type).element_type()) &&
     type == string_struct)
   {
     new_symbol.value = struct_exprt(
@@ -561,7 +570,8 @@ void string_abstractiont::abstract_function_call(
         abstract_type.id()==ID_pointer)
     {
       INVARIANT(
-        str_args.back().type().subtype() == abstract_type.subtype(),
+        to_array_type(str_args.back().type()).element_type() ==
+          to_pointer_type(abstract_type).base_type(),
         "argument array type differs from formal parameter pointer type");
 
       index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
@@ -706,11 +716,14 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
   if(type.id() == ID_array || type.id() == ID_pointer)
   {
     // char* or void* or char[]
-    if(is_char_type(type.subtype()) || type.subtype().id() == ID_empty)
+    if(
+      is_char_type(to_type_with_subtype(type).subtype()) ||
+      to_type_with_subtype(type).subtype().id() == ID_empty)
       map_entry.first->second=pointer_type(string_struct);
     else
     {
-      const typet &subt = build_abstraction_type_rec(type.subtype(), known);
+      const typet &subt =
+        build_abstraction_type_rec(to_type_with_subtype(type).subtype(), known);
       if(!subt.is_nil())
       {
         if(type.id() == ID_array)
@@ -787,7 +800,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
 
     return dest.type() != abstract_type ||
            (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
-            dest.type().subtype() == abstract_type.subtype());
+            to_array_type(dest.type()).element_type() ==
+              to_pointer_type(abstract_type).base_type());
   }
 
   if(object.id()==ID_string_constant)
@@ -801,7 +815,9 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
     return build_symbol_constant(str_len, str_len+1, dest);
   }
 
-  if(object.id()==ID_array && is_char_type(object.type().subtype()))
+  if(
+    object.id() == ID_array &&
+    is_char_type(to_array_type(object.type()).element_type()))
     return build_array(to_array_expr(object), dest, write);
 
   // other constants aren't useful
@@ -928,8 +944,9 @@ bool string_abstractiont::build_pointer(const exprt &object,
     dest=address_of_exprt(dest);
     return false;
   }
-  else if(ptr.pointer.id()==ID_symbol &&
-      is_char_type(object.type().subtype()))
+  else if(
+    ptr.pointer.id() == ID_symbol &&
+    is_char_type(to_pointer_type(object.type()).base_type()))
     // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
     // checks
     return build_wrap(ptr.pointer, dest, write);
diff --git a/src/util/type.h b/src/util/type.h
index 9610c33f141..8c870fb3fc8 100644
--- a/src/util/type.h
+++ b/src/util/type.h
@@ -45,6 +45,8 @@ class typet:public irept
   }
 #endif
 
+  // Deliberately protected -- use type-specific accessor methods instead.
+protected:
   const typet &subtype() const
   {
     if(get_sub().empty())
@@ -52,6 +54,8 @@ class typet:public irept
     return static_cast<const typet &>(get_sub().front());
   }
 
+public:
+  // This method will be protected eventually.
   typet &subtype()
   {
     subt &sub=get_sub();