diff --git a/src/library/class.cpp b/src/library/class.cpp index 772eb683f..9ff85f1e7 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -290,13 +290,13 @@ static pair get_source_target(environment const & env, type_checker if (!tgt) throw exception(sstream() << "invalid transitive instance, resulting type of '" << n << "' is not a class"); optional src; - for (expr const & d : domain) { + unsigned i = domain.size(); + while (i > 0) { + --i; + expr const & d = domain[i]; if (auto it = is_ext_class(tc, mlocal_type(d))) { - if (src) { - throw exception(sstream() << "invalid transitive instance, '" << n - << "' has more than one instance argument"); - } src = it; + break; } } if (!src)