Adding better support for unspecified values in indexed vectors

Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches

7 files changed, 77 insertions, 35 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index c6c08c67..b95bf279 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -341,6 +341,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
       (match to_ast_fexps false k_env exps with
       | Some(fexps) -> E_record(fexps)
       | None -> E_block(List.map (to_ast_exp k_env) exps))
+    | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env) exps)
     | Parse_ast.E_id(id) -> E_id(to_ast_id id)
     | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit)
     | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp)
diff --git a/src/parser.mly b/src/parser.mly
index 0ee7093d..e1647642 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -528,6 +528,8 @@ npats:
 atomic_exp:
   | Lcurly semi_exps Rcurly
     { eloc (E_block $2) }
+  | Nondet Lcurly semi_exps Rcurly
+    { eloc (E_nondet $3) }
   | id
     { eloc (E_id($1)) }
   | lit
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 10cd2b68..0544c573 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -107,6 +107,7 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_wreg -> "BE_wreg"
     | BE_rmem -> "BE_rmem"
     | BE_wmem -> "BE_wmem"
+    | BE_barr -> "BE_barr"
     | BE_undef -> "BE_undef"
     | BE_unspec -> "BE_unspec"
     | BE_nondet -> "BE_nondet") ^ " " ^
@@ -208,6 +209,7 @@ let rec pp_format_t t =
     | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
     | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
     | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
+    | Toptions _ -> "(T_var \"fresh_v\" Unknown)"
 and pp_format_targ = function
   | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
   | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
@@ -224,6 +226,8 @@ and pp_format_n n =
     | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
     | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
     | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
+    | Nneg_inf -> "(Ne_unary Ne_inf)"
+    | Npow _ -> "power_not_implemented"
 and pp_format_e e = 
   "(Effect_aux " ^
   (match e.effect with
@@ -260,7 +264,7 @@ let rec pp_format_nes nes =
        | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> 
 	 "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])"
-       | InS(_,{nexp = Nuvar _},ns)  ->  
+       | InS(_,_,ns)  ->  
 	 "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"
        | CondCons(_,nes_c,nes_t) -> 
          "(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"
@@ -319,6 +323,10 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       kwd "(E_block" 
       (list_pp pp_semi_lem_exp pp_lem_exp) exps
       kwd ")" pp_lem_l l pp_annot annot
+    | E_nondet(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]"
+      kwd "(E_nondet" 
+      (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      kwd ")" pp_lem_l l pp_annot annot
     | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot
     | E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
     | E_cast(typ,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
@@ -369,11 +377,12 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
     | E_internal_exp (l, Base((_,t),_,_,_)) ->
       (match t.t with
 	| Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
-	  match r.nexp with
-	    | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" 
-	                               kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)))
-    (* Should be unreachable *)
-    | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false
+	  (match r.nexp with
+	  | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" 
+	                               kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e))
+          | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
+        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector"))
+    | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ ->  raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload")
   in
   print_e ppf e
 
@@ -549,6 +558,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
+  | BE_barr -> "barr"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")
@@ -788,6 +798,7 @@ let doc_exp, doc_let =
   | E_block exps ->
       let exps_doc = separate_map (semi ^^ hardline) exp exps in
       surround 2 1 lbrace exps_doc rbrace
+(* XXX Need to add E_nondet, not sure how to put the nondet in front of the block *)
   | E_id id -> doc_id id
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index 79f3bf23..a861b65c 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -17,6 +17,7 @@ let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check
 
 let (bit[3]) indexed = [0=1,1=1,2=0]
 let (bit[50]) partial = [0 = 0, 5=1, 32=0; default = 0]
+let (bit[50]) partial_unspec = [0=0, 4=0, 7=1, 49=1]
 
 function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
 and decode x = match_success := x
diff --git a/src/type_check.ml b/src/type_check.ml
index 739cb6d6..73055541 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -42,7 +42,6 @@ let rec fields_to_rec fields rec_env =
 	  | None -> fields_to_rec fields rec_env
       else fields_to_rec fields rec_env
 
-(*No checks necessary, unlike conversion in initial_check*)
 let kind_to_k (K_aux((K_kind baseks),l)) =
   let bk_to_k (BK_aux(bk,l')) =
     match bk with
@@ -65,6 +64,7 @@ let rec typ_to_t (Typ_aux(typ,l)) =
     | Typ_fn (ty1,ty2,e) -> {t = Tfn (typ_to_t ty1,typ_to_t ty2,aeffect_to_effect e)}
     | Typ_tup(tys) -> {t = Ttup (List.map typ_to_t tys) }
     | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) }
+    | Typ_wild -> new_t ()
 and typ_arg_to_targ (Typ_arg_aux(ta,l)) = 
   match ta with
     | Typ_arg_nexp n -> TA_nexp (anexp_to_nexp n)
@@ -246,14 +246,14 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
       let (fst,lst) = (List.hd is),(List.hd (List.rev is)) in
       let inc_or_dec = 
 	if fst < lst then
-	  (let is_increasing = List.fold_left 
+	  (let _ = List.fold_left 
 	     (fun i1 i2 -> if i1 < i2 then i2 
-	       else typ_error l "Indexed vector access was inconsistently increasing") fst (List.tl is) in
+	       else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in
 	   true)
 	else if lst < fst then
-	  (let is_decreasing = List.fold_left
+	  (let _ = List.fold_left
 	     (fun i1 i2 -> if i1 > i2 then i2
-	       else typ_error l "Indexed vector access was inconsistently decreasing") fst (List.tl is) in
+	       else typ_error l "Indexed vector pattern was inconsistently decreasing") fst (List.tl is) in
 	   false)
 	else typ_error l "Indexed vector cannot be determined as either increasing or decreasing" in
       let base,rise = new_n (), new_n () in
@@ -339,10 +339,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
   let Env(d_env,t_env) = envs in
   let rebuild annot = E_aux(e,(l,annot)) in
   match e with
-    | E_block(exps) -> 
+    | E_block exps -> 
       let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in
       (E_aux(E_block(exps'),(l,annot')),t, t_env',sc,ef)
-    | E_id(id) -> 
+    | E_nondet exps ->
+      let checked_exps = List.map (check_exp envs unit_t) exps in
+      let (exps',annot',t_env',sc,t,ef) = check_block t_env envs expect_t exps in (* WRONG WRONG, place holder. Needs to be a map, intersection of envs, and each should return unit *)
+      (E_aux(E_nondet(exps'),(l,annot')),t,t_env,sc,ef)
+    | E_id id -> 
       let i = id_to_string id in
       (match Envmap.apply t_env i with
       | Some(Base((params,t),Constructor,cs,ef)) ->
@@ -661,21 +665,28 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         | _ -> new_t (),new_n (), new_n () in
       let first,last = fst (List.hd eis), fst (List.hd (List.rev eis)) in
       let is_increasing = first <= last in
-      let es,cs,effect,_ = (List.fold_right 
-			      (fun ((i,e),c,ef) (es,cs,effect,prev) -> 
+      let es,cs,effect,contains_skip,_ = (List.fold_right 
+			      (fun ((i,e),c,ef) (es,cs,effect,skips,prev) -> 
 				(*let _ = Printf.printf "Checking increasing %b %i %i\n" is_increasing prev i in*)
-				if is_increasing 
-				then if prev >= i then (((i,e)::es),(c@cs),union_effects ef effect,i) 
-				  else (typ_error l "Indexed vector is not consistently increasing")
-				else if i >= prev then (((i,e)::es),(c@cs),union_effects ef effect,i) 
-				else (typ_error l "Indexed vector is not consistently decreasing"))
+                                let (esn, csn, efn) = (((i,e)::es), (c@cs), union_effects ef effect) in
+				if (is_increasing && prev > i)
+				then (esn,csn,efn,(((prev-i) > 1) || skips),i)
+                                else if prev < i 
+                                then (esn,csn,efn,(((i-prev) > 1) || skips),i)
+                                else if i = prev
+                                then (typ_error l ("Indexed vector contains a duplicate definition of index " ^ (string_of_int i)))
+                                else (typ_error l ("Indexed vector is not consistently " ^ (if is_increasing then "increasing" else "decreasing"))))
 			      (List.map (fun (i,e) -> let (e,_,_,cs,eft) = (check_exp envs item_t e) in ((i,e),cs,eft))
-				 eis) ([],[],pure_e,last)) in
-      let (default',fully_enumerate,cs_d,ef_d) = match default with
-	| Def_val_empty -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e)
-	| Def_val_dec e -> let (de,t,_,cs_d,ef_d) = (check_exp envs item_t e) in
-			   (*Check that ef_d doesn't write to memory or registers? *)
-			   (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in
+				 eis) ([],[],pure_e,false,(if is_increasing then (last+1) else (last-1)))) in
+      let (default',fully_enumerate,cs_d,ef_d) = match (default,contains_skip) with
+	| (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e)
+        | (Def_val_empty,true)  -> 
+          let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in
+          (Def_val_aux(Def_val_dec ( (E_aux( E_lit( L_aux(L_undef, l)), (l, (Base(([],item_t),Emp_local,[],ef)))))),
+                       (l,Base(([],item_t),Emp_local,[],pure_e))),false,[],ef)
+	| (Def_val_dec e,_) -> let (de,t,_,cs_d,ef_d) = (check_exp envs item_t e) in
+			       (*Check that ef_d doesn't write to memory or registers? *)
+			       (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in
       let (base_bound,length_bound,cs_bounds) = 
 	if fully_enumerate
 	then ({nexp=Nconst (big_int_of_int first)},{nexp = Nconst (big_int_of_int (List.length eis))},[])
@@ -847,6 +858,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 			 match lookup_field_type i r with
 			   | NoTyp -> 
 			     typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i)
+                           | Overload _ ->  raise (Reporting_basic.err_unreachable l "Field given overload tannot")
 			   | Base((params,et),tag,cs,ef) ->
 			     let et,cs,_ = subst params et cs ef in
 			     let (e,t',_,c,ef) = check_exp envs et exp in
@@ -866,6 +878,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 		    let i = id_to_string id in
 		    match lookup_field_type i r with
 		      | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+                      | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		      | Base((params,et),tag,cs,ef) ->
 			let et,cs,_ = subst params et cs ef in
 			let (e,t',_,c,ef) = check_exp envs et exp in
@@ -892,6 +905,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 			 match lookup_field_type fi r with
 			   | NoTyp -> 
 			     typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi)
+                           | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 			   | Base((params,et),tag,cs,ef) ->
 			     let et,cs,_ = subst params et cs ef in
 			     let (e,t',_,c,ef) = check_exp envs et exp in
@@ -911,6 +925,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 		    let i = id_to_string id in
 		    match lookup_field_type i r with
 		      | NoTyp -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+                      | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		      | Base((params,et),tag,cs,ef) ->
 			let et,cs,_ = subst params et cs ef in
 			let (e,t',_,c,ef) = check_exp envs et exp in
@@ -933,6 +948,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	      (match lookup_field_type fi r with
 		| NoTyp -> 
 		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+                | Overload _ ->  raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base((params,et),tag,cs,ef) ->
 		  let et,cs,ef = subst params et cs ef in
 		  let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
@@ -945,6 +961,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	      (match lookup_field_type fi r with
 		| NoTyp -> 
 		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+                | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base((params,et),tag,cs,ef) ->
 		  let et,cs,ef = subst params et cs ef in
 		  let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
@@ -958,11 +975,13 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	      (match lookup_field_type fi r with
 		| NoTyp -> 
 		  raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field")
+                | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base((params,et),tag,cs,ef) ->
 		  let et,cs,ef = subst params et cs ef in
 		  let (et',c',acc) = type_coerce (Expr l) d_env false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef)))) expect_t in
-                  (*TODO tHIS should be equate_t*)
-		  t'.t <- Tid i;
+                  equate_t t' {t=Tid i};
+                  (*TODO tHIS should be equate_t 
+		  t'.t <- Tid i;*)
 		  (acc,et',t_env,cs@c',ef))
 	    | records -> typ_error l ("Multiple structs contain field " ^ fi ^ ", try adding a cast to disambiguate"))
 	| _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t'))
@@ -986,6 +1005,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (exp',t'',_,cs',ef') = check_exp envs t' exp in
       let (t',c') = type_consistent (Expr l) d_env unit_t expect_t in
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
+    | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
 		    
 and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) =
   let Env(d_env,t_env) = envs in
@@ -1185,11 +1205,12 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	| Tid i | Tabbrev({t=Tid i},_) ->
 	  (match lookup_record_typ i d_env.rec_env with
 	    | None -> typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)
-	    | Some(((i,rec_kind,fields) as r)) ->
+            | Some(((i,rec_kind,fields) as r)) ->
 	      let fi = id_to_string id in
 	      (match lookup_field_type fi r with
 		| NoTyp -> 
 		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+                | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base((params,et),_,cs,_) ->
 		  let et,cs,ef = subst params et cs ef in
 		  (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef)))
@@ -1377,7 +1398,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
     | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') ->
       (*let _ = Printf.eprintf "Function %s is in env\n" id in*)
       let u,constraints,eft = subst params u constraints eft in
-      let t',cs = type_consistent (Specc l) d_env t u in
+      let _,cs = type_consistent (Specc l) d_env t u in
       let t_env = if is_rec then t_env else Envmap.remove t_env id in
       let funcls,cs_ef = check t_env in
       let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
@@ -1413,6 +1434,7 @@ let check_def envs def =
     let i = id_to_string id in
     let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e)) in
     (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
+  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Unknown "Scattered given to type checker")
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 0d3f467b..134aa2c4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -164,6 +164,7 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_wreg  -> "wreg"
       | Ast.BE_rmem  -> "rmem"
       | Ast.BE_wmem  -> "wmem"
+      | Ast.BE_barr  -> "barr"
       | Ast.BE_undef -> "undef"
       | Ast.BE_unspec-> "unspec"
       | Ast.BE_nondet-> "nondet"
@@ -1214,6 +1215,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_wmem,BE_wmem) -> 0
   | (BE_wmem,_) -> -1
   | (_,BE_wmem) -> 1
+  | (BE_barr,BE_barr) -> 0
+  | (BE_barr,_) -> 1
+  | (_,BE_barr) -> -1
   | (BE_undef,BE_undef) -> 0
   | (BE_undef,_) -> -1
   | (_,BE_undef) -> 1
@@ -1309,7 +1313,7 @@ and conforms_to_e loosely spec actual =
   match (spec.effect,actual.effect,loosely) with
     | (Euvar _,_,true) -> true
     | (_,Euvar _,true) -> false
-    | (_,_,true)       -> false (*Should check actual effect equality, using existing function*)
+    | _                -> false (*Should check actual effect equality, using existing function*)
 
 (*Is checking for structural equality amongst the types, building constraints for kind Nat. 
   When considering two range type applications, will check for consistency instead of equality*)
@@ -1342,7 +1346,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 =
   | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> 
     let (tin,cin) = type_consistent co d_env tin1 tin2 in
     let (tout,cout) = type_consistent co d_env tout1 tout2 in
-    let effect = effects_eq co effect1 effect2 in
+    let _ = effects_eq co effect1 effect2 in
     (t2,csp@cin@cout)
   | Ttup t1s, Ttup t2s ->
     (t2,csp@(List.flatten (List.map snd (List.map2 (type_consistent co d_env) t1s t2s))))
@@ -1354,7 +1358,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 =
       let b2,r2 = new_n (), new_n () in
       let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in
       equate_t t2 t2';
-      (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)]) (*This and above should maybe be In constraints when co is patt and tuvar is an in*)
+      (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)])
   | t,Tuvar _ -> equate_t t2 t1; (t1,csp)
   | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2))
 
@@ -1698,7 +1702,7 @@ let check_tannot l annot constraints efs =
     (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *)
       Base((params,t),tag,cs,e)
     | NoTyp -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation")
-      
+    | Overload _ -> raise (Reporting_basic.err_unreachable l "check_tannot given overload")
 
 let tannot_merge co denv t_older t_newer = 
   match t_older,t_newer with
@@ -1717,4 +1721,4 @@ let tannot_merge co denv t_older t_newer =
 	  let t,cs_b = type_consistent co denv t_n t_o in
 	  Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n)
 	| _,_ -> t_newer)
-    | Overload _, Overload _ -> t_newer
+    | _ -> t_newer
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 5203f51e..bb530896 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -136,6 +136,7 @@ val new_t : unit -> t
 val new_n : unit -> nexp
 val new_o : unit -> order
 val new_e : unit -> effect
+val equate_t : t -> t -> unit
 
 val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect
 val get_abbrev : def_envs -> t -> (t * nexp_range list)