Added a large test case to the test-suite

Commented out some buggy re-sugaring logic from pretty_print_common
where it re-sugared vectors incorrectly

Fixed a bug where the type checker forgot to preserve type signatures
in top-level letbinds

2 files changed, 12 insertions, 4 deletions

diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 3699e1ac..5c3339c6 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -125,6 +125,7 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *)
   (* Special case simple vectors to improve legibility
    * XXX we assume big-endian here, as usual *)
+(*
   | Typ_app(Id_aux (Id "vector", _), [
       Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
       Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
@@ -159,6 +160,7 @@ let doc_typ, doc_atomic_typ, doc_nexp =
       Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
       Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
     (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n)))
+ *)
   | Typ_app(Id_aux (Id "range", _), [
     Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
     Typ_arg_aux(Typ_arg_nexp m, _);]) ->
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 4093e84c..ff9e4313 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -1470,11 +1470,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
    or throws a type error if the coercion cannot be performed. *)
 and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
+  let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
   let rec try_casts m = function
     | [] -> typ_error l ("No valid casts:\n" ^ m)
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
-        try crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ with
+        try
+          let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in
+          annot_exp (E_cast (typ, checked_cast)) typ
+        with
         | Type_error (_, m) -> try_casts m casts
       end
   in
@@ -1494,13 +1498,15 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
    throws a unification error *)
 and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
+  let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
   let rec try_casts m = function
     | [] -> unify_error l ("No valid casts resulted in unification:\n" ^ m)
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification");
         try
-          let annotated_exp = irule infer_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) in
-          annotated_exp, unify l env typ (typ_of annotated_exp)
+          let inferred_cast = irule infer_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) in
+          let ityp = typ_of inferred_cast in
+          annot_exp (E_cast (ityp, inferred_cast)) ityp, unify l env typ ityp
         with
         | Type_error (_, m) -> try_casts m casts
         | Unification_error (_, m) -> try_casts m casts
@@ -1849,7 +1855,7 @@ let check_letdef env (LB_aux (letbind, (l, _))) =
     | LB_val_implicit (P_aux (P_typ (typ_annot, pat), _), bind) ->
        let checked_bind = crule check_exp env (strip_exp bind) typ_annot in
        let tpat, env = bind_pat env (strip_pat pat) typ_annot in
-       DEF_val (LB_aux (LB_val_implicit (tpat, checked_bind), (l, None))), env
+       DEF_val (LB_aux (LB_val_implicit (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot))), checked_bind), (l, None))), env
     | LB_val_implicit (pat, bind) ->
        let inferred_bind = irule infer_exp env (strip_exp bind) in
        let tpat, env = bind_pat env (strip_pat pat) (typ_of inferred_bind) in