From 92a041233cc148fcfce2eccb43ae98a9b970de25 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 1 Nov 2019 01:49:13 +0000 Subject: Add a missing well-formedness check --- src/type_check.ml | 6 +++++- test/typecheck/pass/existential_ast/v3.expect | 2 +- 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#)  | -- cgit v1.2.3