Fix an unnecessary cast insertion on assignments

2 files changed, 12 insertions, 4 deletions

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index ccaceec7..dd0f7afd 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4207,10 +4207,16 @@ let add_bitvector_casts (Defs defs) =
          E_aux (E_if (e1,e2',e3), ann)
       | E_return e' ->
          E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
-      | E_assign (LEXP_aux (lexp,lexp_annot),e') ->
-         E_aux (E_assign (LEXP_aux (lexp,lexp_annot),
-                          make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e'))
-                            (typ_of_annot lexp_annot) e'),ann)
+      | E_assign (LEXP_aux (_,lexp_annot) as lexp,e') -> begin
+         (* The type in the lexp_annot might come from e' rather than being the
+            type of the storage, so ask the type checker what it really is. *)
+         match infer_lexp (env_of_annot lexp_annot) (strip_lexp lexp) with
+         | LEXP_aux (_,lexp_annot') ->
+            E_aux (E_assign (lexp,
+                             make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e'))
+                               (typ_of_annot lexp_annot') e'),ann)
+         | exception _ -> E_aux (e,ann)
+        end
       | E_id id -> begin
         let env = env_of_annot ann in
         match Env.lookup_id id env with
diff --git a/src/type_check.mli b/src/type_check.mli
index ce5324d1..f417c65d 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -297,6 +297,8 @@ val infer_exp : Env.t -> unit exp -> tannot exp
 
 val infer_pat : Env.t -> unit pat -> tannot pat * Env.t * unit exp list
 
+val infer_lexp : Env.t -> unit lexp -> tannot lexp
+
 val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp
 
 val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t