diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re
index 6f9f944255..3a5b54ec5b 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -25,16 +25,16 @@ let right_associative = (level: t) => {
 let max: t = 0;
 
 // ========== TYPES ==========
-let type_sum_ap = 22;
+let type_sum_ap = 11;
 // _____ (Int)
 // + T1 + _____
-let type_plus = 25;
+let type_plus = 12 |> right_associative;
 // _____ -> Int
-let type_arrow = 28 |> right_associative;
+let type_arrow = 13 |> right_associative;
 // Int -> _____
 // String , _____ , String
-let type_prod = 45;
-let type_binder = 38;
+let type_prod = 14;
+let type_binder = 15;
 // forall t -> _____
 // rec t -> _____
 
diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re
index b1ec3b1df0..e4ad513fa6 100644
--- a/src/haz3lcore/tiles/Segment.re
+++ b/src/haz3lcore/tiles/Segment.re
@@ -128,11 +128,15 @@ and remold_typ = (shape, seg: t): t =>
     | Tile(t) =>
       switch (remold_tile(Typ, shape, t)) {
       | None => [Tile(t), ...remold_typ(snd(Tile.shapes(t)), tl)]
+      | Some(t) when !Tile.has_end(Right, t) =>
+        let (_, r) = Tile.nibs(t);
+        let remolded = remold(~shape=r.shape, tl, r.sort);
+        [Tile(t), ...remolded];
       | Some(t) => [Tile(t), ...remold_typ(snd(Tile.shapes(t)), tl)]
       }
     }
   }
-and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
+and remold_typ_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
   switch (seg) {
   | [] => ([], shape, [])
   | [hd, ...tl] =>
@@ -140,7 +144,7 @@ and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
     | Secondary(_)
     | Grout(_)
     | Projector(_) =>
-      let (remolded, shape, rest) = remold_typ_uni(shape, tl);
+      let (remolded, shape, rest) = remold_typ_uni(shape, tl, parent_sorts);
       ([hd, ...remolded], shape, rest);
     | Tile(t) =>
       switch (remold_tile(Typ, shape, t)) {
@@ -150,19 +154,23 @@ and remold_typ_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
         let remolded = remold(~shape=r.shape, tl, r.sort);
         let (_, shape, _) = shape_affix(Left, remolded, r.shape);
         ([Tile(t), ...remolded], shape, []);
-      | Some(t) when t.label == Form.get("comma_typ").label => (
+      | Some(t)
+          when
+            t.label == Form.get("comma_typ").label
+            || t.label == Form.get("typ_plus").label
+            && List.exists((==)(Sort.Exp), parent_sorts) => (
           [],
           shape,
           seg,
         )
       | Some(t) =>
         let (remolded, shape, rest) =
-          remold_typ_uni(snd(Tile.shapes(t)), tl);
+          remold_typ_uni(snd(Tile.shapes(t)), tl, parent_sorts);
         ([Tile(t), ...remolded], shape, rest);
       }
     }
   }
-and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
+and remold_pat_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
   switch (seg) {
   | [] => ([], shape, [])
   | [hd, ...tl] =>
@@ -170,7 +178,7 @@ and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
     | Secondary(_)
     | Grout(_)
     | Projector(_) =>
-      let (remolded, shape, rest) = remold_pat_uni(shape, tl);
+      let (remolded, shape, rest) = remold_pat_uni(shape, tl, parent_sorts);
       ([hd, ...remolded], shape, rest);
     | Tile(t) =>
       switch (remold_tile(Pat, shape, t)) {
@@ -183,12 +191,14 @@ and remold_pat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: Typ}) =>
-          let (remolded_typ, shape, rest) = remold_typ_uni(shape, tl);
-          let (remolded_pat, shape, rest) = remold_pat_uni(shape, rest);
+          let (remolded_typ, shape, rest) =
+            remold_typ_uni(shape, tl, [Sort.Pat, ...parent_sorts]);
+          let (remolded_pat, shape, rest) =
+            remold_pat_uni(shape, rest, parent_sorts);
           ([Piece.Tile(t), ...remolded_typ] @ remolded_pat, shape, rest);
         | _ =>
           let (remolded, shape, rest) =
-            remold_pat_uni(snd(Tile.shapes(t)), tl);
+            remold_pat_uni(snd(Tile.shapes(t)), tl, parent_sorts);
           ([Tile(t), ...remolded], shape, rest);
         }
       }
@@ -205,17 +215,22 @@ and remold_pat = (shape, seg: t): t =>
     | Tile(t) =>
       switch (remold_tile(Pat, shape, t)) {
       | None => [Tile(t), ...remold_pat(snd(Tile.shapes(t)), tl)]
+      | Some(t) when !Tile.has_end(Right, t) =>
+        let (_, r) = Tile.nibs(t);
+        let remolded = remold(~shape=r.shape, tl, r.sort);
+        [Tile(t), ...remolded];
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: Typ}) =>
-          let (remolded, shape, rest) = remold_typ_uni(shape, tl);
+          let (remolded, shape, rest) =
+            remold_typ_uni(shape, tl, [Sort.Pat]);
           [Piece.Tile(t), ...remolded] @ remold_pat(shape, rest);
         | _ => [Tile(t), ...remold_pat(snd(Tile.shapes(t)), tl)]
         }
       }
     }
   }
-and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
+and remold_tpat_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
   switch (seg) {
   | [] => ([], shape, [])
   | [hd, ...tl] =>
@@ -223,7 +238,7 @@ and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
     | Secondary(_)
     | Grout(_)
     | Projector(_) =>
-      let (remolded, shape, rest) = remold_tpat_uni(shape, tl);
+      let (remolded, shape, rest) = remold_tpat_uni(shape, tl, parent_sorts);
       ([hd, ...remolded], shape, rest);
     | Tile(t) =>
       switch (remold_tile(TPat, shape, t)) {
@@ -237,7 +252,7 @@ and remold_tpat_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
         switch (Tile.nibs(t)) {
         | _ =>
           let (remolded, shape, rest) =
-            remold_tpat_uni(snd(Tile.shapes(t)), tl);
+            remold_tpat_uni(snd(Tile.shapes(t)), tl, parent_sorts);
           ([Tile(t), ...remolded], shape, rest);
         }
       }
@@ -254,17 +269,22 @@ and remold_tpat = (shape, seg: t): t =>
     | Tile(t) =>
       switch (remold_tile(TPat, shape, t)) {
       | None => [Tile(t), ...remold_tpat(snd(Tile.shapes(t)), tl)]
+      | Some(t) when !Tile.has_end(Right, t) =>
+        let (_, r) = Tile.nibs(t);
+        let remolded = remold(~shape=r.shape, tl, r.sort);
+        [Tile(t), ...remolded];
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: Typ}) =>
-          let (remolded, shape, rest) = remold_typ_uni(shape, tl);
+          let (remolded, shape, rest) =
+            remold_typ_uni(shape, tl, [Sort.TPat]);
           [Piece.Tile(t), ...remolded] @ remold_tpat(shape, rest);
         | _ => [Tile(t), ...remold_tpat(snd(Tile.shapes(t)), tl)]
         }
       }
     }
   }
-and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
+and remold_exp_uni = (shape, seg: t, parent_sorts): (t, Nib.Shape.t, t) =>
   switch (seg) {
   | [] => ([], shape, [])
   | [hd, ...tl] =>
@@ -272,7 +292,7 @@ and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
     | Secondary(_)
     | Grout(_)
     | Projector(_) =>
-      let (remolded, shape, rest) = remold_exp_uni(shape, tl);
+      let (remolded, shape, rest) = remold_exp_uni(shape, tl, parent_sorts);
       ([hd, ...remolded], shape, rest);
     | Tile(t) =>
       switch (remold_tile(Exp, shape, t)) {
@@ -285,23 +305,29 @@ and remold_exp_uni = (shape, seg: t): (t, Nib.Shape.t, t) =>
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: TPat}) =>
-          let (remolded_tpat, shape, rest) = remold_tpat_uni(shape, tl);
-          let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
+          let (remolded_tpat, shape, rest) =
+            remold_tpat_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
+          let (remolded_exp, shape, rest) =
+            remold_exp_uni(shape, rest, parent_sorts);
           ([Piece.Tile(t), ...remolded_tpat] @ remolded_exp, shape, rest);
         | (_, {shape, sort: Pat}) =>
-          let (remolded_pat, shape, rest) = remold_pat_uni(shape, tl);
-          let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
+          let (remolded_pat, shape, rest) =
+            remold_pat_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
+          let (remolded_exp, shape, rest) =
+            remold_exp_uni(shape, rest, parent_sorts);
           ([Piece.Tile(t), ...remolded_pat] @ remolded_exp, shape, rest);
         | (_, {shape, sort: Typ}) =>
-          let (remolded_typ, shape, rest) = remold_typ_uni(shape, tl);
-          let (remolded_exp, shape, rest) = remold_exp_uni(shape, rest);
+          let (remolded_typ, shape, rest) =
+            remold_typ_uni(shape, tl, [Sort.Exp, ...parent_sorts]);
+          let (remolded_exp, shape, rest) =
+            remold_exp_uni(shape, rest, parent_sorts);
           ([Piece.Tile(t), ...remolded_typ] @ remolded_exp, shape, rest);
         | (_, {shape, sort: Rul}) =>
           // TODO review short circuit
           ([Tile(t)], shape, tl)
         | _ =>
           let (remolded, shape, rest) =
-            remold_exp_uni(snd(Tile.shapes(t)), tl);
+            remold_exp_uni(snd(Tile.shapes(t)), tl, parent_sorts);
           ([Tile(t), ...remolded], shape, rest);
         }
       }
@@ -317,19 +343,27 @@ and remold_rul = (shape, seg: t): t =>
     | Projector(_) => [hd, ...remold_rul(shape, tl)]
     | Tile(t) =>
       switch (remold_tile(Rul, shape, t)) {
+      | Some(t) when !Tile.has_end(Right, t) =>
+        let (_, r) = Tile.nibs(t);
+        let remolded = remold(~shape=r.shape, tl, r.sort);
+        [Tile(t), ...remolded];
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: Exp}) =>
-          let (remolded, shape, rest) = remold_exp_uni(shape, tl);
+          let (remolded, shape, rest) =
+            remold_exp_uni(shape, tl, [Sort.Rul]);
           [Piece.Tile(t), ...remolded] @ remold_rul(shape, rest);
         | (_, {shape, sort: Pat}) =>
-          let (remolded, shape, rest) = remold_pat_uni(shape, tl);
+          let (remolded, shape, rest) =
+            remold_pat_uni(shape, tl, [Sort.Rul]);
           // TODO(d) continuing onto rule might not be right right...
           [Piece.Tile(t), ...remolded] @ remold_rul(shape, rest);
         | _ => failwith("remold_rul unexpected")
         }
       | None =>
-        let (remolded, shape, rest) = remold_exp_uni(shape, [hd, ...tl]);
+        // TODO: not sure whether we should add Rul to parent_sorts here
+        let (remolded, shape, rest) =
+          remold_exp_uni(shape, [hd, ...tl], []);
         switch (remolded) {
         | [] => [Piece.Tile(t), ...remold_rul(shape, tl)]
         | [_, ..._] => remolded @ remold_rul(shape, rest)
@@ -348,16 +382,20 @@ and remold_exp = (shape, seg: t): t =>
     | Tile(t) =>
       switch (remold_tile(Exp, shape, t)) {
       | None => [Tile(t), ...remold_exp(snd(Tile.shapes(t)), tl)]
+      | Some(t) when !Tile.has_end(Right, t) =>
+        let (_, r) = Tile.nibs(t);
+        let remolded = remold(~shape=r.shape, tl, r.sort);
+        [Tile(t), ...remolded];
       | Some(t) =>
         switch (Tile.nibs(t)) {
         | (_, {shape, sort: Pat}) =>
-          let (remolded, shape, rest) = remold_pat_uni(shape, tl);
+          let (remolded, shape, rest) = remold_pat_uni(shape, tl, [Exp]);
           [Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
         | (_, {shape, sort: TPat}) =>
-          let (remolded, shape, rest) = remold_tpat_uni(shape, tl);
+          let (remolded, shape, rest) = remold_tpat_uni(shape, tl, [Exp]);
           [Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
         | (_, {shape, sort: Typ}) =>
-          let (remolded, shape, rest) = remold_typ_uni(shape, tl);
+          let (remolded, shape, rest) = remold_typ_uni(shape, tl, [Exp]);
           [Piece.Tile(t), ...remolded] @ remold_exp(shape, rest);
         | (_, {shape, sort: Rul}) => [Tile(t), ...remold_rul(shape, tl)]
         | _ => [Tile(t), ...remold_exp(snd(Tile.shapes(t)), tl)]