diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 930df5f760..adf6740397 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -763,12 +763,17 @@ end CheckAssignmentQuick
   Auxiliary function for handling constraints of the form `?m a₁ ... aₙ =?= v`.
   It will check whether we can perform the assignment
   ```
-  ?m := fun fvars => t
+  ?m := fun fvars => v
   ```
   The result is `none` if the assignment can't be performed.
   The result is `some newV` where `newV` is a possibly updated `v`. This method may need
   to unfold let-declarations. -/
 def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) := do
+  /- Check whether `mvarId` occurs in the type of `fvars` or not. If it does, return `none`
+     to prevent us from creating the cyclic assignment `?m := fun fvars => v` -/
+  for fvar in fvars do
+    unless (← occursCheck mvarId (← inferType fvar)) do
+      return none
   if !v.hasExprMVar && !v.hasFVar then
     pure (some v)
   else
diff --git a/tests/lean/302.lean b/tests/lean/302.lean
new file mode 100644
index 0000000000..2cc8077042
--- /dev/null
+++ b/tests/lean/302.lean
@@ -0,0 +1 @@
+def f(y:m 0:=a-t):=f a
diff --git a/tests/lean/302.lean.expected.out b/tests/lean/302.lean.expected.out
new file mode 100644
index 0000000000..b078015fbc
--- /dev/null
+++ b/tests/lean/302.lean.expected.out
@@ -0,0 +1,12 @@
+302.lean:1:8-1:11: error: function expected at
+  m
+term has type
+  ?m
+302.lean:1:8-1:11: error: function expected at
+  m
+term has type
+  ?m
+302.lean:1:8-1:11: error: function expected at
+  m
+term has type
+  ?m