Add feature that allows functions to require type variables are constant

can now write e.g.

forall (constant 'n : Int) rather than forall ('n: Int)

which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.

14 files changed, 176 insertions, 94 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 12777506..70845468 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -104,7 +104,7 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
 
 let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, body),no_annot)), no_annot)
 
-let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown)
+let mk_qi_nc nc = QI_aux (QI_constraint nc, Parse_ast.Unknown)
 
 let mk_qi_id k kid =
   let kopt =
@@ -460,9 +460,10 @@ let no_effect = mk_effect []
 
 let quant_add qi typq =
   match qi, typq with
-  | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq
+  | QI_aux (QI_constraint (NC_aux (NC_true, _)), _), _ -> typq
   | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l)
-  | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l)
+  | QI_aux (QI_constant _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l)
+  | QI_aux (QI_constraint nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l)
   | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l)
 
 let quant_items : typquant -> quant_item list = function
@@ -482,7 +483,7 @@ let quant_split typq =
     | _ -> []
   in
   let qi_nc = function
-    | QI_aux (QI_const nc, _) -> [nc]
+    | QI_aux (QI_constraint nc, _) -> [nc]
     | _ -> []
   in
   let qis = quant_items typq in
@@ -497,9 +498,9 @@ let is_quant_kopt = function
   | _ -> false
 
 let is_quant_constraint = function
-  | QI_aux (QI_const _, _) -> true
+  | QI_aux (QI_constraint _, _) -> true
   | _ -> false
-                               
+
 let unaux_nexp (Nexp_aux (nexp, _)) = nexp
 let unaux_order (Ord_aux (ord, _)) = ord
 let unaux_typ (Typ_aux (typ, _)) = typ
@@ -859,7 +860,8 @@ let string_of_kinded_id (KOpt_aux (KOpt_kind (k, kid), _)) = "(" ^ string_of_kid
 
 let string_of_quant_item_aux = function
   | QI_id kopt -> string_of_kinded_id kopt
-  | QI_const constr -> string_of_n_constraint constr
+  | QI_constant kopts -> "is_constant(" ^ Util.string_of_list ", " string_of_kinded_id kopts ^ ")"
+  | QI_constraint constr -> string_of_n_constraint constr
 
 let string_of_quant_item = function
   | QI_aux (qi, _) -> string_of_quant_item_aux qi
@@ -1374,7 +1376,8 @@ and kopts_of_typ_arg (A_aux (ta,_)) =
 let kopts_of_quant_item (QI_aux (qi, _)) = match qi with
   | QI_id kopt ->
      KOptSet.singleton kopt
-  | QI_const nc -> kopts_of_constraint nc
+  | QI_constant kopts -> KOptSet.of_list kopts
+  | QI_constraint nc -> kopts_of_constraint nc
 
 let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
   match nexp with
@@ -1431,7 +1434,8 @@ and tyvars_of_typ_arg (A_aux (ta,_)) =
 let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with
   | QI_id (KOpt_aux (KOpt_kind (_, kid), _)) ->
      KidSet.singleton kid
-  | QI_const nc -> tyvars_of_constraint nc
+  | QI_constant kopts -> KidSet.of_list (List.map kopt_kid kopts)
+  | QI_constraint nc -> tyvars_of_constraint nc
 
 let is_kid_generated kid = String.contains (string_of_kid kid) '#'
 
@@ -1935,11 +1939,16 @@ let subst_kid subst sv v x =
   |> subst sv (mk_typ_arg (A_order (Ord_aux (Ord_var v, Parse_ast.Unknown))))
   |> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v))))
 
+let kopt_subst_kid sv subst (KOpt_aux (KOpt_kind (k, kid), l) as orig) =
+  if Kid.compare kid sv = 0 then KOpt_aux (KOpt_kind (k, subst), l) else orig
+
 let quant_item_subst_kid_aux sv subst = function
-  | 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 (subst_kid constraint_subst sv subst nc)
+  | QI_id kopt ->
+     QI_id (kopt_subst_kid sv subst kopt)
+  | QI_constant kopts ->
+     QI_constant (List.map (kopt_subst_kid sv subst) kopts)
+  | QI_constraint nc ->
+     QI_constraint (subst_kid constraint_subst sv subst nc)
 
 let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l)
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 790a6624..ad52751b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -129,17 +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 }
+let to_ast_kopts ctx (P.KOpt_aux (aux, l)) =
+  let mk_kopt v k =
+    let v = to_ast_var v in
+    let k = to_ast_kind k in
+    KOpt_aux (KOpt_kind (k, v), l), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
   in
-  KOpt_aux (aux, l), ctx
+  match aux with
+  | P.KOpt_kind (attr, vs, None) ->
+     let k = P.K_aux (P.K_int, gen_loc l) in
+     List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr
+  | P.KOpt_kind (attr, vs, Some k) ->
+     List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr
 
 let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
   let aux = match aux with
@@ -171,7 +172,14 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
        end
     | 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)
+         List.fold_right (fun kopt (kopts, ctx) ->
+             let (kopts', ctx), attr = to_ast_kopts ctx kopt in
+             match attr with
+             | None ->
+                kopts' @ kopts, ctx
+             | Some attr ->
+                raise (Reporting.err_typ l (sprintf "Attribute %s cannot appear within an existential type" attr))
+           ) kopts ([], ctx)
        in
        Typ_exist (kopts, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
     | P.ATyp_base (id, kind, nc) ->
@@ -262,19 +270,25 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
   in
   NC_aux (aux, l)
 
-let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
+let to_ast_quant_items 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_constraint nc -> [QI_aux (QI_constraint (to_ast_constraint ctx nc), l)], ctx
   | P.QI_id kopt ->
-     let kopt, ctx = to_ast_kopt ctx kopt in
-     QI_aux (QI_id kopt, l), ctx
+     let (kopts, ctx), attr = to_ast_kopts ctx kopt in
+     match attr with
+     | Some "constant" ->
+        QI_aux (QI_constant kopts, l) :: List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx
+     | Some attr ->
+        raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr))
+     | None ->
+        List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx
 
 let to_ast_typquant ctx (P.TypQ_aux (aux, l)) =
   match aux with
   | P.TypQ_no_forall -> TypQ_aux (TypQ_no_forall, l), ctx
   | P.TypQ_tq quants ->
      let quants, ctx =
-       List.fold_left (fun (qis, ctx) qi -> let qi', ctx = to_ast_quant_item ctx qi in qi' :: qis, ctx) ([], ctx) quants
+       List.fold_left (fun (qis, ctx) qi -> let qis', ctx = to_ast_quant_items ctx qi in qis' @ qis, ctx) ([], ctx) quants
      in
      TypQ_aux (TypQ_tq (List.rev quants), l), ctx
 
@@ -547,9 +561,9 @@ let anon_rec_constructor_typ record_id = function
   | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
   | P.TypQ_aux (P.TypQ_tq quants, l) ->
      let rec quant_arg = function
-       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_none v, l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)]
-       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, v), l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)]
-       | P.QI_aux (P.QI_const _, _) -> []
+       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, _), l)), _) ->
+          List.map (fun v -> P.ATyp_aux (P.ATyp_var v, Generated l)) vs
+       | P.QI_aux (P.QI_constraint _, _) -> []
      in
      match List.concat (List.map quant_arg quants) with
      | [] -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
diff --git a/src/lexer.mll b/src/lexer.mll
index 43426d77..8000879e 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -147,6 +147,7 @@ let kw_table =
      ("scattered",               (fun x -> Scattered));
      ("sizeof",                  (fun x -> Sizeof));
      ("constraint",              (fun x -> Constraint));
+     ("constant",                (fun x -> Constant));
      ("struct",                  (fun x -> Struct));
      ("then",                    (fun x -> Then));
      ("true",                    (fun x -> True));
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index c011f4d0..1e52d708 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3583,7 +3583,7 @@ let rewrite_toplevel_nexps (Defs defs) =
        | [] -> None
        | _ ->
           let new_vars = List.map (fun (kid,nexp) -> QI_aux (QI_id (mk_kopt K_int kid), Generated tq_l)) nexp_map in
-          let new_constraints = List.map (fun (kid,nexp) -> QI_aux (QI_const (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in
+          let new_constraints = List.map (fun (kid,nexp) -> QI_aux (QI_constraint (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in
           let tqs = TypQ_aux (TypQ_tq (qs @ new_vars @ new_constraints),tq_l) in
           let vs =
             VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs,typ),ts_l),id,ext_opt,is_cast),ann) in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 1a77ea12..ba2e5e69 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -153,10 +153,13 @@ and ocaml_typ_arg ctx (A_aux (typ_arg_aux, _) as typ_arg) =
   | A_typ typ -> ocaml_typ ctx typ
   | _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg)
 
-let ocaml_typquant typq =
+let ocaml_typquant (TypQ_aux (_, l) as typq) =
   let ocaml_qi = function
     | QI_aux (QI_id kopt, _) -> zencode_kid (kopt_kid kopt)
-    | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints"
+    | QI_aux (QI_constraint _, _) ->
+       raise (Reporting.err_general l "Ocaml: type quantifiers should no longer contain constraints")
+    | QI_aux (QI_constant _, _) ->
+       raise (Reporting.err_general l "Ocaml: type quantifiers should no longer contain constrant constraints")
   in
   match quant_items typq with
   | [] -> empty
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 91fb0610..5c3a5382 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -172,8 +172,7 @@ and atyp =
 
 and 
 kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
+   KOpt_kind of string option * kid list * kind option (* kind-annotated variable *)
 
 and
 kinded_id = 
@@ -182,7 +181,7 @@ kinded_id =
 type
 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of atyp (* A constraint for this type *)
+ | QI_constraint of atyp (* A constraint for this type *)
 
 
 type 
diff --git a/src/parser.mly b/src/parser.mly
index f764995a..4bc2e5c5 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -181,7 +181,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield Constant
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure
 %token InternalPLet InternalReturn
@@ -549,7 +549,8 @@ 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 ([mk_kopt (KOpt_none v) $startpos $endpos], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+      let kopt = mk_kopt (KOpt_kind (None, [v], None)) $startpos $endpos in
+      mk_typ (ATyp_exist ([kopt], 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 kopt_list Comma typ Dot typ Rcurly
@@ -573,11 +574,19 @@ kind:
   | Bool
     { K_aux (K_bool, loc $startpos $endpos) }
 
+kid_list:
+  | kid
+    { [$1] }
+  | kid kid_list
+    { $1 :: $2 }
+
 kopt:
-  | Lparen kid Colon kind Rparen
-    { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) }
+  | Lparen Constant kid_list Colon kind Rparen
+    { KOpt_aux (KOpt_kind (Some "constant", $3, Some $5), loc $startpos $endpos) }
+  | Lparen kid_list Colon kind Rparen
+    { KOpt_aux (KOpt_kind (None, $2, Some $4), loc $startpos $endpos) }
   | kid
-    { KOpt_aux (KOpt_none $1, loc $startpos $endpos) }
+    { KOpt_aux (KOpt_kind (None, [$1], None), loc $startpos $endpos) }
 
 kopt_list:
   | kopt
@@ -587,7 +596,7 @@ kopt_list:
 
 typquant:
   | kopt_list Comma typ
-    { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in
+    { let qi_nc = QI_aux (QI_constraint $3, loc $startpos($3) $endpos($3)) in
       TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) }
   | kopt_list
     { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) }
@@ -1159,9 +1168,9 @@ r_def_body:
 
 param_kopt:
   | kid Colon kind
-    { KOpt_aux (KOpt_kind ($3, $1), loc $startpos $endpos) }
+    { KOpt_aux (KOpt_kind (None, [$1], Some $3), loc $startpos $endpos) }
   | kid
-    { KOpt_aux (KOpt_none $1, loc $startpos $endpos) }
+    { KOpt_aux (KOpt_kind (None, [$1], None), loc $startpos $endpos) }
 
 param_kopt_list:
   | param_kopt
@@ -1171,7 +1180,7 @@ param_kopt_list:
 
 typaram:
   | Lparen param_kopt_list Rparen Comma typ
-    { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in
+    { let qi_nc = QI_aux (QI_constraint $5, loc $startpos($5) $endpos($5)) in
       mk_typq $2 [qi_nc] $startpos $endpos }
   | Lparen param_kopt_list Rparen
     { mk_typq $2 [] $startpos $endpos }
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f26c74d7..55928e06 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -935,7 +935,8 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) =
     | K_order -> None
     | K_bool -> Some (delimit (separate space [doc_var ctx kid; colon; string "bool"]))
   end
-  | QI_const nc -> None
+  | QI_constraint nc -> None
+  | QI_constant _ -> None
 
 let quant_item_id_name ctx (QI_aux (qi,_)) =
   match qi with
@@ -947,19 +948,22 @@ let quant_item_id_name ctx (QI_aux (qi,_)) =
     | K_order -> None
     | K_bool -> Some (doc_var ctx kid)
   end
-  | QI_const nc -> None
+  | QI_constraint nc -> None
+  | QI_constant _ -> None
 
 let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) =
   match qi with
   | QI_id  _ -> None
-  | QI_const nc -> Some (bquote ^^ braces (doc_arithfact ctx Env.empty nc))
+  | QI_constant _ -> None
+  | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ctx Env.empty nc))
 
 (* At the moment these are all anonymous - when used we rely on Coq to fill
    them in. *)
 let quant_item_constr_name ctx (QI_aux (qi,_)) =
   match qi with
   | QI_id  _ -> None
-  | QI_const nc -> Some underscore
+  | QI_constant _ -> None
+  | QI_constraint nc -> Some underscore
 
 let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) =
   match tq with
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f13b8e1b..ae86a0fd 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1041,7 +1041,8 @@ let doc_typquant_sorts idpp (TypQ_aux (typq,_)) =
        | QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),kid),_)) -> Some (string "`len`")
        | QI_id (KOpt_aux (KOpt_kind (K_aux (K_type,_),kid),_)) -> Some underscore
        | QI_id (KOpt_aux (KOpt_kind (K_aux ((K_order|K_bool),_),kid),_)) -> None
-       | QI_const _ -> None
+       | QI_constraint _ -> None
+       | QI_constant _ -> None
      in
      if List.exists (function (QI_aux (QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),_),_)),_)) -> true | _ -> false) qs then
        let qs_pp = Util.map_filter q qs in
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index ad44f5b8..da44645c 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -210,21 +210,48 @@ and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
+let doc_kind (K_aux (k, _)) =
+  string (match k with
+          | K_int -> "Int"
+          | K_type -> "Type"
+          | K_bool -> "Bool"
+          | K_order -> "Order")
+
+let rec doc_kopts constants =
+  let is_in_group is_constant kind kopt =
+    Kind.compare kind (kopt_kind kopt) = 0 && KOptSet.mem kopt constants = is_constant
+  in
+  function
+  | kopt :: kopts ->
+     let is_constant = KOptSet.mem kopt constants in
+     let group, kopts = Util.take_drop (is_in_group is_constant (kopt_kind kopt)) kopts in
+     let attr = if is_constant then string "constant" ^^ space else empty in
+     parens (attr ^^ separate space (List.map (fun kopt -> doc_kid (kopt_kid kopt)) (kopt :: group))
+             ^^ space ^^ colon
+             ^^ space ^^ doc_kind (kopt_kind kopt))
+     ^^ begin match kopts with
+        | [] -> empty
+        | _ -> doc_kopts constants kopts
+        end
+  | [] -> empty
+
 let doc_quants quants =
-  let doc_qi_kopt (QI_aux (qi_aux, _)) =
-    match qi_aux with
-    | QI_id kopt when is_int_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 -> []
+  let rec get_constants = function
+    | QI_aux (QI_constant kopts, _) :: qis -> KOptSet.union (KOptSet.of_list kopts) (get_constants qis)
+    | _ :: qis -> get_constants qis
+    | [] -> KOptSet.empty
+  in
+  let rec get_kopts = function
+    | QI_aux (QI_id kopt, _) :: qis -> kopt :: get_kopts qis
+    | _ :: qis -> get_kopts qis
+    | [] -> []
   in
   let qi_nc (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_const nc -> [nc]
+    | QI_constraint nc -> [nc]
     | _ -> []
   in
-  let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in
+  let kdoc = doc_kopts (get_constants quants) (get_kopts quants) in
   let ncs = List.concat (List.map qi_nc quants) in
   match ncs with
   | [] -> kdoc
@@ -238,11 +265,12 @@ let doc_param_quants quants =
     | 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 -> []
+    | QI_constraint _ -> []
+    | QI_constant _ -> []
   in
   let qi_nc (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_const nc -> [nc]
+    | QI_constraint nc -> [nc]
     | _ -> []
   in
   let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in
diff --git a/src/slice.ml b/src/slice.ml
index fa574b7f..78009059 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -217,7 +217,7 @@ let add_def_to_graph graph def =
   let scan_quant_item self (QI_aux (aux, _)) =
     match aux with
     | QI_id _ -> ()
-    | QI_const nc ->
+    | QI_constraint nc ->
        IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc)
   in
 
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
index 6b8fede4..fad45412 100644
--- a/src/toFromInterp_backend.ml
+++ b/src/toFromInterp_backend.ml
@@ -129,7 +129,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
   in
   let fromValueTypq (QI_aux (qi_aux, _)) = match qi_aux with
     | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> fromValueKid kid
-    | QI_const _ -> empty
+    | QI_constant _ -> empty
+    | QI_constraint _ -> empty
   in
   let fromValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with
     | TypQ_no_forall -> [empty]
@@ -283,7 +284,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
   in
   let toValueTypq (QI_aux (qi_aux, _)) = match qi_aux with
     | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> toValueKid kid
-    | QI_const _ -> empty
+    | QI_constant _ -> empty
+    | QI_constraint _ -> empty
   in
   let toValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with
     | TypQ_no_forall -> [empty]
diff --git a/src/type_check.ml b/src/type_check.ml
index 0365e2e5..2ce6ea94 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -246,7 +246,8 @@ and strip_quant_item = function
   | QI_aux (qi_aux, _) -> QI_aux (strip_qi_aux qi_aux, Parse_ast.Unknown)
 and strip_qi_aux = function
   | QI_id kinded_id -> QI_id (strip_kinded_id kinded_id)
-  | QI_const constr -> QI_const (strip_n_constraint constr)
+  | QI_constant kopts -> QI_constant (List.map strip_kinded_id kopts)
+  | QI_constraint constr -> QI_constraint (strip_n_constraint constr)
 and strip_kinded_id = function
   | KOpt_aux (kinded_id_aux, _) -> KOpt_aux (strip_kinded_id_aux kinded_id_aux, Parse_ast.Unknown)
 and strip_kinded_id_aux = function
@@ -1312,7 +1313,8 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
   let rec add_quant_item env = function
     | QI_aux (qi, _) -> add_quant_item_aux env qi
   and add_quant_item_aux env = function
-    | QI_const constr -> Env.add_constraint constr env
+    | QI_constraint constr -> Env.add_constraint constr env
+    | QI_constant _ -> env
     | QI_id kopt -> Env.add_typ_var l kopt env
   in
   match quant with
@@ -1811,16 +1813,32 @@ let subst_unifiers unifiers typ =
 let subst_unifiers_typ_arg unifiers typ_arg =
   List.fold_left (fun typ_arg (v, arg) -> typ_arg_subst v arg typ_arg) typ_arg (KBindings.bindings unifiers)
 
-let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
+let instantiate_quant env (v, arg) (QI_aux (aux, l) as qi) =
   match aux with
   | QI_id kopt when Kid.compare (kopt_kid kopt) v = 0 ->
      typ_debug (lazy ("Instantiated " ^ string_of_quant_item qi));
      None
   | QI_id _ -> Some qi
-  | QI_const nc -> Some (QI_aux (QI_const (constraint_subst v arg nc), l))
+  | QI_constant kopts ->
+     let kopts =
+       Util.map_filter (fun kopt ->
+           if Kid.compare (kopt_kid kopt) v = 0 then
+             begin match arg with
+             | A_aux (A_nexp nexp, _) ->
+                if is_nexp_constant (Env.expand_nexp_synonyms env nexp) then None else Some kopt
+             | _ -> Some kopt
+             end
+           else
+             Some kopt
+         ) kopts in
+     begin match kopts with
+     | [] -> None
+     | _ -> Some (QI_aux (QI_constant kopts, l))
+     end
+  | QI_constraint nc -> Some (QI_aux (QI_constraint (constraint_subst v arg nc), l))
 
-let instantiate_quants quants unifier =
-  List.map (instantiate_quant unifier) quants |> Util.option_these
+let instantiate_quants env quants unifier =
+  List.map (instantiate_quant env unifier) quants |> Util.option_these
 
 (* During typechecking, we can run into the following issue, where we
    have a function like
@@ -2374,8 +2392,8 @@ let instantiate_simple_equations =
   in
   let rec find_eqs_quant kid (QI_aux (qi,_)) =
     match qi with
-    | QI_id _ -> []
-    | QI_const nc -> find_eqs kid nc
+    | QI_id _ | QI_constant _ -> []
+    | QI_constraint nc -> find_eqs kid nc
   in
   let rec inst_from_eq = function
     | [] -> KBindings.empty
@@ -2561,7 +2579,8 @@ let rec add_constraints constrs env =
 
 let solve_quant env = function
   | QI_aux (QI_id _, _) -> false
-  | QI_aux (QI_const nc, _) -> prove __POS__ env nc
+  | QI_aux (QI_constant _, _) -> false
+  | QI_aux (QI_constraint nc, _) -> prove __POS__ env nc
 
 (* When doing implicit type coercion, for performance reasons we want
    to filter out the possible casts to only those that could
@@ -3163,7 +3182,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
             typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ));
             let unifiers = unify l env goals ret_typ typ in
             let arg_typ' = subst_unifiers unifiers arg_typ in
-            let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+            let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
             if not (List.for_all (solve_quant env) quants') then
               typ_raise env l (Err_unresolved_quants (f, quants', Env.get_locals env, Env.get_constraints env))
             else ();
@@ -3176,7 +3195,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
         end
      | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
      end
-     
+
   | P_app (f, pats) when Env.is_union_constructor f env ->
      (* Treat Ctor(x, y) as Ctor((x, y)) *)
      bind_pat env (P_aux (P_app (f, [mk_pat (P_tup pats)]),(l,()))) typ
@@ -3198,7 +3217,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
               (* FIXME: There's no obvious goals here *)
               let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in
               let arg_typ' = subst_unifiers unifiers typ1 in
-              let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+              let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
               if (match quants' with [] -> false | _ -> true)
               then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
               else ();
@@ -3216,7 +3235,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
                  typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ));
                  let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in
                  let arg_typ' = subst_unifiers unifiers typ2 in
-                 let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+                 let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
                  if (match quants' with [] -> false | _ -> true)
                  then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
                  else ();
@@ -3875,7 +3894,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
   typ_debug (lazy (string_of_list ", " (fun (kid, arg) -> string_of_kid kid ^ " => " ^ string_of_typ_arg arg) (KBindings.bindings unifiers)));
   all_unifiers := unifiers;
   let typ_args = List.map (subst_unifiers unifiers) typ_args in
-  List.iter (fun unifier -> quants := instantiate_quants !quants unifier) (KBindings.bindings unifiers);
+  List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) (KBindings.bindings unifiers);
   List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) (KBindings.bindings unifiers);
 
   typ_debug (lazy ("Quantifiers " ^ Util.string_of_list ", " string_of_quant_item !quants));
@@ -3897,13 +3916,6 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
          [], List.map implicit_to_int typ_args, xs
   in
 
-  let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
-    match aux with
-    | QI_id kopt when Kid.compare (kopt_kid kopt) v = 0 -> None
-    | QI_id _ -> Some qi
-    | QI_const nc -> Some (QI_aux (QI_const (constraint_subst v arg nc), l))
-  in
-
   let typ_args = match expected_ret_typ with
     | None -> typ_args
     | Some expect when is_exist (Env.expand_synonyms env expect) || is_exist !typ_ret -> typ_args
@@ -3915,7 +3927,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
          let unifiers = KBindings.bindings unifiers in
          typ_debug (lazy (Util.("Unifiers " |> magenta |> clear)
                           ^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers));
-         List.iter (fun unifier -> quants := instantiate_quants !quants unifier) unifiers;
+         List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) unifiers;
          List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) unifiers;
          List.map (fun typ -> List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ unifiers) typ_args
        with Unification_error _ -> typ_args
@@ -3938,7 +3950,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
       let unifiers = KBindings.bindings unifiers in
       typ_debug (lazy (Util.("Unifiers " |> magenta |> clear)
                        ^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers));
-      List.iter (fun unifier -> quants := instantiate_quants !quants unifier) unifiers;
+      List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) unifiers;
       List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) unifiers;
       let remaining_typs =
         List.map (fun typ -> List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ unifiers) remaining_typs
@@ -4084,7 +4096,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
               let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in
               let arg_typ' = subst_unifiers unifiers arg_typ in
-              let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+              let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
               if (match quants' with [] -> false | _ -> true)
               then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
               else ();
@@ -4114,7 +4126,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
               let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in
               let arg_typ' = subst_unifiers unifiers typ1 in
-              let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+              let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
               if (match quants' with [] -> false | _ -> true)
               then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
               else ();
@@ -4131,7 +4143,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
                  typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
                  let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in
                  let arg_typ' = subst_unifiers unifiers typ2 in
-                 let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
+                 let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in
                  if (match quants' with [] -> false | _ -> true)
                  then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
                  else ();
diff --git a/src/type_error.ml b/src/type_error.ml
index e75d2cd4..eed1379a 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -58,7 +58,7 @@ type suggestion =
   | Suggest_none
 
 let rec analyze_unresolved_quant locals ncs = function
-  | QI_aux (QI_const nc, _) ->
+  | QI_aux (QI_constraint nc, _) ->
      let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in
      if gen_kids = [] then
        Suggest_add_constraint nc
@@ -99,7 +99,7 @@ let rec analyze_unresolved_quant locals ncs = function
          else
            Suggest_none
 
-  | QI_aux (QI_id kopt, _) ->
+  | QI_aux (QI_id _, _) | QI_aux (QI_constant _, _) ->
      Suggest_none
 
 let message_of_type_error =