From 9e7de664e7186d3d8e480bdb3c7b4bb2a8293208 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:05:21 +0100
Subject: [PATCH] synth_record : 35/111

---
 flap/src/hopix/hopixTypechecker.ml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index a32f3aa..d09e2b5 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/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