anchor.diff:      | None -> err ("Identifier not found " + (err_id id))
       | Some r -> ()
   
  -let rec resolve_type env t:unit =
  -  let resolve_name id = 
  -    match lookup_name env id true with
  -    | Some _ -> ()
  -    | None -> () 
  -      // TODO: enable code below once we have imported types from F* 
  -      // err ("type not found " + (err_id id))
  +let rec kind_equal k1 k2 =
  +  match (k1, k2) with
  +  | (TYPE i1, TYPE i2) -> i1=i2
  +  | (KApp (ks1, k1), KApp(ks2, k2)) ->
  +    (List.fold2 (fun b k1 k2 -> b && (kind_equal k1 k2)) true ks1 ks2) && (kind_equal k1 k2)
  +  
  +let rec resolve_type env t:kind =
     match t with 
  -  | TName id -> resolve_name id
  -  | TApp (t, ts) -> resolve_type env t; resolve_types env ts
  -  | TArrow (ts, t) -> resolve_types env ts; resolve_type env t
  -  | _ -> ()
  -and resolve_types env ts = List.iter (resolve_type env) ts;
  +  | TName id -> lookup_type env id
  +  | TApp (t, ts) -> 
  +      let k = resolve_type env t in
  +      tc_kind env k ts
  +  | TArrow (ts, t) -> err ("not implemented")
  +  | _ -> err ("not implemented")
  +and tc_kind env k ts = 
  +  let check env k t = 
  +    if kind_equal k (resolve_type env t) then ()
  +    else err ("kind of types not matching") in
  +  match k with
  +  | KApp (ks, k) ->
  +    if (List.length ks <> List.length ts) then err ("number of parameters not match in type construct")
  +    else List.iter2 (fun k t -> check env k t) ks ts;
  +    k
  +  | _ -> err ("wrong kind for the type")
  +and resolve_types env ts = List.map (resolve_type env) ts;
   
   let rec tc_stmt (env:env) (s:stmt):stmt =
     match s with
  
positive.code: 
  let lookup_proc (env:env) (x:id): proc_decl =
    match lookup_name env x false with
    | Some (Proc_decl (proc_decl, _)) -> (proc_decl)
    | _ -> err ("cannot find proc '" + (err_id x) + "'")
  
  let compute_bound (l1:bigint) (h1:bigint) (l2:bigint) (h2:bigint) (op:bop): (bigint * bigint) =
    let s = 
  
negative.code:   | TInt (b1, b2) -> TInt (neg b1, neg b2)
    | _ -> err ("expect int type")
  
  let bnd_equal b1 b2 =
    match (b1, b2) with 
    | (Int i1, Int i2) -> i1 = i2
    | (NegInf, NegInf) -> true
    | (Inf, Inf) -> true
    | _ -> false
  
  let rec typ_equal t1 t2 = 
    match (t1, t2) with
    | (TName (Id x), TName (Id y)) -> x = y
    | (TApp (t1, ts1), TApp (t2, ts2)) ->
      (typ_equal t1 t2) && List.fold2 (fun b t1 t2 -> b && typ_equal t2 t2) true ts1 ts2
    | (TVar _, TVar _) -> internalErr "type variable should be resolved already"
    | (TInt (l1, h1), TInt(l2, h2)) ->
      (bnd_equal l1 l2) && (bnd_equal h1 h2)
    | (TArrow (xs, y), TArrow (us, v)) ->
      List.fold2 (fun b t1 t2 -> b&& typ_equal t1 t2) true xs us && (typ_equal y v)
    | _ -> internalErr "type mismatch"
  
  let is_subtype (t1:typ) (t2:typ): bool =
    match (t1, t2) with
    | (TName (Id "bool"), TName (Id "prop")) -> true
    | (TInt (Int l1, Int h1), TInt (Int l2, Int h2)) ->
      if (l2 <= l1 && h1 <= h2) then true else false
    | _ -> typ_equal t1 t2
  
  let isArithmeticOp op = match op with | BAdd | BSub | BMul | BDiv | BMod -> true | _ -> false
  let isLogicOp op = match op with | BEquiv | BImply | BExply | BAnd | BOr -> true | _ -> false
  