Duplicate variable checking in patterns

src/haz3lcore/TyDi/ErrorPrint.re

@@ -51,6 +51,7 @@ let common_error: Info.error_common => string =
   | NoType(BadLabel(_)) => "Invalid label"
   | NoType(InvalidLabel(_)) => "Invalid label"
   | DuplicateLabel(_, _) => "Duplicate label"
+  | DuplicateVar(_, _) => "Duplicate variable"
   | TupleLabelError(_) => "Invalid tuple label"
   | NoType(UnexpectedLabelSort(_)) => "Unexpected label sort"
   | NoType(BadToken(token)) => prn("\"%s\" isn't a valid token", token)

src/language/statics/Elaborator.re

@@ -311,8 +311,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
         };
       let is_recursive =
         Statics.is_recursive(ctx, p, def, ty1)
-        && Pat.get_bindings(p)
-        |> Option.get
+        && Pat.bound_vars(p)
         |> List.exists(f => VarMap.lookup(co_ctx, f) != None);
       if (!is_recursive) {
         let (def, _) = elaborate(m, def);

src/language/statics/Info.re

@@ -65,6 +65,7 @@ type error_common =
   | Inconsistent(error_inconsistent)
   /* The error on a specific duplicate label */
   | DuplicateLabel(LabeledTuple.label, Typ.t)
+  | DuplicateVar(string, Typ.t)
   /* Tuple/TupLabel contains malformed labels, duplicate labels, and/or invalid labels */
   | TupleLabelError({
       malformed_labels: list(Any.t),
@@ -492,9 +493,12 @@ let rec status_common =
         typ,
       }),
     )
-  | (Duplicate(lab, Just(ty)), _) => InHole(DuplicateLabel(lab, ty))
-  | (Duplicate(lab, _), _) =>
+  | (DuplicateLabel(lab, Just(ty)), _) => InHole(DuplicateLabel(lab, ty))
+  | (DuplicateVar(lab, Just(ty)), _) => InHole(DuplicateVar(lab, ty))
+  | (DuplicateLabel(lab, _), _) =>
     InHole(DuplicateLabel(lab, Unknown(Internal) |> Typ.temp))
+  | (DuplicateVar(lab, _), _) =>
+    InHole(DuplicateVar(lab, Unknown(Internal) |> Typ.temp))
   | (IsMulti, _) => NotInHole(Syn(Unknown(Internal) |> Typ.temp))
   | (NoMeet(PolyEq, tys), _)
   | (NoMeet(_, tys), {term: Unknown(SynSwitch), _}) =>
@@ -546,6 +550,7 @@ let rec status_pat = (ctx: Ctx.t, ty_ana: Typ.t, self: Self.pat): status_pat =>
             Inconsistent(Internal(_) | Expectation(_) | CompareFun(_)) |
             NoType(_) |
             DuplicateLabel(_) |
+            DuplicateVar(_) |
             TupleLabelError(_),
           ) as err,
         ) =>
@@ -583,6 +588,7 @@ let rec status_exp = (ctx: Ctx.t, ty_ana, self: Self.exp): status_exp =>
       | InHole(Common(NoType(_)))
       | InHole(Common(TupleLabelError(_)))
       | InHole(Common(DuplicateLabel(_)))
+      | InHole(Common(DuplicateVar(_)))
       | InHole(TupleExtensionRequiresTuples)
       | InHole(
           FreeVariable(_) | InexhaustiveMatch(_) | UnusedDeferral |
@@ -829,7 +835,8 @@ let fixed_typ_err_common: (error_common, Typ.t) => Typ.t =
     | NoType(InvalidLabel(_))
     | NoType(UnexpectedLabelSort(_)) => Unknown(Internal) |> Typ.temp
     | TupleLabelError({typ, _})
-    | DuplicateLabel(_, typ) => typ_or_ana(typ)
+    | DuplicateLabel(_, typ)
+    | DuplicateVar(_, typ) => typ_or_ana(typ)
     | Inconsistent(Expectation({ana, _})) => ana
     | Inconsistent(Internal(_)) => Unknown(Internal) |> Typ.temp // Should this be some sort of meet?
     | Inconsistent(CompareFun(_)) => typ_or_ana(Atom(Bool) |> Typ.temp)

src/language/statics/Self.re

@@ -30,8 +30,9 @@ type meet_type =
 type t =
   | Just(Typ.t) /* Just a regular type */
   | NoMeet(meet_type, list(Typ.source)) /* Inconsistent types for e.g match, listlits */
-  | Duplicate(LabeledTuple.label, t) /* Duplicate label, marked as duplicate */
+  | DuplicateLabel(LabeledTuple.label, t) /* Duplicate label, marked as duplicate */
   | CompareFun(Typ.t) /* Type equality failed because of arrow type inside */
+  | DuplicateVar(string, t)
   | BadToken(string) /* Invalid expression token, continues with undefined behavior */
   | BadLabel(Any.t) /* TupLabel label component is not a valid Label*/
   | InvalidLabel(LabeledTuple.label, list(LabeledTuple.label)) /* Invalid label in a labeled tuple where these labels are expected */
@@ -108,7 +109,8 @@ let meet_of = (j: meet_type, ty: Typ.t): Typ.t =>
 let typ_of: t => option(Typ.t) =
   fun
   | Just(typ)
-  | Duplicate(_, Just(typ))
+  | DuplicateLabel(_, Just(typ))
+  | DuplicateVar(_, Just(typ))
   | TupleLabelError({typ, _}) => Some(typ)
   | CompareFun(_) => Some(Atom(Bool) |> Typ.fresh)
   | FreeConstructor(name) =>
@@ -125,7 +127,8 @@ let typ_of: t => option(Typ.t) =
     )
   | BadToken(_)
   | IsMulti
-  | Duplicate(_)
+  | DuplicateLabel(_)
+  | DuplicateVar(_)
   | BadLabel(_)
   | InvalidLabel(_)
   | ExplicitNonlabel

src/language/statics/Statics.re

@@ -51,7 +51,8 @@ let rec any_to_info_map =
         ~is_synswitch=false,
         ~co_ctx=CoCtx.empty,
         ~ancestors,
-        ~duplicates=[],
+        ~duplicate_bindings=[],
+        ~duplicate_labels=[],
         ~ctx,
         p,
         m,
@@ -210,7 +211,7 @@ and uexp_to_info_map =
         go(~ana, ~duplicates, e, m) |> (((e, m)) => (es @ [e], m)),
       ([], m),
     );
-  let go_pat = upat_to_info_map(~ctx, ~ancestors, ~duplicates);
+  let go_pat = upat_to_info_map(~ctx, ~ancestors);
   let go_typ = utyp_to_info_map(~ctx, ~ancestors);
   let label_to_info_map =
       (expected_labels, labmode, label: Exp.t, m: Map.t)
@@ -681,7 +682,7 @@ and uexp_to_info_map =
     | Label(name) when label_sort =>
       let self = Self.Just(Label(name) |> Typ.temp);
       List.exists(l => name == l, duplicates)
-        ? atomic(Duplicate(name, self)) : atomic(self);
+        ? atomic(DuplicateLabel(name, self)) : atomic(self);
     | Label(name) =>
       let self = Self.UnexpectedLabelSort(name);
       atomic(self);
@@ -1394,7 +1395,8 @@ and upat_to_info_map =
       ~ctx,
       ~co_ctx,
       ~ancestors: Info.ancestors,
-      ~duplicates: list(string),
+      ~duplicate_bindings: list(string)=[],
+      ~duplicate_labels: list(string)=[],
       ~expected_labels=?,
       ~ana: Typ.t=Unknown(Internal) |> Typ.temp,
       ~under_ascription: bool=false,
@@ -1460,7 +1462,8 @@ and upat_to_info_map =
         ~ctx,
         ~co_ctx,
         ~ancestors,
-        ~duplicates=[],
+        ~duplicate_bindings=[],
+        ~duplicate_labels=[],
         ~expected_labels=?,
         ~ana,
         ~under_ascription=false,
@@ -1475,7 +1478,8 @@ and upat_to_info_map =
       ~ctx,
       ~co_ctx,
       ~ancestors,
-      ~duplicates,
+      ~duplicate_bindings,
+      ~duplicate_labels,
       ~ana,
       ~under_ascription,
       ~override_self?,
@@ -1491,10 +1495,18 @@ and upat_to_info_map =
   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, ~duplicates=[]) =>
+  let ctx_fold = (ctx: Ctx.t, m, ~duplicate_bindings=[], ~duplicate_labels=[]) =>
     List.fold_left2(
       ((ctx, tys, cons, m, info_all), e, ana) =>
-        go(~ctx, ~ana, ~duplicates, ~inferred_label?, e, m)
+        go(
+          ~ctx,
+          ~ana,
+          ~duplicate_bindings,
+          ~duplicate_labels,
+          ~inferred_label?,
+          e,
+          m,
+        )
         |> (
           ((info, m)) => (
             info.ctx,
@@ -1645,12 +1657,21 @@ and upat_to_info_map =
           typ: ctx_typ,
           custom_statics: None,
         });
-      add(
-        ~self=Just(unknown),
-        ~ctx=Ctx.extend(ctx, entry),
-        ~constraint_=Coverage.Constraint.Truth,
-        m,
-      );
+
+      List.exists(l => name == l, duplicate_bindings)
+        ? add(
+            ~self=DuplicateVar(name, Just(unknown)),
+            ~ctx=Ctx.extend(ctx, entry),
+            ~constraint_=Coverage.Constraint.Truth,
+            m,
+          )
+        : add(
+            ~self=Just(unknown),
+            ~ctx=Ctx.extend(ctx, entry),
+            ~constraint_=Coverage.Constraint.Truth,
+            m,
+          );
+
     | TupLabel({term: ExplicitNonlabel, _} as label, p) =>
       let (p, m) = go(~ana, ~ctx, p, m);
       let (_, m) = go(~label_sort=true, ~ctx, ~ana=syn, label, m);
@@ -1672,12 +1693,21 @@ and upat_to_info_map =
               ~ctx,
               ~ana=labmode,
               ~override_self=?label_self,
-              ~duplicates,
+              ~duplicate_bindings,
+              ~duplicate_labels,
               ~label_sort=true,
               label,
               m,
             );
-          let (p, m) = go(~ctx, ~ana=val_mode, ~inferred_label?, p, m);
+          let (p, m) =
+            go(
+              ~ctx,
+              ~ana=val_mode,
+              ~inferred_label?,
+              ~duplicate_bindings,
+              p,
+              m,
+            );
           (lab, p, m);
         | _ =>
           let (lab, m) =
@@ -1694,7 +1724,8 @@ and upat_to_info_map =
                 | (EmptyHole, _) => None
                 | _ => Some(BadLabel(Pat(label)))
                 },
-              ~duplicates,
+              ~duplicate_bindings,
+              ~duplicate_labels,
               label,
               m,
             );
@@ -1782,7 +1813,9 @@ and upat_to_info_map =
 
       let new_labels =
         List.map(p => Pat.match_tup_label(p) |> Option.map(fst), ps);
-      let duplicate_labels =
+      let new_duplicate_bindings =
+        Pat.get_duplicate_bindings(Pat.fresh(term));
+      let new_duplicate_labels =
         LabeledTuple.get_duplicate_labels(Pat.match_tup_label, ps);
       let (ctx, tys, cons, m, info_pats) =
         List.fold_left2(
@@ -1791,7 +1824,10 @@ and upat_to_info_map =
               ~ctx,
               ~ana,
               ~inferred_label?,
-              ~duplicates=duplicate_labels,
+              // Perhaps multiple copies of something in duplicates, but probably not an issue.
+              // Needed so that nested tuples can have duplicate bindings saved.
+              ~duplicate_bindings=duplicate_bindings @ new_duplicate_bindings,
+              ~duplicate_labels=new_duplicate_labels,
               ~expected_labels?,
               e,
               m,
@@ -1862,12 +1898,13 @@ and upat_to_info_map =
       );
     | Label(name) =>
       let self = Self.Just(Label(name) |> Typ.temp);
-      List.exists(l => name == l, duplicates)
-        ? atomic(Duplicate(name, self), Coverage.Constraint.Truth)
+      List.exists(l => name == l, duplicate_labels)
+        ? atomic(DuplicateLabel(name, self), Coverage.Constraint.Truth)
         : atomic(self, Coverage.Constraint.Truth);
     | Parens(p)
     | Projector(_, p) =>
-      let (p, m) = go(~ctx, ~ana, p, m);
+      let (p, m) =
+        go(~ctx, ~ana, p, ~duplicate_bindings, ~duplicate_labels, m);
       add'(~self=p.self, ~ctx=p.ctx, ~constraint_=p.constraint_, m);
     | Constructor(ctr, ty) =>
       let self = Self.of_ctr(ctx, ctr, ana, ty);

src/language/term/Pat.re

@@ -302,3 +302,11 @@ let bound_var_ids = (ctx, pat): list(Binding.t) =>
          }
        }
      );
+
+let get_duplicate_bindings = (pat: t) => {
+  let bindings = bound_vars(pat);
+  List.filter(
+    binding => {List.length(List.filter(x => x == binding, bindings)) > 1},
+    bindings,
+  );
+};

src/web/app/inspector/CursorInspector.re

@@ -164,6 +164,7 @@ let common_err_view =
           ? []
           : [text("Invalid labels: "), ...List.map(code, invalid_labels)]
       )
+    | DuplicateVar(name, _) => [text("Duplicate Variable:"), code(name)]
     | DuplicateLabel(name, _) => [
         text("Duplicate Label:"),
         label_view(name),

test/statics/Test_Statics_Sums.re

@@ -334,6 +334,64 @@ end
     let _ : +Yo = Yo("lol") in ?
     |} |> parse_exp,
     ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns",
+      // #err: type incons#
+      {|
+    case (1,2,3) | (x, y, x) => 0 end
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns with nested tuples",
+      // #err: type incons#
+      {|
+    case (1,(2,3),4) | (x, (x,y), z) => 0 end
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns with labels",
+      // #err: type incons#
+      {|
+    case (1,(2,3),4) | (x=1, (x,y), z) => 0 end
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns with let expressions",
+      // #err: type incons#
+      {|
+    let (x,x) = 1,2 in ?
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns in functions",
+      // #err: type incons#
+      {|
+    fun x,x -> = 1 in ?
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns in labeled tuples",
+      // #err: type incons#
+      {|
+    let (x=a, x=(b, c)) = ? in
+    |} |> parse_exp,
+    ),
+    inconsistent_typecheck(
+      "duplicate variables in patterns in labeled tuples #2",
+      // #err: type incons#
+      {|
+    let (x, x=(x, y)) = ? in
+    |} |> parse_exp,
+    ),
+    fully_consistent_typecheck(
+      "duplicate variable tests: happy",
+      {|
+      let (x=(x, y)) = ? in
+      let (x, x=?) = ? in
+      let (x, x=(z, y=(x=a))) = ? in
+    |},
+      Some(unknown(Internal)),
+    ),
     Alcotest.test_case(
       "Sum type duplicate constructor",
       `Quick,