6 files changed, 10 insertions, 9 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 1f27a0ab..4424fe8d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -803,10 +803,10 @@ end = struct
     | Typ_var kid -> begin
       match KBindings.find kid env.typ_vars with
       | (_, K_type) -> ()
-      | (_, k) -> typ_error env l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
+      | (_, k) -> typ_error env l ("Type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
                                ^ " is " ^ string_of_kind_aux k ^ " rather than Type")
       | exception Not_found ->
-         typ_error env l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
+         typ_error env l ("Unbound type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
     | Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ
     | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 ->
@@ -5080,15 +5080,16 @@ let fold_union_quant quants (QI_aux (qi, l)) =
 let forbid_recursive_types type_l f =
   try f () with
   | Type_error (env, l, err) ->
-     raise (Type_error (env, l, Err_because (err, type_l, Err_other "Recursive types are not allowed")))
+     let msg = "Types are not well-formed within this type definition. Note that recursive types are forbidden." in
+     raise (Type_error (env, l, Err_because (err, type_l, Err_other msg)))
 
 let check_type_union u_l non_rec_env env variant typq (Tu_aux (tu, l)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   match tu with
   | Tu_ty_id (Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) as typ, v) ->
      let typq = mk_typquant (List.map (mk_qi_id K_type) (KidSet.elements (tyvars_of_typ typ))) in
-     forbid_recursive_types u_l (fun () -> wf_binding l non_rec_env (typq, tuple_typ arg_typ));
      wf_binding l env (typq, typ);
+     forbid_recursive_types u_l (fun () -> wf_binding l non_rec_env (typq, tuple_typ arg_typ));
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect
index 6daa067d..2b5b1852 100644
--- a/test/typecheck/fail/struct_rec.expect
+++ b/test/typecheck/fail/struct_rec.expect
@@ -9,5 +9,5 @@ Type error:
   |   |^-----------
   | 4 |}
   |   |^
-  |   | Recursive types are not allowed
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
   | 
diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect
index 5d205606..3d482f40 100644
--- a/test/typecheck/fail/synonym_rec.expect
+++ b/test/typecheck/fail/synonym_rec.expect
@@ -7,5 +7,5 @@ Type error:
   | [synonym_rec.sail]:2:0-10
   | 2 |type T = T
   |   |^--------^
-  |   | Recursive types are not allowed
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
   | 
diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect
index 2d50cea6..7fd07169 100644
--- a/test/typecheck/fail/union_rec.expect
+++ b/test/typecheck/fail/union_rec.expect
@@ -9,5 +9,5 @@ Type error:
   |   |^----------
   | 4 |}
   |   |^
-  |   | Recursive types are not allowed
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
   | 
diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect
index b07910ba..ec610ae6 100644
--- a/test/typecheck/fail/union_recf.expect
+++ b/test/typecheck/fail/union_recf.expect
@@ -9,5 +9,5 @@ Type error:
   |   |^----------
   | 4 |}
   |   |^
-  |   | Recursive types are not allowed
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
   | 
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index bf498a36..0b0dda29 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -7,5 +7,5 @@ Type error:
    | [constrained_struct/v1.sail]:10:0-30
    | 10 |type MyStruct64 = MyStruct(65)
    |    |^----------------------------^
-   |    | Recursive types are not allowed
+   |    | Types are not well-formed within this type definition. Note that recursive types are forbidden.
    |