Add a test case for various simple boolean properties

test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.

  // de Morgan
  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));

introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.

Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.

Also ensure that this test case works correctly in Lem

10 files changed, 132 insertions, 58 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 02e297cb..a771291e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -739,6 +739,8 @@ and string_of_n_constraint = function
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
      string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+  | NC_aux (NC_app (Id_aux (DeIid op, _), [arg1; arg2]), _) ->
+     "(" ^ string_of_typ_arg arg1 ^ " " ^ op ^ " " ^ string_of_typ_arg arg2 ^ ")"
   | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
   | NC_aux (NC_var v, _) -> string_of_kid v
   | NC_aux (NC_true, _) -> "true"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d394fde9..61cde224 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -129,6 +129,18 @@ let format_kind_aux_list = function
   | [kind] -> string_of_kind_aux kind
   | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")"
 
+let to_ast_kopt ctx (P.KOpt_aux (aux, l)) =
+  let aux, ctx = match aux with
+    | P.KOpt_none v ->
+       let v = to_ast_var v in
+       KOpt_kind (K_aux (K_int, gen_loc l), v), { ctx with kinds = KBindings.add v K_int ctx.kinds }
+    | P.KOpt_kind (k, v) ->
+       let v = to_ast_var v in
+       let k = to_ast_kind k in
+       KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
+  in
+  KOpt_aux (aux, l), ctx
+
 let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
   let aux = match aux with
     | P.ATyp_id id -> Typ_id (to_ast_id id)
@@ -157,10 +169,11 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
        | Some kinds ->
           Typ_app (id, List.map2 (to_ast_typ_arg ctx) args kinds)
        end
-    | P.ATyp_exist (kids, nc, atyp) ->
-       let kids = List.map to_ast_var kids in
-       let ctx = { ctx with kinds = List.fold_left (fun kinds kid -> KBindings.add kid K_int kinds) ctx.kinds kids } in
-       Typ_exist (List.map (mk_kopt K_int) kids, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
+    | P.ATyp_exist (kopts, nc, atyp) ->
+       let kopts, ctx =
+         List.fold_right (fun kopt (kopts, ctx) -> let kopt, ctx = to_ast_kopt ctx kopt in (kopt :: kopts, ctx)) kopts ([], ctx)
+       in
+       Typ_exist (kopts, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
     | P.ATyp_base (id, kind, nc) ->
        raise (Reporting.err_unreachable l __POS__ "TODO")
     | _ -> raise (Reporting.err_typ l "Invalid type")
@@ -197,7 +210,7 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
 
 and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
   let aux = match aux with
-    | P.ATyp_app (Id_aux (DeIid op, _), [t1; t2]) ->
+    | P.ATyp_app (Id_aux (DeIid op, _) as id, [t1; t2]) ->
        begin match op with
        | "==" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | "!=" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
@@ -207,7 +220,15 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
        | "<" -> NC_bounded_le (nsum (to_ast_nexp ctx t1) (nint 1), to_ast_nexp ctx t2)
        | "&" -> NC_and (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
        | "|" -> NC_or (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
-       | _ -> raise (Reporting.err_typ l ("Invalid operator in constraint"))
+       | _ ->
+          let id = to_ast_id id in
+          match Bindings.find_opt id ctx.type_constructors with
+          | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id)))
+          | Some kinds when List.length kinds <> 2 ->
+             raise (Reporting.err_typ l (sprintf "%s : %s -> Bool expected %d arguments, given 2"
+                                                 (string_of_id id) (format_kind_aux_list kinds)
+                                                 (List.length kinds)))
+          | Some kinds -> NC_app (id, List.map2 (to_ast_typ_arg ctx) [t1; t2] kinds)
        end
     | P.ATyp_app (id, args) ->
        let id = to_ast_id id in
@@ -230,17 +251,9 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
 let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
   match aux with
   | P.QI_const nc -> QI_aux (QI_const (to_ast_constraint ctx nc), l), ctx
-  | P.QI_id (KOpt_aux (aux, kopt_l)) ->
-     let aux, ctx = match aux with
-       | P.KOpt_none v ->
-          let v = to_ast_var v in
-          KOpt_kind (K_aux (K_int, gen_loc kopt_l), v), { ctx with kinds = KBindings.add v K_int ctx.kinds }
-       | P.KOpt_kind (k, v) ->
-          let v = to_ast_var v in
-          let k = to_ast_kind k in
-          KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
-     in
-     QI_aux (QI_id (KOpt_aux (aux, kopt_l)), l), ctx
+  | P.QI_id kopt ->
+     let kopt, ctx = to_ast_kopt ctx kopt in
+     QI_aux (QI_id kopt, l), ctx
 
 let to_ast_typquant ctx (P.TypQ_aux (aux, l)) =
   match aux with
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a5dbf66e..9b855837 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -163,7 +163,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_wild
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
- | ATyp_exist of kid list * atyp * atyp
+ | ATyp_exist of kinded_id list * atyp * atyp
  | ATyp_base of id * atyp * atyp
 
 and atyp = 
@@ -175,7 +175,7 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
    KOpt_none of kid (* identifier *)
  | KOpt_kind of kind * kid (* kind-annotated variable *)
 
-type 
+and
 kinded_id = 
    KOpt_aux of kinded_id_aux * l
 
diff --git a/src/parser.mly b/src/parser.mly
index 544438c0..1957d7fd 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -78,6 +78,8 @@ let prepend_id str1 = function
 let mk_id i n m = Id_aux (i, loc n m)
 let mk_kid str n m = Kid_aux (Var str, loc n m)
 
+let mk_kopt k n m = KOpt_aux (k, loc n m)
+
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
@@ -550,10 +552,10 @@ atomic_typ:
     { let v = mk_kid "n" $startpos $endpos in
       let atom_id = mk_id (Id "atom") $startpos $endpos in
       let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
-      mk_typ (ATyp_exist ([v], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
-  | Lcurly kid_list Dot typ Rcurly
+      mk_typ (ATyp_exist ([mk_kopt (KOpt_none v) $startpos $endpos], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+  | Lcurly kopt_list Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, ATyp_aux (ATyp_lit (L_aux (L_true, loc $startpos $endpos)), loc $startpos $endpos), $4)) $startpos $endpos }
-  | Lcurly kid_list Comma typ Dot typ Rcurly
+  | Lcurly kopt_list Comma typ Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
   | Lcurly id Colon typ Dot typ Rcurly
     { mk_typ (ATyp_base ($2, $4, $6)) $startpos $endpos }
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ac0195aa..9d169108 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -247,6 +247,7 @@ and lem_nexps_of_typ_arg (A_aux (ta,_)) =
   | A_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
   | A_typ typ -> lem_nexps_of_typ typ
   | A_order _ -> NexpSet.empty
+  | A_bool _ -> NexpSet.empty
 
 let lem_tyvars_of_typ typ =
   NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
@@ -296,6 +297,8 @@ let doc_typ_lem, doc_atomic_typ_lem =
          (string "integer")
       | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
          (string "integer")
+      | Typ_app(Id_aux (Id "atom_bool", _), [A_aux(A_bool nc,_)]) ->
+         (string "bool")
       | Typ_app(id,args) ->
          let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args) in
          if atyp_needed then parens tpp else tpp
@@ -331,6 +334,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | A_typ t -> app_typ true t
       | A_nexp n -> doc_nexp_lem (nexp_simp n)
       | A_order o -> empty
+      | A_bool _ -> empty
   in typ', atomic_typ
 
 (* Check for variables in types that would be pretty-printed. *)
@@ -1013,6 +1017,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
      doc_op equals
        (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
        (doc_typschm_lem false typschm)
+  | TD_abbrev _ -> empty
   | TD_record(id,nm,typq,fs,_) ->
     let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index e0223105..c4b9bdd3 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -70,7 +70,7 @@ let doc_kopt = function
   | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
   | kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
   | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
-                
+
 let doc_int n = string (Big_int.to_string n)
 
 let docstring (l, _) = match l with
@@ -168,6 +168,8 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
      separate space [doc_typ_arg x; doc_typ_arg y]
   | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
      string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+  | Typ_app (id, typs) when Id.compare id (mk_id "atom_bool") = 0 ->
+     string "bool" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
@@ -205,6 +207,7 @@ let doc_quants quants =
     match qi_aux with
     | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
+    | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
     | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
     | QI_const nc -> []
   in
@@ -225,6 +228,7 @@ let doc_param_quants quants =
     match qi_aux with
     | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
     | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
+    | QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
     | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
     | QI_const nc -> []
   in
@@ -567,14 +571,21 @@ let doc_field (typ, id) =
 
 let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
 
+let doc_typ_arg_kind (A_aux (aux, _)) =
+  match aux with
+  | A_nexp _ -> space ^^ string "->" ^^ space ^^string "Int"
+  | A_bool _ -> space ^^ string "->" ^^ space ^^ string "Bool"
+  | A_order  _ -> space ^^ string "->" ^^ space ^^ string "Order"
+  | A_typ _ -> empty
+
 let doc_typdef (TD_aux(td,_)) = match td with
   | TD_abbrev (id, typq, typ_arg) ->
      begin
        match doc_typquant typq with
        | Some qdoc ->
-          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typ_arg typ_arg)
+          doc_op equals (concat [string "type"; space; doc_id id; qdoc; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
        | None ->
-          doc_op equals (concat [string "type"; space; doc_id id]) (doc_typ_arg typ_arg)
+          doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
      end
   | TD_enum (id, _, ids, _) ->
      separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 79b5f619..30318e3f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -271,6 +271,8 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
        A_aux (A_typ (rewrite_typ env typ), l)
     | A_order ord ->
        A_aux (A_order ord, l)
+    | A_bool nc ->
+       A_aux (A_bool nc, l)
   in
 
   let rewrite_annot (l, tannot) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 0f8db0ff..940fbfe5 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -310,10 +310,13 @@ let typ_variants consider_var bound tunions =
 let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
   | KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
 
+let fv_of_abbrev consider_var bound used typq typ_arg =
+  let ts_bound = if consider_var then typq_bindings typq else mt in
+  ts_bound, fv_of_targ consider_var (Nameset.union bound ts_bound) used typ_arg
+
 let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
-  | TD_abbrev(id,typq,A_aux(A_typ typ, l)) ->
-     let typschm = TypSchm_aux (TypSchm_ts (typq,typ), l) in
-     init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
+  | TD_abbrev(id,typq,typ_arg) ->
+     init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
   | TD_record(id,_,typq,tids,_) ->
     let binds = init_env (string_of_id id) in
     let bounds = if consider_var then typq_bindings typq else mt in
diff --git a/src/type_check.ml b/src/type_check.ml
index cc0b9843..befc7302 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -82,7 +82,7 @@ let rec indent n = match n with
 (* Lazily evaluate debugging message. This can make a big performance
    difference; for example, repeated calls to string_of_exp can be costly for
    deeply nested expressions, e.g. with long sequences of monadic binds. *)
-let typ_debug m = if !opt_tc_debug > 1 then prerr_endline (indent !depth ^ Lazy.force m) else ()
+let typ_debug ?level:(level=1) m = if !opt_tc_debug > level then prerr_endline (indent !depth ^ Lazy.force m) else ()
 
 let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.force m) else ()
 
@@ -516,6 +516,7 @@ end = struct
     else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
   let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
+    typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc));
     match aux with
     | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
     | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
@@ -523,7 +524,7 @@ end = struct
        (try
           begin match Bindings.find id env.typ_synonyms env args with
           | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
-          | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
+          | arg -> typ_error l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
           end
         with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
     | NC_true | NC_false | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ | NC_var _ | NC_set _ -> nc
@@ -602,9 +603,13 @@ end = struct
     | A_order _ | A_typ _ | A_bool _ -> arg
     | A_nexp n -> A_aux (A_nexp (f n), l)
 
+  let wf_debug str f x exs =
+    typ_debug ~level:2 (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs)))
+
   (* Check if a type, order, n-expression or constraint is
      well-formed. Throws a type error if the type is badly formed. *)
   let rec wf_typ ?exs:(exs=KidSet.empty) env typ =
+    wf_debug "typ" string_of_typ typ exs;
     let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in
     match typ_aux with
     | Typ_id id when bound_typ_id env id ->
@@ -643,6 +648,7 @@ end = struct
     | A_order ord -> wf_order env ord
     | A_bool nc -> wf_constraint ~exs:exs env nc
   and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
+    wf_debug "nexp" string_of_nexp nexp exs;
     match nexp_aux with
     | Nexp_id _ -> ()
     | Nexp_var kid when KidSet.mem kid exs -> ()
@@ -662,7 +668,7 @@ end = struct
     | Nexp_minus (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2
     | Nexp_exp nexp -> wf_nexp ~exs:exs env nexp (* MAYBE: Could put restrictions on what is allowed here *)
     | Nexp_neg nexp -> wf_nexp ~exs:exs env nexp
-  and wf_order env (Ord_aux (ord_aux, l)) =
+  and wf_order env (Ord_aux (ord_aux, l) as ord) =
     match ord_aux with
     | Ord_var kid ->
        begin
@@ -674,6 +680,7 @@ end = struct
        end
     | Ord_inc | Ord_dec -> ()
   and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
+    wf_debug "constraint" string_of_n_constraint nc exs;
     match nc_aux with
     | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
@@ -690,6 +697,7 @@ end = struct
     | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_app (id, args) -> List.iter (wf_typ_arg ~exs:exs env) args
+    | NC_var kid when KidSet.mem kid exs -> ()
     | NC_var kid ->
        begin match get_typ_var kid env with
        | K_bool -> ()
@@ -1031,8 +1039,9 @@ end = struct
 
   let get_constraints env = env.constraints
 
-  let add_constraint (NC_aux (nc_aux, l) as constr) env =
+  let add_constraint constr env =
     wf_constraint env constr;
+    let (NC_aux (nc_aux, l) as constr) = expand_constraint_synonyms env constr in
     match nc_aux with
     | NC_true -> env
     | _ ->
@@ -1261,6 +1270,7 @@ let solve env nexp = failwith "WIP"
 let prove env nc =
   typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
   let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in
+  typ_debug ~level:2 (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
   let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
     match n1, n2 with
     | Nexp_constant c1, Nexp_constant c2 when f c1 c2 -> true
@@ -1362,6 +1372,7 @@ let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
   | NC_false, NC_false -> true
   | NC_set (kid1, ints1), NC_set (kid2, ints2) when List.length ints1 = List.length ints2 ->
      Kid.compare kid1 kid2 = 0 && List.for_all2 (fun i1 i2 -> i1 = i2) ints1 ints2
+  | NC_var kid1, NC_var kid2 -> Kid.compare kid1 kid2 = 0
   | _, _ -> false
 
 let typ_identical env typ1 typ2 =
@@ -1449,8 +1460,15 @@ and unify_typ_arg l env goals (A_aux (aux1, _) as typ_arg1) (A_aux (aux2, _) as
   | A_typ typ1, A_typ typ2 -> unify_typ l env goals typ1 typ2
   | A_nexp nexp1, A_nexp nexp2 -> unify_nexp l env goals nexp1 nexp2
   | A_order ord1, A_order ord2 -> unify_order l goals ord1 ord2
+  | A_bool nc1, A_bool nc2 -> unify_constraint l goals nc1 nc2
   | _, _ -> unify_error l ("Could not unify type arguments " ^ string_of_typ_arg typ_arg1 ^ " and " ^ string_of_typ_arg typ_arg2)
 
+and unify_constraint l goals (NC_aux (aux1, _) as nc1) (NC_aux (aux2, _) as nc2) =
+  typ_debug (lazy (Util.("Unify constraint " |> magenta |> clear) ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2));
+  match aux1, aux2 with
+  | NC_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_bool nc2)
+  | _, _ -> unify_error l ("Could not unify constraints " ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2)
+
 and unify_order l goals (Ord_aux (aux1, _) as ord1) (Ord_aux (aux2, _) as ord2) =
   typ_print (lazy (Util.("Unify order " |> magenta |> clear) ^ string_of_order ord1 ^ " and " ^ string_of_order ord2));
   match aux1, aux2 with
@@ -1594,6 +1612,7 @@ let rec kid_order_nexp kind_map (Nexp_aux (aux, l) as nexp) =
   | Nexp_app (id, nexps) ->
      List.fold_left (fun (ord, kids) nexp -> let (ord', kids) = kid_order_nexp kids nexp in (ord @ ord', kids)) ([], kind_map) nexps
 
+
 let rec kid_order kind_map (Typ_aux (aux, l) as typ) =
   match aux with
   | Typ_var kid when KBindings.mem kid kind_map ->
@@ -1605,11 +1624,18 @@ let rec kid_order kind_map (Typ_aux (aux, l) as typ) =
      List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kind_map) args
   | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and kid_order_arg kids (A_aux (aux, l) as arg) =
+and kid_order_arg kind_map (A_aux (aux, l) as arg) =
   match aux with
-  | A_typ typ -> kid_order kids typ
-  | A_nexp nexp -> kid_order_nexp kids nexp
-  | A_order _ -> ([], kids)
+  | A_typ typ -> kid_order kind_map typ
+  | A_nexp nexp -> kid_order_nexp kind_map nexp
+  | A_bool nc -> kid_order_constraint kind_map nc
+  | A_order _ -> ([], kind_map)
+and kid_order_constraint kind_map (NC_aux (aux, l) as nc) =
+  match aux with
+  | NC_var kid when KBindings.mem kid kind_map ->
+     ([mk_kopt (unaux_kind (KBindings.find kid kind_map)) kid], KBindings.remove kid kind_map)
+  | NC_var _ -> ([], kind_map)
+  | _ -> unreachable l __POS__ "bad constraint type"
 
 let rec alpha_equivalent env typ1 typ2 =
   let counter = ref 0 in
@@ -1742,8 +1768,10 @@ let rec subtyp l env typ1 typ2 =
   match typ_aux1, typ_aux2 with
   | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
 
-  | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" -> ()
-                                                         
+  | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" ->
+     typ_debug (lazy "Boolean subtype");
+     ()
+
   | Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
      List.iter2 (subtyp l env) typs1 typs2
 
@@ -1762,7 +1790,7 @@ and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
   | A_nexp n1, A_nexp n2 when prove env (nc_eq n1 n2) -> ()
   | A_typ typ1, A_typ typ2 -> subtyp l env typ1 typ2
   | A_order ord1, A_order ord2 when ord_identical ord1 ord2 -> ()
-  | A_bool nc1, A_bool nc2 -> assert false
+  | A_bool nc1, A_bool nc2 when nc_identical nc1 nc2 -> ()
   | _, _ -> typ_error l "Mismatched argument types in subtype check"
 
 let typ_equality l env typ1 typ2 =
@@ -1997,6 +2025,7 @@ let rec combine_constraint b f x y = match b, x, y with
   | _, _, _ -> None
 
 let rec assert_constraint env b (E_aux (exp_aux, _) as exp) =
+  typ_debug ~level:2 (lazy ("Asserting constraint for " ^ string_of_exp exp ^ " : " ^ string_of_typ (typ_of exp)));
   match typ_of exp with
   | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) ->
      Some nc
@@ -2243,14 +2272,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      if prove env nc
      then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
      else typ_error l ("Cannot prove " ^ string_of_n_constraint nc)
-  | E_app (f, [E_aux (E_sizeof nexp, _)]), _ when Id.compare f (mk_id "__solve") = 0 ->
-     Env.wf_nexp env nexp;
-     begin match solve env nexp with
-     | None -> typ_error l ("Coud not solve " ^ string_of_nexp nexp)
-     | Some n ->
-        print_endline ("Solved " ^ string_of_nexp nexp ^ " = " ^ Big_int.to_string n);
-        annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
-     end
+  | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_not_prove") = 0 ->
+     Env.wf_constraint env nc;
+     if prove env nc
+     then typ_error l ("Can prove " ^ string_of_n_constraint nc)
+     else annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
   (* All constructors and mappings are treated as having one argument
      so Ctor(x, y) is checked as Ctor((x, y)) *)
   | E_app (f, x :: y :: zs), _ when Env.is_union_constructor f env || Env.is_mapping f env ->
@@ -2295,10 +2321,19 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      let inferred_exp = infer_funapp l env f xs (Some typ) in
      type_coercion env inferred_exp typ
   | E_if (cond, then_branch, else_branch), _ ->
-     let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
-     let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in
-     let else_branch' = crule check_exp (add_opt_constraint (option_map nc_not (assert_constraint env false cond')) env) else_branch typ in
-     annot_exp (E_if (cond', then_branch', else_branch')) typ
+     (* let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in *)
+     let cond' = irule infer_exp env cond in
+     begin match destruct_exist (typ_of cond') with
+     | Some (kopts, nc, Typ_aux (Typ_app (ab, [A_aux (A_bool flow, _)]), _)) when string_of_id ab = "atom_bool" ->
+        let env = add_existential l kopts nc env in
+        let then_branch' = crule check_exp (Env.add_constraint flow env) then_branch typ in
+        let else_branch' = crule check_exp (Env.add_constraint flow env) else_branch typ in
+        annot_exp (E_if (cond', then_branch', else_branch')) typ
+     | _ ->
+        let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in
+        let else_branch' = crule check_exp (add_opt_constraint (option_map nc_not (assert_constraint env false cond')) env) else_branch typ in
+        annot_exp (E_if (cond', then_branch', else_branch')) typ
+     end
   | E_exit exp, _ ->
      let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
      annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape])
@@ -3251,7 +3286,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
     let updated_unifiers = KBindings.map (subst_unifiers_typ_arg unifiers) previous_unifiers in
     all_unifiers := merge_uvars l updated_unifiers unifiers;
   in
- 
+
   let quants, typ_args, typ_ret, eff =
     match Env.expand_synonyms env f_typ with
     | Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> ref (quant_items typq), typ_args, ref typ_ret, eff
@@ -4271,6 +4306,10 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
 (* FIXME: This code is duplicated with general kind-checking code in environment, can they be merged? *)
 let mk_synonym typq typ_arg =
   let kopts, ncs = quant_split typq in
+  let kopts = List.map (fun kopt -> kopt, fresh_existential (unaux_kind (kopt_kind kopt))) kopts in
+  let ncs = List.map (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) ncs in
+  let typ_arg = List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts in
+  let kopts = List.map snd kopts in
   let rec subst_args kopts args =
     match kopts, args with
     | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
@@ -4283,7 +4322,7 @@ let mk_synonym typq typ_arg =
     | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
        let typ_arg, ncs = subst_args kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
-    | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_order_kopt kopt ->
+    | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
        let typ_arg, ncs = subst_args kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
     | [], [] -> typ_arg, ncs
@@ -4310,11 +4349,8 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
   fun env (TD_aux (tdef, (l, _))) ->
   let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
   match tdef with
-  | TD_abbrev (id, typq, (A_aux (A_typ _, _) as typ_arg)) ->
-     [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
-  (* For type synonyms for non-Type kinds we omit them from the AST *)
   | TD_abbrev (id, typq, typ_arg) ->
-     [], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
+     [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
   | TD_record (id, nmscm, typq, fields, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
   | TD_variant (id, nmscm, typq, arms, _) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 0a0e18f7..04ff48f7 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -84,7 +84,7 @@ type type_error =
 
 exception Type_error of l * type_error;;
 
-val typ_debug : string Lazy.t -> unit
+val typ_debug : ?level:int -> string Lazy.t -> unit
 val typ_print : string Lazy.t -> unit
 
 (** {2 Environments} *)