diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 7f7f3c84ed..2a8a2cce91 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -76,14 +76,16 @@ let elaborated_type =
   (elab_ty |> Typ.normalize(ctx), ctx, co_ctx, term);
 };
 
-let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
-  let (mode, self_ty, ctx, prev_synswitch) =
+let elaborated_pat_type =
+    (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t, Pat.t) => {
+  let (mode, self_ty, ctx, prev_synswitch, term) =
     switch (Id.Map.find_opt(UPat.rep_id(upat), m)) {
-    | Some(Info.InfoPat({mode, ty, ctx, prev_synswitch, _})) => (
+    | Some(Info.InfoPat({mode, ty, ctx, prev_synswitch, term, _})) => (
         mode,
         ty,
         ctx,
         prev_synswitch,
+        term,
       )
     | _ => raise(MissingTypeInfo)
     };
@@ -103,13 +105,14 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
       | Some(syn_ty) => Typ.match_synswitch(syn_ty, ana_ty)
       }
     };
-  (elab_ty |> Typ.normalize(ctx), ctx);
+  (elab_ty |> Typ.normalize(ctx), ctx, term);
 };
 
 let rec elaborate_pattern =
         (m: Statics.Map.t, upat: UPat.t, in_container: bool)
         : (DHPat.t, Typ.t) => {
-  let (elaborated_type, ctx) = elaborated_pat_type(m, upat);
+  // Pulling upat back out of the statics map for statics level elaboration
+  let (elaborated_type, ctx, upat) = elaborated_pat_type(m, upat);
   let elaborate_pattern = (~in_container=false, m, upat) =>
     elaborate_pattern(m, upat, in_container);
   let cast_from = (ty, exp) => fresh_pat_cast(exp, ty, elaborated_type);
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index e2f39597d2..c049ea353a 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -878,6 +878,7 @@ and upat_to_info_map =
       ~co_ctx,
       ~ancestors: Info.ancestors,
       ~mode: Mode.t=Mode.Syn,
+      ~under_ascription: bool=false,
       {ids, term, _} as upat: UPat.t,
       m: Map.t,
     )
@@ -911,6 +912,7 @@ and upat_to_info_map =
         ~co_ctx,
         ~ancestors,
         ~mode,
+        ~under_ascription=false,
         upat: UPat.t,
         m: Map.t,
       ) => {
@@ -920,13 +922,15 @@ and upat_to_info_map =
       ~co_ctx,
       ~ancestors,
       ~mode,
+      ~under_ascription,
       upat,
       m: Map.t,
     );
   };
   let atomic = (self, constraint_) => add(~self, ~ctx, ~constraint_, m);
   let ancestors = [UPat.rep_id(upat)] @ ancestors;
-  let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx);
+  let go = (~under_ascription=false) =>
+    upat_to_info_map(~under_ascription, ~is_synswitch, ~ancestors, ~co_ctx);
   let unknown = Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp;
   let ctx_fold = (ctx: Ctx.t, m) =>
     List.fold_left2(
@@ -1100,29 +1104,37 @@ and upat_to_info_map =
       );
     | Cast(p, ann, _) =>
       let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m);
-      let (p, m) = go(~ctx, ~mode=Ana(ann.term), p, m);
+      let (p, m) =
+        go(~ctx, ~under_ascription=true, ~mode=Ana(ann.term), p, m);
       add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
     };
   // This is to allow lifting single values into a singleton labeled tuple when the label is not present
 
-  print_endline("upat_to_info_map: " ++ UPat.show(upat));
-  print_endline("mode: " ++ Mode.show(mode));
-  switch (mode) {
-  | Ana(ty) =>
-    switch (Typ.weak_head_normalize(ctx, ty).term) {
-    | Prod([{term: TupLabel({term: Label(l1), _}, ana_ty), _}]) =>
-      // We can flatten this by pulling it up on the case match but since OCaml is strict it'll be evaluated.
-      // So for performance reasons we'll just do it here.
-      let (e, m) = go(~mode=Mode.Syn, ~ctx, upat, m);
+  // print_endline("upat_to_info_map: " ++ UPat.show(upat));
+  // print_endline("mode: " ++ Mode.show(mode));
+  print_endline("updat.term" ++ UPat.show(upat));
+  print_endline("under ascription: " ++ string_of_bool(under_ascription));
+  if (under_ascription) {
+    default_case();
+  } else {
+    switch (mode) {
+    | Ana(ty) =>
+      switch (Typ.weak_head_normalize(ctx, ty).term) {
+      | Prod([{term: TupLabel({term: Label(l1), _}, ana_ty), _}]) =>
+        // We can flatten this by pulling it up on the case match but since OCaml is strict it'll be evaluated.
+        // So for performance reasons we'll just do it here.
+        let (e, m) = go(~mode=Mode.Syn, ~ctx, upat, m);
 
-      switch (Typ.weak_head_normalize(ctx, e.ty).term) {
-      | Prod([{term: TupLabel({term: Label(l2), _}, _), _}]) when l1 == l2 =>
-        default_case()
-      | _ => elaborate_singleton_tuple(upat, ana_ty, l1, m)
-      };
+        switch (Typ.weak_head_normalize(ctx, e.ty).term) {
+        | Prod([{term: TupLabel({term: Label(l2), _}, _), _}])
+            when l1 == l2 =>
+          default_case()
+        | _ => elaborate_singleton_tuple(upat, ana_ty, l1, m)
+        };
+      | _ => default_case()
+      }
     | _ => default_case()
-    }
-  | _ => default_case()
+    };
   };
 }
 and utyp_to_info_map =