add __POS__ argument to Err_unreachable for better error reporting

11 files changed, 172 insertions, 172 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 314ac230..db60005d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -955,8 +955,8 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
     let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
       | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
       | _ ->
-        raise (Reporting_basic.err_unreachable l
-          ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
+        raise (Reporting_basic.err_unreachable l __POS__
+         ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
     rewrap (E_tuple (List.map get_id les))
   | LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e))
   | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
@@ -1016,7 +1016,7 @@ let is_order_inc = function
   | Ord_aux (Ord_inc, _) -> true
   | Ord_aux (Ord_dec, _) -> false
   | Ord_aux (Ord_var _, l) ->
-    raise (Reporting_basic.err_unreachable l "is_order_inc called on vector with variable ordering")
+    raise (Reporting_basic.err_unreachable l __POS__ "is_order_inc called on vector with variable ordering")
 
 let is_bit_typ = function
   | Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2ab3cd98..4dcac1b8 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -112,7 +112,7 @@ let typquant_to_quantkinds k_env typquant =
             | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) ->
               (match Envmap.apply k_env (var_to_string v) with
               | Some(typ) -> typ::rst
-              | None -> raise (Reporting_basic.err_unreachable l "Envmap didn't get an entry during typschm processing"))
+              | None -> raise (Reporting_basic.err_unreachable l __POS__ "Envmap didn't get an entry during typschm processing"))
           end)
         qlist
         [])
@@ -157,7 +157,7 @@ let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
 
 let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
   match klst with
-  | [] -> raise (Reporting_basic.err_unreachable l "Kind with empty kindlist encountered")
+  | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Kind with empty kindlist encountered")
   | [k] -> let k_ast,k_typ = to_ast_base_kind k in
            K_aux(K_kind([k_ast]),l), k_typ
   | ks -> let k_pairs = List.map to_ast_base_kind ks in
@@ -204,7 +204,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
                   let rise = match def_ord with
                     | Ord_aux(Ord_inc,dl) ->  to_ast_nexp k_env (make_r b r)
                     | Ord_aux(Ord_dec,dl) ->  to_ast_nexp k_env (make_r r b)
-                    | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in
+                    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Default order not inc or dec") in
                   Typ_app(Id_aux(Id "vector",il),
                           [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
                            Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
@@ -220,7 +220,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
 		let (base,rise) = match def_ord with
 		  | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r)
 		  | Ord_aux(Ord_dec,dl) -> (to_ast_nexp k_env (make_sub_one r)), (to_ast_nexp k_env r)
-		  | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in
+		  | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Default order not inc or dec") in
 		Typ_app(Id_aux(Id "vector",il),
 			[Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
 			 Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
@@ -334,7 +334,7 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg
     | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg)
     | K_Nat  -> Typ_arg_nexp (to_ast_nexp k_env arg)
     | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg)
-    | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))),
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))),
     l)
 
 and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint =
@@ -390,7 +390,7 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant
       let kopt,k_env,k_env_local = (match kind,ktyp with
         | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
 	| None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
-	| _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in
+	| _ -> raise (Reporting_basic.err_unreachable l __POS__ "Envmap in dom is true but apply gives None")) in
       KOpt_aux(kopt,l),k_env,local_names,k_env_local
   in
   match tq with
@@ -528,11 +528,11 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_record fexps ->
        (match to_ast_fexps true k_env def_ord fexps with
         | Some fexps -> E_record fexps
-        | None -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none"))
+        | None -> raise (Reporting_basic.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
     | Parse_ast.E_record_update(exp,fexps) ->
       (match to_ast_fexps true k_env def_ord fexps with
       | Some(fexps) -> E_record_update(to_ast_exp k_env def_ord exp, fexps)
-      | _ -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none"))
+      | _ -> raise (Reporting_basic.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
     | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id)
     | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
     | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
@@ -545,7 +545,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp)
     | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
-    | _ -> raise (Reporting_basic.err_unreachable l "Unparsable construct in to_ast_exp")
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
     ), (l,()))
 
 and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp =
@@ -846,7 +846,7 @@ let to_ast_alias_spec k_env def_ord (Parse_ast.E_aux(e,le)) =
 				  Parse_ast.E_aux(Parse_ast.E_id second,ls)) ->
 	AL_concat(RI_aux(RI_id (to_ast_id first),(lf,())),
 		  RI_aux(RI_id (to_ast_id second),(ls,())))
-      | _ -> raise (Reporting_basic.err_unreachable le "Found an expression not supported by parser in to_ast_alias_spec")
+      | _ -> raise (Reporting_basic.err_unreachable le __POS__ "Found an expression not supported by parser in to_ast_alias_spec")
     ), (le,()))
 
 let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
@@ -991,7 +991,7 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
                  ((Finished def), envs),partial_defs
               | _, true ->
                  typ_error l "Scattered definition ended multiple times" (Some id) None None
-              | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
+              | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Something in partial_defs other than fundef and type"))))
 
 let rec to_ast_defs_helper envs partial_defs = function
   | [] -> ([],envs,partial_defs)
@@ -1004,7 +1004,7 @@ let rec to_ast_defs_helper envs partial_defs = function
                 (match (def_in_progress id partial_defs) with
                  | None ->
                    raise
-                     (Reporting_basic.err_unreachable l "Id stored in place holder not retrievable from partial defs")
+                     (Reporting_basic.err_unreachable l __POS__ "Id stored in place holder not retrievable from partial defs")
                  | Some(d,k) ->
                    if (snd !d)
                    then (fst !d) :: defs, envs, partial_defs
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index ab6d9e2d..55031ff9 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -738,7 +738,7 @@ let reduce_cast typ exp l annot =
      let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in
      if prove nc_env nc
      then exp
-     else raise (Reporting_basic.err_unreachable l
+     else raise (Reporting_basic.err_unreachable l __POS__
                    ("Constant propagation error: literal " ^ Big_int.to_string n ^
                        " does not satisfy constraint " ^ string_of_n_constraint nc))
   | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
@@ -1136,10 +1136,10 @@ let apply_pat_choices choices =
           List.fold_left (fun e (id,e') ->
             E_let (LB_aux (LB_val (P_aux (P_id id, dummyannot),e'),dummyannot),E_aux (e,dummyannot))) e subst
        | Pat_aux (Pat_when _,(l,_)) ->
-          raise (Reporting_basic.err_unreachable l
+          raise (Reporting_basic.err_unreachable l __POS__
                    "Pattern acquired a guard after analysis!")
        | exception Not_found ->
-          raise (Reporting_basic.err_unreachable (exp_loc e)
+          raise (Reporting_basic.err_unreachable (exp_loc e) __POS__
                    "Unable to find case I found earlier!"))
     | exception Not_found -> E_case (e,cases)
   in
@@ -1440,7 +1440,7 @@ let split_defs all_errors splits defs =
     | E_internal_plet _
     | E_internal_return _
     | E_internal_value _
-      -> raise (Reporting_basic.err_unreachable l
+      -> raise (Reporting_basic.err_unreachable l __POS__
                   ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
   and const_prop_fexps ref_vars substs assigns (FES_aux (FES_Fexps (fes,flag), annot)) =
     FES_aux (FES_Fexps (List.map (const_prop_fexp ref_vars substs assigns) fes, flag), annot)
@@ -2198,7 +2198,7 @@ let change_parameter_pat i = function
                            mk_id "==",
                            E_aux (E_lit lit,annot)), annot) in
      P_aux (P_id var, (l,empty_tannot)), ([],[test])
-  | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l
+  | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l __POS__
                                 "Expected variable pattern")
 
 (* TODO: make more precise, preferably with a proper free variables function
@@ -2254,7 +2254,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
   | Typ_aux (Typ_app (Id_aux (Id "atom",_),
                       [Typ_arg_aux (Typ_arg_nexp nexp,l')]),_) ->
      mk_exp nexp l l'
-  | _ -> raise (Reporting_basic.err_unreachable l
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__
                   "atom stopped being an atom?")
 
 let replace_type env typ =
@@ -2268,7 +2268,7 @@ let replace_type env typ =
                       [Typ_arg_aux (Typ_arg_nexp nexp,l')]) ->
      Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
                        [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
-  | _ -> raise (Reporting_basic.err_unreachable l
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__
                   "atom stopped being an atom?")
 
 
@@ -3149,7 +3149,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
     | E_internal_plet _
     | E_internal_return _
     | E_internal_value _
-      -> raise (Reporting_basic.err_unreachable l
+      -> raise (Reporting_basic.err_unreachable l __POS__
                   ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
 
     | E_var (lexp,e1,e2) ->
@@ -4117,7 +4117,7 @@ let add_bitvector_casts (Defs defs) =
       match typ with
       | Typ_aux (Typ_fn (_,ret,_),_) -> ret
       | Typ_aux (_,l) as typ ->
-         raise (Reporting_basic.err_unreachable l
+         raise (Reporting_basic.err_unreachable l __POS__
                   ("Function clause must have function type: " ^ string_of_typ typ ^
                       " is not a function type"))
     in
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 27133542..b47ac21c 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -236,7 +236,7 @@ let doc_nexp ctx nexp =
     | Nexp_app (Id_aux (Id "abs_atom",_), [_])
         -> parens (plussub nexp)
     | _ ->
-       raise (Reporting_basic.err_unreachable l
+       raise (Reporting_basic.err_unreachable l __POS__
                 ("cannot pretty-print nexp \"" ^ string_of_nexp nexp ^ "\""))
   in atomic (nexp_simp nexp)
 
@@ -299,12 +299,12 @@ let drop_duplicate_atoms kids ty =
     match typ with
     | Typ_id _
     | Typ_var _ -> Some full_typ
-    | Typ_fn (arg,res,eff) -> raise (Reporting_basic.err_unreachable l "Function type nested inside existential")
+    | Typ_fn (arg,res,eff) -> raise (Reporting_basic.err_unreachable l __POS__ "Function type nested inside existential")
     | Typ_tup typs ->
        (match Util.map_filter aux_typ typs with
        | [] -> None
        | typs' -> Some (Typ_aux (Typ_tup typs',l)))
-    | Typ_exist _ -> raise (Reporting_basic.err_unreachable l "Nested existential type")
+    | Typ_exist _ -> raise (Reporting_basic.err_unreachable l __POS__ "Nested existential type")
        (* This is an AST type, don't need to check for equivalent nexps *)
     | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)])
         when KidSet.mem kid kids ->
@@ -441,7 +441,7 @@ let doc_typ, doc_atomic_typ =
       | Typ_id (Id_aux (Id "nat", _)) ->
          (match maybe_expand_range_type ty with
          | Some typ -> atomic_typ atyp_needed typ
-         | None -> raise (Reporting_basic.err_unreachable l "Bad range type"))
+         | None -> raise (Reporting_basic.err_unreachable l __POS__ "Bad range type"))
       | Typ_app(Id_aux (Id "implicit", _),_) ->
          (string "Z")
       | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
@@ -686,34 +686,34 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) =
         let el_typ =
           match destruct_vector env typ with
           | Some (_,_,t) -> t
-          | None -> raise (Reporting_basic.err_unreachable l "vector pattern doesn't have vector type")
+          | None -> raise (Reporting_basic.err_unreachable l __POS__ "vector pattern doesn't have vector type")
         in
         let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true (p,el_typ)) pats) in
         if apat_needed then parens ppp else ppp
      | P_vector_concat pats ->
-        raise (Reporting_basic.err_unreachable l
+        raise (Reporting_basic.err_unreachable l __POS__
                  "vector concatenation patterns should have been removed before pretty-printing")
      | P_tup pats  ->
         let typs = match typ with
           | Typ_aux (Typ_tup typs, _) -> typs
-          | _ -> raise (Reporting_basic.err_unreachable l "tuple pattern doesn't have tuple type")
+          | _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern doesn't have tuple type")
         in
         (match pats, typs with
         | [p], [typ'] -> doc_pat ctxt apat_needed (p, typ')
-        | [_], _ -> raise (Reporting_basic.err_unreachable l "tuple pattern length does not match tuple type length")
+        | [_], _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern length does not match tuple type length")
         | _ -> parens (separate_map comma_sp (doc_pat ctxt false) (List.combine pats typs)))
      | P_list pats ->
         let el_typ = match typ with
           | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
               when Id.compare f (mk_id "list") = 0 -> el_typ
-          | _ -> raise (Reporting_basic.err_unreachable l "list pattern not a list")
+          | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list")
         in
         brackets (separate_map semi (fun p -> doc_pat ctxt false (p, el_typ)) pats)
      | P_cons (p,p') ->
         let el_typ = match typ with
           | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
               when Id.compare f (mk_id "list") = 0 -> el_typ
-          | _ -> raise (Reporting_basic.err_unreachable l "list pattern not a list")
+          | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list")
         in
         doc_op (string "::") (doc_pat ctxt true (p, el_typ)) (doc_pat ctxt true (p', typ))
      | P_record (_,_) -> empty (* TODO *)
@@ -737,7 +737,7 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
   | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
     when string_of_id register = "register" -> id
   | Typ_app (id, _) -> id
-  | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id")
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__ "failed to get type id")
 
 (* TODO: maybe Nexp_exp, division? *)
 (* Evaluation of constant nexp subexpressions, because Coq will be able to do those itself *)
@@ -875,7 +875,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
-                 raise (report l "indexing a register's (single bit) bitfield not supported")
+                 raise (report l __POS__ "indexing a register's (single bit) bitfield not supported")
                else
                  let field_ref =
                    doc_id (typ_id_of (typ_of_annot lannot)) ^^
@@ -894,7 +894,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
-                 raise (report l "indexing a register's (single bit) bitfield not supported")
+                 raise (report l __POS__ "indexing a register's (single bit) bitfield not supported")
                else
                  let field_ref =
                    doc_id (typ_id_of (typ_of_annot lannot)) ^^
@@ -927,16 +927,16 @@ let doc_exp_lem, doc_let_lem =
         | _ ->
            liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
     | E_vector_append(le,re) ->
-      raise (Reporting_basic.err_unreachable l
+      raise (Reporting_basic.err_unreachable l __POS__
         "E_vector_append should have been rewritten before pretty-printing")
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
     | E_if(c,t,e) ->
        let epp = if_exp ctxt false c t e in
        if aexp_needed then parens (align epp) else epp
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
-       raise (report l "E_for should have been rewritten before pretty-printing")
+       raise (report l __POS__ "E_for should have been rewritten before pretty-printing")
     | E_loop _ ->
-       raise (report l "E_loop should have been rewritten before pretty-printing")
+       raise (report l __POS__ "E_loop should have been rewritten before pretty-printing")
     | E_let(leb,e) ->
        let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
        if aexp_needed then parens epp else epp
@@ -961,11 +961,11 @@ let doc_exp_lem, doc_let_lem =
                      | (P_aux (P_var (P_aux (P_id id, _), _), _))
                      | (P_aux (P_id id, _))), _), _),
                      body), _), _), _)), _)), _) -> id, body
-                 | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
+                 | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
                let dir = match ord_exp with
                  | E_aux (E_lit (L_aux (L_false, _)), _) -> "_down"
                  | E_aux (E_lit (L_aux (L_true, _)), _) -> "_up"
-                 | _ -> raise (Reporting_basic.err_unreachable l ("Unexpected loop direction " ^ string_of_exp ord_exp))
+                 | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unexpected loop direction " ^ string_of_exp ord_exp))
                in
                let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in
                let combinator = combinator ^ dir in
@@ -994,7 +994,7 @@ let doc_exp_lem, doc_let_lem =
                         (prefix 2 1 (group body_lambda) (expN body))
                      )
                  )
-          | _ -> raise (Reporting_basic.err_unreachable l
+          | _ -> raise (Reporting_basic.err_unreachable l __POS__
              "Unexpected number of arguments for loop combinator")
           end
        | Id_aux (Id (("while" | "until") as combinator), _) ->
@@ -1031,7 +1031,7 @@ let doc_exp_lem, doc_let_lem =
                        (parens (prefix 2 1 (group lambda) (expN cond)))
                        (parens (prefix 2 1 (group lambda) (expN body))))
                  )
-            | _ -> raise (Reporting_basic.err_unreachable l
+            | _ -> raise (Reporting_basic.err_unreachable l __POS__
                "Unexpected number of arguments for loop combinator")
           end
        | Id_aux (Id "early_return", _) ->
@@ -1049,7 +1049,7 @@ let doc_exp_lem, doc_let_lem =
                      doc_atomic_typ ctxt false (typ_of exp)] in
                    true, doc_op colon epp tannot in
                if aexp_needed then parens tepp else tepp
-            | _ -> raise (Reporting_basic.err_unreachable l
+            | _ -> raise (Reporting_basic.err_unreachable l __POS__
                "Unexpected number of arguments for early_return builtin")
           end
        | _ ->
@@ -1075,7 +1075,7 @@ let doc_exp_lem, doc_let_lem =
                  (match arg_typ with
                  | Typ_aux (Typ_tup typs,_) -> typs, ret_typ, eff
                  | _ -> [arg_typ], ret_typ, eff)
-              | _ -> raise (Reporting_basic.err_unreachable l "Function not a function type")
+              | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type")
             in
             let inst =
               match instantiation_of_without_type full_exp with
@@ -1159,10 +1159,10 @@ let doc_exp_lem, doc_let_lem =
             liftR (if aexp_needed then parens (align epp) else epp)
        end
     | E_vector_access (v,e) ->
-      raise (Reporting_basic.err_unreachable l
+      raise (Reporting_basic.err_unreachable l __POS__
         "E_vector_access should have been rewritten before pretty-printing")
     | E_vector_subrange (v,e1,e2) ->
-      raise (Reporting_basic.err_unreachable l
+      raise (Reporting_basic.err_unreachable l __POS__
         "E_vector_subrange should have been rewritten before pretty-printing")
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        (match destruct_tannot fannot with
@@ -1175,10 +1175,10 @@ let doc_exp_lem, doc_let_lem =
              else doc_id id in
            expY fexp ^^ dot ^^ parens fname
         | _ ->
-           raise (report l "E_field expression with no register or record type"))
+           raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "tt"
-    | E_block exps -> raise (report l "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l "Nondet blocks not supported.")
+    | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
+    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
@@ -1235,7 +1235,7 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
            (* when Env.is_record tid env -> *)
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = enclose_record (align (separate_map
                                           (semi_sp ^^ break 1)
                                           (doc_fexp ctxt recordtyp) fexps)) in
@@ -1246,7 +1246,7 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
            when Env.is_record tid env ->
            tid, env
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        if List.length fexps > 1 then
          let _,fields = Env.get_record recordtyp env in
          let var, let_pp =
@@ -1272,7 +1272,7 @@ let doc_exp_lem, doc_let_lem =
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let start, (len, order, etyp) =
          if is_vector_typ t then vector_start_index t, vector_typ_args_of t
-         else raise (Reporting_basic.err_unreachable l
+         else raise (Reporting_basic.err_unreachable l __POS__
            "E_vector of non-vector type") in
        let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
        let expspp =
@@ -1297,10 +1297,10 @@ let doc_exp_lem, doc_let_lem =
            (vepp,aexp_needed) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update(v,e1,e2) ->
-       raise (Reporting_basic.err_unreachable l
+       raise (Reporting_basic.err_unreachable l __POS__
          "E_vector_update should have been rewritten before pretty-printing")
     | E_vector_update_subrange(v,e1,e2,e3) ->
-       raise (Reporting_basic.err_unreachable l
+       raise (Reporting_basic.err_unreachable l __POS__
         "E_vector_update should have been rewritten before pretty-printing")
     | E_list exps ->
        brackets (separate_map semi (expN) exps)
@@ -1330,10 +1330,10 @@ let doc_exp_lem, doc_let_lem =
        let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
        if aexp_needed then parens (align epp) else align epp
     | E_app_infix (e1,id,e2) ->
-       raise (Reporting_basic.err_unreachable l
+       raise (Reporting_basic.err_unreachable l __POS__
          "E_app_infix should have been rewritten before pretty-printing")
     | E_var(lexp, eq_exp, in_exp) ->
-       raise (report l "E_vars should have been removed before pretty-printing")
+       raise (report l __POS__ "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
        begin
          match pat, e1 with
@@ -1374,7 +1374,7 @@ let doc_exp_lem, doc_let_lem =
       (match nexp_simp nexp with
         | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l))
         | _ ->
-          raise (Reporting_basic.err_unreachable l
+          raise (Reporting_basic.err_unreachable l __POS__
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
     | E_return r ->
       let ret_monad = " : MR" in
@@ -1388,7 +1388,7 @@ let doc_exp_lem, doc_let_lem =
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint nc -> wrap_parens (doc_nc_exp ctxt nc)
     | E_internal_value _ ->
-      raise (Reporting_basic.err_unreachable l
+      raise (Reporting_basic.err_unreachable l __POS__
         "unsupported internal expression encountered while pretty-printing")
   and if_exp ctxt (elseif : bool) c t e =
     let if_pp = string (if elseif then "else if" else "if") in
@@ -1441,8 +1441,8 @@ let doc_exp_lem, doc_let_lem =
     group (prefix 3 1 (separate space [pipe; doc_pat ctxt false (pat,typ);bigarrow])
                   (group (top_exp ctxt false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
-    raise (Reporting_basic.err_unreachable l
-      "guarded pattern expression should have been rewritten before pretty-printing")
+    raise (Reporting_basic.err_unreachable l __POS__
+     "guarded pattern expression should have been rewritten before pretty-printing")
 
   and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot)))) = match lexp with
     | LEXP_field (le,id) ->
@@ -1451,7 +1451,7 @@ let doc_exp_lem, doc_let_lem =
     | LEXP_cast (typ,id) -> doc_id (append_id id "_ref")
     | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps)
     | _ ->
-       raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
+       raise (Reporting_basic.err_unreachable l __POS__ ("doc_lexp_deref_lem: Unsupported lexp"))
              (* expose doc_exp_lem and doc_let *)
   in top_exp, let_exp
 
@@ -1519,8 +1519,8 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
           match nexp_simp start with
           | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
           | _ ->
-            raise (Reporting_basic.err_unreachable Parse_ast.Unknown
-              ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
+            raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+             ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
         with
         | _ -> (Big_int.zero, true) in
       doc_op equals
@@ -1580,7 +1580,7 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
            string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :=" ^/^
            string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec." in
           typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline)
-    | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
 
 let args_of_typ l env typs =
   let arg i typ =
@@ -1603,7 +1603,7 @@ let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
      let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
      [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity
   | P_tup pats, Some typs -> List.combine pats typs, identity
-  | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l "Tuple pattern against non-tuple type")
+  | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l __POS__ "Tuple pattern against non-tuple type")
   | P_wild, Some typs ->
      let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in
      List.map wild typs, identity
@@ -1800,8 +1800,8 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let _ = match guard with
     | None -> ()
     | _ ->
-       raise (Reporting_basic.err_unreachable l
-                "guarded pattern expression should have been rewritten before pretty-printing") in
+       raise (Reporting_basic.err_unreachable l __POS__
+               "guarded pattern expression should have been rewritten before pretty-printing") in
   let bodypp = doc_fun_body ctxt exp in
   let bodypp = if effectful eff || not build_ex then bodypp else string "build_ex" ^^ parens bodypp in
   group (prefix 3 1
@@ -1855,8 +1855,8 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
                                        string o;
                                        string "[]"]))
            ^/^ hardline
-         else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
-       else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) *)
+         else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
+       else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
@@ -1880,7 +1880,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
     let i, j = match fr with
     | BF_aux (BF_single i, _) -> (i, i)
     | BF_aux (BF_range (i, j), _) -> (i, j)
-    | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+    | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
         ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
     let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
     (* TODO Assumes normalised, decreasing bitvector slices; however, since
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2b0fee22..c20fe5f4 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -193,8 +193,8 @@ let doc_nexp_lem nexp =
        | Nexp_exp n -> "exp_" ^ mangle_nexp n
        | Nexp_neg n -> "neg_" ^ mangle_nexp n
        | _ ->
-          raise (Reporting_basic.err_unreachable l
-                   ("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\"")) 
+          raise (Reporting_basic.err_unreachable l __POS__
+                  ("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\"")) 
      end in
      string ("'" ^ mangle_nexp full_nexp)
 
@@ -283,8 +283,8 @@ let doc_typ_lem, doc_atomic_typ_lem =
              (* (match nexp_simp m with
                | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
                | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
-               | _ -> raise (Reporting_basic.err_unreachable l
-                 "cannot pretty-print bitvector type with non-constant length")) *)
+               | _ -> raise (Reporting_basic.err_unreachable l __POS__
+                "cannot pretty-print bitvector type with non-constant length")) *)
            | _ -> string "list" ^^ space ^^ typ elem_typ in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
@@ -510,8 +510,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
      let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in
      if apat_needed then parens ppp else ppp
   | P_vector_concat pats ->
-     raise (Reporting_basic.err_unreachable l
-       "vector concatenation patterns should have been removed before pretty-printing")
+     raise (Reporting_basic.err_unreachable l __POS__
+      "vector concatenation patterns should have been removed before pretty-printing")
   | P_tup pats  ->
      (match pats with
       | [p] -> doc_pat_lem ctxt apat_needed p
@@ -552,7 +552,7 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
   | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
     when string_of_id register = "register" -> id
   | Typ_app (id, _) -> id
-  | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id")
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__ "failed to get type id")
 
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
@@ -576,7 +576,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
-                 raise (report l "indexing a register's (single bit) bitfield not supported")
+                 raise (report l __POS__ "indexing a register's (single bit) bitfield not supported")
                else
                  let field_ref =
                    doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
@@ -595,7 +595,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
-                 raise (report l "indexing a register's (single bit) bitfield not supported")
+                 raise (report l __POS__ "indexing a register's (single bit) bitfield not supported")
                else
                  let field_ref =
                    doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
@@ -628,14 +628,14 @@ let doc_exp_lem, doc_let_lem =
         | _ ->
            liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
     | E_vector_append(le,re) ->
-      raise (Reporting_basic.err_unreachable l
-        "E_vector_append should have been rewritten before pretty-printing")
+      raise (Reporting_basic.err_unreachable l __POS__
+       "E_vector_append should have been rewritten before pretty-printing")
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
     | E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e))
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
-       raise (report l "E_for should have been rewritten before pretty-printing")
+       raise (report l __POS__ "E_for should have been rewritten before pretty-printing")
     | E_loop _ ->
-       raise (report l "E_loop should have been rewritten before pretty-printing")
+       raise (report l __POS__ "E_loop should have been rewritten before pretty-printing")
     | E_let(leb,e) ->
        wrap_parens (let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e)
     | E_app(f,args) ->
@@ -659,7 +659,7 @@ let doc_exp_lem, doc_let_lem =
                      | (P_aux (P_var (P_aux (P_id id, _), _), _))
                      | (P_aux (P_id id, _))), _), _),
                      body), _), _), _)), _)), _) -> id, body
-                 | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
+                 | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
                let step = match ord_exp with
                  | E_aux (E_lit (L_aux (L_false, _)), _) ->
                     parens (separate space [string "integerNegate"; expY exp3])
@@ -690,8 +690,8 @@ let doc_exp_lem, doc_let_lem =
                         (prefix 2 1 (group body_lambda) (expN body))
                      )
                  )
-          | _ -> raise (Reporting_basic.err_unreachable l
-             "Unexpected number of arguments for loop combinator")
+          | _ -> raise (Reporting_basic.err_unreachable l __POS__
+            "Unexpected number of arguments for loop combinator")
           end
        | Id_aux (Id (("while" | "until") as combinator), _) ->
           begin
@@ -727,8 +727,8 @@ let doc_exp_lem, doc_let_lem =
                        (parens (prefix 2 1 (group lambda) (expN cond)))
                        (parens (prefix 2 1 (group lambda) (expN body))))
                  )
-            | _ -> raise (Reporting_basic.err_unreachable l
-               "Unexpected number of arguments for loop combinator")
+            | _ -> raise (Reporting_basic.err_unreachable l __POS__
+              "Unexpected number of arguments for loop combinator")
           end
        | Id_aux (Id "early_return", _) ->
           begin
@@ -747,8 +747,8 @@ let doc_exp_lem, doc_let_lem =
                    | _ -> aexp_needed, epp
                in
                if aexp_needed then parens tepp else tepp
-            | _ -> raise (Reporting_basic.err_unreachable l
-               "Unexpected number of arguments for early_return builtin")
+            | _ -> raise (Reporting_basic.err_unreachable l __POS__
+              "Unexpected number of arguments for early_return builtin")
           end
        | _ ->
           begin match destruct_tannot annot with
@@ -783,11 +783,11 @@ let doc_exp_lem, doc_let_lem =
           end
        end
     | E_vector_access (v,e) ->
-      raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+      raise (Reporting_basic.err_unreachable l __POS__
+       "E_vector_access should have been rewritten before pretty-printing")
     | E_vector_subrange (v,e1,e2) ->
-      raise (Reporting_basic.err_unreachable l
-        "E_vector_subrange should have been rewritten before pretty-printing")
+      raise (Reporting_basic.err_unreachable l __POS__
+       "E_vector_subrange should have been rewritten before pretty-printing")
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let ft = typ_of_annot (l,fannot) in
        (match destruct_tannot fannot with
@@ -800,10 +800,10 @@ let doc_exp_lem, doc_let_lem =
              else doc_id_lem id in
            expY fexp ^^ dot ^^ fname
         | _ ->
-           raise (report l "E_field expression with no register or record type"))
+           raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "()"
-    | E_block exps -> raise (report l "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l "Nondet blocks not supported.")
+    | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
+    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
@@ -827,7 +827,7 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
            (* when Env.is_record tid env -> *)
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        wrap_parens (anglebars (space ^^ (align (separate_map
                                         (semi_sp ^^ break 1)
                                         (doc_fexp ctxt recordtyp) fexps)) ^^ space))
@@ -837,14 +837,14 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
            when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
+         | _ ->  raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let start, (len, order, etyp) =
          if is_vector_typ t then vector_start_index t, vector_typ_args_of t
-         else raise (Reporting_basic.err_unreachable l
-           "E_vector of non-vector type") in
+         else raise (Reporting_basic.err_unreachable l __POS__
+          "E_vector of non-vector type") in
        let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
        let start = match nexp_simp start with
          | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i
@@ -870,11 +870,11 @@ let doc_exp_lem, doc_let_lem =
          else (epp,aexp_needed) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update(v,e1,e2) ->
-       raise (Reporting_basic.err_unreachable l
-         "E_vector_update should have been rewritten before pretty-printing")
-    | E_vector_update_subrange(v,e1,e2,e3) ->
-       raise (Reporting_basic.err_unreachable l
+       raise (Reporting_basic.err_unreachable l __POS__
         "E_vector_update should have been rewritten before pretty-printing")
+    | E_vector_update_subrange(v,e1,e2,e3) ->
+       raise (Reporting_basic.err_unreachable l __POS__
+       "E_vector_update should have been rewritten before pretty-printing")
     | E_list exps ->
        brackets (separate_map semi (expN) exps)
     | E_case(e,pexps) ->
@@ -900,7 +900,7 @@ let doc_exp_lem, doc_let_lem =
     | E_app_infix (e1,id,e2) ->
        expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot)))
     | E_var(lexp, eq_exp, in_exp) ->
-       raise (report l "E_vars should have been removed before pretty-printing")
+       raise (report l __POS__ "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
        let epp =
          let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
@@ -928,8 +928,8 @@ let doc_exp_lem, doc_let_lem =
       (match nexp_simp nexp with
         | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
         | _ ->
-          raise (Reporting_basic.err_unreachable l
-            "pretty-printing non-constant sizeof expressions to Lem not supported"))
+          raise (Reporting_basic.err_unreachable l __POS__
+           "pretty-printing non-constant sizeof expressions to Lem not supported"))
     | E_return r ->
       let ta =
         match Util.option_bind (make_printable_type ctxt ctxt.top_env) (Env.get_ret_typ (env_of full_exp)),
@@ -944,8 +944,8 @@ let doc_exp_lem, doc_let_lem =
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint _ -> string "true"
     | E_internal_value _ ->
-      raise (Reporting_basic.err_unreachable l
-        "unsupported internal expression encountered while pretty-printing")
+      raise (Reporting_basic.err_unreachable l __POS__
+       "unsupported internal expression encountered while pretty-printing")
   and if_exp ctxt (elseif : bool) c t e =
     let if_pp = string (if elseif then "else if" else "if") in
     let else_pp = match e with
@@ -977,8 +977,8 @@ let doc_exp_lem, doc_let_lem =
     group (prefix 3 1 (separate space [pipe; doc_pat_lem ctxt false pat;arrow])
                   (group (top_exp ctxt false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
-    raise (Reporting_basic.err_unreachable l
-      "guarded pattern expression should have been rewritten before pretty-printing")
+    raise (Reporting_basic.err_unreachable l __POS__
+     "guarded pattern expression should have been rewritten before pretty-printing")
 
   and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
@@ -987,7 +987,7 @@ let doc_exp_lem, doc_let_lem =
     | LEXP_cast (typ,id) -> doc_id_lem (append_id id "_ref")
     | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps)
     | _ ->
-       raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
+       raise (Reporting_basic.err_unreachable l __POS__ ("doc_lexp_deref_lem: Unsupported lexp"))
              (* expose doc_exp_lem and doc_let *)
   in top_exp, let_exp
 
@@ -1042,8 +1042,8 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
           match nexp_simp start with
           | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
           | _ ->
-            raise (Reporting_basic.err_unreachable Parse_ast.Unknown
-              ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
+            raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+             ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
         with
         | _ -> (Big_int.zero, true) in
       doc_op equals
@@ -1222,7 +1222,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
               fromInterpValuePP ^^ hardline ^^ hardline ^^
                 fromToInterpValuePP ^^ hardline
             else empty)
-    | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
 
 let args_of_typ l env typ =
   let typs = match typ with
@@ -1281,8 +1281,8 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let _ = match guard with
     | None -> ()
     | _ ->
-       raise (Reporting_basic.err_unreachable l
-                "guarded pattern expression should have been rewritten before pretty-printing") in
+       raise (Reporting_basic.err_unreachable l __POS__
+               "guarded pattern expression should have been rewritten before pretty-printing") in
   group (prefix 3 1
     (separate space [doc_id_lem id; patspp; equals])
     (doc_fun_body_lem ctxt (bind exp)))
@@ -1335,8 +1335,8 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
                                        string o;
                                        string "[]"]))
            ^/^ hardline
-         else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
-       else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) *)
+         else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
+       else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
@@ -1370,8 +1370,8 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
     let i, j = match fr with
     | BF_aux (BF_single i, _) -> (i, i)
     | BF_aux (BF_range (i, j), _) -> (i, j)
-    | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
-        ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
+    | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+       ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
     let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
     (* TODO Assumes normalised, decreasing bitvector slices; however, since
        start indices or indexing order do not appear in Lem type annotations,
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index c0b3440d..a90c2bcd 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -257,7 +257,7 @@ let print_err fatal verb_loc l m1 m2 =
 
 type error =
   | Err_general of Parse_ast.l * string
-  | Err_unreachable of Parse_ast.l * string
+  | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
   | Err_todo of Parse_ast.l * string
   | Err_syntax of Lexing.position * string
   | Err_syntax_locn of Parse_ast.l * string
@@ -267,7 +267,7 @@ type error =
 
 let dest_err = function
   | Err_general (l, m) -> ("Error", false, Loc l, m)
-  | Err_unreachable (l, m) -> ("Internal error: Unreachable code", false, Loc l, m)
+  | Err_unreachable (l, (file, line, _, _), m) -> ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m)
   | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
   | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
   | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
@@ -279,7 +279,7 @@ exception Fatal_error of error
 
 (* Abbreviations for the very common cases *)
 let err_todo l m = Fatal_error (Err_todo (l, m))
-let err_unreachable l m = Fatal_error (Err_unreachable (l, m))
+let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
 let err_general l m = Fatal_error (Err_general (l, m))
 let err_typ l m = Fatal_error (Err_type (l,m))
 let err_typ_dual l1 l2 m = Fatal_error (Err_type_dual (l1,l2,m))
diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli
index d2978389..39ac32f0 100644
--- a/src/reporting_basic.mli
+++ b/src/reporting_basic.mli
@@ -80,7 +80,7 @@ type error =
 
   (** Unreachable errors should never be thrown. It means that some
       code was excuted that the programmer thought of as unreachable *)
-  | Err_unreachable of Parse_ast.l * string
+  | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
 
   (** [Err_todo] indicates that some feature is unimplemented; it should be built using [err_todo]. *)
   | Err_todo of Parse_ast.l * string
@@ -99,8 +99,8 @@ val err_todo : Parse_ast.l -> string -> exn
 (** [err_general l m] is an abreviatiation for [Fatal_error (Err_general (b, l, m))] *)
 val err_general : Parse_ast.l -> string -> exn
 
-(** [err_unreachable l m] is an abreviatiation for [Fatal_error (Err_unreachable (b, l, m))] *)
-val err_unreachable : Parse_ast.l -> string -> exn
+(** [err_unreachable l __POS__ m] is an abreviatiation for [Fatal_error (Err_unreachable (l, __POS__, m))] *)
+val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
 
 (** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
 val err_typ : Parse_ast.l -> string -> exn
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 15f100fd..a7505ca7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -319,8 +319,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
   | E_var (lexp, e1, e2) ->
      rewrap (E_var (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
-  | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
-  | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced")
+  | E_internal_return _ -> raise (Reporting_basic.err_unreachable l __POS__ "Internal return found before it should have been introduced")
+  | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l __POS__ " Internal plet found before it should have been introduced")
   | _ -> rewrap exp
 
 let rewrite_let rewriters (LB_aux(letbind,(l,annot))) =
@@ -358,7 +358,7 @@ let rewrite_def rewriters d = match d with
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
-  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
+  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
 
 let rewrite_defs_base rewriters (Defs defs) =
   let rec rewrite ds = match ds with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e818c0e2..8a6b43a0 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -168,16 +168,16 @@ let vector_string_to_bit_list l lit =
     | 'D' -> ['1';'1';'0';'1']
     | 'E' -> ['1';'1';'1';'0']
     | 'F' -> ['1';'1';'1';'1']
-    | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "hexchar_to_binlist given unrecognized character") in
 
   let s_bin = match lit with
     | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex)))
     | L_bin s_bin -> explode s_bin
-    | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "s_bin given non vector literal") in
 
   List.map (function '0' -> L_aux (L_zero, gen_loc l)
                    | '1' -> L_aux (L_one, gen_loc l)
-                   | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) "binary had non-zero or one")) s_bin
+                   | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) __POS__ "binary had non-zero or one")) s_bin
 
 let find_used_vars exp =
   (* Overapproximates the set of used identifiers, but for the use cases below
@@ -479,7 +479,7 @@ let rewrite_sizeof (Defs defs) =
                 a variable in scope. It can't be an existential because the assert rules that out. *)
              | None -> annot_exp (E_id (id_of_kid (orig_kid kid))) l env (atom_typ (nvar (orig_kid kid)))
              | _ ->
-                raise (Reporting_basic.err_unreachable l
+                raise (Reporting_basic.err_unreachable l __POS__
                                                        ("failed to infer nexp for type variable " ^ string_of_kid kid ^
                                                           " of function " ^ string_of_id f))
            end in
@@ -607,7 +607,7 @@ let rewrite_sizeof (Defs defs) =
                  raise (Reporting_basic.err_todo l
                                                  "rewriting as- or id-patterns for sizeof expressions not yet implemented")
               | _ ->
-                 raise (Reporting_basic.err_unreachable l
+                 raise (Reporting_basic.err_unreachable l __POS__
                                                         "unexpected pattern while rewriting function parameters for sizeof expressions"))
           | ptyp ->
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in
@@ -764,7 +764,7 @@ let remove_vector_concat_pat pat =
         | _ ->
            raise
              (Reporting_basic.err_unreachable
-                l "name_vector_concat_elements: Non-vector in vector-concat pattern") in
+                l __POS__ "name_vector_concat_elements: Non-vector in vector-concat pattern") in
       P_vector_concat (List.map aux pats) in
     {id_pat_alg with p_vector_concat = p_vector_concat} in
 
@@ -811,7 +811,7 @@ let remove_vector_concat_pat pat =
                      then Big_int.sub (Big_int.add start length) (Big_int.of_int 1)
                      else Big_int.add (Big_int.sub start length) (Big_int.of_int 1))
           | _ ->
-            raise (Reporting_basic.err_unreachable (fst rannot')
+            raise (Reporting_basic.err_unreachable (fst rannot') __POS__
               ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
          let rec aux typ_opt (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) =
            let ctyp = Env.base_typ_of (env_of_annot cannot) (typ_of_annot cannot) in
@@ -826,7 +826,7 @@ let remove_vector_concat_pat pat =
                 else
                   raise
                     (Reporting_basic.err_unreachable
-                       l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in
+                       l __POS__ ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in
            (match p with
             (* if we see a named vector pattern, remove the name and remember to
               declare it later *)
@@ -935,7 +935,7 @@ let remove_vector_concat_pat pat =
           | _, _ ->
             (*if is_last then*) acc @ [wild Big_int.zero]
         else raise
-          (Reporting_basic.err_unreachable l
+          (Reporting_basic.err_unreachable l __POS__
             ("remove_vector_concats: Non-vector in vector-concat pattern " ^
               string_of_typ (typ_of_annot annot))) in
 
@@ -1165,7 +1165,7 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
   let typ = pat_typ_of p_aux in
   match pat with
   | P_lit lit -> rewrap (E_lit lit)
-  | P_wild -> raise (Reporting_basic.err_unreachable l
+  | P_wild -> raise (Reporting_basic.err_unreachable l __POS__
       "pat_to_exp given wildcard pattern")
   | P_or(pat1, pat2) -> (* todo: insert boolean or *) pat_to_exp pat1 
   | P_not(pat) -> (* todo: insert boolean not *) pat_to_exp pat
@@ -1253,7 +1253,7 @@ let rewrite_guarded_clauses l cs =
       | ((pat,guard,body,annot) as c) :: cs ->
           group_aux (remove_wildcards "g__" pat, [c], annot) [] cs
       | _ ->
-          raise (Reporting_basic.err_unreachable l
+          raise (Reporting_basic.err_unreachable l __POS__
             "group given empty list in rewrite_guarded_clauses") in
     let add_group cs groups = (if_pexp (groups @ fallthrough) cs) :: groups in
     List.fold_right add_group groups []
@@ -1265,7 +1265,7 @@ let rewrite_guarded_clauses l cs =
         let (Pat_aux (_,annot)) = pexp in
         (pat, body, annot)
     | [] ->
-        raise (Reporting_basic.err_unreachable l
+        raise (Reporting_basic.err_unreachable l __POS__
             "if_pexp given empty list in rewrite_guarded_clauses"))
   and if_exp fallthrough current_pat = (function
     | (pat,guard,body,annot) :: ((pat',guard',body',annot') as c') :: cs ->
@@ -1289,7 +1289,7 @@ let rewrite_guarded_clauses l cs =
               fix_eff_exp (annot_exp (E_if (exp,body,else_exp)) (fst annot) (env_of exp) (typ_of body))
           | _, _ -> body)
     | [] ->
-        raise (Reporting_basic.err_unreachable l
+        raise (Reporting_basic.err_unreachable l __POS__
             "if_exp given empty list in rewrite_guarded_clauses")) in
   group [] cs
 
@@ -1424,7 +1424,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
       let start_idx = match start with
       | Nexp_aux (Nexp_constant s, _) -> s
       | _ ->
-        raise (Reporting_basic.err_unreachable l
+        raise (Reporting_basic.err_unreachable l __POS__
           "guard_bitvector_pat called on pattern with non-constant start index") in
       let add_bit_pat (idx, current, guards, dls) pat =
         let idx' =
@@ -1732,9 +1732,9 @@ let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) =
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
           let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
           (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot))))
-       | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
+       | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
      end
-  | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
 
 let updates_vars exp =
   let e_assign ((_, lexp), (u, exp)) =
@@ -2098,7 +2098,7 @@ let rewrite_defs_early_return (Defs defs) =
 
 let swaptyp typ (l,tannot) = match destruct_tannot tannot with
   | Some (env, typ', eff) -> (l, mk_tannot env typ eff)
-  | _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation")
+  | _ -> raise (Reporting_basic.err_unreachable l __POS__ "swaptyp called with empty type annotation")
 
 let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) =
   let pat,guard,exp,pannot = destruct_pexp pexp in
@@ -2175,7 +2175,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
            let pat, _, exp, _ = destruct_pexp pexp in
            env_of exp, pat_typ_of pat, typ_of exp
         | _ ->
-           raise (Reporting_basic.err_unreachable l
+           raise (Reporting_basic.err_unreachable l __POS__
              "rewrite_split_fun_constr_pats: empty auxiliary function")
       in
       let eff = List.fold_left
@@ -2235,7 +2235,7 @@ let rewrite_fix_val_specs (Defs defs) =
        begin
          try Env.get_val_spec id env with
          | _ ->
-            raise (Reporting_basic.err_unreachable (Parse_ast.Unknown)
+            raise (Reporting_basic.err_unreachable (Parse_ast.Unknown) __POS__
               ("No val spec found for " ^ string_of_id id))
        end
   in
@@ -2665,7 +2665,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
      let body = body (annot_exp (E_id id) l env typ) in
      fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body))
   | None ->
-     raise (Reporting_basic.err_unreachable l "no type information")
+     raise (Reporting_basic.err_unreachable l __POS__ "no type information")
 
 
 let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list -> 'a exp) : 'a exp = 
@@ -2961,7 +2961,7 @@ let rewrite_defs_internal_lets =
     | LEXP_id id -> P_aux (P_id id, annot)
     | LEXP_cast (typ, id) -> add_p_typ typ (P_aux (P_id id, annot))
     | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
-    | _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in
+    | _ -> raise (Reporting_basic.err_unreachable l __POS__ "unexpected local lexp") in
 
   let e_let (lb,body) =
     match lb with
@@ -3590,7 +3590,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp =
          match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with
            | None, _ | _, None ->
-              raise (Reporting_basic.err_unreachable el "Could not determine loop bounds")
+              raise (Reporting_basic.err_unreachable el __POS__ "Could not determine loop bounds")
            | Some (kids1, constr1, n1), Some (kids2, constr2, n2) ->
               let kids = kids1 @ kids2 in
               let constr = nc_and constr1 constr2 in
@@ -3696,7 +3696,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
              let pannot = (l, mk_tannot (env_of exp) (typ_of exp) (effect_of exp)) in
              Pat_aux (Pat_exp (pat, exp), pannot)
            | Pat_when _ ->
-             raise (Reporting_basic.err_unreachable l
+             raise (Reporting_basic.err_unreachable l __POS__
                "Guarded patterns should have been rewritten already") in
          let ps = List.map rewrite_pexp ps in
          let expaux = if is_case then E_case (e1, ps) else E_try (e1, ps) in
@@ -3710,7 +3710,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          | Local (_, typ) ->
             add_p_typ typ (annot_pat (P_id id) pl env typ)
          | _ ->
-            raise (Reporting_basic.err_unreachable pl
+            raise (Reporting_basic.err_unreachable pl __POS__
               ("Failed to look up type of variable " ^ string_of_id id)) in
        if effectful exp then
          Same_vars (E_aux (E_assign (lexp,vexp),annot))
@@ -3756,7 +3756,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        | LEXP_aux (LEXP_cast (typ, id), _) ->
           unaux_pat (add_p_typ typ (annot_pat (P_id id) l env (typ_of v))), typ
        | _ ->
-         raise (Reporting_basic.err_unreachable l
+         raise (Reporting_basic.err_unreachable l __POS__
            "E_var with a lexp that is not a variable") in
      let lb = fix_eff_lb (annot_letbind (paux, v) l env typ) in
      let exp = fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body)) in
@@ -4263,7 +4263,7 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
     in aux [] res_pats res_pats'
   in
   let inconsistent () =
-    raise (Reporting_basic.err_unreachable (fst ann)
+    raise (Reporting_basic.err_unreachable (fst ann) __POS__
              ("Inconsistency during exhaustiveness analysis with " ^
                  string_of_rp res_pat))
   in
@@ -4338,12 +4338,12 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
         rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
   end
   | P_record _ ->
-     raise (Reporting_basic.err_unreachable (fst ann)
+     raise (Reporting_basic.err_unreachable (fst ann) __POS__
               "Record pattern not supported")
   | P_vector _
   | P_vector_concat _
   | P_string_append _ ->
-     raise (Reporting_basic.err_unreachable (fst ann)
+     raise (Reporting_basic.err_unreachable (fst ann) __POS__
               "Found pattern that should have been rewritten away in earlier stage")
 
   (*in let _ = printprefix := String.sub (!printprefix) 0 (String.length !printprefix - 2)
@@ -4359,7 +4359,7 @@ let process_pexp env =
   | Pat_aux (Pat_exp (p,_),_) -> 
      List.concat (List.map (remove_clause_from_pattern ctx p) rps)
   | Pat_aux (Pat_when _,(l,_)) ->
-     raise (Reporting_basic.err_unreachable l
+     raise (Reporting_basic.err_unreachable l __POS__
               "Guarded pattern should have been rewritten away")
 
 (* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
@@ -4416,7 +4416,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
   let id,fcl_ann =
     match fcls with
     | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann
-    | [] -> raise (Reporting_basic.err_unreachable (fst f_ann)
+    | [] -> raise (Reporting_basic.err_unreachable (fst f_ann) __POS__
                  "Empty function")
   in
   let env = env_of_annot fcl_ann in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index b459610d..f6da074c 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -594,7 +594,7 @@ let def_of_component graph defset comp =
        | DEF_fundef fundef -> [fundef]
        | DEF_internal_mutrec fundefs -> fundefs
        | _ ->
-          raise (Reporting_basic.err_unreachable (def_loc def)
+          raise (Reporting_basic.err_unreachable (def_loc def) __POS__
             "Trying to merge non-function definition with mutually recursive functions") in
      let fundefs = List.concat (List.map get_fundefs defs) in
      print_dot graph (List.map (fun fd -> string_of_id (id_of_fundef fd)) fundefs);
diff --git a/src/type_check.ml b/src/type_check.ml
index be6950e9..a731130a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2073,17 +2073,17 @@ let destruct_vec_typ l env typ =
 
 let env_of_annot (l, tannot) = match tannot with
   | Some ((env, _, _),_) -> env
-  | None -> raise (Reporting_basic.err_unreachable l "no type annotation")
+  | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
 
 let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
 let typ_of_annot (l, tannot) = match tannot with
   | Some ((_, typ, _), _) -> typ
-  | None -> raise (Reporting_basic.err_unreachable l "no type annotation")
+  | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
 
 let env_of_annot (l, tannot) = match tannot with
   | Some ((env, _, _), _) -> env
-  | None -> raise (Reporting_basic.err_unreachable l "no type annotation")
+  | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
 
 let typ_of (E_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
@@ -2111,7 +2111,7 @@ let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
 let expected_typ_of (l, tannot) = match tannot with
   | Some ((_, _, _), exp_typ) -> exp_typ
-  | None -> raise (Reporting_basic.err_unreachable l "no type annotation")
+  | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
 
 (* Flow typing *)
 
@@ -4414,7 +4414,7 @@ let mk_synonym typq typ =
                                       ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
 
 let check_kinddef env (KD_aux (kdef, (l, _))) =
-  let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
+  let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in
   match kdef with
   | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_int, _)]),_) as kind), id, nmscm, nexp) ->
      [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
@@ -4423,7 +4423,7 @@ let check_kinddef env (KD_aux (kdef, (l, _))) =
 
 let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
   fun env (TD_aux (tdef, (l, _))) ->
-  let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in
+  let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
   match tdef with
   | TD_abbrev (id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ) env
@@ -4456,7 +4456,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
 
 and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   fun env def ->
-  let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Case") in
+  let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Case") in
   match def with
   | DEF_kind kdef -> check_kinddef env kdef
   | DEF_type tdef -> check_typedef env tdef
@@ -4483,7 +4483,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
      [DEF_reg_dec (DEC_aux (DEC_config (id, typ, checked_exp), (l, Some ((env, typ, no_effect), Some typ))))], env
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
-  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
+  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Scattered given to type checker")
 
 and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
   fun env (Defs defs) ->