diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
index 0ffdb0d56..bce404441 100644
--- a/backend/cn/bin/main.ml
+++ b/backend/cn/bin/main.ml
@@ -58,7 +58,7 @@ let frontend ~macros ~incl_dirs ~incl_files astprints ~filename ~magic_comment_c
     ~ignore_bitfields:false;
   Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl;
   Switches.set
-    ([ "inner_arg_temps"; "at_magic_comments" ]
+    ([ "inner_arg_temps"; "at_magic_comments"; "elaboration_normalises_types" ]
      (* TODO (DCM, VIP) figure out how to support liveness checks for read-only
         resources and then switch on "strict_pointer_arith" to elaborate array
         shift to the effectful version. "strict_pointer_relationals" is also
diff --git a/frontend/model/global.lem b/frontend/model/global.lem
index f4143976c..c029d7ef4 100644
--- a/frontend/model/global.lem
+++ b/frontend/model/global.lem
@@ -51,6 +51,7 @@ type cerb_switch =
   | SW_permissive_printf
   | SW_no_integer_provenance
   | SW_CHERI
+  | SW_elaboration_normalises_types
 
 declare ocaml target_rep function SW_strict_reads = `Switches.SW_strict_reads`
 declare ocaml target_rep function SW_forbid_nullptr_free = `Switches.SW_forbid_nullptr_free`
@@ -59,6 +60,7 @@ declare ocaml target_rep function SW_inner_arg_temps = `Switches.SW_inner_arg_te
 declare ocaml target_rep function SW_permissive_printf = `Switches.SW_permissive_printf`
 declare ocaml target_rep function SW_no_integer_provenance = `Switches.SW_no_integer_provenance`
 declare ocaml target_rep function SW_CHERI = `Switches.SW_CHERI`
+declare ocaml target_rep function SW_elaboration_normalises_types = `Switches.SW_elaboration_normalises_types`
 
 
 val is_CHERI: unit -> bool
diff --git a/frontend/model/translation.lem b/frontend/model/translation.lem
index 05c1b1e6b..52935879f 100644
--- a/frontend/model/translation.lem
+++ b/frontend/model/translation.lem
@@ -1410,6 +1410,12 @@ let rec translate_expression is_used ctx variadic_env stdlib tagDefs a_expr =
           (* STD §6.3.1.8#1, bullet 4 *)
           match (AilTypesAux.promotion (Implementation.integerImpl ()) ty1, AilTypesAux.promotion (Implementation.integerImpl ()) ty2) with
             | (Just (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity1')) as ty1'), Just (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity2')) as ty2')) ->
+                let (ity1', ity2') =
+                  if Global.has_switch Global.SW_elaboration_normalises_types then
+                    ( Implementation.normalise_integerType ity1'
+                    , Implementation.normalise_integerType ity2' )
+                  else
+                    (ity1', ity2') in
                 (* "If both operants have the same type, then no further conversion is needed." *)
                 if ty1' = ty2' then
                   (mk_conv_int ity1' e1, mk_conv_int ity2' e2)
diff --git a/frontend/model/translation_aux.lem b/frontend/model/translation_aux.lem
index c1d7cf3b0..0ed88b245 100644
--- a/frontend/model/translation_aux.lem
+++ b/frontend/model/translation_aux.lem
@@ -207,8 +207,16 @@ let ctype_of a_expr =
   match ErrorMonad.runErrorMonad
       (GenTypesAux.interpret_genTypeCategory (Loc.locOf a_expr) (Implementation.integerImpl ())
         (GenTypes.genTypeCategoryOf a_expr)) with
-    | Right (GenTypes.LValueType _ ty _) -> ty
-    | Right (GenTypes.RValueType   ty) -> ty
+    | Right (GenTypes.LValueType _ ty _) ->
+        if Global.has_switch Global.SW_elaboration_normalises_types then
+          Implementation.normalise_ctype ty
+        else
+          ty
+    | Right (GenTypes.RValueType   ty) ->
+        if Global.has_switch Global.SW_elaboration_normalises_types then
+          Implementation.normalise_ctype ty
+        else
+          ty
     | Left (loc, TypingError.TError_MiscError (TypingError.UntypableIntegerConstant n)) ->
         error $ Loc.stringFromLocation loc ^ ": untypable integer constant '" ^ show n ^ "'\n"
     | _ -> error "[Translation_aux.ctype_of] impossible case: TODO move to Exception.t"
diff --git a/ocaml_frontend/switches.ml b/ocaml_frontend/switches.ml
index 4f1576952..7d12ad09b 100644
--- a/ocaml_frontend/switches.ml
+++ b/ocaml_frontend/switches.ml
@@ -40,6 +40,9 @@ type cerb_switch =
   (* set magic comment syntax to "/*$ ... $*/" *)
   | SW_magic_comment_char_dollar
 
+  (* type aliases (e.g. size_t) are normalised during the elaboration to Core.
+     As a result the generated Core has fixed their implementation. *)
+  | SW_elaboration_normalises_types
 
 let internal_ref =
   ref []
@@ -94,6 +97,8 @@ let set strs =
         Some SW_at_magic_comments
     | "magic_comment_char_dollar" ->
         Some (SW_magic_comment_char_dollar)
+    | "elaboration_normalises_types" ->
+        Some SW_elaboration_normalises_types
     | _ ->
         None in
   let pred x = function
@@ -122,7 +127,8 @@ let set strs =
     | SW_permissive_printf
     | SW_zero_initialised
     | SW_at_magic_comments
-    | SW_magic_comment_char_dollar as y ->
+    | SW_magic_comment_char_dollar
+    | SW_elaboration_normalises_types as y ->
         x = y in
   List.iter (fun str ->
     match read_switch str with
diff --git a/ocaml_frontend/switches.mli b/ocaml_frontend/switches.mli
index faa5ae9aa..21795c11d 100644
--- a/ocaml_frontend/switches.mli
+++ b/ocaml_frontend/switches.mli
@@ -40,6 +40,10 @@ type cerb_switch =
   (* set magic comment syntax to "/*$ ... $*/" *)
   | SW_magic_comment_char_dollar
 
+  (* type aliases (e.g. size_t) are normalised during the elaboration to Core.
+     As a result the generated Core has fixed their implementation. *)
+  | SW_elaboration_normalises_types
+
 val get_switches: unit -> cerb_switch list
 val has_switch: cerb_switch -> bool
 val has_switch_pred: (cerb_switch -> bool) -> cerb_switch option