summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2019-02-05 17:27:52 +0000
committerBrian Campbell2019-02-05 17:28:07 +0000
commit2e6b258fee6929e060a6c55c889fd479ee543fc3 (patch)
tree97ebd718292cd899f0caf9a2297b41fc137e99e6 /src
parentf1af348146a5810d1a21ee272d1799adfe2d545b (diff)
Use more general types for lexps in the internal lets rewriting pass
This reduces the amount of unnecessary complex existentials that appear during rewriting.
Diffstat (limited to 'src')
-rw-r--r--src/rewrites.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8fa90643..c6406639 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2904,7 +2904,14 @@ let rewrite_defs_internal_lets =
(* Rewrite assignments to local variables into let bindings *)
let (lhs, rhs) = rewrite_lexp_to_rhs le in
let (LEXP_aux (_, lannot)) = lhs in
- let ltyp = typ_of_annot lannot in
+ let ltyp = typ_of_annot
+ (* The type in the lannot might come from exp rather than being the
+ type of the storage, so ask the type checker what it really is. *)
+ (match infer_lexp (env_of_annot lannot) (strip_lexp lhs) with
+ | LEXP_aux (_,lexp_annot') -> lexp_annot'
+ | _ -> lannot
+ | exception _ -> lannot)
+ in
let rhs = add_e_cast ltyp (rhs exp) in
E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs), annot), body)
| LB_aux (LB_val (pat,exp'),annot') ->