diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index a68171bc52..cf692f8f71 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -70,6 +70,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)]
@@ -300,8 +301,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 | Ana(_), Common(self_pat))
   | (SynFun, Common(IsConstructor(_) as self_pat)) =>
     /* Little bit of a hack. Anything other than a bound ctr will, in
@@ -447,8 +460,9 @@ let fixed_constraint_pat =
     (ctx, mode: Mode.t, self: Self.pat, constraint_: Constraint.t)
     : Constraint.t =>
   switch (status_pat(ctx, mode, self)) {
-  | InHole(_) => Constraint.Hole
+  | InHole(Redundant(None))
   | NotInHole(_) => constraint_
+  | InHole(_) => Constraint.Hole
   };
 
 let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t =>
diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re
index 684b19b01b..9f4f7d48ed 100644
--- a/src/haz3lcore/statics/Self.re
+++ b/src/haz3lcore/statics/Self.re
@@ -40,6 +40,7 @@ type exp =
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type pat =
+  | Redundant(pat)
   | Common(t);
 
 /* What the type would be if the position had been
@@ -64,6 +65,7 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) =
 let typ_of_pat: (Ctx.t, pat) => option(Typ.t) =
   ctx =>
     fun
+    | Redundant(_) => None
     | 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 547e8a8913..840f2a5292 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -273,9 +273,37 @@ and uexp_to_info_map =
     let rules_to_info_map = (rules: list((UPat.t, UExp.t)), m) => {
       let (ps, es) = List.split(rules);
       let branch_ids = List.map(UExp.rep_id, es);
-      let (ps, m) =
-        map_m(go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty)), ps, m);
-      let p_constraints = List.map(Info.pat_constraint, ps);
+      let (ps, m, final_constraint) =
+        List.fold_left(
+          ((ps, m, acc_constraint), p) => {
+            let (p, m) =
+              go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty), p, m);
+            let p_constraint = Info.pat_constraint(p);
+            if (!Incon.is_redundant(p_constraint, acc_constraint)) {
+              (ps @ [p], m, Constraint.Or(p_constraint, acc_constraint));
+            } else {
+              let info =
+                Info.derived_pat(
+                  ~upat=p.term,
+                  ~ctx=p.ctx,
+                  ~mode=p.mode,
+                  ~ancestors=p.ancestors,
+                  ~self=Redundant(p.self),
+                  // Mark patterns as redundant at the top level
+                  // because redundancy doesn't make sense in a smaller context
+                  ~constraint_=p_constraint,
+                );
+              (
+                ps @ [info],
+                // Override the info for the single upat
+                add_info(p.term.ids, InfoPat(info), m),
+                acc_constraint // Redundant patterns are ignored
+              );
+            };
+          },
+          ([], m, Constraint.Falsity),
+          ps,
+        );
       let p_ctxs = List.map(Info.pat_ctx, ps);
       let (es, m) =
         List.fold_left2(
@@ -289,7 +317,7 @@ and uexp_to_info_map =
         es,
         List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es)),
         branch_ids,
-        Constraint.or_constraints(p_constraints),
+        final_constraint,
         m,
       );
     };
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 6cc2adf8f6..86db8d7aa9 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -174,9 +174,18 @@ let rec exp_view = (cls: Term.Cls.t, status: Info.status_exp) =>
   | NotInHole(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 necessarily redundant")])
+    | Some(err) =>
+      div_err([
+        pat_view(cls, InHole(err)),
+        text("; pattern is necessarily redundant"),
+      ])
+    }
   | InHole(Common(error)) => div_err(common_err_view(cls, error))
   | NotInHole(ok) => div_ok(common_ok_view(cls, ok))
   };
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 02379d4d4c..3336617a43 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -94,6 +94,7 @@ let mk_bin_float_op = (op: TermBase.UExp.op_bin_float): DHDoc.t =>
 let mk_bin_string_op = (op: TermBase.UExp.op_bin_string): DHDoc.t =>
   Doc.text(TermBase.UExp.string_op_to_string(op));
 
+// DHExp is annotated here
 let rec mk =
         (
           ~settings: Settings.Evaluation.t,