Bugfix: statics now check that the first argument in a TupLabel is a …

…Label

src/haz3lcore/LabeledTuple.re

@@ -13,6 +13,17 @@ let equal: (option((label, 'a)), option((label, 'b))) => bool =
     };
   };
 
+// This function should only be used for type checking labels
+let match_labels: (label, label) => bool =
+  (label1, label2) => {
+    switch (label1, label2) {
+    // Empty label is a placeholder for checking any label
+    | ("", _)
+    | (_, "") => true
+    | (_, _) => label1 == label2
+    };
+  };
+
 let length = String.length;
 
 let compare = String.compare;

src/haz3lcore/dynamics/PatternMatch.re

@@ -32,7 +32,8 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
     s == s' ? Matches(Environment.empty) : DoesNotMatch;
   | Label(name) =>
     let* name' = Unboxing.unbox(Label, d);
-    name == name' ? Matches(Environment.empty) : DoesNotMatch;
+    LabeledTuple.match_labels(name, name')
+      ? Matches(Environment.empty) : DoesNotMatch;
   | TupLabel(_, x) =>
     let* x' = Unboxing.unbox(TupLabel(dp), d);
     matches(x, x');

src/haz3lcore/lang/term/Typ.re

@@ -289,7 +289,10 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
   | (Bool, _) => None
   | (String, String) => Some(ty1)
   | (String, _) => None
-  | (Label(name1), Label(name2)) when String.equal(name1, name2) =>
+  | (Label(_), Label("")) => Some(ty1)
+  | (Label(""), Label(_)) => Some(ty2)
+  | (Label(name1), Label(name2))
+      when LabeledTuple.match_labels(name1, name2) =>
     Some(ty1)
   | (Label(_), _) => None
   | (Arrow(ty1, ty2), Arrow(ty1', ty2')) =>
@@ -457,13 +460,10 @@ let matched_label = (ctx, ty) =>
   | Prod([ty]) =>
     switch (term_of(weak_head_normalize(ctx, ty))) {
     | TupLabel(lab, ty) => (lab, ty)
-    | _ => (Unknown(Internal) |> temp, ty)
+    | _ => (Label("") |> temp, ty) // Empty label is a placeholder for checking any label
     }
-  | Unknown(SynSwitch) => (
-      Unknown(SynSwitch) |> temp,
-      Unknown(SynSwitch) |> temp,
-    )
-  | _ => (Unknown(Internal) |> temp, ty)
+  | Unknown(SynSwitch) => (Label("") |> temp, Unknown(SynSwitch) |> temp)
+  | _ => (Label("") |> temp, ty)
   };
 
 let rec get_labels = (ctx, ty): list(option(string)) => {

src/haz3lcore/statics/Info.re

@@ -534,7 +534,8 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ =>
     switch (expects) {
     | TypeExpected => NotInHole(Type(ty))
     | TupleExpected(_) => InHole(WantTuple)
-    | LabelExpected(_, dupes) =>
+    | LabelExpected(Unique, _) => NotInHole(Type(ty))
+    | LabelExpected(Duplicate, dupes) =>
       List.exists(l => name == l, dupes)
         ? InHole(Duplicate(ty)) : InHole(WantLabel)
     | ConstructorExpected(_)

src/haz3lcore/statics/MakeTerm.re

@@ -327,7 +327,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           | (["="], []) =>
             // TODO (Anthony): Other cases to convert to string
             switch (l.term) {
-            | String(name)
+            // | String(name)
+            // Currently not allowing Strings to prevent empty Labels
             | Var(name) =>
               Tuple([
                 TupLabel(
@@ -422,7 +423,8 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
       | ([(_id, (["="], []))], []) =>
         // TODO (Anthony): Other cases to convert to string
         switch (l.term) {
-        | String(name)
+        // | String(name)
+        // Currently not allowing Strings to prevent empty Labels
         | Var(name) =>
           ret(
             Tuple([

src/haz3lcore/statics/Mode.re

@@ -60,11 +60,12 @@ let of_forall = (ctx: Ctx.t, name_opt: option(string), mode: t): t =>
     };
   };
 
+// Empty label is a placeholder for checking any label
 let of_label = (ctx: Ctx.t, mode: t): (t, t) =>
   switch (mode) {
   | Syn
   | SynFun
-  | SynTypFun => (Syn, Syn)
+  | SynTypFun => (Ana(Label("") |> Typ.temp), Syn)
   | Ana(ty) =>
     let (ty1, ty2) = Typ.matched_label(ctx, ty);
     (ana(ty1), ana(ty2));

src/haz3lcore/statics/Self.re

@@ -30,7 +30,7 @@ type t =
   | Just(Typ.t) /* Just a regular type */
   | NoJoin(join_type, list(Typ.source)) /* Inconsistent types for e.g match, listlits */
   | Duplicate_Labels(t) /* Duplicate labels in a labeled tuple, treated as regular type (?) */
-  | Duplicate(t) /* Duplicatee label, marked as duplicate */
+  | Duplicate(t) /* Duplicate label, marked as duplicate */
   | BadToken(Token.t) /* Invalid expression token, continues with undefined behavior */
   | BadTrivAp(Typ.t) /* Trivial (nullary) ap on function that doesn't take triv */
   | IsMulti /* Multihole, treated as hole */

src/haz3lcore/statics/Statics.re

@@ -1196,12 +1196,12 @@ and utyp_to_info_map =
     let m = go(t2, m) |> snd;
     add(m);
   | TupLabel(label, t) =>
-    let expects =
+    let expects_label =
       switch (expects) {
       | LabelExpected(_) => expects
-      | _ => TypeExpected
+      | _ => LabelExpected(Unique, [])
       };
-    let m = go'(~expects, label, m) |> snd;
+    let m = go'(~expects=expects_label, label, m) |> snd;
     let m = go(t, m) |> snd;
     add'(~expects=TypeExpected, m);
   | Prod(ts) =>

src/haz3lcore/statics/TermBase.re

@@ -752,7 +752,8 @@ and Typ: {
     | (Bool, _) => false
     | (String, String) => true
     | (String, _) => false
-    | (Label(name1), Label(name2)) => String.equal(name1, name2)
+    | (Label(name1), Label(name2)) =>
+      LabeledTuple.match_labels(name1, name2)
     | (Label(_), _) => false
     | (Ap(t1, t2), Ap(t1', t2')) =>
       eq_internal(n, t1, t1') && eq_internal(n, t2, t2')

src/haz3lweb/view/Type.re

@@ -29,7 +29,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
   | Int => ty_view("Int", "Int")
   | Float => ty_view("Float", "Float")
   | String => ty_view("String", "String")
-  | Label(name) => ty_view("Label", name)
+  | Label(_) => ty_view("Label", "Label")
   | Bool => ty_view("Bool", "Bool")
   | Var(name) => ty_view("Var", name)
   | TupLabel({term: Label(l), _}, ty) =>