Correctly unify types with default declarations and across if blocks for introduced variables.

2 files changed, 25 insertions, 9 deletions

diff --git a/src/test/test4.sail b/src/test/test4.sail
index 50f3fa71..36cb271a 100644
--- a/src/test/test4.sail
+++ b/src/test/test4.sail
@@ -24,7 +24,7 @@ function unit good2 ((nat)  RA ) =
    yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *)
 function unit bad ((bit[1])  RA ) =
 {
-  LOG(0) := "bad";
+  LOG(0) := "oldbad";
   (nat) x := GPR[RA];
 }
 
@@ -42,7 +42,7 @@ let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ]
    expression *)
 function unit bad2 ((bit[1])  RA ) =
 {
-  LOG(0) := "bad2";
+  LOG(0) := "oldbad2";
   (nat) x := DCR[RA];
 }
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e2af4970..3f7ca294 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -918,12 +918,28 @@ let resolve_constraints a = a
 
 let check_tannot l annot constraints efs = 
   match annot with
-  | Some((params,t),tag,cs,e) -> 
-    effects_eq l efs e;
-    let params = Envmap.to_list (t_remove_unifications (Envmap.from_list params) t) in
+    | Some((params,t),tag,cs,e) -> 
+      ignore(effects_eq l efs e);
+      let params = Envmap.to_list (t_remove_unifications (Envmap.from_list params) t) in
     (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *)
-    Some((params,t),tag,cs,e)
-  | None -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation")
-
+      Some((params,t),tag,cs,e)
+    | None -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation")
+      
 
-let tannot_merge l denv t_older t_newer = t_newer
+let tannot_merge l denv t_older t_newer = 
+  match t_older,t_newer with
+    | None,None -> None
+    | None,_ -> t_newer
+    | _,None -> t_older
+    | Some((ps_o,t_o),tag_o,cs_o,ef_o),Some((ps_n,t_n),tag_n,cs_n,ef_n) -> 
+      match tag_o,tag_n with
+	| Default,tag -> 
+	  (match t_n.t with
+	    | Tuvar _ -> let t_o,cs_o,ef_o = subst ps_o t_o cs_o ef_o in
+			 let t,_ = type_consistent l denv t_n t_o in
+			 Some(([],t),tag_n,cs_o,ef_o)
+	    | _ -> t_newer)
+	| Emp_local, Emp_local -> 
+	  let t,cs_b = type_consistent l denv t_n t_o in
+	  Some(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n)
+	| _,_ -> t_newer