Fix error messages for unexpected types.

do not retype the terms in the cases where checking invariant is not mandatory.

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

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