From 9f4a238a4a313978b795810a3e45b3698a736c61 Mon Sep 17 00:00:00 2001
From: adelaett <90894311+adelaett@users.noreply.github.com>
Date: Thu, 7 Dec 2023 13:44:50 +0100
Subject: [PATCH] Fix error messages for unexpected types. do not retype the
 terms in the cases where checking invariant is not mandatory.

---
 compiler/dcalc/invariants.ml | 17 ++++++-----------
 compiler/driver.ml           |  7 ++++---
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml
index d02b5fea..2314afa7 100644
--- a/compiler/dcalc/invariants.ml
+++ b/compiler/dcalc/invariants.ml
@@ -162,18 +162,13 @@ let rec check_typ_no_default ctx ty =
   | TArray ty -> check_typ_no_default ctx ty
   | TDefault _t -> false
   | TAny ->
-    (* found TAny *)
-    Message.emit_warning
-      "Internal error: the type was not fully resolved, it is not possible to \
-       verify whenever the typing_default invariant holds.";
-    true
+    Message.raise_internal_error
+      "Some Dcalc invariants are invalid: TAny was found wheras it the term \
+       was supposed to be well typed."
   | TClosureEnv ->
-    Message.emit_warning
-      "Internal error: In the compilation process, the default invariant for \
-       typing was not checked early enough. Since it's impossible to verify \
-       this invariant at any point due to the closure environment holding an \
-       existential type.";
-    true (* we should not check this one. *)
+    Message.raise_internal_error
+      "Some Dcalc invariants are invalid: TClosureEnv was found wheras it \
+       should only appear later in the compilation process."
 
 let check_type_thunked_or_nodefault ctx ty =
   check_typ_no_default ctx ty
diff --git a/compiler/driver.ml b/compiler/driver.ml
index df6b3e75..51a1fc73 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -542,11 +542,12 @@ module Commands = struct
        check full name-resolution and cycle detection. These are checked during
        translation to dcalc so we run it here and drop the result. *)
     let prg = Dcalc.From_scopelang.translate_program prg in
-    let prg =
-      Shared_ast.Typing.program ~leave_unresolved:false (Program.untype prg)
-    in
+
     (* Additionally, we might want to check the invariants. *)
     if check_invariants then (
+      let prg =
+        Shared_ast.Typing.program ~leave_unresolved:false (Program.untype prg)
+      in
       Message.emit_debug "Checking invariants...";
       let result = Dcalc.Invariants.check_all_invariants prg in
       if not result then