Fix agda#7150 (agda#7113): solve constraints after inferring rewrite …

…expression

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.

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,

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