diff options
| author | Alasdair | 2019-02-20 22:31:51 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-20 22:41:31 +0000 |
| commit | 7253269fb62712e7e8fd94d5d0264d5bed9e8406 (patch) | |
| tree | 9119cd23ce556f0b9b1ffcf719d11fa5dcdbbd77 /src | |
| parent | 09c8c3e212e5959461312d28240f2ae843a19e81 (diff) | |
Fix bug with missing satisfiablity check in subtyping
Thanks to Mark for finding this bug. Regression test is
complex_exist_sat in test/typecheck/pass/
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 3d0f38a6..8de4a904 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1976,9 +1976,17 @@ let rec subtyp l env typ1 typ2 = let env = add_typ_vars l (List.map (mk_kopt K_int) (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2)))) env in let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in if not (kids2 = []) then typ_error env l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else (); - let env = Env.add_constraint (nc_eq nexp1 nexp2) env in - if prove __POS__ env nc2 then () - else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env)) + let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) (Env.get_typ_vars env) in + begin match Constraint.call_smt l vars (nc_eq nexp1 nexp2) with + | Constraint.Sat -> + let env = Env.add_constraint (nc_eq nexp1 nexp2) env in + if prove __POS__ env nc2 then + () + else + typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env)) + | _ -> + typ_error env l ("Constraint " ^ string_of_n_constraint (nc_eq nexp1 nexp2) ^ " is not satisfiable") + end | _, _ -> match typ_aux1, typ_aux2 with | _, Typ_internal_unknown when Env.allow_unknowns env -> () |