Merge branch 'dev' into fix-2099

Author: disconcision

src/language/dynamics/transition/Ascriptions.re

@@ -27,17 +27,10 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
   switch (DHExp.term_of(d)) {
   | Asc(e, t) =>
     switch (DHExp.term_of(e), Typ.term_of(Typ.unroll(t))) {
-    | (Asc(e, t'), t)
+    | (Asc(e, t'), _)
         // This is only necessary because sometimes we add two ascriptions and aren't marking it as a non-value
-        when
-          Typ.is_consistent(
-            Ctx.empty,
-            Typ.unroll(t |> Typ.temp),
-            Typ.unroll(t'),
-          ) =>
-      switch (
-        Typ.meet(Ctx.empty, Typ.unroll(t |> Typ.temp), Typ.unroll(t'))
-      ) {
+        when Typ.is_consistent(Ctx.empty, Typ.unroll(t), Typ.unroll(t')) =>
+      switch (Typ.meet(Ctx.empty, Typ.unroll(t), Typ.unroll(t'))) {
       | Some(t) => Some(recur(Asc(e, t) |> DHExp.fresh))
       | None => None //TODO  This is an impossible case since we checked consistency
       }
@@ -133,26 +126,26 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
           |> DHExp.fresh,
         ),
       );
-    | (If(cond, e1, e2), t) =>
+    | (If(cond, e1, e2), _) =>
       Some(
         IdTagged.fast_copy(
           DHExp.rep_id(e),
           If(
             recur(cond),
-            recur(Asc(e1, t |> Typ.temp) |> DHExp.fresh),
-            recur(Asc(e2, t |> Typ.temp) |> DHExp.fresh),
+            recur(Asc(e1, t) |> DHExp.fresh),
+            recur(Asc(e2, t) |> DHExp.fresh),
           )
           |> DHExp.fresh,
         ),
       )
-    | (Match(scrut, rules), t) =>
+    | (Match(scrut, rules), _) =>
       Some(
         IdTagged.fast_copy(
           DHExp.rep_id(e),
           Match(
             scrut,
             List.map(
-              ((p, body)) => (p, Asc(body, t |> Typ.temp) |> DHExp.fresh),
+              ((p, body)) => (p, Asc(body, t) |> DHExp.fresh),
               rules,
             ),
           )

test/evaluator/Test_Evaluator_Sum_Types.re

@@ -28,25 +28,47 @@ let tests = (
       )
     }),
     test_case(
-      "Constructors can pass through consistent ascriptions", `Quick, () => {
-      evaluation_test(
-        {|A : (+A +B) : (+A + ?)|},
-        constructor(
-          "A",
-          Some(
+      "Constructors can pass through consistent ascriptions",
+      `Quick,
+      () => {
+        evaluation_test(
+          {|A : (+A +B) : (+A + ?)|},
+          constructor(
+            "A",
             Some(
-              Typ.(
-                sum([
-                  Variant("A", ConstructorMap.empty_variant_ann, None),
-                  Variant("B", ConstructorMap.empty_variant_ann, None),
-                ])
+              Some(
+                Typ.(
+                  sum([
+                    Variant("A", ConstructorMap.empty_variant_ann, None),
+                    Variant("B", ConstructorMap.empty_variant_ann, None),
+                  ])
+                ),
               ),
             ),
           ),
-        ),
-        elaborate(parse_exp({|A : (+A +B) : (+A + ?)|})),
-      )
-    }),
+          elaborate(parse_exp({|A : (+A +B) : (+A + ?)|})),
+        );
+        evaluation_test(
+          "Ascriptions don't do unnecessary unrolling",
+          asc(
+            empty_hole(),
+            Typ.rec_(
+              TPat.var("X"),
+              Typ.sum([
+                Variant(
+                  "A",
+                  ConstructorMap.empty_variant_ann,
+                  Some(Typ.var("X")),
+                ),
+              ]),
+            ),
+          ),
+          elaborate(
+            parse_exp("(if true then ? else ?) : (rec X -> + A(X))"),
+          ),
+        );
+      },
+    ),
     test_case(
       "Constructors don't pass through inconsistent ascriptions", `Quick, () => {
       evaluation_test(