diff --git a/src/haz3lcore/dynamics/Constraint.re b/src/haz3lcore/dynamics/Constraint.re
new file mode 100644
index 0000000000..a56f435e55
--- /dev/null
+++ b/src/haz3lcore/dynamics/Constraint.re
@@ -0,0 +1,153 @@
+open Sexplib.Std;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t =
+  | Truth
+  | Falsity
+  | Hole
+  | Int(int)
+  | NotInt(int)
+  | Float(float)
+  | NotFloat(float)
+  | String(string)
+  | NotString(string)
+  | And(t, t)
+  | Or(t, t)
+  | InjL(t)
+  | InjR(t)
+  | Pair(t, t);
+
+let rec dual = (c: t): t =>
+  switch (c) {
+  | Truth => Falsity
+  | Falsity => Truth
+  | Hole => Hole
+  | Int(n) => NotInt(n)
+  | NotInt(n) => Int(n)
+  | Float(n) => NotFloat(n)
+  | NotFloat(n) => Float(n)
+  | String(s) => NotString(s)
+  | NotString(s) => String(s)
+  | And(c1, c2) => Or(dual(c1), dual(c2))
+  | Or(c1, c2) => And(dual(c1), dual(c2))
+  | InjL(c1) => Or(InjL(dual(c1)), InjR(Truth))
+  | InjR(c2) => Or(InjR(dual(c2)), InjL(Truth))
+  | Pair(c1, c2) =>
+    Or(
+      Pair(c1, dual(c2)),
+      Or(Pair(dual(c1), c2), Pair(dual(c1), dual(c2))),
+    )
+  };
+
+/** substitute Truth for Hole */
+let rec truify = (c: t): t =>
+  switch (c) {
+  | Hole => Truth
+  | Truth
+  | Falsity
+  | Int(_)
+  | NotInt(_)
+  | Float(_)
+  | NotFloat(_)
+  | String(_)
+  | NotString(_) => c
+  | And(c1, c2) => And(truify(c1), truify(c2))
+  | Or(c1, c2) => Or(truify(c1), truify(c2))
+  | InjL(c) => InjL(truify(c))
+  | InjR(c) => InjR(truify(c))
+  | Pair(c1, c2) => Pair(truify(c1), truify(c2))
+  };
+
+/** substitute Falsity for Hole */
+let rec falsify = (c: t): t =>
+  switch (c) {
+  | Hole => Falsity
+  | Truth
+  | Falsity
+  | Int(_)
+  | NotInt(_)
+  | Float(_)
+  | NotFloat(_)
+  | String(_)
+  | NotString(_) => c
+  | And(c1, c2) => And(falsify(c1), falsify(c2))
+  | Or(c1, c2) => Or(falsify(c1), falsify(c2))
+  | InjL(c) => InjL(falsify(c))
+  | InjR(c) => InjR(falsify(c))
+  | Pair(c1, c2) => Pair(falsify(c1), falsify(c2))
+  };
+
+let is_injL =
+  fun
+  | InjL(_) => true
+  | _ => false;
+
+let is_injR =
+  fun
+  | InjR(_) => true
+  | _ => false;
+
+let unwrapL =
+  fun
+  | InjL(c) => c
+  | _ => failwith("input can only be InjL(_)");
+
+let unwrapR =
+  fun
+  | InjR(c) => c
+  | _ => failwith("input can only be InjR(_)");
+
+let unwrap_pair =
+  fun
+  | Pair(c1, c2) => (c1, c2)
+  | _ => failwith("input can only be pair(_, _)");
+
+let rec or_constraints = (lst: list(t)): t =>
+  switch (lst) {
+  | [] => Falsity
+  | [xi] => xi
+  | [xi, ...xis] => Or(xi, or_constraints(xis))
+  };
+
+let rec ctr_of_nth_variant = (num_variants, nth): (t => t) =>
+  if (num_variants == 1) {
+    Fun.id;
+  } else if (nth == 0) {
+    xi => InjL(xi);
+  } else {
+    xi => InjR(xi |> ctr_of_nth_variant(num_variants - 1, nth - 1));
+  };
+
+let of_ap = (ctx, mode, ctr: option(Constructor.t), arg: t, syn_ty): t =>
+  switch (ctr) {
+  | Some(name) =>
+    let ty =
+      switch (mode) {
+      | Mode.Ana(ty) => Some(ty)
+      | Syn => syn_ty
+      | _ => None
+      };
+    switch (ty) {
+    | Some(ty) =>
+      switch (Typ.weak_head_normalize(ctx, ty)) {
+      | Sum(map) =>
+        let num_variants = ConstructorMap.cardinal(map);
+        switch (ConstructorMap.nth(map, name)) {
+        | Some(nth) => arg |> ctr_of_nth_variant(num_variants, nth)
+        | None => Falsity
+        };
+      | _ => Falsity
+      }
+    | None => Falsity
+    };
+  | None => Falsity
+  };
+
+let of_ctr = (ctx, mode, name, self) => {
+  let syn_ty =
+    switch (self) {
+    | Self.IsConstructor({syn_ty, _}) => syn_ty
+    | _ => assert(false) // impossible
+    };
+  of_ap(ctx, mode, Some(name), Truth, syn_ty);
+};
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 764f40a644..b960dae875 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -376,7 +376,8 @@ let rec dhexp_of_uexp =
           |> OptUtil.sequence;
         let d = DHExp.Case(d_scrut, d_rules, 0);
         switch (err_status) {
-        | InHole(Common(Inconsistent(Internal(_)))) =>
+        | InHole(Common(Inconsistent(Internal(_))))
+        | InHole(InexhaustiveMatch(Some(Inconsistent(Internal(_))))) =>
           DHExp.InconsistentBranches(id, 0, d)
         | _ => ConsistentCase(d)
         };
@@ -393,6 +394,13 @@ let rec dhexp_of_uexp =
 and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
   switch (Id.Map.find_opt(Term.UPat.rep_id(upat), m)) {
   | Some(InfoPat({mode, self, ctx, _})) =>
+    // NOTE: for the current implementation, redundancy is considered a static error
+    // but not a runtime error.
+    let self =
+      switch (self) {
+      | Redundant(self) => self
+      | _ => self
+      };
     let err_status = Info.status_pat(ctx, mode, self);
     let maybe_reason: option(ErrStatus.HoleReason.t) =
       switch (err_status) {
diff --git a/src/haz3lcore/dynamics/Incon.re b/src/haz3lcore/dynamics/Incon.re
new file mode 100644
index 0000000000..6f5c6af13f
--- /dev/null
+++ b/src/haz3lcore/dynamics/Incon.re
@@ -0,0 +1,145 @@
+open Sets;
+
+let is_inconsistent_int = (xis: list(Constraint.t)): bool => {
+  let (int_set, not_int_list) =
+    List.fold_left(
+      ((int_set, not_int_list), xi: Constraint.t) =>
+        switch (xi) {
+        | Int(n) => (IntSet.add(n, int_set), not_int_list)
+        | NotInt(n) => (int_set, [n, ...not_int_list])
+        | _ => failwith("input can only be Int | NotInt")
+        },
+      (IntSet.empty, []),
+      xis,
+    );
+  IntSet.cardinal(int_set) > 1
+  || List.exists(IntSet.mem(_, int_set), not_int_list);
+};
+
+let is_inconsistent_float = (xis: list(Constraint.t)): bool => {
+  let (float_set, not_float_list) =
+    List.fold_left(
+      ((float_set, not_float_list), xi: Constraint.t) =>
+        switch (xi) {
+        | Float(n) => (FloatSet.add(n, float_set), not_float_list)
+        | NotFloat(n) => (float_set, [n, ...not_float_list])
+        | _ => failwith("input can only be Float | NotFloat")
+        },
+      (FloatSet.empty, []),
+      xis,
+    );
+  FloatSet.cardinal(float_set) > 1
+  || List.exists(FloatSet.mem(_, float_set), not_float_list);
+};
+
+let is_inconsistent_string = (xis: list(Constraint.t)): bool => {
+  let (string_set, not_string_list) =
+    List.fold_left(
+      ((string_set, not_string_list), xi: Constraint.t) =>
+        switch (xi) {
+        | String(s) => (StringSet.add(s, string_set), not_string_list)
+        | NotString(s) => (string_set, [s, ...not_string_list])
+        | _ => failwith("input can only be String | NotString")
+        },
+      (StringSet.empty, []),
+      xis,
+    );
+  StringSet.cardinal(string_set) > 1
+  || List.exists(StringSet.mem(_, string_set), not_string_list);
+};
+
+let rec is_inconsistent = (xis: list(Constraint.t)): bool =>
+  switch (xis) {
+  | [] => false
+  | _
+      when
+        List.exists(Constraint.is_injL, xis)
+        && List.exists(Constraint.is_injR, xis) =>
+    true
+  | [xi, ...xis'] =>
+    switch (xi) {
+    | Truth => is_inconsistent(xis')
+    | Falsity => true
+    | Hole => assert(false) // Impossible
+    | And(xi1, xi2) => is_inconsistent([xi1, xi2, ...xis'])
+    | Or(xi1, xi2) =>
+      is_inconsistent([xi1, ...xis']) && is_inconsistent([xi2, ...xis'])
+    | InjL(_) =>
+      switch (List.partition(Constraint.is_injL, xis)) {
+      | (injLs, []) =>
+        injLs |> List.map(Constraint.unwrapL) |> is_inconsistent
+      | (injLs, others) => is_inconsistent(others @ injLs)
+      }
+    | InjR(_) =>
+      switch (List.partition(Constraint.is_injR, xis)) {
+      | (injRs, []) =>
+        injRs |> List.map(Constraint.unwrapR) |> is_inconsistent
+      | (injRs, others) => is_inconsistent(others @ injRs)
+      }
+    | Int(_)
+    | NotInt(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Int(_)
+          | NotInt(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (ns, []) => is_inconsistent_int(ns)
+      | (ns, others) => is_inconsistent(others @ ns)
+      }
+    | Float(_)
+    | NotFloat(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Float(_)
+          | NotFloat(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (fs, []) => is_inconsistent_float(fs)
+      | (fs, others) => is_inconsistent(others @ fs)
+      }
+    | String(_)
+    | NotString(_) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.String(_)
+          | NotString(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (ss, []) => is_inconsistent_string(ss)
+      | (ss, others) => is_inconsistent(others @ ss)
+      }
+    | Pair(_, _) =>
+      switch (
+        List.partition(
+          fun
+          | Constraint.Pair(_) => true
+          | _ => false,
+          xis,
+        )
+      ) {
+      | (pairs, []) =>
+        let (xisL, xisR) =
+          pairs |> List.map(Constraint.unwrap_pair) |> List.split;
+        is_inconsistent(xisL) || is_inconsistent(xisR);
+      | (pairs, others) => is_inconsistent(others @ pairs)
+      }
+    }
+  };
+
+let is_redundant = (xi_cur: Constraint.t, xi_pre: Constraint.t): bool =>
+  is_inconsistent(
+    Constraint.[And(truify(xi_cur), dual(falsify(xi_pre)))],
+  );
+
+let is_exhaustive = (xi: Constraint.t): bool =>
+  is_inconsistent(Constraint.[dual(truify(xi))]);
diff --git a/src/haz3lcore/dynamics/Sets.re b/src/haz3lcore/dynamics/Sets.re
new file mode 100644
index 0000000000..5c2179da68
--- /dev/null
+++ b/src/haz3lcore/dynamics/Sets.re
@@ -0,0 +1,23 @@
+module IntSet =
+  Set.Make({
+    type t = int;
+    let compare = compare;
+  });
+
+module BoolSet =
+  Set.Make({
+    type t = bool;
+    let compare = compare;
+  });
+
+module FloatSet =
+  Set.Make({
+    type t = float;
+    let compare = compare;
+  });
+
+module StringSet =
+  Set.Make({
+    type t = string;
+    let compare = compare;
+  });
diff --git a/src/haz3lcore/statics/ConstructorMap.re b/src/haz3lcore/statics/ConstructorMap.re
index c9ff0667dc..a350d16d92 100644
--- a/src/haz3lcore/statics/ConstructorMap.re
+++ b/src/haz3lcore/statics/ConstructorMap.re
@@ -99,3 +99,12 @@ let rec is_ground = (is_ground_value: 'a => bool, map: t('a)): bool =>
   | [(_, head), ...tail] =>
     is_ground_value(head) && tail |> is_ground(is_ground_value)
   };
+
+let nth = (map: t('a), ctr: Constructor.t): option(int) => {
+  // TODO: use List.find_index instead, which is available for OCaml 5.1
+  let ctrs_sorted = map |> sort |> ctrs_of;
+  List.find_opt(
+    nth => List.nth(ctrs_sorted, nth) == ctr,
+    List.init(List.length(ctrs_sorted), Fun.id),
+  );
+};
diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index 83f6ee86a0..11c44b1120 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -66,6 +66,7 @@ type error_common =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error_exp =
   | FreeVariable(Var.t) /* Unbound variable (not in typing context) */
+  | InexhaustiveMatch(option(error_common))
   | UnusedDeferral
   | BadPartialAp(Self.error_partial_ap)
   | Common(error_common);
@@ -73,6 +74,7 @@ type error_exp =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error_pat =
   | ExpectedConstructor /* Only construtors can be applied */
+  | Redundant(option(error_pat))
   | Common(error_common);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -214,6 +216,7 @@ type pat = {
   cls: Term.Cls.t,
   status: status_pat,
   ty: Typ.t,
+  constraint_: Constraint.t,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -316,6 +319,7 @@ let exp_co_ctx: exp => CoCtx.t = ({co_ctx, _}) => co_ctx;
 let exp_ty: exp => Typ.t = ({ty, _}) => ty;
 let pat_ctx: pat => Ctx.t = ({ctx, _}) => ctx;
 let pat_ty: pat => Typ.t = ({ty, _}) => ty;
+let pat_constraint: pat => Constraint.t = ({constraint_, _}) => constraint_;
 
 let rec status_common =
         (ctx: Ctx.t, mode: Mode.t, self: Self.t): status_common =>
@@ -370,8 +374,20 @@ let rec status_common =
     InHole(Inconsistent(Internal(Typ.of_source(tys))))
   };
 
-let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
+let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
   switch (mode, self) {
+  | (_, Redundant(self)) =>
+    let additional_err =
+      switch (status_pat(ctx, mode, self)) {
+      | InHole(Common(Inconsistent(Internal(_) | Expectation(_))) as err)
+      | InHole(Common(NoType(_)) as err) => Some(err)
+      | NotInHole(_) => None
+      | InHole(Common(Inconsistent(WithArrow(_))))
+      | InHole(ExpectedConstructor | Redundant(_)) =>
+        // ExpectedConstructor cannot be a reason to hole-wrap the entire pattern
+        failwith("InHole(Redundant(impossible_err))")
+      };
+    InHole(Redundant(additional_err));
   | (Syn | SynTypFun | Ana(_), Common(self_pat))
   | (SynFun, Common(IsConstructor(_) as self_pat)) =>
     /* Little bit of a hack. Anything other than a bound ctr will, in
@@ -391,9 +407,24 @@ let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
    depending on the mode, which represents the expectations of the
    surrounding syntactic context, and the self which represents the
    makeup of the expression / pattern itself. */
-let status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp =>
+let rec status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp =>
   switch (self, mode) {
   | (Free(name), _) => InHole(FreeVariable(name))
+  | (InexhaustiveMatch(self), _) =>
+    let additional_err =
+      switch (status_exp(ctx, mode, self)) {
+      | InHole(Common(Inconsistent(Internal(_)) as inconsistent_err)) =>
+        Some(inconsistent_err)
+      | NotInHole(_)
+      | InHole(Common(Inconsistent(Expectation(_) | WithArrow(_)))) => None /* Type checking should fail and these errors would be nullified */
+      | InHole(Common(NoType(_)))
+      | InHole(
+          FreeVariable(_) | InexhaustiveMatch(_) | UnusedDeferral |
+          BadPartialAp(_),
+        ) =>
+        failwith("InHole(InexhaustiveMatch(impossible_err))")
+      };
+    InHole(InexhaustiveMatch(additional_err));
   | (IsDeferral(InAp), Ana(ana)) => NotInHole(AnaDeferralConsistent(ana))
   | (IsDeferral(_), _) => InHole(UnusedDeferral)
   | (IsBadPartialAp(_ as info), _) => InHole(BadPartialAp(info))
@@ -509,11 +540,36 @@ let fixed_typ_ok: ok_pat => Typ.t =
   | Ana(Consistent({join, _})) => join
   | Ana(InternallyInconsistent({ana, _})) => ana;
 
-let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t =>
+let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t => {
+  // TODO: get rid of unwrapping (probably by changing the implementation of error_exp.Redundant)
+  let self =
+    switch (self) {
+    | Redundant(self) => self
+    | _ => self
+    };
   switch (status_pat(ctx, mode, self)) {
   | InHole(_) => Unknown(Internal)
   | NotInHole(ok) => fixed_typ_ok(ok)
   };
+};
+
+let fixed_constraint_pat =
+    (
+      upat: UPat.t,
+      ctx,
+      mode: Mode.t,
+      self: Self.pat,
+      constraint_: Constraint.t,
+    )
+    : Constraint.t =>
+  switch (upat.term) {
+  | TypeAnn(_) => constraint_
+  | _ =>
+    switch (fixed_typ_pat(ctx, mode, self)) {
+    | Unknown(_) => Constraint.Hole
+    | _ => constraint_
+    }
+  };
 
 let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t =>
   switch (status_exp(ctx, mode, self)) {
@@ -533,11 +589,24 @@ let derived_exp =
 
 /* Add derivable attributes for pattern terms */
 let derived_pat =
-    (~upat: UPat.t, ~ctx, ~co_ctx, ~mode, ~ancestors, ~self): pat => {
+    (~upat: UPat.t, ~ctx, ~co_ctx, ~mode, ~ancestors, ~self, ~constraint_)
+    : pat => {
   let cls = Cls.Pat(UPat.cls_of_term(upat.term));
   let status = status_pat(ctx, mode, self);
   let ty = fixed_typ_pat(ctx, mode, self);
-  {cls, self, mode, ty, status, ctx, co_ctx, ancestors, term: upat};
+  let constraint_ = fixed_constraint_pat(upat, ctx, mode, self, constraint_);
+  {
+    cls,
+    self,
+    mode,
+    ty,
+    status,
+    ctx,
+    co_ctx,
+    ancestors,
+    term: upat,
+    constraint_,
+  };
 };
 
 /* Add derivable attributes for types */
diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re
index 89e8352d41..052bf581ef 100644
--- a/src/haz3lcore/statics/Self.re
+++ b/src/haz3lcore/statics/Self.re
@@ -49,12 +49,14 @@ type error_partial_ap =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type exp =
   | Free(Var.t)
+  | InexhaustiveMatch(exp)
   | IsDeferral(Term.UExp.deferral_position)
   | IsBadPartialAp(error_partial_ap)
   | Common(t);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type pat =
+  | Redundant(pat)
   | Common(t);
 
 let join_of = (j: join_type, ty: Typ.t): Typ.t =>
@@ -80,13 +82,15 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) =
   ctx =>
     fun
     | Free(_)
+    | InexhaustiveMatch(_)
     | IsDeferral(_)
     | IsBadPartialAp(_) => None
     | Common(self) => typ_of(ctx, self);
 
-let typ_of_pat: (Ctx.t, pat) => option(Typ.t) =
+let rec typ_of_pat: (Ctx.t, pat) => option(Typ.t) =
   ctx =>
     fun
+    | Redundant(pat) => typ_of_pat(ctx, pat)
     | Common(self) => typ_of(ctx, self);
 
 /* The self of a var depends on the ctx; if the
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 637dbdf6b0..73d4f02265 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -348,11 +348,12 @@ and uexp_to_info_map =
     /* add co_ctx to pattern */
     let (p, m) =
       go_pat(~is_synswitch=false, ~co_ctx=e.co_ctx, ~mode=mode_pat, p, m);
-    add(
-      ~self=Just(Arrow(p.ty, e.ty)),
-      ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx),
-      m,
-    );
+    // TODO: factor out code
+    let unwrapped_self: Self.exp = Common(Just(Arrow(p.ty, e.ty)));
+    let is_exhaustive = p |> Info.pat_constraint |> Incon.is_exhaustive;
+    let self =
+      is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self);
+    add'(~self, ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m);
   | TypFun({term: Var(name), _} as utpat, body)
       when !Ctx.shadows_typ(ctx, name) =>
     let mode_body = Mode.of_forall(ctx, Some(name), mode);
@@ -425,8 +426,13 @@ and uexp_to_info_map =
         p,
         m,
       );
-    add(
-      ~self=Just(body.ty),
+    // TODO: factor out code
+    let unwrapped_self: Self.exp = Common(Just(body.ty));
+    let is_exhaustive = p_ana |> Info.pat_constraint |> Incon.is_exhaustive;
+    let self =
+      is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self);
+    add'(
+      ~self,
       ~co_ctx=
         CoCtx.union([def.co_ctx, CoCtx.mk(ctx, p_ana.ctx, body.co_ctx)]),
       m,
@@ -467,19 +473,91 @@ and uexp_to_info_map =
     let e_tys = List.map(Info.exp_ty, es);
     let e_co_ctxs =
       List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es));
-    /* Add co-ctxs to patterns */
-    let (_, m) =
-      map_m(
-        ((p, co_ctx)) =>
-          go_pat(~is_synswitch=false, ~co_ctx, ~mode=Mode.Ana(scrut.ty), p),
-        List.combine(ps, e_co_ctxs),
-        m,
-      );
-    add(
-      ~self=Self.match(ctx, e_tys, branch_ids),
-      ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs),
-      m,
-    );
+    let unwrapped_self: Self.exp =
+      Common(Self.match(ctx, e_tys, branch_ids));
+    let constraint_ty =
+      switch (scrut.ty) {
+      | Unknown(_) =>
+        map_m(go_pat(~is_synswitch=false, ~co_ctx=CoCtx.empty), ps, m)
+        |> fst
+        |> List.map(Info.pat_ty)
+        |> Typ.join_all(~empty=Unknown(Internal), ctx)
+      | ty => Some(ty)
+      };
+    let (self, m) =
+      switch (constraint_ty) {
+      | Some(constraint_ty) =>
+        let pats_to_info_map = (ps: list(UPat.t), m) => {
+          /* Add co-ctxs to patterns */
+          List.fold_left(
+            ((m, acc_constraint), (p, co_ctx)) => {
+              let p_constraint =
+                go_pat(
+                  ~is_synswitch=false,
+                  ~co_ctx,
+                  ~mode=Mode.Ana(constraint_ty),
+                  p,
+                  m,
+                )
+                |> fst
+                |> Info.pat_constraint;
+              let (p, m) =
+                go_pat(
+                  ~is_synswitch=false,
+                  ~co_ctx,
+                  ~mode=Mode.Ana(scrut.ty),
+                  p,
+                  m,
+                );
+              let is_redundant =
+                Incon.is_redundant(p_constraint, acc_constraint);
+              let self = is_redundant ? Self.Redundant(p.self) : p.self;
+              let info =
+                Info.derived_pat(
+                  ~upat=p.term,
+                  ~ctx=p.ctx,
+                  ~co_ctx=p.co_ctx,
+                  ~mode=p.mode,
+                  ~ancestors=p.ancestors,
+                  ~self,
+                  // Mark patterns as redundant at the top level
+                  // because redundancy doesn't make sense in a smaller context
+                  ~constraint_=p_constraint,
+                );
+              (
+                // Override the info for the single upat
+                add_info(p.term.ids, InfoPat(info), m),
+                is_redundant
+                  ? acc_constraint  // Redundant patterns are ignored
+                  : Constraint.Or(p_constraint, acc_constraint),
+              );
+            },
+            (m, Constraint.Falsity),
+            List.combine(ps, e_co_ctxs),
+          );
+        };
+        let (m, final_constraint) = pats_to_info_map(ps, m);
+        let is_exhaustive = Incon.is_exhaustive(final_constraint);
+        let self =
+          is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self);
+        (self, m);
+      | None =>
+        /* Add co-ctxs to patterns */
+        let (_, m) =
+          map_m(
+            ((p, co_ctx)) =>
+              go_pat(
+                ~is_synswitch=false,
+                ~co_ctx,
+                ~mode=Mode.Ana(scrut.ty),
+                p,
+              ),
+            List.combine(ps, e_co_ctxs),
+            m,
+          );
+        (unwrapped_self, m);
+      };
+    add'(~self, ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), m);
   | TyAlias(typat, utyp, body) =>
     let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd;
     switch (typat.term) {
@@ -553,7 +631,7 @@ and upat_to_info_map =
       m: Map.t,
     )
     : (Info.pat, Map.t) => {
-  let add = (~self, ~ctx, m) => {
+  let add = (~self, ~ctx, ~constraint_, m) => {
     let info =
       Info.derived_pat(
         ~upat,
@@ -562,42 +640,74 @@ and upat_to_info_map =
         ~mode,
         ~ancestors,
         ~self=Common(self),
+        ~constraint_,
       );
     (info, add_info(ids, InfoPat(info), m));
   };
-  let atomic = self => add(~self, ~ctx, m);
+  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 unknown = Typ.Unknown(is_synswitch ? SynSwitch : Internal);
   let ctx_fold = (ctx: Ctx.t, m) =>
     List.fold_left2(
-      ((ctx, tys, m), e, mode) =>
+      ((ctx, tys, cons, m), e, mode) =>
         go(~ctx, ~mode, e, m)
-        |> (((info, m)) => (info.ctx, tys @ [info.ty], m)),
-      (ctx, [], m),
+        |> (
+          ((info, m)) => (
+            info.ctx,
+            tys @ [info.ty],
+            cons @ [info.constraint_],
+            m,
+          )
+        ),
+      (ctx, [], [], m),
     );
+  let hole = self => atomic(self, Constraint.Hole);
   switch (term) {
   | MultiHole(tms) =>
     let (_, m) = multi(~ctx, ~ancestors, m, tms);
-    add(~self=IsMulti, ~ctx, m);
-  | Invalid(token) => atomic(BadToken(token))
-  | EmptyHole => atomic(Just(unknown))
-  | Int(_) => atomic(Just(Int))
-  | Float(_) => atomic(Just(Float))
-  | Triv => atomic(Just(Prod([])))
-  | Bool(_) => atomic(Just(Bool))
-  | String(_) => atomic(Just(String))
+    add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m);
+  | Invalid(token) => hole(BadToken(token))
+  | EmptyHole => hole(Just(unknown))
+  | Int(int) => atomic(Just(Int), Constraint.Int(int))
+  | Float(float) => atomic(Just(Float), Constraint.Float(float))
+  | Triv => atomic(Just(Prod([])), Constraint.Truth)
+  | Bool(bool) =>
+    atomic(
+      Just(Bool),
+      bool
+        ? Constraint.InjL(Constraint.Truth)
+        : Constraint.InjR(Constraint.Truth),
+    )
+  | String(string) => atomic(Just(String), Constraint.String(string))
   | ListLit(ps) =>
     let ids = List.map(UPat.rep_id, ps);
     let modes = Mode.of_list_lit(ctx, List.length(ps), mode);
-    let (ctx, tys, m) = ctx_fold(ctx, m, ps, modes);
-    add(~self=Self.listlit(~empty=unknown, ctx, tys, ids), ~ctx, m);
+    let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes);
+    let rec cons_fold_list = cs =>
+      switch (cs) {
+      | [] => Constraint.InjL(Constraint.Truth) // Left = nil, Right = cons
+      | [hd, ...tl] =>
+        Constraint.InjR(Constraint.Pair(hd, cons_fold_list(tl)))
+      };
+    add(
+      ~self=Self.listlit(~empty=unknown, ctx, tys, ids),
+      ~ctx,
+      ~constraint_=cons_fold_list(cons),
+      m,
+    );
   | Cons(hd, tl) =>
     let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m);
     let (tl, m) =
       go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m);
-    add(~self=Just(List(hd.ty)), ~ctx=tl.ctx, m);
-  | Wild => atomic(Just(unknown))
+    add(
+      ~self=Just(List(hd.ty)),
+      ~ctx=tl.ctx,
+      ~constraint_=
+        Constraint.InjR(Constraint.Pair(hd.constraint_, tl.constraint_)),
+      m,
+    );
+  | Wild => atomic(Just(unknown), Constraint.Truth)
   | Var(name) =>
     /* NOTE: The self type assigned to pattern variables (Unknown)
        may be SynSwitch, but SynSwitch is never added to the context;
@@ -605,25 +715,50 @@ and upat_to_info_map =
     let ctx_typ =
       Info.fixed_typ_pat(ctx, mode, Common(Just(Unknown(Internal))));
     let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ});
-    add(~self=Just(unknown), ~ctx=Ctx.extend(ctx, entry), m);
+    add(
+      ~self=Just(unknown),
+      ~ctx=Ctx.extend(ctx, entry),
+      ~constraint_=Constraint.Truth,
+      m,
+    );
   | Tuple(ps) =>
     let modes = Mode.of_prod(ctx, mode, List.length(ps));
-    let (ctx, tys, m) = ctx_fold(ctx, m, ps, modes);
-    add(~self=Just(Prod(tys)), ~ctx, m);
+    let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes);
+    let rec cons_fold_tuple = cs =>
+      switch (cs) {
+      | [] => Constraint.Truth
+      | [elt] => elt
+      | [hd, ...tl] => Constraint.Pair(hd, cons_fold_tuple(tl))
+      };
+    add(
+      ~self=Just(Prod(tys)),
+      ~ctx,
+      ~constraint_=cons_fold_tuple(cons),
+      m,
+    );
   | Parens(p) =>
     let (p, m) = go(~ctx, ~mode, p, m);
-    add(~self=Just(p.ty), ~ctx=p.ctx, m);
-  | Constructor(ctr) => atomic(Self.of_ctr(ctx, ctr))
+    add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
+  | Constructor(ctr) =>
+    let self = Self.of_ctr(ctx, ctr);
+    atomic(self, Constraint.of_ctr(ctx, mode, ctr, self));
   | Ap(fn, arg) =>
-    let fn_mode = Mode.of_ap(ctx, mode, UPat.ctr_name(fn));
+    let ctr = UPat.ctr_name(fn);
+    let fn_mode = Mode.of_ap(ctx, mode, ctr);
     let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m);
     let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
     let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m);
-    add(~self=Just(ty_out), ~ctx=arg.ctx, m);
+    add(
+      ~self=Just(ty_out),
+      ~ctx=arg.ctx,
+      ~constraint_=
+        Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)),
+      m,
+    );
   | TypeAnn(p, ann) =>
     let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m);
     let (p, m) = go(~ctx, ~mode=Ana(ann.ty), p, m);
-    add(~self=Just(ann.ty), ~ctx=p.ctx, m);
+    add(~self=Just(ann.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
   };
 }
 and utyp_to_info_map =
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 4bc9a68d35..99ed8fd0fb 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -173,10 +173,21 @@ let typ_err_view = (ok: Info.error_typ) =>
     ]
   };
 
-let exp_view = (cls: Term.Cls.t, status: Info.status_exp) =>
+let rec exp_view = (cls: Term.Cls.t, status: Info.status_exp) =>
   switch (status) {
   | InHole(FreeVariable(name)) =>
     div_err([code_err(name), text("not found")])
+  | InHole(InexhaustiveMatch(additional_err)) =>
+    let cls_str = Term.Cls.show(cls);
+    switch (additional_err) {
+    | None => div_err([text(cls_str ++ " is inexhaustive")])
+    | Some(err) =>
+      let cls_str = String.uncapitalize_ascii(cls_str);
+      div_err([
+        exp_view(cls, InHole(Common(err))),
+        text("; " ++ cls_str ++ " is inexhaustive"),
+      ]);
+    };
   | InHole(UnusedDeferral) =>
     div_err([text("Deferral must appear as a function argument")])
   | InHole(BadPartialAp(NoDeferredArgs)) =>
@@ -199,9 +210,15 @@ let exp_view = (cls: Term.Cls.t, status: Info.status_exp) =>
   | NotInHole(Common(ok)) => div_ok(common_ok_view(cls, ok))
   };
 
-let pat_view = (cls: Term.Cls.t, status: Info.status_pat) =>
+let rec pat_view = (cls: Term.Cls.t, status: Info.status_pat) =>
   switch (status) {
   | InHole(ExpectedConstructor) => div_err([text("Expected a constructor")])
+  | InHole(Redundant(additional_err)) =>
+    switch (additional_err) {
+    | None => div_err([text("Pattern is redundant")])
+    | Some(err) =>
+      div_err([pat_view(cls, InHole(err)), text("; pattern is redundant")])
+    }
   | InHole(Common(error)) => div_err(common_err_view(cls, error))
   | NotInHole(ok) => div_ok(common_ok_view(cls, ok))
   };