synth_record : 35/111

flap/src/hopix/hopixTypechecker.ml

@@ -139,6 +139,7 @@ and synth_record
   -> ty Position.located list option -> HopixTypes.aty
   =
   fun tenv field tlist ->
+  (* Translate the types *)
   let fl = fst (List.hd field) in
   let cons, _, _ =
     HopixTypes.lookup_type_constructor_of_label fl.position fl.value tenv
@@ -148,7 +149,23 @@ and synth_record
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
     | None -> HopixTypes.type_error fl.position "No types ??"
   in
-  (* TODO: Typecheck *)
+  (* Type checking *)
+  List.iter
+    (fun (Position.{ position = label_pos; value = label_val }, expr) ->
+      let label_scheme =
+        try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
+        | HopixTypes.Unbound (pos, Label (LId i)) ->
+          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+      in
+      let arrow =
+        try HopixTypes.instantiate_type_scheme label_scheme tlist' with
+        | HopixTypes.InvalidInstantiation { expected; given } ->
+          invalid_instantiation (Position.position expr) expected given
+      in
+      let _, expected = HopixTypes.destruct_function_type label_pos arrow in
+      let given = synth_expression tenv expr in
+      check_equal_types label_pos ~expected ~given)
+    field;
   ATyCon (cons, tlist')
 
 and synth_fun