diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 532592f815..2a90459ff3 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -1938,6 +1938,10 @@ class csimp_fn {
         case expr_kind::Proj:   return visit_proj(e, is_let_val);
         case expr_kind::App:    return visit_app(e, is_let_val);
         case expr_kind::Const:  return visit_constant(e, is_let_val);
+        /* We erase MData for now. We should revisit this decision when we rewrite the compiler in Lean, since we
+           are probably going to store debugging information in this kind of node.
+           We erase it here because `ir.cpp` does not support it, and produced `unreachable` code at issue #616 */
+        case expr_kind::MData:  return visit(mdata_expr(e), is_let_val);
         default:                return e;
         }
     }
diff --git a/tests/lean/run/616.lean b/tests/lean/run/616.lean
new file mode 100644
index 0000000000..ff3a8407bd
--- /dev/null
+++ b/tests/lean/run/616.lean
@@ -0,0 +1,3 @@
+def bug : Monad (λ α : Type _ => α → Prop) where
+  pure x := (.=x)
+  bind s f y := ∃ x, s x ∧ f x y