Some work on improving error messages

We now store the location where type variables were bound, so we can
use this information when printing error messages.

Factor type errors out into type_error.ml. This means that
Type_check.check is now Type_error.check, as it previously it handled
wrapping the type_errors into reporting_basic
errors. Type_check.check' has therefore been renamed to
Type_check.check.

12 files changed, 239 insertions, 132 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 6daca6b4..8182e82c 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -3495,7 +3495,7 @@ let sgen_finish = function
 let bytecode_ast ctx rewrites (Defs defs) =
   let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
   let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in
-  let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
+  let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
   let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
   let cdefs = List.concat (List.rev chunks) in
   rewrites cdefs
@@ -3517,7 +3517,7 @@ let compile_ast ctx (Defs defs) =
 
     let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
     let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in
-    let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
+    let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
     let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
     let cdefs = List.concat (List.rev chunks) in
     let cdefs = optimize ctx cdefs in
@@ -3584,4 +3584,4 @@ let compile_ast ctx (Defs defs) =
     Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl ^^ postamble)
     |> print_endline
   with
-    Type_error (l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ string_of_type_error err)
+    Type_error (l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 03fd8496..781e4e41 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -676,4 +676,4 @@ let rec eval_frame' ast = function
 let eval_frame ast frame =
   try eval_frame' ast frame with
   | Type_check.Type_error (l, err) ->
-     raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
+     raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
diff --git a/src/isail.ml b/src/isail.ml
index 0bfb06e2..414fc50d 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -364,7 +364,7 @@ let handle_input' input =
 let handle_input input =
   try handle_input' input with
   | Type_check.Type_error (l, err) ->
-     print_endline (Type_check.string_of_type_error err)
+     print_endline (Type_error.string_of_type_error err)
   | Reporting_basic.Fatal_error err ->
      Reporting_basic.print_error err
   | exn ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 98ef5034..eb88072f 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -735,7 +735,7 @@ let reduce_cast typ exp l annot =
   let typ' = Env.base_typ_of env typ in
   match exp, destruct_exist env typ' with
   | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
-     let nc_env = Env.add_typ_var kid BK_int env in
+     let nc_env = Env.add_typ_var l kid BK_int env in
      let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in
      if prove nc_env nc
      then exp
@@ -4117,7 +4117,7 @@ let rewrite_toplevel_nexps (Defs defs) =
     | TypQ_aux (TypQ_no_forall,_) -> None
     | TypQ_aux (TypQ_tq qs, tq_l) ->
        let env = env_of_annot ann in
-       let env = add_typquant tqs env in
+       let env = add_typquant tq_l tqs env in
        let nexp_map, typ = rewrite_typ_in_spec env [] typ in
        match nexp_map with
        | [] -> None
@@ -4202,7 +4202,7 @@ type options = {
 let recheck defs =
   let w = !Util.opt_warnings in
   let () = Util.opt_warnings := false in
-  let r = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
+  let r = Type_error.check (Type_check.Env.no_casts Type_check.initial_env) defs in
   let () = Util.opt_warnings := w in
   r
 
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 8c5f5b14..5437c2cd 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -371,7 +371,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
   match t with
   | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) ->
      begin
-       let mk_typ nexp = 
+       let mk_typ nexp =
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
        match Type_check.solve env size with
diff --git a/src/process_file.ml b/src/process_file.ml
index 34c1a255..2e69f59b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -182,7 +182,7 @@ let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f
 
 let load_file order env f =
   let ast = convert_ast order (preprocess_ast (parse_file f)) in
-  Type_check.check env ast
+  Type_error.check env ast
 
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
@@ -191,7 +191,7 @@ let opt_dno_cast = ref false
 
 let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
   let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in
-  let ast, env = Type_check.check env defs in
+  let ast, env = Type_error.check env defs in
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in
   let () = if !opt_just_check then exit 0 else () in
   (ast, env)
@@ -356,7 +356,7 @@ let rewrite_step defs (name,rewriter) =
 let rewrite rewriters defs =
   try List.fold_left rewrite_step defs rewriters with
   | Type_check.Type_error (l, err) ->
-     raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
+     raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
 
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
 let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)]
diff --git a/src/rewrites.ml b/src/rewrites.ml
index dff8e3e5..0ea6ef79 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -418,7 +418,7 @@ let rewrite_sizeof (Defs defs) =
          let inst =
            try instantiation_of orig_exp with
            | Type_error (l, err) ->
-             raise (Reporting_basic.err_typ l (string_of_type_error err)) in
+             raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) in
          (* Rewrite the inst using orig_kid so that each type variable has it's
             original name rather than a mangled typechecker name *)
          let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in
@@ -431,7 +431,7 @@ let rewrite_sizeof (Defs defs) =
                 let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in
                 (try rewrite_trivial_sizeof_exp sizeof with
                 | Type_error (l, err) ->
-                  raise (Reporting_basic.err_typ l (string_of_type_error err)))
+                  raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)))
              (* If the type variable is Not_found then it was probably
                 introduced by a P_var pattern, so it likely exists as
                 a variable in scope. It can't be an existential because the assert rules that out. *)
@@ -642,7 +642,7 @@ let rewrite_sizeof (Defs defs) =
                                           (Bindings.empty, []) defs in
   let defs = List.map (rewrite_sizeof_valspec params_map) defs in
   (* Defs defs *)
-  fst (check initial_env (Defs defs))
+  fst (Type_error.check initial_env (Defs defs))
 
 let rewrite_defs_remove_assert defs =
   let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with
@@ -1653,7 +1653,7 @@ let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
      write_reg_ref (vector_access (GPR, i)) exp
  *)
 let rewrite_register_ref_writes (Defs defs) =
-  let (Defs write_reg_spec) = fst (check Env.empty (Defs (List.map gen_vs
+  let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
     [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in
   let lexp_ref_exp (LEXP_aux (_, annot) as lexp) =
     try
@@ -1888,7 +1888,7 @@ let rewrite_defs_early_return (Defs defs) =
     FD_aux (FD_function (rec_opt, tannot_opt, effect_opt,
       List.map (rewrite_funcl_early_return rewriters) funcls), a) in
 
-  let (Defs early_ret_spec) = fst (check Env.empty (Defs [gen_vs
+  let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs
     ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in
 
   rewrite_defs_base
@@ -2352,7 +2352,7 @@ let rewrite_vector_concat_assignments defs =
          begin
            try check_exp env e_aux unit_typ with
            | Type_error (l, err) ->
-             raise (Reporting_basic.err_typ l (string_of_type_error err))
+             raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
          end
        else E_aux (e_aux, annot)
     | _ -> E_aux (e_aux, annot)
@@ -2378,7 +2378,7 @@ let rewrite_tuple_assignments defs =
        begin
          try check_exp env let_exp unit_typ with
          | Type_error (l, err) ->
-           raise (Reporting_basic.err_typ l (string_of_type_error err))
+           raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
        end
     | _ -> E_aux (e_aux, annot)
   in
@@ -3224,7 +3224,7 @@ let rewrite_defs_remove_superfluous_returns =
 
 
 let rewrite_defs_remove_e_assign (Defs defs) =
-  let (Defs loop_specs) = fst (check Env.empty (Defs (List.map gen_vs
+  let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
     [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
      ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
      ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
@@ -3260,7 +3260,7 @@ let merge_funcls (Defs defs) =
     | d -> d
   in Defs (List.map merge_in_def defs)
 
-let recheck_defs defs = fst (check initial_env defs)
+let recheck_defs defs = fst (Type_error.check initial_env defs)
 
 let rewrite_defs_lem = [
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
@@ -3355,7 +3355,7 @@ let rewrite_check_annot =
        else ());
       exp
     with
-      Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
+      Type_error (l, err) -> raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
   in
   let check_pat pat =
     prerr_endline ("CHECKING PAT: " ^ string_of_pat pat ^ " : " ^ string_of_typ (pat_typ_of pat));
diff --git a/src/specialize.ml b/src/specialize.ml
index 465c5398..0090cdfd 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -429,11 +429,11 @@ let reorder_typedefs (Defs defs) =
 let specialize_ids ids ast =
   let ast = List.fold_left (fun ast id -> specialize_id id ast) ast (IdSet.elements ids) in
   let ast = reorder_typedefs ast in
-  let ast, _ = Type_check.check Type_check.initial_env ast in
+  let ast, _ = Type_error.check Type_check.initial_env ast in
   let ast =
     List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids)
   in
-  let ast, env = Type_check.check Type_check.initial_env ast in
+  let ast, env = Type_error.check Type_check.initial_env ast in
   let ast = remove_unused_valspecs env ast in
   ast, env
 
@@ -527,7 +527,7 @@ let specialize_variants ((Defs defs) as ast) env =
 
   let ast = Defs (specialize_variants' defs) in
   let ast = List.fold_left (fun ast id -> rewrite_polymorphic_constructors id ast) ast !ctors in
-  Type_check.check Type_check.initial_env ast
+  Type_error.check Type_check.initial_env ast
 
 let rec specialize ast env =
   prerr_endline (Util.log_line __MODULE__ __LINE__ "Performing specialisation pass");
diff --git a/src/state.ml b/src/state.ml
index 112b4ee2..c591f753 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -510,5 +510,5 @@ let generate_regstate_defs mwords defs =
   defs
 
 let add_regstate_defs mwords env (Defs defs) =
-  let reg_defs, env = check env (generate_regstate_defs mwords defs) in
+  let reg_defs, env = Type_error.check env (generate_regstate_defs mwords defs) in
   env, append_ast (Defs defs) reg_defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 523b0343..9c5bfc64 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -84,50 +84,13 @@ type type_error =
   (* First parameter is the error that caused us to start doing type
      coercions, the second is the errors encountered by all possible
      coercions *)
-  | Err_no_casts of unit exp * type_error * type_error list
+  | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list
-  | Err_subtype of typ * typ * n_constraint list
+  | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
 
-let pp_type_error err =
-  let open PPrint in
-  let rec pp_err = function
-    | Err_no_casts (exp, trigger, []) ->
-       (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
-       ^^ hardline ^^ (string "Failed because" ^//^ pp_err trigger)
-    | Err_no_casts (exp, trigger, errs) ->
-       (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
-       ^/^ string "Failed because" ^//^ pp_err trigger
-    | Err_no_overloading (id, errs) ->
-       string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
-         group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_err err) errs)
-    | Err_subtype (typ1, typ2, []) ->
-       separate space [ string (string_of_typ typ1);
-                        string "is not a subtype of";
-                        string (string_of_typ typ2) ]
-    | Err_subtype (typ1, typ2, constrs) ->
-       separate space [ string (string_of_typ typ1);
-                        string "is not a subtype of";
-                        string (string_of_typ typ2) ]
-       ^/^ string "in context"
-       ^//^ string (string_of_list ", " string_of_n_constraint constrs)
-    | Err_no_num_ident id ->
-       string "No num identifier" ^^ space ^^ string (string_of_id id)
-    | Err_unresolved_quants (id, quants) ->
-       string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
-       ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants)
-    | Err_other str -> string str
-  in
-  pp_err err
-
-let rec string_of_type_error err =
-  let open PPrint in
-  let b = Buffer.create 20 in
-  ToBuffer.pretty 1. 120 b (pp_type_error err);
-  "\n" ^ Buffer.contents b
-
 exception Type_error of l * type_error;;
 
 let typ_error l m = raise (Type_error (l, Err_other m))
@@ -326,8 +289,10 @@ module Env : sig
   val get_constraints : t -> n_constraint list
   val add_constraint : n_constraint -> t -> t
   val get_typ_var : kid -> t -> base_kind_aux
+  val get_typ_var_loc : kid -> t -> Ast.l
   val get_typ_vars : t -> base_kind_aux KBindings.t
-  val add_typ_var : kid -> base_kind_aux -> t -> t
+  val get_typ_var_locs : t -> Ast.l KBindings.t
+  val add_typ_var : l -> kid -> base_kind_aux -> t -> t
   val get_ret_typ : t -> typ option
   val add_ret_typ : typ -> t -> t
   val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t
@@ -383,7 +348,7 @@ end = struct
       union_ids : (typquant * typ) Bindings.t;
       registers : typ Bindings.t;
       variants : (typquant * type_union list) Bindings.t;
-      typ_vars : base_kind_aux KBindings.t;
+      typ_vars : (Ast.l * base_kind_aux) KBindings.t;
       typ_synonyms : (t -> typ_arg list -> typ) Bindings.t;
       num_defs : nexp Bindings.t;
       overloads : (id list) Bindings.t;
@@ -431,10 +396,15 @@ end = struct
   let add_prover f env = { env with prove = f }
 
   let get_typ_var kid env =
-    try KBindings.find kid env.typ_vars with
+    try snd (KBindings.find kid env.typ_vars) with
+    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+
+  let get_typ_var_loc kid env =
+    try fst (KBindings.find kid env.typ_vars) with
     | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
 
-  let get_typ_vars env = env.typ_vars
+  let get_typ_vars env = KBindings.map snd env.typ_vars
+  let get_typ_var_locs env = KBindings.map fst env.typ_vars
 
   let bk_counter = ref 0
   let bk_name () = let kid = mk_kid ("bk#" ^ string_of_int !bk_counter) in incr bk_counter; kid
@@ -555,10 +525,13 @@ end = struct
 
        let rename_kid kid = if KBindings.mem kid env.typ_vars then prepend_kid "syn#" kid else kid in
        let add_typ_var env kid =
-         if KBindings.mem kid env.typ_vars then
-           (rebindings := kid :: !rebindings; { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) BK_int env.typ_vars })
-         else
-           { env with typ_vars = KBindings.add kid BK_int env.typ_vars }
+         try
+           let (l, _) = KBindings.find kid env.typ_vars in
+           rebindings := kid :: !rebindings;
+           { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, BK_int) env.typ_vars }
+         with
+         | Not_found ->
+            { env with typ_vars = KBindings.add kid (l, BK_int) env.typ_vars }
        in
 
        let env = List.fold_left add_typ_var env kids in
@@ -647,9 +620,9 @@ end = struct
     | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id)
     | Typ_var kid -> begin
       match KBindings.find kid env.typ_vars with
-      | BK_type -> ()
-      | k -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ ^
-                             " is " ^ string_of_base_kind_aux k ^ " rather than Type")
+      | (_, BK_type) -> ()
+      | (_, k) -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
+                               ^ " is " ^ string_of_base_kind_aux k ^ " rather than Type")
       | exception Not_found ->
          typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
@@ -738,7 +711,7 @@ end = struct
   let get_val_spec id env =
     try
       let bind = Bindings.find id env.top_val_specs in
-      typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)));
+      typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, (_, bk)) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)));
       let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
       typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind'));
       bind'
@@ -930,13 +903,13 @@ end = struct
             end
        end
 
-  let add_typ_var kid k env =
+  let add_typ_var l kid k env =
     if KBindings.mem kid env.typ_vars
     then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
     else
       begin
         typ_print (lazy ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k));
-        { env with typ_vars = KBindings.add kid k env.typ_vars }
+        { env with typ_vars = KBindings.add kid (l, k) env.typ_vars }
       end
 
   let add_num_def id nexp env =
@@ -1032,13 +1005,13 @@ end = struct
     }
 end
 
-let add_typquant (quant : typquant) (env : Env.t) : Env.t =
+let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
   let rec add_quant_item env = function
     | QI_aux (qi, _) -> add_quant_item_aux env qi
   and add_quant_item_aux env = function
     | QI_const constr -> Env.add_constraint constr env
-    | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_int env
-    | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var kid k env
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid BK_int env
+    | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var l kid k env
     | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!"
   in
   match quant with
@@ -1067,11 +1040,11 @@ let destruct_exist env typ =
      Some (List.map snd fresh_kids, nc, typ)
   | _ -> None
 
-let add_existential kids nc env =
-  let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids in
+let add_existential l kids nc env =
+  let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids in
   Env.add_constraint nc env
 
-let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids
+let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids
 
 let is_exist = function
   | Typ_aux (Typ_exist (_, _, _), _) -> true
@@ -1110,16 +1083,16 @@ let destruct_numeric env typ =
 let bind_numeric l typ env =
   match destruct_numeric env typ with
   | Some (kids, nc, nexp) ->
-     nexp, add_existential kids nc env
+     nexp, add_existential l kids nc env
   | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric")
 
 (** Pull an (potentially)-existentially qualified type into the global
    typing environment **)
-let bind_existential typ env =
+let bind_existential l typ env =
   match destruct_numeric env typ with
-  | Some (kids, nc, nexp) -> atom_typ nexp, add_existential kids nc env
+  | Some (kids, nc, nexp) -> atom_typ nexp, add_existential l kids nc env
   | None -> match destruct_exist env typ with
-            | Some (kids, nc, typ) -> typ, add_existential kids nc env
+            | Some (kids, nc, typ) -> typ, add_existential l kids nc env
             | None -> typ, env
 
 let destruct_range env typ =
@@ -1260,7 +1233,7 @@ let solve env nexp =
       try KBindings.find kid !bindings with
       | Not_found -> fresh_var kid
     in
-    let env = Env.add_typ_var (mk_kid "solve#") BK_int env in
+    let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") BK_int env in
     let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env))
                                  (nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp))
     in
@@ -1744,11 +1717,11 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
   | _, _ when alpha_equivalent env typ1 typ2 -> ()
   (* Special cases for two numeric (atom) types *)
   | Some (kids1, nc1, nexp1), Some ([], _, nexp2) ->
-     let env = add_existential kids1 nc1 env in
-     if prove env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
+     let env = add_existential l kids1 nc1 env in
+     if prove env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
   | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
-     let env = add_existential kids1 nc1 env in
-     let env = add_typ_vars (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2))) env in
+     let env = add_existential l kids1 nc1 env in
+     let env = add_typ_vars l (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2))) env in
      let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in
      let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
      let constr var_of =
@@ -1756,16 +1729,14 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
          (nc_constraint env var_of (nc_negate nc2))
      in
      if prove_z3' env constr then ()
-     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
+     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
   | _, _ ->
   match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with
   | Some (kids, nc, typ1), _ ->
-     let env = add_existential kids nc env in subtyp l env typ1 typ2
-  (* | None, ([], _, typ2) ->
-     typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *)
+     let env = add_existential l kids nc env in subtyp l env typ1 typ2
   | None, (kids, nc, typ2) ->
      typ_debug (lazy "Subtype check with unification");
-     let env = add_typ_vars kids env in
+     let env = add_typ_vars l kids env in
      let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in
      let unifiers, existential_kids, existential_nc =
        try unify l env typ2 typ1 with
@@ -1776,7 +1747,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
      let env = match existential_kids, existential_nc with
        | [], None -> env
        | _, Some enc ->
-          let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env existential_kids in
+          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env existential_kids in
           Env.add_constraint enc env
        | _, None -> assert false (* Cannot have existential_kids without existential_nc *)
      in
@@ -1785,7 +1756,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
          (nc_constraint env var_of (nc_negate nc))
      in
      if prove_z3' env constr then ()
-     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
+     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
 
 let typ_equality l env typ1 typ2 =
   subtyp l env typ1 typ2; subtyp l env typ2 typ1
@@ -2208,7 +2179,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
            typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
            try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with
            | Type_error (_, err) ->
-              typ_print (lazy ("Error : " ^ string_of_type_error err));
+              typ_debug (lazy "Error");
               try_overload (errs @ [(f, err)], fs)
          end
      in
@@ -2330,7 +2301,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
     | _ -> failwith "Cannot switch type for unannotated function"
   in
   let rec try_casts trigger errs = function
-    | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, trigger, errs))
+    | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, typ_of annotated_exp, typ, trigger, errs))
     | (cast :: casts) -> begin
         typ_print (lazy ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ));
         try
@@ -2392,7 +2363,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ =
   | tpat, env, [] -> tpat, env
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
-  let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in
+  let (Typ_aux (typ_aux, _) as typ), env = bind_existential l typ env in
   typ_print (lazy ("Binding " ^ string_of_pat pat ^  " to " ^ string_of_typ typ));
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in
   let switch_typ pat typ = match pat with
@@ -2575,7 +2546,7 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
      begin
        match typ_nexps typ with
        | [nexp] ->
-          Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env)
+          Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env)
        | [] ->
           typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
        | nexps ->
@@ -2588,7 +2559,7 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_
   match typ_pat_aux, typ_arg_aux with
   | TP_wild, _ -> env
   | TP_var kid, Typ_arg_nexp nexp ->
-     Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env)
+     Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env)
   | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ
   | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order"
   | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
@@ -2878,7 +2849,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
            typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
            try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with
            | Type_error (_, err) ->
-              typ_print (lazy ("Error : " ^ string_of_type_error err));
+              typ_debug (lazy "Error");
               try_overload (errs @ [(f, err)], fs)
          end
      in
@@ -2901,7 +2872,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with
        | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
           let loop_kid = mk_kid ("loop_" ^ string_of_id v) in
-          let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env (loop_kid :: kids1 @ kids2) in
+          let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env (loop_kid :: kids1 @ kids2) in
           let env = Env.add_constraint (nc_and nc1 nc2) env in
           let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in
           let loop_vtyp = atom_typ (nvar loop_kid) in
@@ -3051,7 +3022,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
              | [], None -> env
              | _, Some enc ->
                 let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in
-                let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_int env) env ex_kids in
+                let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) BK_int env) env ex_kids in
                 Env.add_constraint enc env
              | _, None -> assert false (* Cannot have ex_kids without ex_nc *)
            in
@@ -3087,7 +3058,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
          typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)));
          if ex_kids = [] then () else (typ_debug (lazy ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc)); ex_goal := ex_nc);
          record_unifiers unifiers;
-         let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env ex_kids in
+         let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env ex_kids in
          let typs' = List.map (subst_unifiers unifiers) typs in
          let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in
          let ret_typ' =
@@ -3538,7 +3509,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
   in
   check_tannotopt env quant vtyp_ret tannotopt;
   typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)));
-  let funcl_env = add_typquant quant env in
+  let funcl_env = add_typquant l quant env in
   let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
   let eff = List.fold_left union_effects no_effect (List.map funcl_effect funcls) in
   let vs_def, env, declared_eff =
@@ -3566,7 +3537,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
          | Some op, None -> Env.add_smt_op id op env
          | _, _ -> env
        in
-       Env.wf_typ (add_typquant quants env) typ;
+       Env.wf_typ (add_typquant l quants env) typ;
        typ_debug (lazy "CHECKED WELL-FORMED VAL SPEC");
        let env =
        (* match ext_opt with
@@ -3582,7 +3553,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
     | Typ_aux (Typ_fn (_,_,eff),_) -> eff
     | _ -> no_effect
   in
-  [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant quants env) typ) env
+  [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant l quants env) typ) env
 
 let check_default env (DT_aux (ds, l)) =
   match ds with
@@ -3685,7 +3656,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
                                Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id b, _)), _)]), _)
             when string_of_id v = "vector" && string_of_id b = "bit" ->
           let size = Big_int.to_int size in
-          let (Defs defs), env = check' env (Bitfield.macro id size order ranges) in
+          let (Defs defs), env = check env (Bitfield.macro id size order ranges) in
           defs, env
        | _ ->
           typ_error l "Bad bitfield type"
@@ -3721,20 +3692,15 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
      let defs, env = check_def env def
      in List.map (fun def -> DEF_comm (DC_comm_struct def)) defs, env
 
-and check' : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
   fun env (Defs defs) ->
   match defs with
   | [] -> (Defs []), env
   | def :: defs ->
      let (def, env) = check_def env def in
-     let (Defs defs, env) = check' env (Defs defs) in
+     let (Defs defs, env) = check env (Defs defs) in
      (Defs (def @ defs)), env
 
-let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
-  fun env defs ->
-  try check' env defs with
-  | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
-
 let initial_env =
   Env.empty
   |> Env.add_prover prove
diff --git a/src/type_check.mli b/src/type_check.mli
index 1c0e2f09..feacd38a 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -70,17 +70,15 @@ val opt_no_lexp_bounds_check : bool ref
 (** {2 Type errors} *)
 
 type type_error =
-  | Err_no_casts of unit exp * type_error * type_error list
+  | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list
-  | Err_subtype of typ * typ * n_constraint list
+  | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
 
 exception Type_error of l * type_error;;
 
-val string_of_type_error : type_error -> string
-
 (** {2 Environments} *)
 
 (** The env module defines the internal type checking environment, and
@@ -126,7 +124,9 @@ module Env : sig
 
   val get_typ_vars : t -> base_kind_aux KBindings.t
 
-  val add_typ_var : kid -> base_kind_aux -> t -> t
+  val get_typ_var_locs : t -> Ast.l KBindings.t
+
+  val add_typ_var : Ast.l -> kid -> base_kind_aux -> t -> t
 
   val is_record : id -> t -> bool
 
@@ -186,7 +186,7 @@ end
 
 (** Push all the type variables and constraints from a typquant into
    an environment *)
-val add_typquant : typquant -> Env.t -> Env.t
+val add_typquant : Ast.l -> typquant -> Env.t -> Env.t
 
 (** When the typechecker creates new type variables it gives them
    fresh names of the form 'fvXXX#name, where XXX is a number (not
@@ -322,12 +322,12 @@ Some invariants that will hold of a fully checked AST are:
 
  - Toplevel expressions such as typedefs and some subexpressions such
    as letbinds may have None as their tannots if it doesn't make sense
-   for them to have type annotations. *)
-val check : Env.t -> 'a defs -> tannot defs * Env.t
+   for them to have type annotations.
 
-(** Like check but throws type_errors rather than Sail generic errors
-   from Reporting_basic. *)
-val check' : Env.t -> 'a defs -> tannot defs * Env.t
+   check throws type_errors rather than Sail generic errors from
+   Reporting_basic. For a function that uses generic errors, use
+   Type_error.check *)
+val check : Env.t -> 'a defs -> tannot defs * Env.t
 
 (** The initial type checking environment *)
 val initial_env : Env.t
diff --git a/src/type_error.ml b/src/type_error.ml
new file mode 100644
index 00000000..78db65bc
--- /dev/null
+++ b/src/type_error.ml
@@ -0,0 +1,141 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open PPrint
+open Util
+open Ast
+open Ast_util
+open Type_check
+
+let bullet f xs =
+  group (separate_map hardline (fun x -> string "* " ^^ nest 2 (f x)) xs)
+
+let pp_nexp, pp_n_constraint =
+  let rec string_of_nexp = function
+    | Nexp_aux (nexp, _) -> string_of_nexp_aux nexp
+  and string_of_nexp_aux = function
+    | Nexp_id id -> string_of_id id
+    | Nexp_var kid -> string_of_kid kid
+    | Nexp_constant c -> Big_int.to_string c
+    | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")"
+    | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")"
+    | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")"
+    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_nexp nexps ^ ")"
+    | Nexp_exp n -> "2 ^ " ^ string_of_nexp n
+    | Nexp_neg n -> "- " ^ string_of_nexp n
+  in
+
+  let string_of_n_constraint = function
+    | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
+    | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
+    | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
+    | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
+    | NC_aux (NC_or (nc1, nc2), _) ->
+       "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
+    | NC_aux (NC_and (nc1, nc2), _) ->
+       "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
+    | NC_aux (NC_set (kid, ns), _) ->
+       string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+    | NC_aux (NC_true, _) -> "true"
+    | NC_aux (NC_false, _) -> "false"
+  in
+
+  let pp_nexp' nexp =
+    string (string_of_nexp nexp)
+  in
+
+  let pp_n_constraint' nc =
+    string (string_of_n_constraint nc)
+  in
+
+  pp_nexp', pp_n_constraint'
+
+let rec pp_type_error = function
+  | Err_no_casts (exp, typ_from, typ_to, trigger, _) ->
+     let coercion =
+       group (string "Tried performing type coercion from" ^/^ Pretty_print_sail.doc_typ typ_from
+              ^/^ string "to" ^/^ Pretty_print_sail.doc_typ typ_to
+              ^/^ string "on" ^/^ Pretty_print_sail.doc_exp exp)
+     in
+     coercion ^^ hardline ^^ (string "Failed because" ^/^ pp_type_error trigger)
+
+  | Err_no_overloading (id, errs) ->
+     string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
+       group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_type_error err) errs)
+
+  | Err_subtype (typ1, typ2, constrs, locs) ->
+     enclose (string (Util.termcode 1)) (string (Util.termcode 21))
+             (separate space [ string (string_of_typ typ1);
+                               string "is not a subtype of";
+                               string (string_of_typ typ2) ])
+     ^/^ string "in context"
+     ^/^ bullet pp_n_constraint constrs
+     ^/^ string "where"
+     ^/^ bullet (fun (kid, l) -> string (string_of_kid kid ^ " bound at " ^ Reporting_basic.loc_to_string l ^ "\n")) (KBindings.bindings locs)
+
+  | Err_no_num_ident id ->
+     string "No num identifier" ^^ space ^^ string (string_of_id id)
+
+  | Err_unresolved_quants (id, quants) ->
+     string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
+     ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants)
+
+  | Err_other str -> string str
+
+let rec string_of_type_error err =
+  let open PPrint in
+  let b = Buffer.create 20 in
+  ToBuffer.pretty 1. 400 b (pp_type_error err);
+  "\n" ^ Buffer.contents b
+
+let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+  fun env defs ->
+  try Type_check.check env defs with
+  | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))