[FTypeChecker] More informative error message (and more robust code) when typechecking variants.

client/Datatype.ml

@@ -46,6 +46,8 @@ module Env = struct
     }
 
   exception UnexpectedRecord
+  exception DeclarationNotFound of tyconstr_id
+  exception LabelNotFound of label_id
 
   let empty = {
       datatypes = TyConstrMap.empty;
@@ -64,19 +66,17 @@ module Env = struct
       labels = add_labels e.labels tdescr.labels_descr;
     }
 
-  let find_label { labels ; _ } (Label l) =
-    LabelMap.find (Label l) labels
-
-  let find_decl { datatypes ; _ } (Type tid) =
-    TyConstrMap.find (Type tid) datatypes
-
-  let label_index { labels_descr ; _ } l =
-    let combine i ldescr = (i, ldescr.label_name) in
-    List.mapi combine labels_descr
-    |> List.find (fun (_, l') -> l = l')
-    |> fst
-
-  let () = ignore label_index
+  let find_label { labels ; _ } label =
+    try
+      LabelMap.find label labels
+    with Not_found ->
+       raise (LabelNotFound label)
+
+  let find_decl { datatypes ; _ } tid =
+    try
+      TyConstrMap.find tid datatypes
+    with Not_found ->
+       raise (DeclarationNotFound tid)
 
   let map (type b1 b2 t1 t2)
     (f : (b1, t1) decl -> (b2, t2) decl)

client/Datatype.mli

@@ -34,6 +34,8 @@ module Env : sig
   type ('b, 't) t
 
   exception UnexpectedRecord
+  exception DeclarationNotFound of tyconstr_id
+  exception LabelNotFound of label_id
 
   val empty: ('b, 't) t
   val add_decl: ('b, 't) t -> ('b, 't) decl -> ('b, 't) t

client/FPrinter.ml

@@ -216,5 +216,14 @@ let print_type_error e =
       str "Scope error." ++
       str "The variable %s is bound twice in a pattern." x
   | ContextNotAbsurd ->
-       str "Type error." ++
-       str "The type equations in the typing environment are not contradictory."
+      str "Type error." ++
+      str "The type equations in the typing environment are not contradictory."
+  | UnexpectedRecord ->
+      str "Type error." ++
+      str "A record was expected."
+  | DeclarationNotFound (Datatype.Type tid) ->
+      str "Scope error." ++
+      str "Unknown type declaration : %s." tid
+  | LabelNotFound (Datatype.Label lid) ->
+      str "Scope error." ++
+      str "Unknown variant constructor : %s." lid

client/FTypeChecker.ml

@@ -11,6 +11,10 @@ type type_error =
   | UnboundTypeVariable of tyvar
   | TwoOccurencesOfSameVariable of string
   | ContextNotAbsurd
+  | UnexpectedRecord
+  | DeclarationNotFound of Datatype.tyconstr_id
+  | LabelNotFound of Datatype.label_id
+
 
 and arity_requirement = Index of int | Total of int
 
@@ -439,9 +443,17 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
 
 and typeof_variant datatype_env lbl (tid, tyargs) =
   let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
-    Datatype.Env.find_decl datatype_env tid in
+    try
+      Datatype.Env.find_decl datatype_env tid
+    with Datatype.Env.DeclarationNotFound _ ->
+      raise (TypeError (DeclarationNotFound tid))
+  in
   let Datatype.{ arg_type; _ } =
-    List.find (fun l -> l.Datatype.label_name = lbl) labels_descr in
+    try
+      List.find (fun l -> l.Datatype.label_name = lbl) labels_descr
+    with Datatype.Env.LabelNotFound _ ->
+      raise (TypeError (LabelNotFound lbl))
+  in
   begin
     match data_kind with
     | Datatype.Variant ->
@@ -483,6 +495,7 @@ let typeof datatype_env t =
 
 let typeof_result datatype_env u =
   match typeof datatype_env u with
-  | v -> Ok v
+  | v ->
+      Ok v
   | exception TypeError e ->
-    Error e
+      Error e

client/FTypeChecker.mli

@@ -13,6 +13,9 @@ type type_error =
   | UnboundTypeVariable of tyvar
   | TwoOccurencesOfSameVariable of string
   | ContextNotAbsurd
+  | UnexpectedRecord
+  | DeclarationNotFound of Datatype.tyconstr_id
+  | LabelNotFound of Datatype.label_id
 
 (* An arity-related requirement on a certain (sum or product) type
    arising during type-checking:

client/test/TestF.ml

@@ -124,6 +124,14 @@ let option_env =
   in
   Datatype.Env.add_decl Datatype.Env.empty option_typedecl
 
+(* We test this example in an empty datatype environment. It should raise
+   an error indicating that it did not find the label. *)
+let not_in_env =
+  let alpha = 0 in
+  let label = Datatype.Label "None" in
+  let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+  variant label datatype unit
+
 (* None *)
 let none =
   let alpha = 0 in
@@ -675,6 +683,7 @@ let test_suite =
       test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
       test_type_error "match variable bound twice" Datatype.Env.empty
         match_variable_bound_twice;
+      test_type_error "not in env" Datatype.Env.empty not_in_env;
       test_ok_from_ast "unit" option_env unit;
       test_ok_from_ast "none" option_env none;
       test_ok_from_ast "some" option_env some;