Stefan pushed to branch master at Stefan / Typer
Commits: 3fb126a2 by Stefan Monnier at 2016-11-11T14:17:20-05:00 * src/lparse.ml: Fix missing type error detection after unify
* src/lparse.ml (_lexp_p_check.unify_with_arrow) (lexp_p_infer_and_check): Pay attention to the un-satisfied constraints returned by Unif.unify.
- - - - -
2 changed files:
- src/lparse.ml - tests/eval_test.ml
Changes:
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -388,12 +388,18 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with - | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow ^ " does not match"); dltype, dltype + | Some (_, (t1,t2)::_) + -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 + ^ " and " + ^ lexp_string t2 + ^ " do not match"); + dltype, dltype + | Some subst -> global_substitution := subst; arg, body
in let infer_lambda_body kind var def_arg_type body subst = @@ -444,12 +450,17 @@ and lexp_p_infer_and_check pexp ctx t i = let (e, inferred_t) = _lexp_p_infer pexp ctx i in let subst, _ = !global_substitution in (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with - | Some subst -> global_substitution := subst | None -> lexp_error (pexp_location pexp) e ("Type mismatch! Context expected `" ^ lexp_string t ^ "` but expression has type `" - ^ lexp_string inferred_t ^ "`\n")); + ^ lexp_string inferred_t ^ "`\n") + | Some (_, (t1,t2)::_) + -> lexp_error (pexp_location pexp) e + ("Type mismatch! Context expected `" + ^ lexp_string t2 ^ "` but expression has type `" + ^ lexp_string t1 ^ "`\n") + | Some subst -> global_substitution := subst); e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -251,7 +251,8 @@ let _ = test_eval_eqv_named "my_list = cons 1 (cons 2 (cons 3 - (cons 4 (nil (a := Int)))))" + (cons 4 (nil %%(a := Int) + ))))"
"length my_list; head my_list;
View it on GitLab: https://gitlab.com/monnier/typer/commit/3fb126a2a5be3f992b9b1922384600b21235...
Afficher les réponses par date