michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 13:56:05 -07:00
parent 9b6b162a7c
commit e9664cb042
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/type_checker.cpp
View file

@ -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<module_idx>(), memoize, extra_opaque));
checker1.check(d.get_type(), d.get_params());
if (d.is_definition()) {

3
tests/lua/tc6.lua Normal file
View file

@ -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)