diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index 61d7483930..6150787d74 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -33,6 +33,7 @@ module rec DHExp: {
     | Prj(t, int)
     | Constructor(string)
     | ConsistentCase(case)
+    | InexhaustiveCase(MetaVar.t, HoleInstanceId.t, case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
@@ -87,6 +88,7 @@ module rec DHExp: {
     | Prj(t, int)
     | Constructor(string)
     | ConsistentCase(case)
+    | InexhaustiveCase(MetaVar.t, HoleInstanceId.t, case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
@@ -126,6 +128,7 @@ module rec DHExp: {
     | Prj(_) => "Prj"
     | Constructor(_) => "Constructor"
     | ConsistentCase(_) => "ConsistentCase"
+    | InexhaustiveCase(_, _, _) => "InexhaustiveCase"
     | InconsistentBranches(_, _, _) => "InconsistentBranches"
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
@@ -174,6 +177,12 @@ module rec DHExp: {
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
       )
+    | InexhaustiveCase(u, i, Case(scrut, rules, n)) =>
+      InexhaustiveCase(
+        u,
+        i,
+        Case(strip_casts(scrut), List.map(strip_casts_rule, rules), n),
+      )
     | InconsistentBranches(u, i, Case(scrut, rules, n)) =>
       InconsistentBranches(
         u,
@@ -284,7 +293,8 @@ module rec DHExp: {
     | (
         InconsistentBranches(u1, i1, case1),
         InconsistentBranches(u2, i2, case2),
-      ) =>
+      )
+    | (InexhaustiveCase(u1, i1, case1), InexhaustiveCase(u2, i2, case2)) =>
       u1 == u2 && i1 == i2 && fast_equal_case(case1, case2)
     | (EmptyHole(_), _)
     | (NonEmptyHole(_), _)
@@ -292,7 +302,8 @@ module rec DHExp: {
     | (FreeVar(_), _)
     | (InvalidText(_), _)
     | (Closure(_), _)
-    | (InconsistentBranches(_), _) => false
+    | (InconsistentBranches(_), _)
+    | (InexhaustiveCase(_), _) => false
     };
   }
   and fast_equal_case = (Case(d1, rules1, i1), Case(d2, rules2, i2)) => {
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 126dee2e21..a397ef7e4b 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -69,6 +69,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
       }
     /* Forms with special ana rules but no particular typing requirements */
     | ConsistentCase(_)
+    | InexhaustiveCase(_)
     | InconsistentBranches(_)
     | Sequence(_)
     | Let(_)
@@ -271,7 +272,11 @@ let rec dhexp_of_uexp =
         | InHole(
             InexhaustiveMatch(Some(Common(Inconsistent(Internal(_))))),
           ) =>
+          // TODO: review
+          // If multiple errors are associated with a case expression,
+          // DHExp.InconsistentBranches is prioritized.
           DHExp.InconsistentBranches(id, 0, d)
+        | InHole(InexhaustiveMatch(_)) => DHExp.InexhaustiveCase(id, 0, d)
         | _ => ConsistentCase(d)
         };
       | TyAlias(_, _, e) => dhexp_of_uexp(m, e)
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index 529ca04260..3efea0f886 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -304,6 +304,7 @@ and matches_cast_Sum =
   | BinFloatOp(_)
   | BinStringOp(_)
   | InconsistentBranches(_)
+  | InexhaustiveCase(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
   | FailedCast(_, _, _)
@@ -409,6 +410,7 @@ and matches_cast_Tuple =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -544,6 +546,7 @@ and matches_cast_Cons =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -988,6 +991,11 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
       Indet(Closure(env, InconsistentBranches(u, i, Case(d1, rules, n))))
       |> return
 
+    | InexhaustiveCase(u, i, Case(d1, rules, n)) =>
+      //TODO: revisit this, consider some kind of dynamic casting
+      Indet(Closure(env, InexhaustiveCase(u, i, Case(d1, rules, n))))
+      |> return
+
     | EmptyHole(u, i) => Indet(Closure(env, EmptyHole(u, i))) |> return
 
     | NonEmptyHole(reason, u, i, d1) =>
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 18d4ea2b44..157fcc96e5 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -150,6 +150,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | BoundVar(_)
   | Let(_)
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | Fun(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -412,6 +413,13 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* i = hii_add_instance(u, env);
     Closure(env, InconsistentBranches(u, i, Case(scrut, rules, case_i)))
     |> return;
+
+  | InexhaustiveCase(u, _, Case(scrut, rules, case_i)) =>
+    let* scrut = pp_uneval(env, scrut);
+    let* rules = pp_uneval_rules(env, rules);
+    let* i = hii_add_instance(u, env);
+    Closure(env, InexhaustiveCase(u, i, Case(scrut, rules, case_i)))
+    |> return;
   }
 
 and pp_uneval_rules =
@@ -501,7 +509,8 @@ let rec track_children_of_hole =
   | NonEmptyHole(_, u, i, d) =>
     let hii = track_children_of_hole(hii, parent, d);
     hii |> HoleInstanceInfo.add_parent((u, i), parent);
-  | InconsistentBranches(u, i, Case(scrut, rules, _)) =>
+  | InconsistentBranches(u, i, Case(scrut, rules, _))
+  | InexhaustiveCase(u, i, Case(scrut, rules, _)) =>
     let hii = track_children_of_hole(hii, parent, scrut);
     let hii = track_children_of_hole_rules(hii, parent, rules);
     hii |> HoleInstanceInfo.add_parent((u, i), parent);
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 92f8cff0fe..45acf7caf2 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -89,6 +89,10 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);
     ConsistentCase(Case(d3, rules, n));
+  | InexhaustiveCase(u, i, Case(d3, rules, n)) =>
+    let d3 = subst_var(d1, x, d3);
+    let rules = subst_var_rules(d1, x, rules);
+    InexhaustiveCase(u, i, Case(d3, rules, n));
   | InconsistentBranches(u, i, Case(d3, rules, n)) =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);
diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re
index 52e9b0bdbd..7c0de89b5e 100644
--- a/src/haz3lweb/view/dhcode/DHCode.re
+++ b/src/haz3lweb/view/dhcode/DHCode.re
@@ -77,6 +77,7 @@ let view_of_layout = (~font_metrics: FontMetrics.t, l: DHLayout.t): Node.t => {
                ([with_cls("exception", txt)], ds)
              | NonEmptyHole(_)
              | InconsistentBranches(_)
+             | InexhaustiveCase(_)
              | Invalid(_) =>
                let offset = start.col - indent;
                let decoration =
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.re b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
index 83893613e4..97a71fb2b9 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.re
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
@@ -12,6 +12,7 @@ type t =
   | NonEmptyHole(ErrStatus.HoleReason.t, HoleInstance.t)
   | VarHole(VarErrStatus.HoleReason.t, HoleInstance.t)
   | InconsistentBranches(HoleInstance.t)
+  | InexhaustiveCase(HoleInstance.t)
   | Invalid(HoleInstance.t)
   | FailedCastDelim
   | FailedCastDecoration
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
index 3ff0d8ef48..474528202e 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
@@ -11,6 +11,7 @@ type t =
   | NonEmptyHole(ErrStatus.HoleReason.t, HoleInstance.t)
   | VarHole(VarErrStatus.HoleReason.t, HoleInstance.t)
   | InconsistentBranches(HoleInstance.t)
+  | InexhaustiveCase(HoleInstance.t)
   | Invalid(HoleInstance.t)
   | FailedCastDelim
   | FailedCastDecoration
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index ac241cd6f0..3336617a43 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -66,6 +66,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | Let(_)
   | FixF(_)
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => DHDoc_common.precedence_max
   | BinBoolOp(op, _, _) => precedence_bin_bool_op(op)
   | BinIntOp(op, _, _) => precedence_bin_int_op(op)
@@ -175,6 +176,8 @@ let rec mk =
       | InvalidText(u, i, t) => DHDoc_common.mk_InvalidText(t, (u, i))
       | InconsistentBranches(u, i, Case(dscrut, drs, _)) =>
         go_case(dscrut, drs) |> annot(DHAnnot.InconsistentBranches((u, i)))
+      | InexhaustiveCase(u, i, Case(dscrut, drs, _)) =>
+        go_case(dscrut, drs) |> annot(DHAnnot.InexhaustiveCase((u, i)))
       | BoundVar(x) => text(x)
       | Constructor(name) => DHDoc_common.mk_ConstructorLit(name)
       | BoolLit(b) => DHDoc_common.mk_BoolLit(b)