From a90e8176e6498cb86d6c2e29cc32490874df9761 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:51:59 +0100
Subject: [PATCH] =?UTF-8?q?synth=5Ftagged=20-=20pire=20impl=C3=A9mentation?=
 =?UTF-8?q?=20ever?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d09e2b5..6982529 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -117,7 +117,41 @@ and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located
   -> ty Position.located list option -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv cons tlist e_args_list -> failwith "Students! This is your job! (synth_tagged)"
+  fun tenv cons tlist e_args_list ->
+  let cons_scheme =
+    try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
+    | HopixTypes.Unbound (pos, Constructor (KId c)) ->
+      HopixTypes.type_error pos (Printf.sprintf "Unbound constructor `%s'." c)
+  in
+  let tys =
+    List.map
+      (fun x -> HopixTypes.internalize_ty tenv x)
+      (match tlist with
+       | Some t -> t
+       | None -> HopixTypes.type_error cons.position "No types ??")
+  in
+  let tcons =
+    try HopixTypes.instantiate_type_scheme cons_scheme tys with
+    | HopixTypes.InvalidInstantiation { expected; given } ->
+      invalid_instantiation cons.position expected given
+  in
+  let targs = List.map (fun x -> synth_expression tenv x) e_args_list in
+  let expected_args, result =
+    HopixTypes.destruct_function_type_maximally cons.position tcons
+  in
+  (try
+     List.iter2
+       (fun expected given -> check_equal_types cons.position ~expected ~given)
+       expected_args
+       targs
+   with
+   | Invalid_argument _ ->
+     (* 35-bad *)
+     check_equal_types
+       cons.position
+       ~expected:result
+       ~given:(HopixTypes.ATyArrow (result, result)));
+  result
 
 and synth_apply
   :  HopixTypes.typing_environment -> expression Position.located