Handle type errors

sigmaid.ml

@@ -31,7 +31,15 @@ let main () =
           (Scoper.string_of_id id);
         exit 1
     in
-    let typed_prog = Typer.type_check scoped_prog in
+    let typed_prog =
+      try Typer.type_check scoped_prog
+      with Typer.Application_of_non_functionnal_value ty ->
+        Format.eprintf
+          "Type error: Application of non functional value.
+expected an arrow type, found %s.@."
+        (Scoper.string_of_sty ty);
+        exit 1
+    in
     Format.fprintf out_fmter "#NAME %s.@\n" (Filename.chop_extension file);
     Printer.declare_labels out_fmter !Base.labels;
     Printer.print out_fmter typed_prog;

typer.ml

@@ -93,24 +93,39 @@ let rec type_check env ty : sterm -> tterm = function
   | Svar (x, ty') -> tcast (Tvar (x, ty')) ty' ty
   | Sconst (x, ty', def) -> tcast (Tconst (x, ty', type_check env ty' def)) ty' ty
   | Spar t -> Tpar (type_check env ty t)
-  | Sapp (t1, t2) ->
+  | Sapp (t1, t2) as t ->
     (* We don't know what type should be associated with t2
        so we infer a type for t1 and decompose it as an arrow *)
     let tt1 = type_term env t1 in
-    let (ty1l, ty1r) = sty_decompose_arrow (infer tt1) in
+    let (ty1l, ty1r) =
+      try
+        sty_decompose_arrow (infer tt1)
+      with Application_of_non_functionnal_value ty' ->
+        Format.eprintf "Type error: error while checking %s against %s,
+inferred type for %s is %s, an arrow type was expected.@."
+          (string_of_sterm t) (string_of_sty ty) (string_of_sterm t1) (string_of_sty ty');
+        exit 1
+    in
     (* Now we check that the application is typable at type ty *)
     tcast (Tapp (tt1, type_check env ty1l t2, ty1l, ty1r)) ty1r ty
-  | Sabst (x, ty', body) ->
-    (* First decompose ty as an arrow *)
-    let (tyl, tyr) = sty_decompose_arrow ty in
-    if eq ty' tyl then
-      Tabst (x, tyl, type_check ((x, tyl) :: env) tyr body, tyr)
-    else
-      (* We use eta-expansion to cast the variable x. *)
-      Tabst (x, tyl, Tapp (Tabst (x, ty', type_check ((x, ty') :: env) tyr body, tyr),
-                           tcast (Tvar (x, tyl)) tyl ty',
-                           ty',
-                           tyr), tyr)
+  | Sabst (x, ty', body) as t ->
+     (* First decompose ty as an arrow *)
+     let (tyl, tyr) =
+       try
+         sty_decompose_arrow ty
+       with Application_of_non_functionnal_value _ ->
+         Format.eprintf "Type error: error while checking %s against %s,
+the type of an abstraction should be an arrow.@."
+          (string_of_sterm t) (string_of_sty ty);
+        exit 1 in
+     if eq ty' tyl then
+       Tabst (x, tyl, type_check ((x, tyl) :: env) tyr body, tyr)
+     else
+       (* We use eta-expansion to cast the variable x. *)
+       Tabst (x, tyl, Tapp (Tabst (x, ty', type_check ((x, ty') :: env) tyr body, tyr),
+                            tcast (Tvar (x, tyl)) tyl ty',
+                            ty',
+                            tyr), tyr)
   | Strue ty' -> (match ty with
     | Stbool ty when eq ty ty' -> Ttrue ty
     | _ -> Format.eprintf "Type error: error while checking true %s against %s,
@@ -191,9 +206,17 @@ and type_term env : sterm -> tterm = function
   | Svar (x, ty) -> Tvar (x, ty)
   | Sconst (x, ty, def) -> Tconst (x, ty, type_check env ty def)
   | Spar t -> Tpar (type_term env t)
-  | Sapp (t1, t2) ->
+  | Sapp (t1, t2) as t ->
     let tt1 = type_term env t1 in
-    let (ty1l, ty1r) = sty_decompose_arrow (infer tt1) in
+    let (ty1l, ty1r) =
+      try
+        sty_decompose_arrow (infer tt1)
+      with Application_of_non_functionnal_value ty ->
+        Format.eprintf "Type error: error while inferring the type of %s,
+inferred type for %s is %s, an arrow type was expected.@."
+          (string_of_sterm t) (string_of_sterm t1) (string_of_sty ty);
+        exit 1
+    in
     Tapp (tt1, type_check env ty1l t2, ty1l, ty1r)
   | Sabst (x, ty, body) ->
     let tbody = type_term ((x, ty) :: env) body in

typer.mli

@@ -28,3 +28,5 @@ type typed_tree = tline list
 
 val infer : tterm -> sty
 val type_check : Scoper.scoped_tree -> typed_tree
+
+exception Application_of_non_functionnal_value of sty