From 274aeed30facb0bc0b9f5bd0c537014ea83cc986 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jan 2019 15:40:25 -0800 Subject: [PATCH] fix(library/compiler/compiler): make sure that the type of functions that return closures match their arity Before this commit, we could have a LLNF function `f` of arity 0 and type `_obj -> _obj`. Now, this kind of function has type `_obj`. --- src/library/compiler/compiler.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 651596571f..5055c0424f 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -76,11 +76,22 @@ static environment cache_stage1(environment env, comp_decls const & ds) { return env; } +static expr ensure_arity(expr const & t, unsigned arity) { + if (arity == 0) { + if (is_pi(t)) return mk_enf_object_type(); // closure + else return t; + } + lean_assert(is_pi(t)); + return ensure_arity(binding_body(t), arity-1); +} + static environment cache_stage2(environment env, comp_decls const & ds) { for (comp_decl const & d : ds) { name n = d.fst(); expr v = d.snd(); expr t = ll_infer_type(env, v); + unsigned arity = get_num_nested_lambdas(v); + v = ensure_arity(t, arity); lean_trace(name({"compiler", "stage2"}), tout() << n << " : " << t << "\n";); env = register_stage2_decl(env, n, t, v); }