Type formers (#2413)

Author: MaxCarroll0

src/language/statics/ConstructorStaticsHelpers.re

@@ -323,31 +323,3 @@ let ctr_uses =
     }
   )
   |> CoCtx.union;
-
-// A constructor pattern's payload, as a component of the type it matches.
-let payload_former = (ctr: Constructor.t): MatchedTyp.former => {
-  match_: (ctx, ty) =>
-    Typ.get_sum_constructors(ctx, ty)
-    |> Option.map(
-         List.find_map(
-           fun
-           | ConstructorMap.Variant(name, _, payload)
-               when Constructor.equal(name, ctr) =>
-             Some([payload |> Option.value(~default=Typ.gap)])
-           | _ => None,
-         ),
-       )
-    |> Option.join,
-  build:
-    fun
-    | [payload] =>
-      Sum([
-        ConstructorMap.Variant(
-          ctr,
-          ConstructorMap.empty_variant_ann,
-          Some(payload),
-        ),
-      ])
-      |> Typ.temp
-    | _ => Typ.gap,
-};

src/language/statics/CustomStatics.re

@@ -197,7 +197,7 @@ let invalid_args_fallback =
     let (arg_info, arg_elab, m) = uexp_to_info_map(~ctx, ~ana=syn, arg, m);
     add(
       ~elab_term=mk_builtin_ap_elab(fn_info, arg_elab),
-      ~elab_syn_ty=unknown,
+      ~formation=MatchedTyp.identity(unknown),
       ~marks=[error],
       ~co_ctx=CoCtx.union([fn_info.co_ctx, arg_info.co_ctx]),
       m,
@@ -260,7 +260,7 @@ let handle_tuple_operation =
       let result_type = compute_result_type(labeled_tup_info, labels);
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg_elab),
-        ~elab_syn_ty=result_type,
+        ~formation=MatchedTyp.identity(result_type),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, tup_info.co_ctx]),
         m,
@@ -479,7 +479,7 @@ let group_by_label_statics =
 
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg_elab),
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, table_info.co_ctx]),
         m,
@@ -528,14 +528,17 @@ let to_lvs_statics =
 
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-        ~elab_syn_ty=
-          IdTagged.FreshGrammar.Typ.(
-            list(
-              prod([
-                tup_label(label("label"), string()),
-                tup_label(label("value"), joined_typ),
-              ]),
-            )
+        ~formation=
+          MatchedTyp.form(
+            MatchedTyp.list_former,
+            [
+              IdTagged.FreshGrammar.Typ.(
+                prod([
+                  tup_label(label("label"), string()),
+                  tup_label(label("value"), joined_typ),
+                ])
+              ),
+            ],
           ),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
@@ -544,7 +547,7 @@ let to_lvs_statics =
     | _ =>
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-        ~elab_syn_ty=ty_out,
+        ~formation=MatchedTyp.identity(ty_out),
         ~marks=[BuiltinError(ToLvsMissingLabelsOnTuple(ty_out))],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
         m,
@@ -553,15 +556,15 @@ let to_lvs_statics =
   | Unknown(_) =>
     add(
       ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-      ~elab_syn_ty=ty_out,
+      ~formation=MatchedTyp.identity(ty_out),
       ~marks=[],
       ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
       m,
     )
   | _ =>
     add(
       ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-      ~elab_syn_ty=ty_out,
+      ~formation=MatchedTyp.identity(ty_out),
       ~marks=[BuiltinError(ToLvsMissingLabelsOnTuple(ty_out))],
       ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
       m,
@@ -597,23 +600,27 @@ let omit_all_labels_statics =
 
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-        ~elab_syn_ty=Typ.to_product(entries),
+        ~formation=
+          MatchedTyp.form(
+            MatchedTyp.prod_former(List.length(entries)),
+            entries,
+          ),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
         m,
       );
     | Unknown(_) =>
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-        ~elab_syn_ty=ty_out,
+        ~formation=MatchedTyp.identity(ty_out),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
         m,
       )
     | _ =>
       add(
         ~elab_term=mk_builtin_ap_elab(fn_info, arg.elab_term),
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[BuiltinError(ArgumentMustBeTuple)],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg.co_ctx]),
         m,
@@ -662,7 +669,8 @@ let custom_statics_deferred_ap =
       let (_, m) = validate_label_arguments((module S), ~ctx, labels, m);
 
       add(
-        ~elab_syn_ty=Arrow(unknown, unknown) |> Typ.temp,
+        ~formation=
+          MatchedTyp.form(MatchedTyp.arrow_former, [unknown, unknown]),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, tup_info.co_ctx]),
         m,
@@ -674,7 +682,7 @@ let custom_statics_deferred_ap =
         validate_label_arguments((module S), ~ctx, [pivot_label], m);
 
       add(
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, table_info.co_ctx]),
         m,
@@ -684,7 +692,7 @@ let custom_statics_deferred_ap =
       let (arg_info, _, m) = uexp_to_info_map(~ctx, ~ana=syn, arg, m);
 
       add(
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[],
         ~co_ctx=CoCtx.union([fn_info.co_ctx, arg_info.co_ctx]),
         m,
@@ -702,7 +710,7 @@ let custom_statics_deferred_ap =
         );
 
       add(
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[BuiltinError(AtLeast2Arguments)],
         ~co_ctx=combined_co_ctx,
         m,
@@ -720,7 +728,7 @@ let custom_statics_deferred_ap =
         );
 
       add(
-        ~elab_syn_ty=unknown,
+        ~formation=MatchedTyp.identity(unknown),
         ~marks=[BuiltinError(Exactly2Arguments)],
         ~co_ctx=combined_co_ctx,
         m,
@@ -742,7 +750,8 @@ let custom_statics_deferred_ap =
         |> Typ.to_product;
 
       add(
-        ~elab_syn_ty=Arrow(ty_in', unknown) |> Typ.temp,
+        ~formation=
+          MatchedTyp.form(MatchedTyp.arrow_former, [ty_in', unknown]),
         ~marks=[],
         ~co_ctx=combined_co_ctx,
         m,