make ModuleTypechecker use Typechecker.typecheck_nonrec

src/frontend/errorReporting.ml

@@ -595,10 +595,11 @@ let make_type_error_message = function
         NormalLine("tests must be stage-1 non-recursive bindings.");
       ]
 
-  | NonemptyManualQuantifier(rng) ->
+  | TestMustBeUnitToUnit(rng, pty) ->
       [
         NormalLine(Printf.sprintf "at %s:" (Range.to_string rng));
-        NormalLine("no type/row variable should be bound here.");
+        NormalLine("tests must be of type unit -> unit, but this one has type");
+        DisplayLine(Display.show_poly_type pty);
       ]
 
 

src/frontend/moduleTypechecker.ml

@@ -692,30 +692,6 @@ and typecheck_binding_list (config : typecheck_config) (tyenv : Typeenv.t) (utbi
   return ((quant, ssig), binds)
 
 
-and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (ident : var_name ranged) (utast1 : untyped_abstract_tree) (ty_expected_opt : mono_type option) =
-  let open ResultMonad in
-  let presub = { pre with level = Level.succ pre.level; } in
-  let evid = EvalVarID.fresh ident in
-  let* (e1_raw, ty1) = Typechecker.typecheck presub tyenv utast1 in
-  let e1 = e1_raw in
-  let* () =
-    match ty_expected_opt with
-    | None              -> return ()
-    | Some(ty_expected) -> unify ty1 ty_expected
-  in
-(*
-  let should_be_polymorphic = is_nonexpansive_expression e1 in
-*)
-  let should_be_polymorphic = true in
-    let pty =
-      if should_be_polymorphic then
-        TypeConv.generalize pre.level (TypeConv.erase_range_of_type ty1)
-      else
-        TypeConv.lift_poly (TypeConv.erase_range_of_type ty1)
-    in
-  return (evid, e1, pty)
-
-
 and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind : untyped_binding) : (binding list * StructSig.t abstracted) ok =
   let open ResultMonad in
   let (rng, utbindmain) = utbind in
@@ -738,56 +714,28 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
       if valattr.ValueAttribute.is_test then
         match (stage, valbind) with
         | (Stage1, UTNonRec(utletbind)) ->
-            let
-              UTLetBinding{
-                identifier  = ident;
-                quantifier  = mnquant;
-                parameters  = param_units;
-                return_type = mntyopt_ret;
-                body        = utast_body;
-              } = utletbind
-            in
-            let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
-            let* () = check_empty_manual_quantifier rng mnquant in
-            let (_, test_name) = ident in
-            let ty_expected =
+            let pty_expected =
               let ty_dom = (Range.dummy "test-dom", BaseType(UnitType)) in
               let ty_cod = (Range.dummy "test-cod", BaseType(UnitType)) in
-              (Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod))
+              Poly(Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod))
             in
-            let* (evid, e1, _pty) = typecheck_nonrec pre tyenv ident utast1 (Some(ty_expected)) in
-            return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty))
+            let* (test_name, pty1, evid, e1) = Typechecker.typecheck_nonrec pre tyenv utletbind in
+            if TypeConv.poly_type_equal pty_expected pty1 then
+              return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty))
+            else
+              err @@ TestMustBeUnitToUnit(rng, pty1)
 
         | _ ->
             err @@ TestMustBeStage1NonRec(rng)
       else
         let* (rec_or_nonrecs, ssig) =
           match valbind with
           | UTNonRec(utletbind) ->
-              let
-                UTLetBinding{
-                  identifier  = ident;
-                  quantifier  = ManualQuantifier(typarams, rowparams);
-                  parameters  = param_units;
-                  return_type = _mntyopt_ret;
-                  body        = utast_body;
-                } = utletbind
-              in
-              let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
-              let* (typarammap, _) = pre.type_parameters |> add_type_parameters (Level.succ Level.bottom) typarams in
-              let* (rowparammap, _) = pre.row_parameters |> add_row_parameters (Level.succ Level.bottom) rowparams in
-              let pre =
-                { pre with
-                  type_parameters = typarammap;
-                  row_parameters  = rowparammap;
-                }
-              in
-              let* (evid, e1, pty) = typecheck_nonrec pre tyenv ident utast1 None in
+              let* (varnm, pty1, evid, e1) = Typechecker.typecheck_nonrec pre tyenv utletbind in
               let ssig =
-                let (_, varnm) = ident in
                 let ventry =
                   {
-                    val_type  = pty;
+                    val_type  = pty1;
                     val_name  = Some(evid);
                     val_stage = pre.stage;
                   }

src/frontend/typeError.ml

@@ -69,4 +69,4 @@ type type_error =
   | ValueAttributeError                  of ValueAttribute.error
   | ModuleAttributeError                 of ModuleAttribute.error
   | TestMustBeStage1NonRec               of Range.t
-  | NonemptyManualQuantifier             of Range.t
+  | TestMustBeUnitToUnit                 of Range.t * poly_type

src/frontend/typecheckUtil.ml

@@ -124,13 +124,3 @@ let add_row_parameters (lev : Level.t) (rowvars : (row_variable_name ranged * ma
     ) (rowparammap, Alist.empty)
   in
   return (rowparammap, Alist.to_list bridacc)
-
-
-let check_empty_manual_quantifier (rng : Range.t) (mnquant : manual_quantifier) : unit ok =
-  let open ResultMonad in
-  match mnquant with
-  | ManualQuantifier([], []) ->
-      return ()
-
-  | _ ->
-      err @@ NonemptyManualQuantifier(rng)

src/frontend/typechecker.ml

@@ -648,7 +648,7 @@ let rec typecheck (pre : pre) (tyenv : Typeenv.t) ((rng, utastmain) : untyped_ab
       return (PatternMatch(rng, eO, patbrs), beta)
 
   | UTLetIn(UTNonRec(utletbind), utast2) ->
-      let* (varnm, evid, e1, pty1) = typecheck_nonrec pre tyenv utletbind in
+      let* (varnm, pty1, evid, e1) = typecheck_nonrec pre tyenv utletbind in
       let tyenv =
         let ventry =
           {
@@ -1226,7 +1226,7 @@ and typecheck_letrec (pre : pre) (tyenv : Typeenv.t) (utrecbinds : untyped_let_b
   return tuples
 
 
-and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_binding) : (var_name * EvalVarID.t * abstract_tree * poly_type) ok =
+and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_binding) : (var_name * poly_type * EvalVarID.t * abstract_tree) ok =
   let open ResultMonad in
   let
     UTLetBinding{
@@ -1258,7 +1258,7 @@ and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_bi
     (* If `e1` should be typed monomorphically: *)
       TypeConv.lift_poly (TypeConv.erase_range_of_type ty1)
   in
-  return (varnm, evid, e1, pty1)
+  return (varnm, pty1, evid, e1)
 
 
 and typecheck_let_mutable (pre : pre) (tyenv : Typeenv.t) (ident : var_name ranged) (utastI : untyped_abstract_tree) : (Typeenv.t * EvalVarID.t * abstract_tree * mono_type) ok =

src/frontend/typechecker.mli

@@ -7,6 +7,8 @@ val typecheck : pre -> type_environment -> untyped_abstract_tree -> (abstract_tr
 
 val typecheck_letrec : pre -> type_environment -> untyped_let_binding list -> ((var_name * poly_type * EvalVarID.t * letrec_binding) list, type_error) result
 
+val typecheck_nonrec : pre -> type_environment -> untyped_let_binding -> (var_name * poly_type * EvalVarID.t * abstract_tree, type_error) result
+
 val main : typecheck_config -> stage -> Typeenv.t -> untyped_abstract_tree -> (mono_type * abstract_tree, type_error) result
 
 val are_unifiable : mono_type -> mono_type -> bool