Expression type checking, not complete

4 files changed, 214 insertions, 42 deletions

diff --git a/src/finite_map.ml b/src/finite_map.ml
index 72fb15ac..3058e0c9 100644
--- a/src/finite_map.ml
+++ b/src/finite_map.ml
@@ -57,6 +57,7 @@ module type Fmap = sig
   val insert : 'a t -> (k * 'a) -> 'a t
   (* Keys from the right argument replace those from the left *)
   val union : 'a t -> 'a t -> 'a t
+  val intersect : 'a t -> 'a t -> 'a t
   val big_union : 'a t list -> 'a t
   val merge : (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
   val apply : 'a t -> k -> 'a option
@@ -92,6 +93,7 @@ module Fmap_map(Key : Set.OrderedType) : Fmap
   let insert m (k,v) = M.add k v m
   let union m1 m2 = 
     M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2
+  let intersect m1 m2 = m2 (*WRITE ME TODO*)
   let merge f m1 m2 = M.merge f m1 m2
   let apply m k = 
     try
diff --git a/src/type_check.ml b/src/type_check.ml
index 68c672ce..59ee8920 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2,6 +2,7 @@ open Ast
 open Type_internal
 type kind = Type_internal.kind
 type typ = Type_internal.t
+type 'a exp = 'a Ast.exp
 type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
@@ -194,7 +195,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
     | P_typ(typ,pat) -> 
       let t = typ_to_t typ in
       let (pat',env,constraints,u) = check_pattern envs pat in
-      let (t',constraint') = type_eq l u t in
+      let (t',constraint') = type_consistent l u t in
       (P_aux(P_typ(typ,pat'),(l,Some(([],t'),Emp,constraint'@constraints))),env,constraints@constraint',t)
     | P_id id -> 
       let t = new_t () in
@@ -205,6 +206,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
       (match Envmap.apply t_env i with
 	| None | Some None -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
 	| Some(Some((params,t),Constructor,constraints)) -> 
+          let t = subst params t in
 	  (match t.t with
 	    | Tid id -> if pats = [] then 
 		(P_aux(p,(l,Some((params,t),Constructor,constraints))),Envmap.empty,constraints,t)
@@ -212,7 +214,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    | Tfn(t1,t2,ef) -> 
 	      let ((P_aux(P_tup(pats'),_)),env,constraints,u) = 
 		check_pattern envs (P_aux(P_tup(pats),(l,annot))) in
-	      let (t',constraint') = type_eq l u t1 in
+	      let (t',constraint') = type_consistent l u t1 in
 	      (P_aux(P_app(id,pats'),(l,Some((params,t2),Constructor,constraints))),env,constraints,t2)
 	    | _ -> typ_error l ("Identifier " ^ i ^ " is not bound to a constructor"))
 	| Some(Some((params,t),tag,constraints)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a constructor"))
@@ -224,7 +226,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    List.map (fun (tan,id,l,pat) -> 
 	      let (pat,env,constraints,u) = check_pattern envs pat in
 	      let (Some((vs,t),tag,cs)) = tan in
-	      let (t',cs') = type_eq l u t in 
+	      let (t',cs') = type_consistent l u t in 
 	      let pat = FP_aux(FP_Fpat(id,pat),(l,Some((vs,t'),tag,cs@cs'@constraints))) in
 	      (pat,env,cs@cs'@constraints)) typ_pats in
 	  let pats' = List.map (fun (a,b,c) -> a) pat_checks in
@@ -241,7 +243,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints)))
 	  pats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_eq l u t in t',cs) ts ((new_t ()),[]) in
+      let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent l u t in t',cs) ts ((new_t ()),[]) in
       let t = {t = Tapp("vector",[(TA_nexp {nexp= Nconst 0});(TA_nexp {nexp= Nconst (List.length ts)});(TA_ord{order=Oinc});(TA_typ u)])} in
       (P_aux(P_vector(pats'),(l,Some(([],t),Emp,cs@constraints))), env,cs@constraints,t)
     | P_vector_indexed(ipats) -> 
@@ -267,7 +269,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints)))
 	  ipats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let (u,cs) = List.fold_right (fun u (t,cs) -> type_eq l u t) ts (new_t (),[]) in
+      let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent l u t) ts (new_t (),[]) in
       let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);
 				  (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in
       let cs = if inc_or_dec 
@@ -298,7 +300,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
       let or_init = new_o () in
       let ts = List.map 
 	(fun t->let ti= { t = Tapp("vector",[TA_nexp(new_n ());TA_nexp(new_n ());TA_ord(or_init);TA_typ t_init])} in
-	 type_eq l t ti) ts in
+	 type_consistent l t ti) ts in
       let ts,cs = List.split ts in
       let base,rise = new_n (),new_n () in
       let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord or_init);(TA_typ t_init)])} in
@@ -320,31 +322,117 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    (pat'::pats,t::ts,env::t_envs,cons@constraints))
 	  pats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_eq l u t in t',cs@cs') ts (new_t (),[]) in
+      let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent l u t in t',cs@cs') ts (new_t (),[]) in
       let t = {t = Tapp("list",[TA_typ u])} in
       (P_aux(P_list(pats'),(l,Some(([],t),Emp,constraints@cs))), env,constraints@cs,t)
       
-
-let rec check_exp envs expect_t (E_aux(e,annot)) =
+let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp * t * tannot emap * nexp_range list) =
   let Env(d_env,t_env) = envs in
+  let rebuild annot = E_aux(e,(l,annot)) in
   match e with
     | E_block(exps) -> 
-      let (exps',annot',envs,sc) = check_block t_env envs expect_t exps in
-      (E_aux(E_block(exps'),annot'), envs,sc)
-    | E_id(id) -> (match Envmap.apply t_env (id_to_string id) with
-		    | Some(typ) -> (E_aux(e,annot),t_env,[])
-		    | None -> (E_aux(e,annot),t_env,[]))
-    | _ -> (E_aux(e,annot),t_env,[])
+      let (exps',annot',t_env',sc,t) = check_block t_env envs expect_t exps in
+      (E_aux(E_block(exps'),(l,annot')),t, t_env',sc)
+    | E_id(id) -> 
+      let i = id_to_string id in
+      (match Envmap.apply t_env i with
+      | Some(Some((params,t),Constructor,cs)) ->
+        (match t.t with
+        | Tfn({t = Tid "unit"},t',ef) -> 
+          let t' = subst params t' in
+          let t',cs',e' = type_coerce l t' (rebuild (Some((params,{t=Tfn(unit_t,t',ef)}),Constructor,cs))) expect_t in
+          (e',t',t_env,cs@cs')
+        | Tfn(t1,t',e) -> 
+          typ_error l ("Constructor " ^ i ^ " expects arguments of type INSERT TYPE PRINTER HERE, found none")
+        | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
+      | Some(Some((params,t),Enum,cs)) ->
+        let t' = subst params t in
+        let t',cs',e' = type_coerce l t' (rebuild (Some((params,t'),Enum,cs))) expect_t in
+        (e',t',t_env,cs@cs')
+      | Some(Some(tp,Default,cs)) | Some(Some(tp,Spec,cs)) ->
+        typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
+      | Some(Some((params,t),tag,cs)) ->
+        (match t.t,expect_t.t with 
+        | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
+        | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
+          let tannot = Some((params,t),External,cs) in
+          let t' = subst params t' in
+          let t',cs',e' = type_coerce l t' (rebuild tannot) expect_t' in
+          (e',t',t_env,cs@cs')
+        | Tapp("register",[TA_typ(t')]),_ ->
+          let tannot = Some((params,t),External,cs) in
+          let t' = subst params t' in
+          let t',cs',e' = type_coerce l t' (rebuild tannot) expect_t in
+          (e',t',t_env,cs@cs')
+        | Tapp("reg",[TA_typ(t)]),_ ->
+          let tannot = Some((params,t),Emp,cs) in
+          let t',cs',e' = type_coerce l t (rebuild tannot) expect_t in
+          (e',t',t_env,cs@cs')
+        | _ -> 
+          let t',cs',e' = type_coerce l t (rebuild (Some((params,t),tag,cs))) expect_t in
+          (e',t',t_env,cs@cs')
+        )
+      | Some None | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
+    | E_lit (L_aux(lit,l')) ->
+      let t = (match lit with
+        | L_unit  -> {t = Tid "unit"} 
+	| L_zero  -> {t = Tid "bit"}
+	| L_one   -> {t = Tid "bit"}
+	| L_true  -> {t = Tid "bool"}
+	| L_false -> {t = Tid "bool"}
+	| L_num i -> {t = Tapp("enum",
+			       [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};TA_ord{order = Oinc}])}
+	| L_hex s -> {t = Tapp("vector",
+			       [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst ((String.length s)*4)};
+				TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])}
+	| L_bin s -> {t = Tapp("vector",
+			       [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst(String.length s)};
+				TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])}
+	| L_string s -> {t = Tid "string"}
+	| L_undef -> new_t ()) in
+      let t',cs',e' = type_coerce l t (rebuild (Some (([],t),Emp,[]))) expect_t in
+      (e',t',t_env,cs')
+    | E_cast(typ,e) ->
+      let t = typ_to_t typ in
+      let t',cs = type_consistent l t expect_t in
+      let (e',u,t_env,cs') = check_exp envs t' e in
+      (e',t',t_env,cs@cs')
+    | E_app(id,parms) -> (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
+    | E_app_infix(lft,op,rht) -> (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
+    | E_tuple(exps) ->
+      (match expect_t.t with
+      | Ttup ts ->
+        let tl = List.length ts in
+        let el = List.length exps in
+        if tl = el then
+          let exps,typs,consts = 
+            List.fold_right2 (fun e t (exps,typs,consts) -> let (e',t',_,c) = check_exp envs t e in ((e'::exps),(t'::typs),c@consts))
+              exps ts ([],[],[]) in
+          let t = {t = Ttup typs} in
+          (E_aux(E_tuple(exps),(l,Some(([],t),Emp,consts))),t,t_env,consts)
+        else typ_error l ("Expected a tuple with length " ^ (string_of_int tl) ^ " found one of length " ^ (string_of_int el))
+      | Tuvar _ ->
+        let exps,typs,consts = 
+          List.fold_right (fun e (exps,typs,consts) -> let (e',t,_,c) = check_exp envs (new_t ()) e in ((e'::exps),(t::typs),c@consts)) exps ([],[],[]) in
+        expect_t.t <- Ttup typs;
+        (E_aux(E_tuple(exps),(l,Some(([],expect_t),Emp,consts))),expect_t,t_env,consts)
+      | _ -> typ_error l "Found a tuple when expecting a value of type INSERT TYPE PRINTING HERE")
+    | E_if(cond,then_,else_) ->
+      let (cond',_,_,c1) = check_exp envs bool_t cond in
+      let then',then_t,then_env,then_c = check_exp envs expect_t then_ in
+      let else',else_t,else_env,else_c = check_exp envs expect_t else_ in
+      (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp,c1@then_c@else_c))),expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1)
+    | _ -> (E_aux(e,(l,annot)),expect_t,t_env,[])
 		    
-and check_block orig_envs envs expect_t exps =
+and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t) =
   let Env(d_env,t_env) = envs in
   match exps with
-    | [] -> ([],(Parse_ast.Unknown,None),orig_envs,[])
-    | [e] -> let (E_aux(e',annot),envs,sc) = check_exp envs expect_t e in
-	     ([E_aux(e',annot)],annot,orig_envs,sc)
-    | e::exps -> let (e',t_env,sc) = check_exp envs expect_t (*wrong*) e in
-		 let (exps',annot',orig_envs,sc') = check_block orig_envs (Env(d_env,t_env)) expect_t exps in
-		 ((e'::exps'),annot',orig_envs,sc@sc')
+    | [] -> ([],None,orig_envs,[],unit_t)
+    | [e] -> let (E_aux(e',(l,annot)),t,envs,sc) = check_exp envs expect_t e in
+	     ([E_aux(e',(l,annot))],annot,orig_envs,sc,t)
+    | e::exps -> let (e',t',t_env,sc) = check_exp envs unit_t e in
+		 let (exps',annot',orig_envs,sc',t) = check_block orig_envs (Env(d_env,t_env)) expect_t exps in
+		 ((e'::exps'),annot',orig_envs,sc@sc',t)
 
 (*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
 let check_type_def envs (TD_aux(td,(l,annot))) =
@@ -370,7 +458,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
       let arms' = List.map 
 	(fun (Tu_aux(tu,l')) -> 
 	  match tu with 
-	    | Tu_id i -> ((id_to_string i),(arm_t {t=Tid "unit"}))
+	    | Tu_id i -> ((id_to_string i),(arm_t unit_t))
 	    | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t typ))))
 	arms in
       let t_env = List.fold_right (fun (id,tann) t_env -> Envmap.insert t_env (id,tann)) arms' t_env in
@@ -493,12 +581,12 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) ->
 	let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) pat in
-	let u,cs = type_eq l t' param_t in
-	let exp,_,constraints = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in
+	let u,cs = type_consistent l t' param_t in
+	let exp,_,_,constraints = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in
 	(FCL_aux((FCL_Funcl(id,pat',exp)),(l,tannot)),constraints'@cs@constraints)) funcls) in
   match (in_env,tannot) with
     | Some(Some( (params,u),Spec,constraints)), Some( (p',t),Emp,c') ->
-      let t',cs = type_eq l t u in
+      let t',cs = type_consistent l (subst p' t) (subst params u) in
       let t_env = if is_rec then t_env else Envmap.remove t_env id in
       let funcls,cs = check t_env in
       let cs' = resolve_constraints cs in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index b2280524..693afdcc 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -75,6 +75,7 @@ type nexp_range =
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list) option
 
+type exp = tannot Ast.exp
 
 let t_count = ref 0
 let n_count = ref 0
@@ -104,8 +105,9 @@ let new_e _ =
   e_count := i + 1;
   { effect = Euvar { eindex = i; esubst = None }}
   
-
 let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};TA_ord{order=Oinc}])}
+let unit_t = { t = Tid "unit" } 
+let bool_t = {t = Tid "bool" }
 
 let initial_kind_env = 
   Envmap.from_list [ 
@@ -126,6 +128,55 @@ let initial_typ_env =
     ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure)}),External,[]));
   ]
 
+let rec t_subst s_env t =
+  match t.t with
+  | Tvar i -> (match Envmap.apply s_env i with
+               | Some(TA_typ t1) -> t1
+               | _ -> t)
+  | Tid _ | Tuvar _ -> t
+  | Tfn(t1,t2,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(e_subst s_env e)) }
+  | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
+  | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
+and ta_subst s_env ta =
+  match ta with
+  | TA_typ t -> TA_typ (t_subst s_env t)
+  | TA_nexp n -> TA_nexp (n_subst s_env n)
+  | TA_eft e -> TA_eft (e_subst s_env e)
+  | TA_ord o -> TA_ord (o_subst s_env o)
+and n_subst s_env n =
+  match n.nexp with
+  | Nvar i -> (match Envmap.apply s_env i with
+               | Some(TA_nexp n1) -> n1
+               | _ -> n)
+  | Nconst _ | Nuvar _ -> n
+  | N2n n1 -> { nexp = N2n (n_subst s_env n1) }
+  | Nneg n1 -> { nexp = Nneg (n_subst s_env n1) }
+  | Nadd(n1,n2) -> { nexp = Nadd(n_subst s_env n1,n_subst s_env n2) }
+  | Nmult(n1,n2) -> { nexp = Nmult(n_subst s_env n1,n_subst s_env n2) }
+and o_subst s_env o =
+  match o.order with
+  | Ovar i -> (match Envmap.apply s_env i with
+               | Some(TA_ord o1) -> o1
+               | _ -> o)
+  | _ -> o
+and e_subst s_env e =
+  match e.effect with
+  | Evar i -> (match Envmap.apply s_env i with
+               | Some(TA_eft e1) -> e1
+               | _ -> e)
+  | _ -> e
+
+let subst k_env t =
+  let subst_env = Envmap.from_list
+    (List.map (fun (id,k) -> (id, 
+                              match k.k with
+                              | K_Typ -> TA_typ (new_t ())
+                              | K_Nat -> TA_nexp (new_n ())
+                              | K_Ord -> TA_ord (new_o ())
+                              | K_Efct -> TA_eft (new_e ())
+                              | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "substitution given an environment with a non-base-kind kind"))) k_env) 
+  in
+  t_subst subst_env t
 
 let eq_error l msg = raise (Reporting_basic.err_typ l msg)
 
@@ -187,20 +238,40 @@ let rec nexp_eq n1 n2 =
   | n,Nuvar _ -> n2.nexp <- n1.nexp; true
   | _,_ -> false
 
-(*Is checking for structural equality amongst the types, building constraints for kind Nat. Note: needs an environment to handle type abbreviations*)
-let rec type_eq l t1 t2 = 
+(*Is checking for structural equality amongst the types, building constraints for kind Nat. 
+  When considering two enum type applications, will check for consistency instead of equality
+  Note: needs an environment to handle type abbreviations*)
+let rec type_consistent l t1 t2 = 
   match t1.t,t2.t with
   | Tvar v1,Tvar v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
   | Tid v1,Tid v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*)
   | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> 
-    let (tin,cin) = type_eq l tin1 tin2 in
-    let (tout,cout) = type_eq l tout1 tout2 in
+    let (tin,cin) = type_consistent l tin1 tin2 in
+    let (tout,cout) = type_consistent l tout1 tout2 in
     let effect = effects_eq l effect1 effect2 in
     (t2,cin@cout)
   | Ttup t1s, Ttup t2s ->
-    (t2,(List.flatten (List.map snd (List.map2 (type_eq l) t1s t2s))))
+    (t2,(List.flatten (List.map snd (List.map2 (type_consistent l) t1s t2s))))
   | Tapp(id1,args1), Tapp(id2,args2) ->
     if id1=id2 && (List.length args2 = List.length args2) then
+      if id1="enum" then
+        (match args1,args2 with
+        | [TA_nexp b1;TA_nexp r1; TA_ord o1],[TA_nexp b2;TA_nexp r2;TA_ord o2] ->
+          (match (order_eq l o1 o2).order with
+          | Oinc -> 
+            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
+            then (t2,[])
+            else (t2, [GtEq(l,b1,b2);LtEq(l,r1,r2)])
+          | Odec ->
+            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
+            then (t2,[])
+            else (t2, [LtEq(l,b1,b2);GtEq(l,r1,r2)])
+          | _ ->
+            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
+            then (t2,[])
+            else (t2, [Eq(l,b1,b2);Eq(l,r1,r2)]))
+        | _ -> raise (Reporting_basic.err_unreachable l "enum application incorrectly kinded"))
+      else          
       (t2,(List.flatten (List.map2 (type_arg_eq l) args1 args2)))
     else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match")
   | Tuvar _, t -> t1.t <- t2.t; (t2,[])
@@ -209,21 +280,22 @@ let rec type_eq l t1 t2 =
 
 and type_arg_eq l ta1 ta2 = 
   match ta1,ta2 with
-  | TA_typ t1,TA_typ t2 -> snd (type_eq l t1 t2)
+  | TA_typ t1,TA_typ t2 -> snd (type_consistent l t1 t2)
   | TA_nexp n1,TA_nexp n2 -> if nexp_eq n1 n2 then [] else [Eq(l,n1,n2)]
   | TA_eft e1,TA_eft e2 -> (ignore(effects_eq l e1 e2);[])
   | TA_ord o1,TA_ord o2 -> (ignore(order_eq l o1 o2);[])
   | _,_ -> eq_error l "Type arguments must be of the same kind" 
 
 
-let rec type_coerce l t1 t2 = 
-  match t1.t,t2.t with
+let rec type_coerce l t1 e t2 = 
+  (t2,[],e)
+  (*match t1.t,t2.t with
   | Tid v1,Tid v2 -> if v1 = v2 then (None,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*)
   | Ttup t1s, Ttup t2s ->
-    (None,(List.flatten (List.map snd (List.map2 (type_eq l) t1s t2s))))
+    (None,(List.flatten (List.map snd (List.map2 (type_consistent l) t1s t2s))))
   | Tapp(id1,args1), Tapp(id2,args2) ->
     if id1=id2 && (List.length args2 = List.length args2) then
       (None,(List.flatten (List.map2 (type_arg_eq l) args1 args2)))
     else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match")
-  | _,_ -> let (t2,consts) = type_eq l t1 t2 in
-	     (None,consts)
+  | _,_ -> let (t2,consts) = type_consistent l t1 t2 in
+	     (None,consts)*)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index dabcf646..3a8c669d 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -4,7 +4,6 @@ module Nameset : sig
   val pp : Format.formatter -> t -> unit
 end
 
-
 type kind = { mutable k : k_aux }
 and k_aux =
   | K_Typ
@@ -71,9 +70,13 @@ type nexp_range =
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list) option
 
+type exp = tannot Ast.exp
+
 val initial_kind_env : kind Envmap.t
 val initial_typ_env : tannot Envmap.t
 val nat_t : t
+val unit_t : t
+val bool_t : t
 
 val reset_fresh : unit -> unit
 val new_t : unit -> t
@@ -81,8 +84,15 @@ val new_n : unit -> nexp
 val new_o : unit -> order
 val new_e : unit -> effect
 
-(* type_eq mutates to unify variables, and will raise an exception if two types cannot be equal *)
-val type_eq : Parse_ast.l -> t -> t -> t * nexp_range list
+val subst : (string * kind) list -> t -> t
+
+
+(* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where
+   t1 and t2 are both enum types and t1 is contained within the range of t2: i.e.
+   enum 2 5 inc is consistent with enum 0 10 inc, but not vice versa.
+   type_consistent mutates uvars to perform unification and will raise an error if the [[t1]] and [[t2]] are inconsitent
+*)
+val type_consistent : Parse_ast.l -> t -> t -> t * nexp_range list
 
 (* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second *)
-val type_coerce : Parse_ast.l -> t -> t -> t option * nexp_range list
+val type_coerce : Parse_ast.l -> t -> exp -> t -> t * nexp_range list * exp