From b8ea69b3cd948db92fd9fa9898dfee82761a1e28 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 May 2016 14:20:16 -0700 Subject: [PATCH] fix(library/compiler/reduce_arity): incorrect assertion --- src/library/compiler/reduce_arity.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/reduce_arity.cpp b/src/library/compiler/reduce_arity.cpp index da0789f77d..f63108ef14 100644 --- a/src/library/compiler/reduce_arity.cpp +++ b/src/library/compiler/reduce_arity.cpp @@ -43,9 +43,12 @@ class remove_args_fn : public compiler_step_visitor { buffer args; get_app_args(e, args); buffer new_args; - lean_assert(args.size() == bv->size()); for (unsigned i = 0; i < args.size(); i++) { - if ((*bv)[i]) + /* The case i >= bv->size() can happen when the function is returning a closure. + We eta-expand terms, but we may miss cases where the type is opaque (e.g., IO a), + or the type is dependent (e.g., T b) where (T is defined as T b := bool.cases_on b nat (nat -> nat)). + */ + if (i >= bv->size() || (*bv)[i]) new_args.push_back(visit(args[i])); } return mk_app(fn, new_args);