Add type variable information also to other errors involving constraints

src/lib/type_check.ml

@@ -1059,7 +1059,7 @@ let rec subtyp l env typ1 typ2 =
       let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
       let prop = nc_eq nexp1 nexp2 in
       if prove __POS__ env prop then ()
-      else typ_raise l (Err_subtype (typ1, typ2, Some prop, Env.get_constraint_reasons env, Env.get_typ_var_locs env))
+      else typ_raise l (Err_subtype (typ1, typ2, Some prop, Env.get_constraint_reasons env, Env.get_typ_vars_info env))
   | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
       let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
       let env =
@@ -1081,7 +1081,7 @@ let rec subtyp l env typ1 typ2 =
             let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
             if prove __POS__ env nc2 then ()
             else
-              typ_raise l (Err_subtype (typ1, typ2, Some nc2, Env.get_constraint_reasons env, Env.get_typ_var_locs env))
+              typ_raise l (Err_subtype (typ1, typ2, Some nc2, Env.get_constraint_reasons env, Env.get_typ_vars_info env))
         | _ -> typ_error l ("Constraint " ^ string_of_n_constraint (nc_eq nexp1 nexp2) ^ " is not satisfiable")
       end
   | _, _ -> (
@@ -1126,17 +1126,17 @@ let rec subtyp l env typ1 typ2 =
               if prove __POS__ env nc then ()
               else
                 typ_raise l
-                  (Err_subtype (typ1, typ2, Some nc, Env.get_constraint_reasons orig_env, Env.get_typ_var_locs env))
+                  (Err_subtype (typ1, typ2, Some nc, Env.get_constraint_reasons orig_env, Env.get_typ_vars_info env))
           | None, None ->
-              typ_raise l (Err_subtype (typ1, typ2, None, Env.get_constraint_reasons env, Env.get_typ_var_locs env))
+              typ_raise l (Err_subtype (typ1, typ2, None, Env.get_constraint_reasons env, Env.get_typ_vars_info env))
         )
     )
 
 and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
   typ_print
     (lazy (("Subtype arg " |> Util.green |> Util.clear) ^ string_of_typ_arg arg1 ^ " and " ^ string_of_typ_arg arg2));
   let raise_failed_constraint nc =
-    typ_raise l (Err_failed_constraint (nc, Env.get_locals env, Env.get_constraints env))
+    typ_raise l (Err_failed_constraint (nc, Env.get_locals env, Env.get_typ_vars_info env, Env.get_constraints env))
   in
   match (aux1, aux2) with
   | A_nexp n1, A_nexp n2 ->
@@ -2905,7 +2905,9 @@ and infer_lexp env (LE_aux (lexp_aux, (l, uannot)) as lexp) =
           in
           if !opt_no_lexp_bounds_check || prove __POS__ env check then
             annot_lexp (LE_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ slice_len)
-          else typ_raise l (Err_failed_constraint (check, Env.get_locals env, Env.get_constraints env))
+          else
+            typ_raise l
+              (Err_failed_constraint (check, Env.get_locals env, Env.get_typ_vars_info env, Env.get_constraints env))
       | _ -> typ_error l "Cannot assign slice of non vector type"
     end
   | LE_vector (v_lexp, exp) -> begin
@@ -2918,14 +2920,22 @@ and infer_lexp env (LE_aux (lexp_aux, (l, uannot)) as lexp) =
           let bounds_check = nc_and (nc_lteq (nint 0) nexp) (nc_lt nexp len) in
           if !opt_no_lexp_bounds_check || prove __POS__ env bounds_check then
             annot_lexp (LE_vector (inferred_v_lexp, inferred_exp)) elem_typ
-          else typ_raise l (Err_failed_constraint (bounds_check, Env.get_locals env, Env.get_constraints env))
+          else
+            typ_raise l
+              (Err_failed_constraint
+                 (bounds_check, Env.get_locals env, Env.get_typ_vars_info env, Env.get_constraints env)
+              )
       | Typ_app (id, [A_aux (A_nexp len, _)]) when Id.compare id (mk_id "bitvector") = 0 ->
           let inferred_exp = infer_exp env exp in
           let nexp, env = bind_numeric l (typ_of inferred_exp) env in
           let bounds_check = nc_and (nc_lteq (nint 0) nexp) (nc_lt nexp len) in
           if !opt_no_lexp_bounds_check || prove __POS__ env bounds_check then
             annot_lexp (LE_vector (inferred_v_lexp, inferred_exp)) bit_typ
-          else typ_raise l (Err_failed_constraint (bounds_check, Env.get_locals env, Env.get_constraints env))
+          else
+            typ_raise l
+              (Err_failed_constraint
+                 (bounds_check, Env.get_locals env, Env.get_typ_vars_info env, Env.get_constraints env)
+              )
       | Typ_id id -> begin
           match exp with
           | E_aux (E_id field, _) ->

src/lib/type_error.ml

@@ -251,15 +251,16 @@ let message_of_type_error =
             Line ("Could not resolve quantifiers for " ^ string_of_id id);
             Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants);
           ]
-    | Err_failed_constraint (check, locals, ncs) ->
+    | Err_failed_constraint (check, locals, _, ncs) ->
         Line ("Failed to prove constraint: " ^ string_of_n_constraint (constraint_simp check))
-    | Err_subtype (typ1, typ2, nc, all_constraints, all_vars) ->
+    | Err_subtype (typ1, typ2, nc, all_constraints, tyvars) ->
         let nc = Option.map constraint_simp nc in
         let typ1, typ2 = (simp_typ typ1, simp_typ typ2) in
         let nc_vars = match nc with Some nc -> tyvars_of_constraint nc | None -> KidSet.empty in
         (* Variables appearing in the types and constraint *)
         let appear_vars =
-          KBindings.bindings all_vars
+          KBindings.bindings tyvars.vars
+          |> List.map (fun (v, (l, _)) -> (v, l))
           |> List.filter (fun (v, _) ->
                  KidSet.mem v (KidSet.union nc_vars (KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2)))
              )
@@ -285,7 +286,7 @@ let message_of_type_error =
             (fun (substs, new_vars) (v, _) ->
               if is_kid_generated v || has_underscore v then (
                 let v' = readable_name v in
-                if (not (KBindings.mem v' all_vars)) && not (KidSet.mem v' new_vars) then
+                if (not (KBindings.mem v' tyvars.vars)) && not (KidSet.mem v' new_vars) then
                   (KBindings.add v (nvar v') substs, KidSet.add v' new_vars)
                 else (substs, new_vars)
               )

src/lib/type_error.mli

@@ -89,8 +89,8 @@ type type_error =
   | Err_no_casts of uannot 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 * (mut * typ) Bindings.t * type_variables * n_constraint list
-  | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * n_constraint list
-  | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * Ast.l KBindings.t
+  | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * type_variables * n_constraint list
+  | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * type_variables
   | Err_no_num_ident of id
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * string option * type_error

src/lib/type_internal.ml

@@ -104,8 +104,8 @@ type type_error =
   | Err_no_casts of uannot 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 * (mut * typ) Bindings.t * type_variables * n_constraint list
-  | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * n_constraint list
-  | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * Ast.l KBindings.t
+  | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * type_variables * n_constraint list
+  | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * type_variables
   | Err_no_num_ident of id
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * string option * type_error