diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs
index 89608da4fa3..b420790a0a7 100644
--- a/src/full/Agda/TypeChecking/Rules/Def.hs
+++ b/src/full/Agda/TypeChecking/Rules/Def.hs
@@ -995,6 +995,10 @@ checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb _ _) rh
 
       (proof, eqt) <- inferExpr eq
 
+      -- Andreas, 2024-02-27, issue #7150
+      -- trigger instance search to resolve instances in rewrite-expression
+      solveAwakeConstraints
+
       -- Andreas, 2016-04-14, see also Issue #1796
       -- Run the size constraint solver to improve with-abstraction
       -- in case the with-expression contains size metas.
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs
index 51135f4c66d..dc3fe388e6b 100644
--- a/src/full/Agda/TypeChecking/Rules/Term.hs
+++ b/src/full/Agda/TypeChecking/Rules/Term.hs
@@ -1567,8 +1567,8 @@ isModuleFreeVar i = do
 inferExprForWith :: Arg A.Expr -> TCM (Term, Type)
 inferExprForWith (Arg info e) = verboseBracket "tc.with.infer" 20 "inferExprForWith" $
   applyRelevanceToContext (getRelevance info) $ do
-    reportSDoc "tc.with.infer" 20 $ "inferExprforWith " <+> prettyTCM e
-    reportSLn  "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e)
+    reportSDoc "tc.with.infer" 20 $ "inferExprForWith " <+> prettyTCM e
+    reportSLn  "tc.with.infer" 80 $ "inferExprForWith " ++ show (deepUnscope e)
     traceCall (InferExpr e) $ do
       -- Andreas, 2024-02-26, issue #7148:
       -- The 'instantiateFull' here performs necessary eta-contraction,
diff --git a/test/Succeed/Issue7150.agda b/test/Succeed/Issue7150.agda
new file mode 100644
index 00000000000..5fa5713eb32
--- /dev/null
+++ b/test/Succeed/Issue7150.agda
@@ -0,0 +1,18 @@
+-- Andreas, 2024-02-27, issue #7150.
+-- Reported as #7113 and testcase by buggymcbugfix.
+-- Regression in 2.6.4: instance search runs too late,
+-- making a rewrite fail.
+
+open import Agda.Builtin.Equality
+
+record Semiring : Set₁ where
+  field
+    Carrier   : Set
+    one       : Carrier
+    mul       : Carrier → Carrier → Carrier
+    left-unit : (r : Carrier) → mul one r ≡ r
+
+open Semiring {{...}}
+
+foo : {{R : Semiring}} (r : Carrier) → mul one r ≡ r
+foo r rewrite left-unit r = refl