diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 794229da85..e002da5439 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -969,7 +969,7 @@ expr elaborator::visit_lambda(expr const & e, constraint_seq & cs) {
 
 expr elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) {
     constraint_seq t_cs;
-    expr t      = visit(get_typed_expr_type(e), t_cs);
+    expr t      = ensure_type(visit_expecting_type(get_typed_expr_type(e), t_cs), t_cs);
     constraint_seq v_cs;
     expr v      = visit_expecting_type_of(get_typed_expr_expr(e), t, v_cs);
     expr v_type = infer_type(v, v_cs);
diff --git a/tests/lean/run/965.lean b/tests/lean/run/965.lean
new file mode 100644
index 0000000000..5af339523f
--- /dev/null
+++ b/tests/lean/run/965.lean
@@ -0,0 +1,7 @@
+import algebra.bundled
+variable G : Group
+check (1 : G)
+check (1 : Group.carrier G)
+set_option pp.coercions true
+check (1 : G)
+check (1 : Group.carrier G)