diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index e72282dd63..0c8c5f52b6 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -817,6 +817,17 @@ struct unifier_fn {
         lean_unreachable(); // LCOV_EXCL_LINE
     }
 
+    /** \brief Return true if type of \c e is Type.
+        \remark constraints are discarded */
+    bool is_type(expr const & e) {
+        constraint_seq cs;
+        optional<expr> t = infer(e, cs);
+        if (!t)
+            return false;
+        t = whnf(*t, cs);
+        return is_sort(*t);
+    }
+
     optional<declaration> is_delta(expr const & e) {
         return m_tc->is_delta(e);
     }
@@ -1030,9 +1041,14 @@ struct unifier_fn {
         }
 
         if (is_eq_deltas(lhs, rhs)) {
-            // we need to create a backtracking point for this one
-            add_cnstr(c, cnstr_group::Basic);
-            return true;
+            if (!split_delta(lhs) && is_type(lhs)) {
+                // If lhs (and consequently rhs) is a type, and not case-split is generated, then process delta constraint eagerly.
+                return process_delta(c);
+            } else {
+                // we need to create a backtracking point for this one
+                add_cnstr(c, cnstr_group::Basic);
+                return true;
+            }
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
@@ -1651,6 +1667,15 @@ struct unifier_fn {
         return true;
     }
 
+    // Return true if we should case-split on a delta constraint where \c lhs is the left-hand-side
+    bool split_delta(expr const & lhs) {
+        expr lhs_fn     = get_app_fn(lhs);
+        lean_assert(is_constant(lhs_fn));
+        declaration d   = *m_env.find(const_name(lhs_fn));
+        return (m_config.m_kind == unifier_kind::Liberal &&
+                (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name())));
+    }
+
     /**
         \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded.
         We consider two possible solutions:
@@ -1679,8 +1704,7 @@ struct unifier_fn {
             return unfold_delta(c, justification());
 
         justification a;
-        if (m_config.m_kind == unifier_kind::Liberal &&
-            (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))) {
+        if (split_delta(lhs)) {
             // add case_split for t =?= s
             a = mk_assumption_justification(m_next_assumption_idx);
             add_case_split(std::unique_ptr<case_split>(new delta_unfold_case_split(*this, j, c)));
diff --git a/tests/lean/run/809.lean b/tests/lean/run/809.lean
new file mode 100644
index 0000000000..a99ddbf37f
--- /dev/null
+++ b/tests/lean/run/809.lean
@@ -0,0 +1,23 @@
+import data.finset data.num data.nat data.int algebra.ring
+open finset num nat int algebra
+
+check @finset.insert _ _ 1 (@finset.empty ℕ)
+
+check '{1, 2, 3}               -- finset num
+check ('{1, 2, 3} : finset ℕ)
+check ('{1, 2, 3} : finset ℕ)  -- finset ℕ
+check ('{1, 2, 3} : finset ℤ)  -- finset ℤ
+
+example : finset nat :=
+insert 1 (insert 2 (insert 3 empty))
+
+check insert 1 (insert 2 (insert 3 empty)) -- finset num
+check (insert 1 (insert 2 (insert 3 empty)) : finset nat)
+
+check (insert (1:nat) (insert (2:nat) (insert (3:nat) empty)))
+
+definition foo_nat (x : finset ℕ) : finset ℕ := x
+definition foo_int (x : finset ℤ) : finset ℤ := x
+
+check foo_nat '{1, 2, 3}  -- finset ℕ
+check foo_int '{1, 2, 3}  -- finset ℤ
diff --git a/tests/lean/run/809b.lean b/tests/lean/run/809b.lean
new file mode 100644
index 0000000000..3b4197664d
--- /dev/null
+++ b/tests/lean/run/809b.lean
@@ -0,0 +1,21 @@
+import algebra.ring data.finset
+open finset nat algebra
+
+constant A : Type₁
+constants a b : A
+axiom decA : decidable_eq A
+attribute decA [instance]
+notation 5 := a
+notation 5 := b
+
+definition foo1 : finset nat :=
+'{ 1, 2, 5, 5 }
+
+definition foo2 : finset nat :=
+'{ 1, 2, 3 }
+
+definition foo3 : finset nat :=
+'{ 1 }
+
+noncomputable definition foo4 : finset A :=
+'{ 5, 5, b }