diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index e7aafc384b..29212da50f 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -174,7 +174,7 @@ let rec elaborate_pattern =
         | (_, Some({typ: syn_ty, _})) => syn_ty
         | _ => Unknown(Internal) |> Typ.temp
         };
-      upat |> cast_from(t);
+      upat |> cast_from(t |> Typ.normalize(ctx));
     };
   (dpat, elaborated_type);
 };
@@ -193,6 +193,9 @@ let rec elaborate_pattern =
    the "elaborated type" at the top, so you should fresh_cast EVERYWHERE
    just in case.
 
+   Important invariant: any cast in an elaborated expression should have
+   normalized types.
+
    [Matt] A lot of these fresh_cast calls are redundant, however if you
    want to remove one, I'd ask you instead comment it out and leave
    a comment explaining why it's redundant.  */
@@ -251,7 +254,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         | (_, Some({typ: syn_ty, _})) => syn_ty
         | _ => Unknown(Internal) |> Typ.temp
         };
-      uexp |> cast_from(t);
+      uexp |> cast_from(t |> Typ.normalize(ctx));
     | Fun(p, e, env, n) =>
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re
index 80596c64f8..cfface7fc9 100644
--- a/src/haz3lcore/dynamics/Unboxing.re
+++ b/src/haz3lcore/dynamics/Unboxing.re
@@ -118,14 +118,21 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         when name1 == name2 =>
       Matches(d3)
     | (SumWithArg(_), Ap(_, {term: Constructor(_), _}, _)) => DoesNotMatch
-    | (SumWithArg(name), Cast(d1, {term: Sum(_), _}, {term: Sum(s2), _}))
-        when
-          ConstructorMap.get_entry(name, s2) != None
-          || ConstructorMap.has_bad_entry(s2) =>
-      let* d1 = unbox(SumWithArg(name), d1);
-      Matches(d1 |> fixup_cast);
-    | (SumWithArg(_), Cast(_, {term: Sum(_), _}, {term: Sum(_), _})) =>
-      IndetMatch
+    | (SumWithArg(name), Cast(d1, {term: Sum(s1), _}, {term: Sum(s2), _})) =>
+      let get_entry_or_bad = s =>
+        switch (ConstructorMap.get_entry(name, s)) {
+        | Some(x) => Some(x)
+        | None when ConstructorMap.has_bad_entry(s) =>
+          Some(Typ.temp(Unknown(Internal)))
+        | None => None
+        };
+      switch (get_entry_or_bad(s1), get_entry_or_bad(s2)) {
+      | (Some(x), Some(y)) =>
+        let* d1 = unbox(SumWithArg(name), d1);
+        Matches(Cast(d1, x, y) |> Exp.fresh |> fixup_cast);
+      | _ => IndetMatch
+      };
+    // There should be some sort of failure here when the cast doesn't go through.
 
     /* Any cast from unknown is indet */
     | (_, Cast(_, {term: Unknown(_), _}, _)) => IndetMatch