diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index 78daecb526..6072f38fa3 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -40,13 +40,17 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs
           let eNew ← instantiateMVars eNew
-          let eEqE ← mkEq e e
-          let eEqEAbst := mkApp eEqE.appFn! eAbst
-          let motive := Lean.mkLambda `_a BinderInfo.default α eEqEAbst
+          let eType ← inferType e
+          let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
           unless (← isTypeCorrect motive) do
             throwTacticEx `rewrite mvarId "motive is not type correct"
-          let eqRefl ← mkEqRefl e
-          let eqPrf ← mkEqNDRec motive eqRefl heq
+          unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do
+            -- NB: using motive.arrow? would disallow motives where the dependency
+            -- can be reduced away
+            throwTacticEx `rewrite mvarId "motive is dependent"
+          let u1 ← getLevel α
+          let u2 ← getLevel eType
+          let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
diff --git a/tests/lean/motiveNotTypeCorect.lean b/tests/lean/motiveNotTypeCorect.lean
index a999327af0..cd9b84fc34 100644
--- a/tests/lean/motiveNotTypeCorect.lean
+++ b/tests/lean/motiveNotTypeCorect.lean
@@ -6,3 +6,14 @@ def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
   := by
   rw [h] -- tactic 'rewrite' failed, motive is not type correct
   sorry
+
+def K (x : α) (y : β) : β := y
+example (h : true = false) (A : (b : Bool) → K b Type) (h2 : A false) : A true := by
+  -- the motive is dependent on `true`, but in a non-essential way, so this works fine
+  rw [h]
+  exact h2
+
+example (h : true = false) (A : (b : Bool) → if b then Prop else Nat) : A true :=
+  by
+    rw [h] -- tactic 'rewrite' failed, motive is dependent
+    exact 0
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out
index cee57716ed..bee1a003f4 100644
--- a/tests/lean/motiveNotTypeCorect.lean.expected.out
+++ b/tests/lean/motiveNotTypeCorect.lean.expected.out
@@ -5,3 +5,7 @@ h : f t = t
 d : D (f t)
 P : (t : Nat) → D t → Prop
 ⊢ P (f t) d
+motiveNotTypeCorect.lean:18:8-18:9: error: tactic 'rewrite' failed, motive is dependent
+h : true = false
+A : (b : Bool) → if b = true then Prop else Nat
+⊢ A true