Improve error messages for unsolved function quantifiers

For example, for a function like

```
val aget_X : forall 'n, 0 <= 'n <= 31. int('n) -> bits(64)

function test(n : int) -> unit = {
  let y = aget_X(n);
  ()
}
```

we get the message

> Could not resolve quantifiers for aget_X (0 <= 'ex7# & 'ex7# <= 31)
>
> Try adding named type variables for n : atom('ex7#)
>
> The property (0 <= n & n <= 31) must hold

which suggests adding a name for the type variable 'ex7#, and gives
the property in terms of the variable n. If we give n a type variable name:

```
val test : int -> unit

function test(n as 'N) = {
  let y = aget_X(n);
  ()
}
```

It will suggest a constraint involving the type variable name

> Could not resolve quantifiers for aget_X (0 <= 'ex6# & 'ex6# <= 31)
>
> Try adding the constraint (0 <= 'N & 'N <= 31)

13 files changed, 318 insertions, 238 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 0f98caff..2e7b6b65 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -458,17 +458,17 @@ let rec split_block l = function
 let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) =
   let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in
   match p_aux with
-  | P_id id when global -> mk_apat (AP_global (id, pat_typ_of pat))
-  | P_id id -> mk_apat (AP_id (id, pat_typ_of pat))
-  | P_wild -> mk_apat (AP_wild (pat_typ_of pat))
+  | P_id id when global -> mk_apat (AP_global (id, typ_of_pat pat))
+  | P_id id -> mk_apat (AP_id (id, typ_of_pat pat))
+  | P_wild -> mk_apat (AP_wild (typ_of_pat pat))
   | P_tup pats -> mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats))
-  | P_app (id, [subpat]) -> mk_apat (AP_app (id, anf_pat ~global:global subpat, pat_typ_of pat))
-  | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)), pat_typ_of pat))
+  | P_app (id, [subpat]) -> mk_apat (AP_app (id, anf_pat ~global:global subpat, typ_of_pat pat))
+  | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)), typ_of_pat pat))
   | P_typ (_, pat) -> anf_pat ~global:global pat
   | P_var (pat, _) -> anf_pat ~global:global pat
   | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat))
-  | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (pat_typ_of pat)))
-  | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (pat_typ_of pat))
+  | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat)))
+  | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat))
   | _ -> anf_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat)
 
 let rec apat_globals (AP_aux (aux, _, _)) =
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 9966742e..9490366f 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1082,7 +1082,7 @@ let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
   | Nexp_neg n -> tyvars_of_nexp n
   | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
 
-let rec tyvars_of_nc (NC_aux (nc, _)) =
+let rec tyvars_of_constraint (NC_aux (nc, _)) =
   match nc with
   | NC_equal (nexp1, nexp2)
   | NC_bounded_ge (nexp1, nexp2)
@@ -1092,7 +1092,7 @@ let rec tyvars_of_nc (NC_aux (nc, _)) =
   | NC_set (kid, _) -> KidSet.singleton kid
   | NC_or (nc1, nc2)
   | NC_and (nc1, nc2) ->
-     KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2)
+     KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
   | NC_app (id, nexps) ->
      List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
   | NC_true
@@ -1112,7 +1112,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) =
      List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta))
        KidSet.empty tas
   | Typ_exist (kids, nc, t) ->
-     let s = KidSet.union (tyvars_of_typ t) (tyvars_of_nc nc) in
+     let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in
      List.fold_left (fun s k -> KidSet.remove k s) s kids
 and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) =
   match ta with
@@ -1123,7 +1123,7 @@ and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) =
 let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with
   | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
      KidSet.singleton kid
-  | QI_const nc -> tyvars_of_nc nc
+  | QI_const nc -> tyvars_of_constraint nc
 
 let is_kid_generated kid = String.contains (string_of_kid kid) '#'
 
@@ -1488,3 +1488,128 @@ and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fe
 
 and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) ->
   FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot))
+
+(**************************************************************************)
+(* 1. Substitutions                                                       *)
+(**************************************************************************)
+
+let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
+and nexp_subst_aux sv subst = function
+  | Nexp_id v -> Nexp_id v
+  | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid
+  | Nexp_constant c -> Nexp_constant c
+  | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps)
+  | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
+  | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
+
+let rec nexp_set_to_or l subst = function
+  | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Empty set in constraint")
+  | [int] -> NC_equal (subst, nconstant int)
+  | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
+
+let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
+and nc_subst_nexp_aux l sv subst = function
+  | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_set (kid, ints) as set_nc ->
+     if Kid.compare kid sv = 0
+     then nexp_set_to_or l (mk_nexp subst) ints
+     else set_nc
+  | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
+  | NC_false -> NC_false
+  | NC_true -> NC_true
+
+let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
+and typ_subst_nexp_aux sv subst = function
+  | Typ_internal_unknown -> Typ_internal_unknown
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> Typ_var kid
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs)
+  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
+  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst nc, typ_subst_nexp sv subst typ)
+and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l)
+and typ_subst_arg_nexp_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ)
+  | Typ_arg_order ord -> Typ_arg_order ord
+
+let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l)
+and typ_subst_typ_aux sv subst = function
+  | Typ_internal_unknown -> Typ_internal_unknown
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs)
+  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ)
+and typ_subst_arg_typ sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_typ_aux sv subst arg, l)
+and typ_subst_arg_typ_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ)
+  | Typ_arg_order ord -> Typ_arg_order ord
+
+let order_subst_aux sv subst = function
+  | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid
+  | Ord_inc -> Ord_inc
+  | Ord_dec -> Ord_dec
+
+let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l)
+
+let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l)
+and typ_subst_order_aux sv subst = function
+  | Typ_internal_unknown -> Typ_internal_unknown
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> Typ_var kid
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs)
+  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ)
+and typ_subst_arg_order sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_order_aux sv subst arg, l)
+and typ_subst_arg_order_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ)
+  | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord)
+
+let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l)
+and typ_subst_kid_aux sv subst = function
+  | Typ_internal_unknown -> Typ_internal_unknown
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs)
+  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args)
+  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) nc, typ_subst_kid sv subst typ)
+and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l)
+and typ_subst_arg_kid_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp)
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ)
+  | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord)
+
+let quant_item_subst_kid_aux sv subst = function
+  | QI_id (KOpt_aux (KOpt_none kid, l)) as qid ->
+     if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid
+  | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid ->
+     if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid
+  | QI_const nc -> QI_const (nc_subst_nexp sv (Nexp_var subst) nc)
+
+let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l)
+
+let typquant_subst_kid_aux sv subst = function
+  | TypQ_tq quants -> TypQ_tq (List.map (quant_item_subst_kid sv subst) quants)
+  | TypQ_no_forall -> TypQ_no_forall
+
+let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ea287190..fae7b81c 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -320,6 +320,7 @@ val union_effects : effect -> effect -> effect
 
 val tyvars_of_nexp : nexp -> KidSet.t
 val tyvars_of_typ : typ -> KidSet.t
+val tyvars_of_constraint : n_constraint -> KidSet.t
 val tyvars_of_quant_item : quant_item -> KidSet.t
 val is_kid_generated : kid -> bool
 
@@ -353,7 +354,6 @@ val subst : id -> 'a exp -> 'a exp -> 'a exp
 
 val hex_to_bin : string -> string
 
-
 (** locate takes an expression and recursively sets the location in
    every subexpression to the provided location. Expressions build
    using mk_exp and similar do not have locations, so they can then be
@@ -366,3 +366,30 @@ val locate_pat : l -> 'a pat -> 'a pat
 val locate_lexp : l -> 'a lexp -> 'a lexp
 
 val locate_typ : l -> typ -> typ
+
+(** Substitutions *)
+
+(* The function X_subst_Y substitutes a Y into something of type X, if
+   X = Y then the function is just X_subst. Substitutions are always
+   unwrapped from their aux constructors. *)
+val nexp_subst : kid -> nexp_aux -> nexp -> nexp
+val nc_subst_nexp : kid -> nexp_aux -> n_constraint -> n_constraint
+val order_subst : kid -> order_aux -> order -> order
+
+(* kid must be Int-kinded *)
+val typ_subst_nexp : kid -> nexp_aux -> typ -> typ
+val typ_subst_arg_nexp : kid -> nexp_aux -> typ_arg -> typ_arg
+
+(* kid must be Type-kinded *)
+val typ_subst_typ : kid -> typ_aux -> typ -> typ
+val typ_subst_arg_typ : kid -> typ_aux -> typ_arg -> typ_arg
+
+(* kid must be Order-kinded *)
+val typ_subst_order : kid -> order_aux -> typ -> typ
+val typ_subst_arg_order : kid -> order_aux -> typ_arg -> typ_arg
+
+val typ_subst_kid : kid -> kid -> typ -> typ
+val typ_subst_arg_kid : kid -> kid -> typ_arg -> typ_arg
+
+val quant_item_subst_kid : kid -> kid -> quant_item -> quant_item
+val typquant_subst_kid : kid -> kid -> typquant -> typquant
diff --git a/src/c_backend.ml b/src/c_backend.ml
index d825bbae..392f2349 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1617,7 +1617,7 @@ let rec compile_def ctx = function
 
   | DEF_val (LB_aux (LB_val (pat, exp), _)) ->
      c_debug (lazy ("Compiling letbind " ^ string_of_pat pat));
-     let ctyp = ctyp_of_typ ctx (pat_typ_of pat) in
+     let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in
      let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in
      let setup, call, cleanup = compile_aexp ctx aexp in
      let apat = anf_pat ~global:true pat in
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 2ea8bb00..540e96a1 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -592,13 +592,13 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
         recursive call that has an empty_tannot we must not use the
         annotation in the whole vector_concat pattern. *)
      let open Type_check in
-     begin match destruct_vector (pat_env_of pat) (pat_typ_of pat) with
+     begin match destruct_vector (env_of_pat pat) (typ_of_pat pat) with
      | Some (Nexp_aux (Nexp_constant n, _), _, _) ->
         let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in
         let init_match, init_bind = pattern_match env pat (V_vector init) in
         let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in
         init_match && rest_match, Bindings.merge combine init_bind rest_bind
-     | _ -> failwith ("Bad vector annotation " ^ string_of_typ (Type_check.pat_typ_of pat))
+     | _ -> failwith ("Bad vector annotation " ^ string_of_typ (Type_check.typ_of_pat pat))
      end
   | P_tup [pat] -> pattern_match env pat value
   | P_tup pats | P_list pats ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f7a481e6..258b4e1f 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1811,7 +1811,7 @@ let split_defs all_errors splits defs =
            (match spl p' with
            | None -> None
            | Some ps ->
-              let kids = equal_kids (pat_env_of p') kid in
+              let kids = equal_kids (env_of_pat p') kid in
               Some (List.map (fun (p,sub,pchoices,ksub) ->
                 P_aux (P_var (p,tp),(l,annot)), sub, pchoices,
                 List.concat
@@ -2325,7 +2325,7 @@ let rewrite_size_parameters env (Defs defs) =
     let (_,nexp_map) = List.fold_left add_parameter (0,NexpMap.empty) types in
     let nexp_list = NexpMap.bindings nexp_map in
 (* let () =
- print_endline ("Type of pattern for " ^ string_of_id id ^": " ^string_of_typ (pat_typ_of pat));
+ print_endline ("Type of pattern for " ^ string_of_id id ^": " ^string_of_typ (typ_of_pat pat));
  print_endline ("Types : " ^ String.concat ", " (List.map string_of_typ types));
  print_endline ("Nexp map for " ^ string_of_id id);
  List.iter (fun (nexp, i) -> print_endline ("  " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list
@@ -2871,7 +2871,7 @@ let mk_subrange_pattern vannot vstart vend =
           let end_len = Big_int.pred (Big_int.sub len vend) in
           (* Wrap pat in its type; in particular the type checker won't
              manage P_wild in the middle of a P_vector_concat *)
-          let pat = P_aux (P_typ (pat_typ_of pat, pat),(Generated (pat_loc pat),empty_tannot)) in
+          let pat = P_aux (P_typ (typ_of_pat pat, pat),(Generated (pat_loc pat),empty_tannot)) in
           let pats = if Big_int.greater end_len Big_int.zero then
               [pat;P_aux (P_typ (vector_typ (nconstant end_len) ord typ,
                                  P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot))]
@@ -3373,7 +3373,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
     else
       (* When there's no argument to case split on for a kid, we'll add a
          case expression instead *)
-      let env = pat_env_of pat in
+      let env = env_of_pat pat in
       let split = default_split (mk_tannot env int_typ no_effect) (KidSet.singleton kid) in
       let extra_splits = ExtraSplits.singleton (fn_id, fn_l)
         (KBindings.singleton kid split) in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 62a56c3d..77e3072b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -187,7 +187,7 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
   match pat_aux with
   | P_id id ->
      begin
-       match Env.lookup_id id (pat_env_of pat) with
+       match Env.lookup_id id (env_of_pat pat) with
        | Local (_, _) | Unbound -> zencode ctx id
        | Enum _ -> zencode_upper ctx id
        | _ -> failwith ("Ocaml: Cannot pattern match on register: " ^ string_of_pat pat)
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f1726ce4..2810d0ee 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1817,7 +1817,7 @@ let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) =
    that they've been merged. *)
 
 let rec atom_constraint ctxt (pat, typ) =
-  let typ = Env.base_typ_of (pat_env_of pat) typ in
+  let typ = Env.base_typ_of (env_of_pat pat) typ in
   match pat, typ with
   | P_aux (P_id id, _),
       Typ_aux (Typ_app (Id_aux (Id "atom",_),
diff --git a/src/rewriter.ml b/src/rewriter.ml
index a7505ca7..3eb0ffe6 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -103,7 +103,7 @@ let rec remove_p_typ = function
   | pat -> pat
 
 let add_p_typ typ (P_aux (paux, annot) as pat) =
-  let typ' = resolve_generated_kids (pat_env_of pat) typ in
+  let typ' = resolve_generated_kids (env_of_pat pat) typ in
   if KidSet.is_empty (generated_kids typ') then
     P_aux (P_typ (typ', remove_p_typ pat), annot)
   else pat
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c470d906..313d30e5 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -592,7 +592,7 @@ let rewrite_sizeof (Defs defs) =
         let penv = env_of_annot pannot in
         let peff = effect_of_annot (snd pannot) in
         if KidSet.is_empty nvars then paux else
-          match pat_typ_of paux with
+          match typ_of_pat paux with
           | Typ_aux (Typ_tup typs, _) ->
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ typs), l) in
              (match pat with
@@ -1156,8 +1156,8 @@ let subst_id_exp exp (id1,id2) =
 
 let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
   let rewrap e = E_aux (e,(l,annot)) in
-  let env = pat_env_of p_aux in
-  let typ = pat_typ_of p_aux in
+  let env = env_of_pat p_aux in
+  let typ = typ_of_pat p_aux in
   match pat with
   | P_lit lit -> rewrap (E_lit lit)
   | P_wild -> raise (Reporting_basic.err_unreachable l __POS__
@@ -1322,7 +1322,7 @@ let contains_bitvector_pexp = function
 
 let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
 
-  let env = try pat_env_of pat with _ -> Env.empty in
+  let env = try env_of_pat pat with _ -> Env.empty in
 
   (* first introduce names for bitvector patterns *)
   let name_bitvector_roots =
@@ -1360,7 +1360,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     } in
   let pat, env = bind_pat_no_guard env
     (strip_pat ((fold_pat name_bitvector_roots pat) false))
-    (pat_typ_of pat) in
+    (typ_of_pat pat) in
 
   (* Then collect guard expressions testing whether the literal bits of a
      bitvector pattern match those of a given bitvector, and collect let
@@ -1607,7 +1607,7 @@ let rewrite_defs_remove_numeral_pats =
     fold_pat { (compute_pat_alg None compose_guard_opt) with p_lit = p_lit outer_env } in
   let pat_aux (pexp_aux, a) =
     let pat,guard,exp,a = destruct_pexp (Pat_aux (pexp_aux, a)) in
-    let guard',pat = guard_pat (pat_env_of pat) pat in
+    let guard',pat = guard_pat (env_of_pat pat) pat in
     match compose_guard_opt guard guard' with
     | Some g -> Pat_aux (Pat_when (pat, g, exp), a)
     | None -> Pat_aux (Pat_exp (pat, exp), a) in
@@ -2131,7 +2131,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
            let pat, guard, exp, annot = destruct_pexp pexp in
            match pat with
              | P_aux (P_app (constr_id, args), pannot) ->
-                let argstup_typ = tuple_typ (List.map pat_typ_of args) in
+                let argstup_typ = tuple_typ (List.map typ_of_pat args) in
                 let pannot' = swaptyp argstup_typ pannot in
                 let pat' =
                   match args with
@@ -2172,7 +2172,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
       let env, args_typ, ret_typ = match funcls with
         | FCL_aux (FCL_Funcl (_, pexp), _) :: _ ->
            let pat, _, exp, _ = destruct_pexp pexp in
-           env_of exp, pat_typ_of pat, typ_of exp
+           env_of exp, typ_of_pat pat, typ_of exp
         | _ ->
            raise (Reporting_basic.err_unreachable l __POS__
              "rewrite_split_fun_constr_pats: empty auxiliary function")
@@ -3032,13 +3032,13 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno
        | [] -> pexp
        | gs ->
           let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in
-          check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp)
+          check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp)
      end
   | Pat_when (pat, guard, exp) ->
      begin
        let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in
        let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in
-       check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp)
+       check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp)
      end
 
 
@@ -3077,7 +3077,7 @@ let rec bindings_of_pat (P_aux (p_aux, p_annot) as pat) =
   | P_record _ -> failwith "record patterns not yet implemented"
   (* we assume the type-checker has already checked the two sides have the same bindings *)
   | P_or (left, right) -> bindings_of_pat left
-  | P_as (p, id) -> [annot_pat (P_id id) unk (pat_env_of p) (pat_typ_of p)]
+  | P_as (p, id) -> [annot_pat (P_id id) unk (env_of_pat p) (typ_of_pat p)]
   | P_cons (left, right) -> bindings_of_pat left @ bindings_of_pat right
   (* todo: is this right for negated patterns? *)
   | P_not p
@@ -3093,11 +3093,11 @@ let rec bindings_of_pat (P_aux (p_aux, p_annot) as pat) =
 let rec binding_typs_of_pat (P_aux (p_aux, p_annot) as pat) =
   match p_aux with
   | P_lit _ | P_wild -> []
-  | P_id id -> [pat_typ_of pat]
+  | P_id id -> [typ_of_pat pat]
   | P_record _ -> failwith "record patterns not yet implemented"
   (* we assume the type-checker has already checked the two sides have the same bindings *)
   | P_or (left, right) -> binding_typs_of_pat left
-  | P_as (p, id) -> [pat_typ_of p]
+  | P_as (p, id) -> [typ_of_pat p]
   | P_cons (left, right) -> binding_typs_of_pat left @ binding_typs_of_pat right
   (* todo: is this right for negated patterns? *)
   | P_not p
@@ -3226,7 +3226,7 @@ let construct_toplevel_string_append_func env f_id pat =
        let tup_arg_pat = match arg_pats with
          | [] -> assert false
          | [arg_pat] -> arg_pat
-         | arg_pats -> annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map pat_typ_of arg_pats))
+         | arg_pats -> annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map typ_of_pat arg_pats))
        in
 
        let some_pat = annot_pat (P_app (mk_id "Some",
@@ -3402,7 +3402,7 @@ let rec rewrite_defs_pat_string_append =
        let tup_arg_pat = match arg_pats with
          | [] -> assert false
          | [arg_pat] -> arg_pat
-         | arg_pats -> annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map pat_typ_of arg_pats))
+         | arg_pats -> annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map typ_of_pat arg_pats))
        in
 
        let some_pat = annot_pat (P_app (mk_id "Some",
@@ -3450,13 +3450,13 @@ let rec rewrite_defs_pat_string_append =
          | [] -> assert false
          | [arg_pat] -> annot_letbind
                           (P_tup [arg_pat; annot_pat (P_id len_id) unk env nat_typ], new_binding)
-                          unk env (tuple_typ [pat_typ_of arg_pat; nat_typ])
+                          unk env (tuple_typ [typ_of_pat arg_pat; nat_typ])
          | arg_pats -> annot_letbind
                          (P_tup
-                            [annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map pat_typ_of arg_pats));
+                            [annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map typ_of_pat arg_pats));
                              annot_pat (P_id len_id) unk env nat_typ],
                           new_binding)
-                         unk env (tuple_typ [tuple_typ (List.map pat_typ_of arg_pats); nat_typ])
+                         unk env (tuple_typ [tuple_typ (List.map typ_of_pat arg_pats); nat_typ])
        in
        let new_let = annot_exp (E_let (new_letbind, new_match)) unk env (typ_of expr) in
 
@@ -3562,7 +3562,7 @@ let rewrite_defs_mapping_patterns =
       expr_ref := e;
       p
     in
-    let env = pat_env_of pat in
+    let env = env_of_pat pat in
     match pat with
       (*
           mapping(args) if g => expr ----> s# if mapping_matches(s#)
@@ -3769,10 +3769,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
   let tuple_pat = function
     | [] -> annot_pat P_wild l env unit_typ
     | [pat] ->
-       let typ = pat_typ_of pat in
+       let typ = typ_of_pat pat in
        add_p_typ typ pat
     | pats ->
-       let typ = tuple_typ (List.map pat_typ_of pats) in
+       let typ = tuple_typ (List.map typ_of_pat pats) in
        add_p_typ typ (annot_pat (P_tup pats) l env typ) in
 
   let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars =
@@ -5029,8 +5029,8 @@ let rewrite_check_annot =
       Type_error (l, err) -> raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
   in
   let check_pat pat =
-    prerr_endline ("CHECKING PAT: " ^ string_of_pat pat ^ " : " ^ string_of_typ (pat_typ_of pat));
-    let _, _ = bind_pat_no_guard (pat_env_of pat) (strip_pat pat) (pat_typ_of pat) in
+    prerr_endline ("CHECKING PAT: " ^ string_of_pat pat ^ " : " ^ string_of_typ (typ_of_pat pat));
+    let _, _ = bind_pat_no_guard (env_of_pat pat) (strip_pat pat) (typ_of_pat pat) in
     pat
   in
 
diff --git a/src/type_check.ml b/src/type_check.ml
index cf1d8ef9..3e6ec2a3 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -92,7 +92,7 @@ type type_error =
      coercions *)
   | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
-  | Err_unresolved_quants of id * quant_item list
+  | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list
   | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
@@ -216,136 +216,10 @@ and strip_kind_aux = function
 and strip_base_kind = function
   | BK_aux (bk_aux, _) -> BK_aux (bk_aux, Parse_ast.Unknown)
 
-
-(**************************************************************************)
-(* 1. Substitutions                                                       *)
-(**************************************************************************)
-
-let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
-and nexp_subst_aux sv subst = function
-  | Nexp_id v -> Nexp_id v
-  | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid
-  | Nexp_constant c -> Nexp_constant c
-  | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
-  | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
-  | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
-  | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps)
-  | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
-  | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
-
-let rec nexp_set_to_or l subst = function
-  | [] -> typ_error l "Cannot substitute into empty nexp set"
-  | [int] -> NC_equal (subst, nconstant int)
-  | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
-
-let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
-and nc_subst_nexp_aux l sv subst = function
-  | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
-  | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
-  | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
-  | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
-  | NC_set (kid, ints) as set_nc ->
-     if Kid.compare kid sv = 0
-     then nexp_set_to_or l (mk_nexp subst) ints
-     else set_nc
-  | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
-  | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
-  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
-  | NC_false -> NC_false
-  | NC_true -> NC_true
-
-let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
-and typ_subst_nexp_aux sv subst = function
-  | Typ_internal_unknown -> Typ_internal_unknown
-  | Typ_id v -> Typ_id v
-  | Typ_var kid -> Typ_var kid
-  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2)
-  | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
-  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
-  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst nc, typ_subst_nexp sv subst typ)
-and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l)
-and typ_subst_arg_nexp_aux sv subst = function
-  | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
-  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ)
-  | Typ_arg_order ord -> Typ_arg_order ord
-
-let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l)
-and typ_subst_typ_aux sv subst = function
-  | Typ_internal_unknown -> Typ_internal_unknown
-  | Typ_id v -> Typ_id v
-  | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
-  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2)
-  | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
-  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ)
-and typ_subst_arg_typ sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_typ_aux sv subst arg, l)
-and typ_subst_arg_typ_aux sv subst = function
-  | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
-  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ)
-  | Typ_arg_order ord -> Typ_arg_order ord
-
-let order_subst_aux sv subst = function
-  | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid
-  | Ord_inc -> Ord_inc
-  | Ord_dec -> Ord_dec
-
-let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l)
-
-let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l)
-and typ_subst_order_aux sv subst = function
-  | Typ_internal_unknown -> Typ_internal_unknown
-  | Typ_id v -> Typ_id v
-  | Typ_var kid -> Typ_var kid
-  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2)
-  | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs)
-  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ)
-and typ_subst_arg_order sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_order_aux sv subst arg, l)
-and typ_subst_arg_order_aux sv subst = function
-  | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
-  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ)
-  | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord)
-
-let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l)
-and typ_subst_kid_aux sv subst = function
-  | Typ_internal_unknown -> Typ_internal_unknown
-  | Typ_id v -> Typ_id v
-  | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid
-  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs)
-  | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2)
-  | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs)
-  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args)
-  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) nc, typ_subst_kid sv subst typ)
-and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l)
-and typ_subst_arg_kid_aux sv subst = function
-  | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp)
-  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ)
-  | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord)
-
-let quant_item_subst_kid_aux sv subst = function
-  | QI_id (KOpt_aux (KOpt_none kid, l)) as qid ->
-     if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid
-  | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid ->
-     if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid
-  | QI_const nc -> QI_const (nc_subst_nexp sv (Nexp_var subst) nc)
-
-let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l)
-
-let typquant_subst_kid_aux sv subst = function
-  | TypQ_tq quants -> TypQ_tq (List.map (quant_item_subst_kid sv subst) quants)
-  | TypQ_no_forall -> TypQ_no_forall
-
-let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l)
-
 let adding = Util.("Adding " |> darkgray |> clear)
 
 (**************************************************************************)
-(* 2. Environment                                                         *)
+(* 1. Environment                                                         *)
 (**************************************************************************)
 
 module Env : sig
@@ -1366,7 +1240,7 @@ and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) =
   | Typ_arg_order (Ord_aux (Ord_var _, _)) -> false
 
 (**************************************************************************)
-(* 3. Subtyping and constraint solving                                    *)
+(* 2. Subtyping and constraint solving                                    *)
 (**************************************************************************)
 
 let rec simp_typ (Typ_aux (typ_aux, l)) = Typ_aux (simp_typ_aux typ_aux, l)
@@ -1489,7 +1363,7 @@ let prove env (NC_aux (nc_aux, _) as nc) =
   | _ -> prove_z3 env nc
 
 (**************************************************************************)
-(* 4. Unification                                                         *)
+(* 3. Unification                                                         *)
 (**************************************************************************)
 
 let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) =
@@ -1759,7 +1633,7 @@ let merge_unifiers l kid uvar1 uvar2 =
   | None, None -> None
 
 let rec unify l env typ1 typ2 =
-  typ_print (lazy ("Unify " ^ string_of_typ typ1 ^ " with " ^ string_of_typ typ2));
+  typ_print (lazy (Util.("Unify " |> magenta |> clear) ^ string_of_typ typ1 ^ " with " ^ string_of_typ typ2));
   let goals = KidSet.inter (KidSet.diff (typ_frees typ1) (typ_frees typ2)) (typ_frees typ1) in
 
   let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) =
@@ -1845,7 +1719,7 @@ let merge_uvars l unifiers1 unifiers2 =
   | Unification_error (_, m) -> typ_error l ("Could not merge unification variables: " ^ m)
 
 (**************************************************************************)
-(* 4.5. Subtyping with existentials                                       *)
+(* 3.5. Subtyping with existentials                                       *)
 (**************************************************************************)
 
 let destruct_atom_nexp env typ =
@@ -2012,7 +1886,7 @@ let subtype_check env typ1 typ2 =
   | Type_error _ -> false
 
 (**************************************************************************)
-(* 5. Type checking expressions                                           *)
+(* 4. Type checking expressions                                           *)
 (**************************************************************************)
 
 (* The type checker produces a fully annoted AST - tannot is the type
@@ -2168,9 +2042,9 @@ let typ_of (E_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
 let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
-let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
+let typ_of_pat (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
-let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot)
+let env_of_pat (P_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
 let typ_of_pexp (Pat_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
@@ -2701,7 +2575,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ =
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
   let (Typ_aux (typ_aux, _) as typ), env = bind_existential l typ env in
-  typ_print (lazy ("Binding " ^ string_of_pat pat ^  " to " ^ string_of_typ typ));
+  typ_print (lazy (Util.("Binding " |> yellow |> clear) ^ string_of_pat pat ^  " to " ^ string_of_typ typ));
   let annot_pat pat typ' = P_aux (pat, (l, Some ((env, typ', no_effect), Some typ))) in
   let switch_typ pat typ = match pat with
     | P_aux (pat_aux, (l, Some ((env, _, eff), exp_typ))) -> P_aux (pat_aux, (l, Some ((env, typ, eff), exp_typ)))
@@ -2887,15 +2761,15 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      typ_error l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat)
   | P_as (pat, id) ->
      let (typed_pat, env, guards) = bind_pat env pat typ in
-     annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards
+     annot_pat (P_as (typed_pat, id)) (typ_of_pat typed_pat), Env.add_local id (Immutable, typ_of_pat typed_pat) env, guards
   (* This is a special case for flow typing when we match a constant numeric literal. *)
   | P_lit (L_aux (L_num n, _) as lit) when is_atom typ ->
      let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in
      annot_pat (P_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, []
   | _ ->
      let (inferred_pat, env, guards) = infer_pat env pat in
-     match subtyp l env typ (pat_typ_of inferred_pat) with
-     | () -> switch_typ inferred_pat (pat_typ_of inferred_pat), env, guards
+     match subtyp l env typ (typ_of_pat inferred_pat) with
+     | () -> switch_typ inferred_pat (typ_of_pat inferred_pat), env, guards
      | exception (Type_error _ as typ_exn) ->
         match pat_aux with
         | P_lit lit ->
@@ -2952,8 +2826,8 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      in
      let pats, env, guards = List.fold_left fold_pats ([], env, []) (pat :: pats) in
      let len = nexp_simp (nint (List.length pats)) in
-     let etyp = pat_typ_of (List.hd pats) in
-     List.iter (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats;
+     let etyp = typ_of_pat (List.hd pats) in
+     List.iter (fun pat -> typ_equality l env etyp (typ_of_pat pat)) pats;
      annot_pat (P_vector pats) (dvector_typ env len etyp), env, guards
   | P_vector_concat (pat :: pats) ->
      let fold_pats (pats, env, guards) pat =
@@ -2962,9 +2836,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      in
      let inferred_pats, env, guards =
        List.fold_left fold_pats ([], env, []) (pat :: pats) in
-     let (len, _, vtyp) = destruct_vec_typ l env (pat_typ_of (List.hd inferred_pats)) in
+     let (len, _, vtyp) = destruct_vec_typ l env (typ_of_pat (List.hd inferred_pats)) in
      let fold_len len pat =
-       let (len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in
+       let (len', _, vtyp') = destruct_vec_typ l env (typ_of_pat pat) in
        typ_equality l env vtyp vtyp';
        nsum len len'
      in
@@ -2973,7 +2847,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
   | P_string_append pats ->
      let fold_pats (pats, env, guards) pat =
        let inferred_pat, env, guards' = infer_pat env pat in
-       typ_equality l env (pat_typ_of inferred_pat) string_typ;
+       typ_equality l env (typ_of_pat inferred_pat) string_typ;
        pats @ [inferred_pat], env, guards' @ guards
      in
      let typed_pats, env, guards =
@@ -2982,8 +2856,8 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      annot_pat (P_string_append typed_pats) string_typ, env, guards
   | P_as (pat, id) ->
      let (typed_pat, env, guards) = infer_pat env pat in
-     annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat),
-     Env.add_local id (Immutable, pat_typ_of typed_pat) env,
+     annot_pat (P_as (typed_pat, id)) (typ_of_pat typed_pat),
+     Env.add_local id (Immutable, typ_of_pat typed_pat) env,
      guards
   | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat)
 
@@ -3462,8 +3336,14 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
          then
            let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in
            (iuargs, ret_typ, env)
-         else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
-                           ^ " not resolved during application of " ^ string_of_id f ^ " unresolved args: " ^ string_of_list ", " (fun (_, exp) -> string_of_exp exp) uargs)
+         else typ_raise l (Err_unresolved_quants (f, quants, Env.get_locals env, Env.get_constraints env))
+(*
+           typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
+                           ^ " not resolved during application of " ^ string_of_id f
+                           ^ " unresolved args: " ^ string_of_list ", " (fun (_, exp) -> string_of_exp exp) uargs
+                           ^ "\nAll constraints: " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
+                           ^ "\nLocals: " ^ string_of_list ", " (fun (id, (mut, typ)) -> string_of_id id ^ " : " ^ string_of_typ typ) (Bindings.bindings (Env.get_locals env)))
+ *)
        end
     | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args))
          when List.for_all (fun kid -> is_bound kid env) (KidSet.elements (typ_frees typ)) ->
@@ -3862,7 +3742,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
      typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat)
 
 (**************************************************************************)
-(* 6. Effect system                                                       *)
+(* 5. Effect system                                                       *)
 (**************************************************************************)
 
 let effect_of_annot = function
@@ -4375,7 +4255,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
     | Some id -> id
     | None -> typ_error l "funcl list is empty"
   in
-  typ_print (lazy ("\nChecking function " ^ string_of_id id));
+  typ_print (lazy ("\n" ^ Util.("Check function " |> cyan |> clear) ^ string_of_id id));
   let have_val_spec, (quant, typ), env =
     try true, Env.get_val_spec id env, env with
     | Type_error (l, _) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 8d2b02a9..ae46d956 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -76,7 +76,7 @@ val opt_constraint_synonyms : bool ref
 type type_error =
   | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
-  | Err_unresolved_quants of id * quant_item list
+  | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list
   | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
@@ -95,7 +95,7 @@ module Env : sig
   type t
 
   (** Note: Most get_ functions assume the identifiers exist, and throw
-     type errors if it doesn't. *)
+     type errors if they don't. *)
 
   (** Get the quantifier and type for a function identifier, freshening
       type variables. *)
@@ -321,9 +321,8 @@ val env_of_annot : Ast.l * tannot -> Env.t
 val typ_of : tannot exp -> typ
 val typ_of_annot : Ast.l * tannot -> typ
 
-
-val pat_typ_of : tannot pat -> typ
-val pat_env_of : tannot pat -> Env.t
+val typ_of_pat : tannot pat -> typ
+val env_of_pat : tannot pat -> Env.t
 
 val typ_of_pexp : tannot pexp -> typ
 val env_of_pexp : tannot pexp -> Env.t
@@ -367,11 +366,6 @@ val string_of_uvar : uvar -> string
 
 val subst_unifiers : uvar KBindings.t -> typ -> typ
 
-val typ_subst_nexp : kid -> nexp_aux -> typ -> typ
-val typ_subst_typ : kid -> typ_aux -> typ -> typ
-val typ_subst_order : kid -> order_aux -> typ -> typ
-val typ_subst_kid : kid -> kid -> typ -> typ
-
 val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option
 
 val alpha_equivalent : Env.t -> typ -> typ -> bool
diff --git a/src/type_error.ml b/src/type_error.ml
index 78db65bc..5e2ce628 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -58,35 +58,6 @@ let bullet f xs =
   group (separate_map hardline (fun x -> string "* " ^^ nest 2 (f x)) xs)
 
 let pp_nexp, pp_n_constraint =
-  let rec string_of_nexp = function
-    | Nexp_aux (nexp, _) -> string_of_nexp_aux nexp
-  and string_of_nexp_aux = function
-    | Nexp_id id -> string_of_id id
-    | Nexp_var kid -> string_of_kid kid
-    | Nexp_constant c -> Big_int.to_string c
-    | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")"
-    | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")"
-    | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")"
-    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_nexp nexps ^ ")"
-    | Nexp_exp n -> "2 ^ " ^ string_of_nexp n
-    | Nexp_neg n -> "- " ^ string_of_nexp n
-  in
-
-  let string_of_n_constraint = function
-    | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
-    | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
-    | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
-    | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
-    | NC_aux (NC_or (nc1, nc2), _) ->
-       "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
-    | NC_aux (NC_and (nc1, nc2), _) ->
-       "(" ^ 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_true, _) -> "true"
-    | NC_aux (NC_false, _) -> "false"
-  in
-
   let pp_nexp' nexp =
     string (string_of_nexp nexp)
   in
@@ -94,9 +65,90 @@ let pp_nexp, pp_n_constraint =
   let pp_n_constraint' nc =
     string (string_of_n_constraint nc)
   in
-
   pp_nexp', pp_n_constraint'
 
+let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
+and nexp_subst_aux sv subst = function
+  | Nexp_id v -> Nexp_id v
+  | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid
+  | Nexp_constant c -> Nexp_constant c
+  | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps)
+  | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
+  | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
+
+let rec nexp_set_to_or l subst = function
+  | [] -> typ_error l "Cannot substitute into empty nexp set"
+  | [int] -> NC_equal (subst, nconstant int)
+  | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
+
+let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
+and nc_subst_nexp_aux l sv subst = function
+  | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_set (kid, ints) as set_nc ->
+     if Kid.compare kid sv = 0
+     then nexp_set_to_or l (mk_nexp subst) ints
+     else set_nc
+  | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
+  | NC_false -> NC_false
+  | NC_true -> NC_true
+
+let rec analyze_unresolved_quant locals ncs = function
+  | QI_aux (QI_const nc, _) ->
+     let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in
+     if gen_kids = [] then
+       string ("Try adding the constraint: " ^ string_of_n_constraint nc)
+     else
+       (* If there are generated kind-identifiers in the constraint,
+          we don't want to make a suggestion based on them, so try to
+          look for generated kid free nexps in the set of constraints
+          that are equal to the generated identifier. This often
+          occurs due to how the type-checker introduces new type
+          variables. *)
+       let is_subst v = function
+         | NC_aux (NC_equal (Nexp_aux (Nexp_var v', _), nexp), _)
+              when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
+            [(v, nexp)]
+         | NC_aux (NC_equal (nexp, Nexp_aux (Nexp_var v', _)), _)
+              when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
+            [(v, nexp)]
+         | _ -> []
+       in
+       let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in
+       let nc = List.fold_left (fun nc (v, nexp) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+       if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
+         string ("Try adding the constraint " ^ string_of_n_constraint nc)
+       else
+         (* If we have a really anonymous type-variable, try to find a
+            regular variable that corresponds to it. *)
+         let is_linked v = function
+           | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
+                when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 ->
+              [(v, nid id, typ)]
+           | (id, (mut, typ)) ->
+              prerr_endline (string_of_id id ^ " : " ^ string_of_typ typ);
+              []
+         in
+         let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in
+         (string "Try adding named type variables for"
+          ^//^ string (Util.string_of_list ", " (fun (_, nexp, typ) -> string_of_nexp nexp ^ " : " ^ string_of_typ typ) substs))
+         ^^ twice hardline ^^
+         let nc = List.fold_left (fun nc (v, nexp, _) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+         if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
+           string ("The property " ^ string_of_n_constraint nc ^ " must hold")
+         else
+           empty
+
+  | QI_aux (QI_id kopt, _) ->
+     empty
+
 let rec pp_type_error = function
   | Err_no_casts (exp, typ_from, typ_to, trigger, _) ->
      let coercion =
@@ -123,9 +175,11 @@ let rec pp_type_error = function
   | Err_no_num_ident id ->
      string "No num identifier" ^^ space ^^ string (string_of_id id)
 
-  | Err_unresolved_quants (id, quants) ->
-     string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
-     ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants)
+  | Err_unresolved_quants (id, quants, locals, ncs) ->
+     (string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
+      ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants))
+     ^^ twice hardline
+     ^^ group (separate_map hardline (analyze_unresolved_quant locals ncs) quants)
 
   | Err_other str -> string str