fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion

closes #1279

src/frontends/lean/elaborator.cpp

@@ -463,6 +463,8 @@ bool elaborator::is_monad(expr const & e) {
     try {
         expr m = mk_app(m_ctx, get_monad_name(), e);
         return static_cast<bool>(m_ctx.mk_class_instance(m));
+    } catch (app_builder_exception &) {
+        return false;
     } catch (class_exception &) {
         return false;
     }

tests/lean/1279.lean

@@ -0,0 +1,12 @@
+structure Category : Type 2 :=
+  (Obj : Type)
+  (Hom : Obj → Obj → Type)
+  (compose : Π ⦃A B C : Obj⦄, Hom A B → Hom B C → Hom A C)
+
+open Category
+
+structure Functor (source target : Category) : Type :=
+  (onObjects     : Obj source → Obj target)
+  (onMorphisms   : Π ⦃A B : Obj source⦄, Hom source A B → Hom target (onObjects A) (onObjects B))
+  (functoriality : Π ⦃A B C : Obj source⦄ (f : Hom source A B) (g : Hom source B C),
+                    onMorphisms (compose source g f) = compose target (onMorphisms g) (onMorphisms f))

tests/lean/1279.lean.expected.out

@@ -0,0 +1,8 @@
+1279.lean:12:33: error: type mismatch at application
+  compose source g f
+term
+  f
+has type
+  Hom source A B
+but is expected to have type
+  Hom source C ?m_1