diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 7763e5bd1f..af527dbdfc 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -31,11 +31,16 @@ static expr compile_equations_core(environment & env, options const & opts,
                                    expr const & eqns) {
     type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
     trace_compiler(tout() << "compiling\n" << eqns << "\n";);
-    trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";);
-    trace_compiler(tout() << "nested recursion: " << has_nested_rec(eqns) << "\n";);
+    trace_compiler(tout() << "recursive:          " << is_recursive_eqns(ctx, eqns) << "\n";);
+    trace_compiler(tout() << "nested recursion:   " << has_nested_rec(eqns) << "\n";);
+    trace_compiler(tout() << "using_well_founded: " << is_wf_equations(eqns) << "\n";);
     equations_header const & header = get_equations_header(eqns);
     lean_assert(header.m_is_meta || !has_nested_rec(eqns));
+
     if (header.m_is_meta) {
+        if (is_wf_equations(eqns)) {
+            throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
+        }
         return mk_equations_result(unbounded_rec(env, opts, mctx, lctx, eqns));
     }
 
diff --git a/tests/lean/meta_wf_error.lean b/tests/lean/meta_wf_error.lean
new file mode 100644
index 0000000000..716e365425
--- /dev/null
+++ b/tests/lean/meta_wf_error.lean
@@ -0,0 +1,14 @@
+def R : (Σ _ : nat, nat) → (Σ _ : nat, nat) → Prop :=
+sigma.lex nat.lt (λ _, empty_relation)
+
+def Rwf : well_founded R :=
+sigma.lex_wf nat.lt_wf (λ _, empty_wf)
+
+meta def Div : nat → nat → nat
+| x y :=
+  if h : 0 < y ∧ y ≤ x
+  then
+    have x - y < x, from nat.sub_lt (nat.lt_of_lt_of_le h.left h.right) h.left,
+    Div (x - y) y + 1
+  else 0
+using_well_founded R Rwf
diff --git a/tests/lean/meta_wf_error.lean.expected.out b/tests/lean/meta_wf_error.lean.expected.out
new file mode 100644
index 0000000000..afa6e0998d
--- /dev/null
+++ b/tests/lean/meta_wf_error.lean.expected.out
@@ -0,0 +1 @@
+meta_wf_error.lean:7:9: error: invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion