21 files changed, 377 insertions, 130 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 0b83ece2..c7ba2e9a 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -12,6 +12,7 @@ metavar num,numZero,numOne ::=
   {{ ocaml big_int }}
   {{ hol num }}
   {{ lem integer }}
+  {{ isa int }}
   {{ com Numeric literals }}
 
 metavar nat ::=
@@ -19,12 +20,14 @@ metavar nat ::=
   {{ ocaml int }}
   {{ lex numeric }}
   {{ lem nat }}
-
+  {{ isa nat }}
+  
 metavar hex ::=
   {{ phantom }}
   {{ lex numeric }}
   {{ ocaml string }}
   {{ lem string }}
+  {{ isa string }}
   {{ com Bit vector literal, specified by C-style hex number }}
 
 metavar bin ::=
@@ -32,6 +35,7 @@ metavar bin ::=
   {{ lex numeric }}
   {{ ocaml string }}
   {{ lem string }}
+  {{ isa string }}
   {{ com Bit vector literal, specified by C-style binary number }}
 
 metavar string ::=
@@ -39,6 +43,7 @@ metavar string ::=
   {{ ocaml string }}
   {{ lem string }}
   {{ hol string }}
+  {{ isa string }}
   {{ com String literals }}
 
 metavar regexp ::=
@@ -46,6 +51,7 @@ metavar regexp ::=
   {{ ocaml string }}
   {{ lem string }}
   {{ hol string }}
+  {{ isa string }}
   {{ com Regular expresions, as a string literal }}
 
 metavar real ::=
@@ -53,12 +59,14 @@ metavar real ::=
   {{ ocaml string }}
   {{ lem string }}
   {{ hol string }}
+  {{ isa string }}
   {{ com Real number literal }}
 
 metavar value ::=
   {{ phantom }}
   {{ ocaml value }}
   {{ lem value }}
+  {{ isa value }}
 
 embed
 {{ ocaml
@@ -89,23 +97,40 @@ type annot 'a = l * 'a
 
 }}
 
+embed
+{{ isa
+
+datatype "l" = Unknown 
+
+datatype "value" = Val
+
+datatype "loop" = While | Until
+
+type_synonym "annot" = l
+
+}}
+
 metavar x , y , z ::=
   {{ ocaml text }}
   {{ lem string }}
   {{ hol string }}
+  {{ isa string }}
   {{ com identifier }}
   {{ ocamlvar "[[x]]" }}
   {{ lemvar "[[x]]" }}
 
+
 metavar ix ::=
   {{ lex alphanum }}
   {{ ocaml text }}
   {{ lem string }}
   {{ hol string }}
+  {{ isa string }}
   {{ com infix identifier }}
   {{ ocamlvar "[[ix]]" }}
   {{ lemvar "[[ix]]" }}
 
+
 grammar
 
 l :: '' ::=                                     {{ phantom }}
@@ -195,7 +220,7 @@ effect :: 'Effect_' ::=
   {{ aux _ l }}
   | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }}
   | pure                                 :: M :: pure {{ com sugar for empty effect set }}
-    {{ lem (Effect_set []) }}
+    {{ ichlo (Effect_set []) }} 
 
 typ :: 'Typ_' ::=
   {{ com type expressions, of kind Type }}
@@ -238,7 +263,7 @@ kinded_id :: 'KOpt_' ::=
   {{ com optionally kind-annotated identifier }}
   {{ aux _ l }}
   | kind kid       :: :: kind {{ com kind-annotated variable }}
-  | kid            :: S :: none {{ ichlo [[kinded_id]] }}
+  | kid            :: S :: none {{ ichlo [[kid]] }}
 
 quant_item :: 'QI_' ::=
   {{ com kinded identifier or Int constraint }}
@@ -315,15 +340,18 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
                                                         {{ ocaml bool }}
                                                         {{ lem bool }}
                                                         {{ hol bool }}
+							{{ isa bool }}
   {{ com optional semi-colon }}
   |                                                     :: :: no
     {{ hol F }}
     {{ ocaml false }}
     {{ lem false }}
+    {{ isa False }}
   | ';'                                                 :: :: yes
     {{ hol T }}
     {{ ocaml true }}
     {{ lem true }}
+    {{ isa True }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Patterns                                                     %
@@ -602,7 +630,7 @@ exp :: 'E_' ::=
 
 %  and maybe with nice syntax
 
-  | switch exp { case pexp1  ... case pexpn } :: :: case
+  | match exp { pexp1 '|'  ... '|' pexpn } :: :: case
     {{ com pattern matching }}
 %  | ( typ ) exp                                      :: :: Typed
 %    {{ com Type-annotated expressions }}
@@ -758,7 +786,8 @@ effect_opt :: 'Effect_opt_' ::=
 % Generate a pexp, but from slightly different syntax (= rather than ->)
 pexp_funcl :: 'Pat_funcl_' ::=
   {{ auxparam 'a }}
-  {{ icho ('a pexp) }}
+  {{ ocaml ('a pexp) }}
+  {{ isa pexp }}
   {{ lem (pexp 'a) }}
   | pat = exp                       :: :: exp {{ ichlo (Pat_aux (Pat_exp [[pat]] [[exp]],Unknown)) }}
   | ( pat when exp1 ) = exp         :: :: when {{ ichlo (Pat_aux (Pat_when [[pat]] [[exp1]] [[exp]],Unknown)) }}
@@ -831,17 +860,18 @@ val_spec_aux :: 'VS_' ::=
   {{ com value type specification }}
   {{ ocaml  VS_val_spec of typschm * id * (string * string) list * bool }}
   {{ lem VS_val_spec of typschm * id * list (string * string) * bool }}
+  {{ isa  typschm * id  * (string => string option) * bool }}
   | val typschm id                                  :: S :: val_spec
     {{ com specify the type of an upcoming definition }}
-    {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }}
+    {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} {{ isa }}
   | val cast typschm id                             :: S :: cast
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }}
+    {{ ocaml  (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }} {{ isa }}
   | val extern typschm id                           :: S :: extern_no_rename
     {{ com specify the type of an external function }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] ([[Some id]]) false) }} {{ lem }}
+    {{ ocaml  (VS_val_spec [[typschm]] [[id]] (Some [[id]]) false) }} {{ lem }} {{ isa }}
   | val extern typschm id = string                  :: S :: extern_spec
     {{ com specify the type of a function from Lem }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] ([[Some string]]) false) }} {{ lem }}
+    {{ ocaml  (VS_val_spec [[typschm]] [[id]] (Some [[string]]) false) }} {{ lem }} {{ isa }}
 %where the string must provide an explicit path to the required function but will not be checked
 
 default_spec :: 'DT_' ::=
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index e8148597..8be5cc6b 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -91,7 +91,7 @@ lemma liftState_read_memt[liftState_simp]:
            split: option.splits intro: bindS_cong)
 
 lemma liftState_read_mem[liftState_simp]:
-  shows "liftState r (read_mem BCa BCb rk asz a sz) = read_memS BCa BCb rk a sz"
+  shows "liftState r (read_mem BCa BCb rk asz a sz) = read_memS BCa BCb rk asz a sz"
   by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
                  read_memtS_def
                  prod.case_distrib option.case_distrib[where h = "liftState r"]
@@ -118,7 +118,7 @@ lemma liftState_write_memt[liftState_simp]:
   by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits)
 
 lemma liftState_write_mem[liftState_simp]:
-  "liftState r (write_mem BCa BCv wk addrsize addr sz v) = write_memS BCa BCv wk addr sz v"
+  "liftState r (write_mem BCa BCv wk addrsize addr sz v) = write_memS BCa BCv wk addrsize addr sz v"
   by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp
            split: option.splits)
 
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 1e9f50cc..2fbd7a56 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -214,11 +214,11 @@ lemma no_throw_mem_builtins:
   "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
   "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
-  "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
+  "\<And>BCa BCv rk asz a sz s. ignore_throw (read_memS BCa BCv rk asz a sz) s = read_memS BCa BCv rk asz a sz s"
   "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s"
   "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s"
   "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s"
-  "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s"
+  "\<And>BCa BCv wk asz addr sz v s. ignore_throw (write_memS BCa BCv wk asz addr sz v) s = write_memS BCa BCv wk asz addr sz v s"
   "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index f2e0add5..4c26b641 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -189,10 +189,7 @@ let rec run frame =
  *)
 
 let initial_state ast env =
-  let lstate, gstate =
-    Interpreter.initial_state ast env safe_primops
-  in
-  (lstate, { gstate with Interpreter.allow_registers = false })
+  Interpreter.initial_state ~registers:false ast env safe_primops
 
 let rw_exp ok not_ok istate =
   let evaluate e_aux annot =
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 608d25e1..89a4ba82 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -321,6 +321,25 @@ let const_props defs ref_vars =
     with
     | _ -> exp
   in
+  let constants =
+    let add m = function
+      | DEF_val (LB_aux (LB_val (P_aux ((P_id id | P_typ (_,P_aux (P_id id,_))),_), exp),_))
+           when Constant_fold.is_constant exp ->
+         Bindings.add id exp m
+      | _ -> m
+    in
+    match defs with
+    | Defs defs ->
+       List.fold_left add Bindings.empty defs
+  in
+  let replace_constant (E_aux (e,annot) as exp) =
+    match e with
+    | E_id id ->
+       (match Bindings.find_opt id constants with
+        | Some e -> e
+        | None -> exp)
+    | _ -> exp
+  in
   let rec const_prop_exp substs assigns ((E_aux (e,(l,annot))) as exp) =
     (* Functions to treat lists and tuples of subexpressions as possibly
        non-deterministic: that is, we stop making any assumptions about
@@ -633,6 +652,8 @@ let const_props defs ref_vars =
      e.g., (length(op : bits(32)) : int(32)) becomes 32 even if op is not constant.
   *)
   and const_prop_try_fn env (id, args) (l, annot) =
+    let exp_orig = E_aux (E_app (id, args), (l, annot)) in
+    let args = List.map replace_constant args in
     let exp = E_aux (E_app (id, args), (l, annot)) in
     let rec is_overload_of f =
       Env.get_overloads f env
@@ -651,15 +672,27 @@ let const_props defs ref_vars =
        (match destruct_atom_nexp env (typ_of exp) with
         | Some (Nexp_aux (Nexp_constant i, _)) ->
            E_aux (E_lit (mk_lit (L_num i)), (l, annot))
-        | _ -> exp)
-    | _ -> exp
+        | _ -> exp_orig)
+    | _ -> exp_orig
 
   and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
     let rec check_exp_pat (E_aux (e,(l,annot)) as exp) (P_aux (p,(l',_)) as pat) =
       match e, p with
       | _, P_wild -> DoesMatch ([],[])
       | _, P_typ (_,p') -> check_exp_pat exp p'
-      | _, P_id id' when pat_id_is_variable env id' -> DoesMatch ([id',exp],[])
+      | _, P_id id' when pat_id_is_variable env id' ->
+         let exp_typ = typ_of exp in
+         let pat_typ = typ_of_pat pat in
+         let goals = KidSet.diff (tyvars_of_typ pat_typ) (tyvars_of_typ exp_typ) in
+         let unifiers =
+           try Type_check.unify l env goals pat_typ exp_typ
+           with _ -> KBindings.empty in
+         let is_nexp (k,a) = match a with
+           | A_aux (A_nexp n,_) -> Some (k,n)
+           | _ -> None
+         in
+         let kbindings = Util.map_filter is_nexp (KBindings.bindings unifiers) in
+         DoesMatch ([id',exp],kbindings)
       | E_tuple es, P_tup ps ->
          let rec check = function
            | DoesNotMatch -> fun _ -> DoesNotMatch
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 572c0a18..9acfeb26 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -949,9 +949,9 @@ let initial_gstate primops ast env =
     typecheck_env = env;
   }
 
-let rec initialize_registers gstate =
+let rec initialize_registers allow_registers gstate =
   let process_def = function
-    | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), annot)) ->
+    | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), annot)) when allow_registers ->
        begin
          let env = Type_check.env_of_annot annot in
          let typ = Type_check.Env.expand_synonyms env typ in
@@ -959,7 +959,7 @@ let rec initialize_registers gstate =
          let exp = Type_check.check_exp env exp typ in
          { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers }
        end
-    | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
+    | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) when allow_registers ->
        { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers }
     | DEF_fundef fdef ->
        { gstate with fundefs = Bindings.add (id_of_fundef fdef) fdef gstate.fundefs }
@@ -967,10 +967,16 @@ let rec initialize_registers gstate =
   in
   function
   | Defs (def :: defs) ->
-     initialize_registers (process_def def) (Defs defs)
+     initialize_registers allow_registers (process_def def) (Defs defs)
   | Defs [] -> gstate
 
-let initial_state ast env primops = initial_lstate, initialize_registers (initial_gstate primops ast env) ast
+let initial_state ?(registers=true) ast env primops =
+  let gstate = initial_gstate primops ast env in
+  let gstate =
+    { (initialize_registers registers gstate ast)
+      with allow_registers = registers }
+  in
+  initial_lstate, gstate
 
 type value_result =
   | Value_success of value
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 0c63e020..c011f4d0 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -120,7 +120,7 @@ let kidset_bigunion = function
   | h::t -> List.fold_left KidSet.union h t
 
 (* TODO: deal with non-set constraints, intersections, etc somehow *)
-let extract_set_nc l var nc =
+let extract_set_nc env l var nc =
   let vars = Spec_analysis.equal_kids_ncs var [nc] in
   let rec aux_or (NC_aux (nc,l)) =
     match nc with
@@ -133,12 +133,13 @@ let extract_set_nc l var nc =
        | _, _ -> None)
     | _ -> None
   in
-  let rec aux (NC_aux (nc,l) as nc_full) =
+  (* Lazily expand constraints to keep close to the original form *)
+  let rec aux expanded (NC_aux (nc,l) as nc_full) =
     let re nc = NC_aux (nc,l) in
     match nc with
     | NC_set (id,is) when KidSet.mem id vars -> Some (is,re NC_true)
     | NC_and (nc1,nc2) ->
-       (match aux nc1, aux nc2 with
+       (match aux expanded nc1, aux expanded nc2 with
        | None, None -> None
        | None, Some (is,nc2') -> Some (is, re (NC_and (nc1,nc2')))
        | Some (is,nc1'), None -> Some (is, re (NC_and (nc1',nc2)))
@@ -148,8 +149,8 @@ let extract_set_nc l var nc =
        (match aux_or nc_full with
        | Some is -> Some (is, re NC_true)
        | None -> None)
-    | _ -> None
-  in match aux nc with
+    | _ -> if expanded then None else aux true (Env.expand_constraint_synonyms env nc_full)
+  in match aux false nc with
   | Some is -> is
   | None ->
      raise (Reporting.err_general l ("No set constraint for " ^ string_of_kid var ^
@@ -290,7 +291,7 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
        let find_insts k (insts,nc) =
          let inst,nc' =
            if KidSet.mem (kopt_kid k) vars then
-             let is,nc' = extract_set_nc l (kopt_kid k) nc in
+             let is,nc' = extract_set_nc env l (kopt_kid k) nc in
              Some is,nc'
            else None,nc
          in (k,inst)::insts,nc'
@@ -329,6 +330,7 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
   let variants = size_nvars_ty ty in
   match variants with
   | [] -> None
+  | [l,_] when List.for_all (function (_,None) -> true | _ -> false) l -> None
   | sample::_ ->
      if List.length variants > size_set_limit then
        cannot ql
@@ -341,9 +343,9 @@ let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
      in
      let name_seg = function
        | (_,None) -> ""
-       | (k,Some i) -> string_of_kid (kopt_kid k) ^ Big_int.to_string i
+       | (k,Some i) -> "#" ^ string_of_kid (kopt_kid k) ^ Big_int.to_string i
      in
-     let name l i = String.concat "_" (i::(List.map name_seg l)) in
+     let name l i = String.concat "" (i::(List.map name_seg l)) in
      Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants)
 
 let reduce_nexp subst ne =
@@ -391,7 +393,16 @@ let refine_constructor refinements l env id args =
        match Type_check.destruct_exist (Type_check.Env.expand_synonyms env constr_ty) with
        | None -> None
        | Some (kopts,nc,constr_ty) ->
-          let bindings = Type_check.unify l env (tyvars_of_typ constr_ty) constr_ty arg_ty  in
+          (* Remove existentials in argument types to prevent unification failures *)
+          let unwrap (Typ_aux (t,_) as typ) = match t with
+            | Typ_exist (_,_,typ) -> typ
+            | _ -> typ
+          in
+          let arg_ty = match arg_ty with
+            | Typ_aux (Typ_tup ts,annot) -> Typ_aux (Typ_tup (List.map unwrap ts),annot)
+            | _ -> arg_ty
+          in
+          let bindings = Type_check.unify l env (tyvars_of_typ constr_ty) constr_ty arg_ty in
           let find_kopt kopt = try Some (KBindings.find (kopt_kid kopt) bindings) with Not_found -> None in
           let bindings = List.map find_kopt kopts in
           let matches_refinement (mapping,_,_) =
@@ -405,8 +416,12 @@ let refine_constructor refinements l env id args =
           match List.find matches_refinement irefinements with
           | (_,new_id,_) -> Some (E_app (new_id,args))
           | exception Not_found ->
+             let print_map kopt = function
+               | None -> string_of_kid (kopt_kid kopt) ^ " -> _"
+               | Some ta -> string_of_kid (kopt_kid kopt) ^ " -> " ^ string_of_typ_arg ta
+             in
              (Reporting.print_err l "Monomorphisation"
-                ("Unable to refine constructor " ^ string_of_id id);
+                ("Unable to refine constructor " ^ string_of_id id ^ " using mapping " ^ String.concat "," (List.map2 print_map kopts bindings));
               None)
     end
     | _ -> None
@@ -715,7 +730,7 @@ let split_defs all_errors splits env defs =
          | Nexp_var kvar ->
            let ncs = Env.get_constraints env in
            let nc = List.fold_left nc_and nc_true ncs in
-           (match extract_set_nc l kvar nc with
+           (match extract_set_nc env l kvar nc with
            | (is,_) -> List.map (mk_lit (Some kvar)) is
            | exception Reporting.Fatal_error (Reporting.Err_general (_,msg)) -> cannot msg)
          | _ -> cannot ("unsupport atom nexp " ^ string_of_nexp nexp)
@@ -886,48 +901,50 @@ let split_defs all_errors splits env defs =
       | vars -> split_pat vars pat
     in
     let map_pat (P_aux (p,(l,tannot)) as pat) =
-      match map_pat_by_loc pat with
-      | Some l -> VarSplit l
-      | None ->
-         match p with
-         | P_app (id,args) ->
-            begin
-              match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with
-              | (_,variants) ->
-(* TODO: what changes to the pattern and what substitutions do we need in general?
-                 let kid,kid_annot =
-                   match args with
-                   | [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann
-                   | _ -> 
-                      raise (Reporting.err_general l
-                               ("Pattern match not currently supported by monomorphisation: "
-                               ^ string_of_pat pat))
+      let try_by_location () =
+        match map_pat_by_loc pat with
+        | Some l -> VarSplit l
+        | None -> NoSplit
+      in
+      match p with
+      | P_app (id,args) ->
+         begin
+            match List.find (fun (id',_) -> Id.compare id id' = 0) refinements with
+            | (_,variants) ->
+(* TODO: at changes to the pattern and what substitutions do we need in general?
+               let kid,kid_annot =
+                 match args with
+                 | [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann
+                 | _ -> 
+                    raise (Reporting.err_general l
+                             ("Pattern match not currently supported by monomorphisation: "
+                             ^ string_of_pat pat))
+               in
+               let map_inst (insts,id',_) =
+                 let insts =
+                   match insts with [(v,Some i)] -> [(kid,Nexp_aux (Nexp_constant i, Generated l))]
+                   | _ -> assert false
                  in
-                 let map_inst (insts,id',_) =
-                   let insts =
-                     match insts with [(v,Some i)] -> [(kid,Nexp_aux (Nexp_constant i, Generated l))]
-                     | _ -> assert false
-                   in
 (*
-                   let insts,_ = split_insts insts in
-                   let insts = List.map (fun (v,i) ->
-                     (??,
-                      Nexp_aux (Nexp_constant i,Generated l)))
-                     insts in
-  P_aux (P_app (id',args),(Generated l,tannot)),
+                 let insts,_ = split_insts insts in
+                 let insts = List.map (fun (v,i) ->
+                   (??,
+                    Nexp_aux (Nexp_constant i,Generated l)))
+                   insts in
+  P_aux (app (id',args),(Generated l,tannot)),
 *)
-                   P_aux (P_app (id',[P_aux (P_id (id_of_kid kid),kid_annot)]),(Generated l,tannot)),
-                   kbindings_from_list insts
-                 in
+                 P_aux (P_app (id',[P_aux (P_id (id_of_kid kid),kid_annot)]),(Generated l,tannot)),
+                 kbindings_from_list insts
+               in
 *)
-                 let map_inst (insts,id',_) =
-                   P_aux (P_app (id',args),(Generated l,tannot)),
-                   KBindings.empty
-                 in
-                 ConstrSplit (List.map map_inst variants)
-              | exception Not_found -> NoSplit
-            end
-         | _ -> NoSplit
+               let map_inst (insts,id',_) =
+                 P_aux (P_app (id',args),(Generated l,tannot)),
+                 KBindings.empty
+               in
+               ConstrSplit (List.map map_inst variants)
+            | exception Not_found -> try_by_location ()
+          end
+       | _ -> try_by_location ()
     in
 
     let check_single_pat (P_aux (_,(l,annot)) as p) =
@@ -1741,7 +1758,8 @@ type env = {
   top_kids : kid list; (* Int kids bound by the function type *)
   var_deps : dependencies Bindings.t;
   kid_deps : dependencies KBindings.t;
-  referenced_vars : IdSet.t
+  referenced_vars : IdSet.t;
+  globals : bool Bindings.t (* is_value or not *)
 }
 
 let rec split3 = function
@@ -1799,6 +1817,19 @@ let update_env env deps pat typ_env_pre typ_env_post =
   let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in
   update_env_new_kids { env with var_deps = var_deps } deps typ_env_pre typ_env_post
 
+(* A function argument may end up with fresh type variables due to coercing
+   unification (which will eventually be existentially bound in the type of
+   the function).  Here we record the dependencies for these variables. *)
+
+let add_arg_only_kids env typ_env typ deps =
+  let all_vars = tyvars_of_typ typ in
+  let check_kid kid kid_deps =
+    if KBindings.mem kid kid_deps then kid_deps
+    else KBindings.add kid deps kid_deps
+  in
+  let kid_deps = KidSet.fold check_kid all_vars env.kid_deps in
+  { env with kid_deps }
+
 let assigned_vars_exps es =
   List.fold_left (fun vs exp -> IdSet.union vs (Spec_analysis.assigned_vars exp))
     IdSet.empty es
@@ -1983,39 +2014,40 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
      follow the type checker in processing them in-order to detect the automatic
      unpacking of existentials.  When we spot a new type variable (using
      update_env_new_kids) we set them to depend on the previous argument. *)
-  let non_det_args es =
+  let non_det_args es typs =
     let assigns = remove_assigns es " assigned in non-deterministic expressions" in
-    let rec aux prev_typ_env prev_deps env = function
-      | [] -> [], empty
-      | h::t ->
+    let rec aux env = function
+      | [], _ -> [], empty, env
+      | (E_aux (_,ann) as h)::t, typ::typs ->
          let typ_env = env_of h in
-         let env = update_env_new_kids env prev_deps prev_typ_env typ_env in
          let new_deps, _, new_r = analyse_exp fn_id env assigns h in
-         let t_deps, t_r = aux typ_env new_deps env t in
-         new_deps::t_deps, merge new_r t_r
+         let env = add_arg_only_kids env typ_env typ new_deps in
+         let t_deps, t_r, t_env = aux env (t,typs) in
+         new_deps::t_deps, merge new_r t_r, t_env
     in
-    let deps, r = match es with
-      | [] -> [], empty
-      | h::t ->
-         let new_deps, _, new_r = analyse_exp fn_id env assigns h in
-         let t_deps, t_r = aux (env_of h) new_deps env t in
-         new_deps::t_deps, merge new_r t_r
-    in
-    (deps, assigns, r)
+    let deps, r, env = aux env (es,typs) in
+    (deps, assigns, r, env)
   in
   let merge_deps deps = List.fold_left dmerge dempty deps in
   let deps, assigns, r =
     match e with
     | E_block es ->
-       let rec aux assigns = function
+       let rec aux env assigns = function
          | [] -> (dempty, assigns, empty)
          | [e] -> analyse_exp fn_id env assigns e
+         (* There's also a lone assignment case below where no env update is needed *)
+         | E_aux (E_assign (lexp,e1),ann)::e2::es ->
+            let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in
+            let assigns,r2 = analyse_lexp fn_id env assigns d1 lexp in
+            let env = update_env_new_kids env d1 (env_of_annot ann) (env_of e2) in
+            let d3, assigns, r3 = aux env assigns (e2::es) in
+            (d3, assigns, merge (merge r1 r2) r3)
          | e::es ->
             let _, assigns, r' = analyse_exp fn_id env assigns e in
-            let d, assigns, r = aux assigns es in
+            let d, assigns, r = aux env assigns es in
             d, assigns, merge r r'
        in
-       aux assigns es
+       aux env assigns es
     | E_nondet es ->
        let _, assigns, r = non_det es in
        (dempty, assigns, r)
@@ -2033,27 +2065,35 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
                | _ ->
                   if IdSet.mem id env.referenced_vars then
                     Unknown (l, string_of_id id ^ " may be modified via a reference"),assigns,empty
-                  else
-                    Unknown (l, string_of_id id ^ " is not in the environment"),assigns,empty
+                  else match Bindings.find id env.globals with
+                       | true -> dempty,assigns,empty (* value *)
+                       | false -> Unknown (l, string_of_id id ^ " is a global but not a value"),assigns,empty
+                       | exception Not_found ->
+                          Unknown (l, string_of_id id ^ " is not in the environment"),assigns,empty
        end
     | E_lit _ -> (dempty,assigns,empty)
     | E_cast (_,e) -> analyse_exp fn_id env assigns e
     | E_app (id,args) ->
-       let deps, assigns, r = non_det_args args in
        let typ_env = env_of_annot (l,annot) in
-       let (_,fn_typ) = Env.get_val_spec id typ_env in
-       let fn_effect = match fn_typ with
-         | Typ_aux (Typ_fn (_,_,eff),_) -> eff
-         | _ -> Effect_aux (Effect_set [],Unknown)
+       let (_,fn_typ) = Env.get_val_spec_orig id typ_env in
+       let kid_inst = instantiation_of exp in
+       let kid_inst = KBindings.fold (fun kid -> KBindings.add (orig_kid kid)) kid_inst KBindings.empty in
+       let fn_typ = subst_unifiers kid_inst fn_typ in
+       let arg_typs, fn_effect = match fn_typ with
+         | Typ_aux (Typ_fn (args,_,eff),_) -> args,eff
+         | _ -> [], Effect_aux (Effect_set [],Unknown)
        in
+       (* We have to use the types from the val_spec here so that we can track
+          any type variables that are generated by the coercing unification that
+          the type checker applies after inferring the type of an argument, and
+          that only appear in the unifiers. *)
+       let deps, assigns, r, env = non_det_args args arg_typs in
        let eff_dep = match fn_effect with
          | Effect_aux (Effect_set ([] | [BE_aux (BE_undef,_)]),_) -> dempty
          | _ -> Unknown (l, "Effects from function application")
        in
-       let kid_inst = instantiation_of exp in
        let kid_inst = KBindings.map (simplify_size_typ_arg env typ_env) kid_inst in
        (* Change kids in instantiation to the canonical ones from the type signature *)
-       let kid_inst = KBindings.fold (fun kid -> KBindings.add (orig_kid kid)) kid_inst KBindings.empty in
        let kid_deps = KBindings.map (deps_of_typ_arg l fn_id env deps) kid_inst in
        let rdep,r' =
          if Id.compare fn_id id == 0 then
@@ -2142,6 +2182,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
        let env = update_env env d1 pat (env_of_annot (l,annot)) (env_of e2) in
        let d2,assigns,r2 = analyse_exp fn_id env assigns e2 in
        (d2,assigns,merge r1 r2)
+    (* There's a more general assignment case above to update env inside a block. *)
     | E_assign (lexp,e1) ->
        let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in
        let assigns,r2 = analyse_lexp fn_id env assigns d1 lexp in
@@ -2283,7 +2324,7 @@ let rec translate_loc l =
   | Generated l -> translate_loc l
   | _ -> None
 
-let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
+let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions globals =
   let pats = 
     match pat with
     | P_aux (P_tup pats,_) -> pats
@@ -2413,7 +2454,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
   in
   let kid_deps = KBindings.merge merge_kid_deps_eqns kid_deps eqn_kid_deps in
   let referenced_vars = Constant_propagation.referenced_vars body in
-  { top_kids; var_deps; kid_deps; referenced_vars }
+  { top_kids; var_deps; kid_deps; referenced_vars; globals }
 
 (* When there's more than one pick the first *)
 let merge_set_asserts _ x y =
@@ -2544,13 +2585,13 @@ let print_result r =
                                   (Failures.bindings r.failures)))) in
   ()
 
-let analyse_funcl debug tenv (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
+let analyse_funcl debug tenv constants (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
   let _ = if debug > 2 then print_endline (string_of_id id) else () in
   let pat,guard,body,_ = destruct_pexp pexp in
   let (tq,_) = Env.get_val_spec id tenv in
   let set_assertions = find_set_assertions body in
   let _ = if debug > 2 then print_set_assertions set_assertions in
-  let aenv = initial_env id l tq pat body set_assertions in
+  let aenv = initial_env id l tq pat body set_assertions constants in
   let _,_,r = analyse_exp id aenv Bindings.empty body in
   let r = match guard with
     | None -> r
@@ -2567,11 +2608,14 @@ let analyse_funcl debug tenv (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
   let _ = if debug > 2 then print_result r else ()
   in r
 
-let analyse_def debug env = function
+let analyse_def debug env globals = function
   | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) ->
-     List.fold_left (fun r f -> merge r (analyse_funcl debug env f)) empty funcls
+     globals, List.fold_left (fun r f -> merge r (analyse_funcl debug env globals f)) empty funcls
+
+  | DEF_val (LB_aux (LB_val (P_aux ((P_id id | P_typ (_,P_aux (P_id id,_))),_), exp),_)) ->
+     Bindings.add id (Constant_fold.is_constant exp) globals, empty
 
-  | _ -> empty
+  | _ -> globals, empty
 
 let detail_to_split = function
   | Total -> None
@@ -2585,7 +2629,11 @@ let argset_to_list splits =
   List.map argelt l
 
 let analyse_defs debug env (Defs defs) =
-  let r = List.fold_left (fun r d -> merge r (analyse_def debug env d)) empty defs in
+  let def (globals,r) d =
+    let globals,r' = analyse_def debug env globals d in
+    globals, merge r r'
+  in
+  let _,r = List.fold_left def (Bindings.empty,empty) defs in
 
   (* Resolve the interprocedural dependencies *)
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 5fa2b377..0365e2e5 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2786,6 +2786,25 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
          end
      in
      try_overload ([], Env.get_overloads f env)
+  | E_app (f, [x; y]), _ when string_of_id f = "and_bool" || string_of_id f = "or_bool" ->
+     (* We have to ensure that the type of y in (x || y) and (x && y)
+        is non-empty, otherwise it could force the entire type of the
+        expression to become empty even when unevaluted due to
+        short-circuiting. *)
+     begin match destruct_exist (typ_of (irule infer_exp env y)) with
+     | None | Some (_, NC_aux (NC_true, _), _) ->
+        let inferred_exp = infer_funapp l env f [x; y] (Some typ) in
+        type_coercion env inferred_exp typ
+     | Some _ ->
+        let inferred_exp = infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] (Some typ) in
+        type_coercion env inferred_exp typ
+     | exception Type_error _ ->
+        let inferred_exp = infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] (Some typ) in
+        type_coercion env inferred_exp typ
+     end
+  | E_app (f, xs), _ ->
+     let inferred_exp = infer_funapp l env f xs (Some typ) in
+     type_coercion env inferred_exp typ
   | E_return exp, _ ->
      let checked_exp = match Env.get_ret_typ env with
        | Some ret_typ -> crule check_exp env exp ret_typ
@@ -2795,9 +2814,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_tuple exps, Typ_tup typs when List.length exps = List.length typs ->
      let checked_exps = List.map2 (fun exp typ -> crule check_exp env exp typ) exps typs in
      annot_exp (E_tuple checked_exps) typ
-  | E_app (f, xs), _ ->
-     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' = try irule infer_exp env cond with Type_error _ -> crule check_exp env cond bool_typ in
      begin match destruct_exist (typ_of cond') with
@@ -3163,7 +3179,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      
   | P_app (f, pats) when Env.is_union_constructor f env ->
      (* Treat Ctor(x, y) as Ctor((x, y)) *)
-     bind_pat env (mk_pat (P_app (f, [mk_pat (P_tup pats)]))) typ
+     bind_pat env (P_aux (P_app (f, [mk_pat (P_tup pats)]),(l,()))) typ
 
   | P_app (f, pats) when Env.is_mapping f env ->
      begin
@@ -3686,6 +3702,12 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
          end
      in
      try_overload ([], Env.get_overloads f env)
+  | E_app (f, [x; y]) when string_of_id f = "and_bool" || string_of_id f = "or_bool" ->
+     begin match destruct_exist (typ_of (irule infer_exp env y)) with
+     | None | Some (_, NC_aux (NC_true, _), _) -> infer_funapp l env f [x; y] None
+     | Some _ -> infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] None
+     | exception Type_error _ -> infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] None
+     end
   | E_app (f, xs) -> infer_funapp l env f xs None
   | E_loop (loop_type, measure, cond, body) ->
      let checked_cond = crule check_exp env cond bool_typ in
diff --git a/test/mono/assign_range.sail b/test/mono/assign_range.sail
new file mode 100644
index 00000000..baf3ed43
--- /dev/null
+++ b/test/mono/assign_range.sail
@@ -0,0 +1,32 @@
+default Order dec
+$include <prelude.sail>
+
+val use : forall 'n, 'n >= 8. int('n) -> int
+
+function use(n) = {
+  let x : bits('n) = sail_sign_extend(0x12, n);
+  unsigned(x)
+}
+
+val test1 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test1(n) = {
+  size : {'m, 'm >= 8. int('m)} = n * 8;
+  use(size)
+}
+
+val test2 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test2(n) = {
+  size : range(8,32) = n * 8;
+  use(size)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test1(2) == 18);
+  assert(test1(4) == 18);
+  assert(test2(2) == 18);
+  assert(test2(4) == 18);
+}
diff --git a/test/mono/pass/assign_range b/test/mono/pass/assign_range
new file mode 100644
index 00000000..13642ef2
--- /dev/null
+++ b/test/mono/pass/assign_range
@@ -0,0 +1 @@
+assign_range.sail -auto_mono
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index c2c15c12..acadd4e2 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/complex_exist_sat/v1.expect b/test/typecheck/pass/complex_exist_sat/v1.expect
index b1937f47..4090165a 100644
--- a/test/typecheck/pass/complex_exist_sat/v1.expect
+++ b/test/typecheck/pass/complex_exist_sat/v1.expect
@@ -4,5 +4,5 @@ Type error:
   |                  ^
   | Tried performing type coercion from int(3) to {('q : Int), 'q in {0, 1}. int((2 * 'q))} on 3
   | Coercion failed because:
-  | Constraint 3 == (2 * 'ex1#) is not satisfiable
+  | Constraint 3 == (2 * 'ex2#) is not satisfiable
   | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 7bbd59ad..7bb8a4ab 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex195#)
+   | * datasize('ex196#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 24b927a5..4b9bd7cc 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
+   | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex152# bound here
+   |    | 'ex153# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex154# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex157# bound here
+   |    | 'ex158# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index a2c08583..52eb2f13 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
+   | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex152# bound here
+   |    | 'ex153# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex154# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex157# bound here
+   |    | 'ex158# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index cf86b765..0e43cd52 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex196# & ('ex196# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 80526204..011ecbdf 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex114# & ('ex114# + 1) <= 3)
+   |    * (0 <= 'ex115# & ('ex115# + 1) <= 3)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex117# & ('ex117# + 1) <= 3)
+   |    * (0 <= 'ex118# & ('ex118# + 1) <= 3)
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 0b705b50..9a34f688 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex114# & ('ex114# + 1) <= 4)
+   |    * (0 <= 'ex115# & ('ex115# + 1) <= 4)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex117# & ('ex117# + 1) <= 4)
+   |    * (0 <= 'ex118# & ('ex118# + 1) <= 4)
    | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex.sail b/test/typecheck/pass/short_circuit_bool_ex.sail
new file mode 100644
index 00000000..5cfdc1dc
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex.sail
@@ -0,0 +1,36 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+/*
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+*/
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if ok() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.expect b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
new file mode 100644
index 00000000..fc98db1b
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[short_circuit_bool_ex/v1.sail]:25:36-40
+25 |  if (true | assertive(n) > 0) then true else true
+   |                                    ^--^
+   | Tried performing type coercion from bool(true) to bool(0 == 1) on true
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.sail b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
new file mode 100644
index 00000000..2faf12af
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if bad() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file