From ffc90f6a3545ce12e487cba0304200be8d7d21da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Jul 2022 13:55:06 -0700
Subject: [PATCH] fix: bug at `ll_infer_type`

---
 src/library/compiler/ll_infer_type.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/library/compiler/ll_infer_type.cpp b/src/library/compiler/ll_infer_type.cpp
index 52418470a7..9167aeb861 100644
--- a/src/library/compiler/ll_infer_type.cpp
+++ b/src/library/compiler/ll_infer_type.cpp
@@ -62,6 +62,10 @@ class ll_infer_type_fn {
     expr infer_cases(expr const & e) {
         buffer<expr> args;
         get_app_args(e, args);
+        if (args.size() == 1) {
+            // This can happen for empty types. That is, the only argument is the major premise.
+            return mk_enf_object_type();
+        }
         lean_assert(args.size() >= 2);
         bool first = true;
         expr r     = *g_bot;