Add a missing well-formedness check

2 files changed, 6 insertions, 2 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index af4a7f65..93b6da36 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1335,10 +1335,12 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
 let expand_bind_synonyms l env (typq, typ) =
   typq, Env.expand_synonyms (add_typquant l typq env) typ
 
-let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) =
+let wf_binding l env (typq, typ) =
   let env = add_typquant l typq env in
   Env.wf_typ env typ
 
+let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) = wf_binding l env (typq, typ)
+
 (* Create vectors with the default order from the environment *)
 
 let default_order_error_string =
@@ -5077,11 +5079,13 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
   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
+     wf_binding l env (typq, typ);
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
   | Tu_ty_id (arg_typ, v) ->
      let typ' = mk_typ (Typ_fn ([arg_typ], ret_typ, no_effect)) in
+     wf_binding l env (typq, typ');
      env
      |> Env.add_union_id v (typq, typ')
      |> Env.add_val_spec v (typq, typ')
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index e2823692..ca83adb9 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('ex270#)
+   | * datasize('ex273#)
    |