diff --git a/bin/main.ml b/bin/main.ml
index 69d847f..9b51f55 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -68,6 +68,7 @@ Supported options:|}
     ];
   ));
   Krml.(Warn.parse_warn_error !Options.warn_error);
+  Krml.(Warn.parse_warn_error "-6");
 
   Krml.Helpers.is_readonly_builtin_lid_ :=
     (let is_readonly_pure_lid_ = !Krml.Helpers.is_readonly_builtin_lid_ in
@@ -120,6 +121,7 @@ Supported options:|}
   Printf.printf "3️⃣ Monomorphization, datatypes\n";
   let files = if runtime_cg then Eurydice.RuntimeCg.disable_cg_monomorphization#visit_files () files else files in
   let files = Krml.Monomorphization.functions files in
+  Eurydice.Logging.log "Phase2.4" "%a" pfiles files;
   let files = Krml.Monomorphization.datatypes files in
   Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
   let files =
@@ -144,23 +146,30 @@ Supported options:|}
   let files = Krml.DataTypes.optimize files in
   let _, files = Krml.DataTypes.everything files in
   let files = Eurydice.Cleanup2.remove_trivial_ite#visit_files () files in
+  Eurydice.Logging.log "Phase2.65" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in
   let files = Krml.Structs.pass_by_ref files in
   let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
   let files = Krml.Simplify.optimize_lets files in
   (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
+  Eurydice.Logging.log "Phase2.7" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files (0, 0) files in
+  Eurydice.Logging.log "Phase2.71" "%a" pfiles files;
   let files = Krml.Simplify.sequence_to_let#visit_files () files in
+  Eurydice.Logging.log "Phase2.72" "%a" pfiles files;
   let files = Krml.Simplify.hoist#visit_files [] files in
   let files = Krml.Simplify.fixup_hoist#visit_files () files in
+  Eurydice.Logging.log "Phase2.75" "%a" pfiles files;
   let files = Krml.Simplify.misc_cosmetic#visit_files () files in
   let files = Krml.Simplify.let_to_sequence#visit_files () files in
   let files = Krml.Inlining.cross_call_analysis files in
+  Eurydice.Logging.log "Phase2.8" "%a" pfiles files;
   let files = Krml.Simplify.remove_unused files in
   let files = Eurydice.Cleanup2.remove_array_from_fn#visit_files () files in
   (* Macros stemming from globals *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
-  let files = if runtime_cg then Eurydice.RuntimeCg.erase_and_decay_cgs#visit_files (0, 0) files else files in
+  Eurydice.Logging.log "Phase2.9" "%a" pfiles files;
+  let files = if runtime_cg then Eurydice.RuntimeCg.decay_cgs#visit_files (0, 0) files else files in
 
 
   Eurydice.Logging.log "Phase3" "%a" pfiles files;
@@ -168,6 +177,8 @@ Supported options:|}
   if errors then
     exit 1;
 
+  let files = if runtime_cg then Eurydice.RuntimeCg.erase_cgs#visit_files (0, 0) files else files in
+
   let scope_env = Krml.Simplify.allocate_c_env files in
   let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
   let macros =
diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml
index b3f0717..90f04b2 100644
--- a/lib/Cleanup2.ml
+++ b/lib/Cleanup2.ml
@@ -31,6 +31,11 @@ let expr_of_array_length (n_cgs, i) = function
   | TCgArray (_, n) -> with_type (TInt SizeT) (expr_of_cg n_cgs i n)
   | _ -> failwith "impossible"
 
+let decay x =
+  match x.typ with
+  | TArray (t, _) | TCgArray (t, _) -> { x with typ = TBuf (t, false) }
+  | _ -> x
+
 let remove_implicit_array_copies = object(self)
 
   inherit Krml.DeBruijn.map_counting_cg as super
@@ -53,10 +58,16 @@ let remove_implicit_array_copies = object(self)
         in
         (nest 0 es).node
     | _ ->
+        (* We need to decay the types because the cg-runtime compilation scheme
+           sometimes is too smart for its own good, and ends up finding the only
+           suitable monomorphization, which combined with single-field data type
+           elimination, tells us *statically* that we have an array for this
+           subexpression, which is stronger than what the type-checker
+           concludes... *)
         let zero = Krml.(Helpers.zero Constant.SizeT) in
         (* let _ = *)
         ELet (H.sequence_binding (),
-          H.with_unit (EBufBlit (rhs, zero, lhs, zero, n)),
+          H.with_unit (EBufBlit (decay rhs, zero, decay lhs, zero, n)),
           lift 1 (self#visit_expr_w env e2))
 
   method! visit_ELet env b e1 e2 =
@@ -72,6 +83,7 @@ let remove_implicit_array_copies = object(self)
           let env = self#extend (fst env) b in
           (* let _ = blit e1 (a.k.a. src) b (a.k.a. dst) in *)
           ELet (H.sequence_binding (),
+            (* TODO: possibly need decay here *)
             H.with_unit (EBufBlit (lift 1 e1, zero, with_type b.typ (EBound 0), zero, n)),
             (* -- crossing second binder, not #extending since this is going to be lifted by one *)
             (* e2 *)
@@ -230,8 +242,18 @@ let remove_trivial_into = object(self)
     let e = self#visit_expr_w () e in
     let es = List.map (self#visit_expr env) es in
     match e.node, es with
-    | ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], [ t1; t2 ]), [ e1 ] when t1 = t2 ->
-        e1.node
+    | ETApp ({ node = EQualified (["core"; "convert"; _ ], "into"); _ }, [], [ t1; t2 ]), [ e1 ] ->
+        begin match t1, t2 with
+        | _ when t1 = t2 ->
+            e1.node
+        | TCgArray (t1', _), TArray (t2', _) when t1' = t2' ->
+            (* Resolution of runtime cg found only a single choice that,
+               in combination with single-element data type elimination, now
+               gives us knowledge that there's only possible choice... *)
+            ECast (e1, t2)
+        | _ ->
+            EApp (e, es)
+        end
     | _ ->
         EApp (e, es)
 end
diff --git a/lib/RuntimeCg.ml b/lib/RuntimeCg.ml
index 47ff0ee..9f648c8 100644
--- a/lib/RuntimeCg.ml
+++ b/lib/RuntimeCg.ml
@@ -2,6 +2,7 @@
 
 
 open Krml.Ast
+open Krml.PrintAst.Ops
 
 module H = Krml.Helpers
 
@@ -72,9 +73,9 @@ let enumerate_cg_monomorphizations files =
     let known = Hashtbl.mem Krml.MonomorphizationState.state (t, ts, cgs) in
     let builtin = match List.hd (fst t) with "Eurydice" | "core" -> true | _ -> false in
     if known then
-      Krml.(let open PrintAst.Ops in KPrint.bprintf "KNOWN: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
+      Krml.(KPrint.bprintf "KNOWN: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
     else if not builtin then begin
-      Krml.(let open PrintAst.Ops in KPrint.bprintf "RUNTIME_MONOMORPHIZATION: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
+      Krml.(KPrint.bprintf "RUNTIME_MONOMORPHIZATION: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
       if Hashtbl.mem known_concrete_arguments t then begin
         let existing = Hashtbl.find known_concrete_arguments t in
         if not (List.mem (ts, cgs) existing) then
@@ -98,11 +99,11 @@ let enumerate_cg_monomorphizations files =
       match decl with
       | DFunction (_, _, n_cgs, n, _, _, _, _) ->
           if n_cgs = 0 && n = 0 then
-            let _ = Krml.(KPrint.bprintf "Visiting %a\n" PrintAst.Ops.plid (lid_of_decl decl)) in
+            let _ = Krml.(KPrint.bprintf "Visiting %a\n" plid (lid_of_decl decl)) in
             super#visit_decl env decl
       | DGlobal (_, _, n, _, _) ->
           if n = 0 then
-            let _ = Krml.(KPrint.bprintf "Visiting %a\n" PrintAst.Ops.plid (lid_of_decl decl)) in
+            let _ = Krml.(KPrint.bprintf "Visiting %a\n" plid (lid_of_decl decl)) in
             super#visit_decl env decl
       | _ ->
           ()
@@ -124,7 +125,7 @@ let enumerate_cg_monomorphizations files =
                 let cgs, _ = Krml.KList.split n_cgs es in
                 if not (Hashtbl.mem seen (lid, (cgs, ts))) then begin
                   Krml.KPrint.bprintf "Visiting (recursive): %a\n"
-                    Krml.PrintAst.Ops.pexpr (with_type TUnit (ETApp (e, cgs, ts)));
+                    pexpr (with_type TUnit (ETApp (e, cgs, ts)));
                   assert (n_cgs = List.length cgs && n = List.length ts);
                   Hashtbl.add seen (lid, (cgs, ts)) ();
                   let body = Krml.DeBruijn.(subst_cen (List.length binders - n_cgs) cgs (subst_ten ts body)) in
@@ -174,7 +175,6 @@ let debug missing =
   Krml.KPrint.bprintf "DEBUG RUNTIME MONOMORPHIZATION:\n";
   Hashtbl.iter (fun lid args ->
     let open Krml in
-    let open PrintAst.Ops in
     KPrint.bprintf "%a:\n" plid lid;
     List.iter (fun (ts, cgs) ->
       KPrint.bprintf "  %a ++ %a\n" ptyps ts pcgs cgs
@@ -211,7 +211,7 @@ let replace =
       | TCgArray (t1, cg1), TCgArray (t2, cg2) ->
           matches_t t1 t2 && cg1 = cg2
       | TArray (t1, _), TCgArray (t2, _) ->
-          (* TODO: compute mappings and check they coincide *)
+          (* TODO: compute mgus and check they coincide *)
           matches_t t1 t2
       | TCgApp (t1, cg1), TCgApp (t2, cg2) ->
           matches_t t1 t2 && matches_cg cg1 cg2
@@ -222,7 +222,7 @@ let replace =
       | t1, t2 ->
           t1 = t2
     in
-    Krml.(let open PrintAst.Ops in KPrint.bprintf "  MATCH: %a | %a ? %b\n" ptyp t1 ptyp t2 r);
+    Krml.(KPrint.bprintf "  MATCH: %a | %a ? %b\n" ptyp t1 ptyp t2 r);
     r
 
   and matches_cg cg1 cg2 =
@@ -235,7 +235,7 @@ let replace =
   let replace t ts cgs =
     let builtin = match List.hd (fst t) with "Eurydice" | "core" -> true | _ -> false in
     if not builtin then begin
-      Krml.(let open PrintAst.Ops in KPrint.bprintf "REPLACE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
+      Krml.(KPrint.bprintf "REPLACE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
       (* let candidates = Hashtbl.find missing t in *)
       (* Pull ALL the candidates from monomorphization *)
       let candidates = Hashtbl.fold (fun (lid, ts, cgs) (_, mono_lid) acc ->
@@ -248,12 +248,12 @@ let replace =
       match candidates with
       | [] -> fold_tapp (t, ts, cgs)
       | [ ts', cgs', lid ] ->
-          Krml.(let open PrintAst.Ops in KPrint.bprintf "  FOUND: %a: %a ++ %a\n" plid t ptyps ts' pcgs cgs');
-          Krml.(let open PrintAst.Ops in KPrint.bprintf "  AKA: %a\n" plid lid);
+          Krml.(KPrint.bprintf "  FOUND: %a: %a ++ %a\n" plid t ptyps ts' pcgs cgs');
+          Krml.(KPrint.bprintf "  AKA: %a\n" plid lid);
           TQualified lid
       | _ ->
           List.iter (fun (ts, cgs, _) ->
-            Krml.(let open PrintAst.Ops in KPrint.bprintf "  CANDIDATE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
+            Krml.(KPrint.bprintf "  CANDIDATE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
           ) candidates;
           failwith "TODO: multiple candidates, need to be subtler"
     end else
@@ -279,15 +279,28 @@ let replace =
    arguments of TCgArray's to runtime expressions, in order to implement blit
    operations to materialize array copies. We now remove those, and manually
    decay TCgArrays into TBufs, relying on Checker to validate this pass. *)
-let erase_and_decay_cgs = object(self)
+let decay_cgs = object(self)
   inherit Krml.DeBruijn.map_counting_cg as super
 
   method! visit_ELet env b e1 e2 =
     match b.typ, e1.node with
-    | TCgArray (t, _), EAny ->
-        let n = Cleanup2.expr_of_array_length (fst env) b.typ in
-        let typ = TBuf (t, false) in
-        ELet ({ b with typ }, with_type typ (EBufCreate (Stack, H.any, n)),
+    | TCgArray _, EAny ->
+        let rec convert t0 =
+          match t0 with
+          | TCgArray (t, _) ->
+              (* Krml.KPrint.bprintf "n_cgs=%d, n=%d, i_cg=%d\n" (fst (fst env)) (snd (fst env)) i_cg; *)
+              let n = Cleanup2.expr_of_array_length (fst env) t0 in
+              let t, init = convert t in
+              let typ = TBuf (t, false) in
+              typ, with_type typ (EBufCreate (Stack, init, n))
+          | TArray (_, _) ->
+              let n = Cleanup2.expr_of_array_length (fst env) t0 in
+              t0, with_type t0 (EBufCreate (Stack, H.any, n))
+          | _ ->
+              t0, H.any
+        in
+        let typ, init = convert b.typ in
+        ELet ({ b with typ }, init,
           self#visit_expr_w (self#extend (fst env) { b with typ }) e2)
     | _ ->
         super#visit_ELet env b e1 e2
@@ -296,6 +309,21 @@ let erase_and_decay_cgs = object(self)
     super#visit_TBuf env t false
 
   method! visit_DFunction _ cc flags n_cgs n t name bs e =
+    (* Setting up environment properly *)
+    super#visit_DFunction (n_cgs, 0) cc flags n_cgs n t name bs e
+end
+
+
+(* This happens much later. The previous phases left n_cgs in place over
+   DFunctions so that remove_implicit_array_copies could convert length
+   arguments of TCgArray's to runtime expressions, in order to implement blit
+   operations to materialize array copies. We now remove those, and manually
+   decay TCgArrays into TBufs, relying on Checker to validate this pass. *)
+let erase_cgs = object(_self)
+  inherit Krml.DeBruijn.map_counting_cg as super
+
+  method! visit_DFunction _ cc flags n_cgs n t name bs e =
+    (* Discarding n_cgs *)
     super#visit_DFunction (n_cgs, 0) cc flags 0 n t name bs e
 
 end