Fix type simplification dangling type variable problem

Affected trivial short-circuiting in the prover backends.

src/lib/type_env.ml

@@ -910,7 +910,7 @@ and expand_synonyms env (Typ_aux (typ, l)) =
         end
       with Not_found -> Typ_aux (Typ_id id, l)
     )
-  | Typ_exist (kopts, nc, typ) ->
+  | Typ_exist (kopts, nc, typ) -> (
       let nc = expand_constraint_synonyms env nc in
 
       (* When expanding an existential synonym we need to take care
@@ -941,7 +941,13 @@ and expand_synonyms env (Typ_aux (typ, l)) =
         List.fold_left (fun typ kid -> typ_subst kid (arg_nexp (nvar (prepend_kid "syn#" kid))) typ) typ !rebindings
       in
       let env = add_constraint nc env in
-      Typ_aux (Typ_exist (kopts, nc, expand_synonyms env typ), l)
+      let typ = expand_synonyms env typ in
+      (* When simplifying type variables might be removed (e.g., in 'b & false). Don't bind them or
+         the type checker can get upset. *)
+      let used_vars = KidSet.union (tyvars_of_constraint nc) (tyvars_of_typ typ) in
+      let kopts = List.filter (fun k -> KidSet.mem (kopt_kid k) used_vars) kopts in
+      match kopts with [] -> typ | _ -> Typ_aux (Typ_exist (kopts, nc, typ), l)
+    )
   | Typ_var v -> Typ_aux (Typ_var v, l)
 
 and expand_arg_synonyms env (A_aux (typ_arg, l)) =

test/typecheck/pass/false_existential.sail

@@ -0,0 +1,12 @@
+default Order dec
+$include <prelude.sail>
+
+/* Careless simplification of the existential type can leave an unused
+   'b binding that the type checker rejects. */
+
+val some_bool : unit -> bool
+
+function main() -> unit = {
+  let x : {('b : Bool), true. bool('b & false)} = some_bool() & false;
+  if x then print_endline("bad") else print_endline("good")
+}