Fix issue where statements in blocks had incorrect environments

3 files changed, 9 insertions, 1 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 74f252f4..363761f5 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2755,6 +2755,9 @@ let rewrite_check_annot =
     try
       prerr_endline ("CHECKING: " ^ string_of_exp exp ^ " : " ^ string_of_typ (typ_of exp));
       let _ = check_exp (env_of exp) (strip_exp exp) (typ_of exp) in
+      (if not (alpha_equivalent (env_of exp) (typ_of exp) (Env.expand_synonyms (env_of exp) (typ_of exp)))
+       then raise (Reporting_basic.err_typ Parse_ast.Unknown "Found synonym in annotation")
+       else ());
       exp
     with
       Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
diff --git a/src/type_check.ml b/src/type_check.ml
index 2260416d..6c158f9e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1994,7 +1994,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   match (exp_aux, typ_aux) with
   | E_block exps, _ ->
      begin
-       let rec check_block l env exps typ = match exps with
+       let rec check_block l env exps typ =
+         let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
+         let annot_exp exp typ = annot_exp_effect exp typ no_effect in
+         match exps with
          | [] -> typ_equality l env typ unit_typ; []
          | [exp] -> [crule check_exp env exp typ]
          | (E_aux (E_assign (lexp, bind), _) :: exps) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 99385b31..355740dc 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -231,6 +231,8 @@ val string_of_uvar : uvar -> string
 
 val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option
 
+val alpha_equivalent : Env.t -> typ -> typ -> bool
+
 (* Throws Invalid_argument if the argument is not a E_app expression *)
 val instantiation_of : tannot exp -> uvar KBindings.t