From e9664cb042edb4468e524e2f98164e45b0d5a0ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 13:56:05 -0700 Subject: [PATCH] fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 14 +++++++++++++- tests/lua/tc6.lua | 3 +++ 2 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 tests/lua/tc6.lua diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 29cf9ebec..95f5045bd 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -445,12 +445,24 @@ static void check_name(environment const & env, name const & n) { throw_already_declared(env, n); } +static void check_duplicated_params(environment const & env, declaration const & d) { + level_param_names ls = d.get_params(); + while (!is_nil(ls)) { + auto const & p = head(ls); + ls = tail(ls); + if (std::find(ls.begin(), ls.end(), p) != ls.end()) { + throw_kernel_exception(env, sstream() << "failed to add declaration to environment, duplicate universe level parameter: '" + << p << "'", d.get_type()); + } + } +} + certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) { check_no_mlocal(env, d.get_type()); if (d.is_definition()) check_no_mlocal(env, d.get_value()); check_name(env, d.get_name()); - + check_duplicated_params(env, d); type_checker checker1(env, g, mk_default_converter(env, optional(), memoize, extra_opaque)); checker1.check(d.get_type(), d.get_params()); if (d.is_definition()) { diff --git a/tests/lua/tc6.lua b/tests/lua/tc6.lua new file mode 100644 index 000000000..f8e6fa95c --- /dev/null +++ b/tests/lua/tc6.lua @@ -0,0 +1,3 @@ +local env = environment() +local l = mk_param_univ("l") +check_error(function() env = add_decl(env, mk_var_decl("A", {l, l}, mk_sort(l))) end)