[ fix #7029 ] Check that function does not have unsolved metas when w…

…e add a rewrite rule to it and confluence checking is enabled

src/full/Agda/TypeChecking/Errors.hs

@@ -1485,6 +1485,10 @@ instance PrettyTCM TypeError where
         [ prettyTCM q , " is not a legal rewrite rule, since the head symbol"
         , prettyTCM f , "is not a postulate, a function, or a constructor"
         ]
+      HeadSymbolDefContainsMetas f -> hsep
+        [ prettyTCM q , "is not a legal rewrite rule, since the definition of the head symbol"
+        , prettyTCM f , "contains unsolved metavariables and confluence checking is enabled."
+        ]
       ConstructorParamsNotGeneral c vs -> vcat
         [ prettyTCM q <+> text " is not a legal rewrite rule, since the constructor parameters are not fully general:"
         , nest 2 $ text "Constructor: " <+> prettyTCM c

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -4736,6 +4736,7 @@ data IllegalRewriteRuleReason
   | HeadSymbolIsProjection QName
   | HeadSymbolIsProjectionLikeFunction QName
   | HeadSymbolNotPostulateFunctionConstructor QName
+  | HeadSymbolDefContainsMetas QName
   | ConstructorParamsNotGeneral ConHead Args
   | ContainsUnsolvedMetaVariables (Set MetaId)
   | BlockedOnProblems (Set ProblemId)

src/full/Agda/TypeChecking/Rewriting.hs

@@ -60,6 +60,8 @@ import Agda.Interaction.Options
 import Agda.Syntax.Abstract.Name
 import Agda.Syntax.Common
 import Agda.Syntax.Internal as I
+import Agda.Syntax.Internal.MetaVars
+import Agda.Syntax.Internal.Pattern
 
 import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Monad
@@ -337,10 +339,15 @@ checkRewriteRule q = do
     checkAxFunOrCon :: QName -> Definition -> TCM ()
     checkAxFunOrCon f def = case theDef def of
       Axiom{}        -> return ()
-      def@Function{} -> whenJust (maybeRight (funProjection def)) $ \proj ->
-        case projProper proj of
+      def@Function{} -> do
+        whenJust (maybeRight (funProjection def)) $ \proj -> case projProper proj of
           Just{} -> typeError $ IllegalRewriteRule q (HeadSymbolIsProjection f)
           Nothing -> typeError $ IllegalRewriteRule q (HeadSymbolIsProjectionLikeFunction f)
+        whenM (isJust . optConfluenceCheck <$> pragmaOptions) $ do
+          let simpleClause cl = (patternsToElims (namedClausePats cl) , clauseBody cl)
+          cls <- instantiateFull $ map simpleClause $ funClauses def
+          unless (noMetas cls) $ typeError $ IllegalRewriteRule q (HeadSymbolDefContainsMetas f)
+
       Constructor{}  -> return ()
       AbstractDefn{} -> return ()
       Primitive{}    -> return () -- TODO: is this fine?

test/Fail/Issue7029.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --rewriting --confluence-check --with-K #-}
+
+open import Agda.Builtin.Equality
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+myrefl : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≡ x
+myrefl = ?
+
+UIP : ∀ {ℓ} {A : Set ℓ} {x : A} → myrefl {ℓ} {A} {x} ≡ refl
+UIP with refl ← myrefl = refl
+
+{-# REWRITE UIP #-}

test/Fail/Issue7029.err

@@ -0,0 +1,3 @@
+Issue7029.agda:13,1-20
+UIP is not a legal rewrite rule, since the definition of the head symbol myrefl contains unsolved metavariables and confluence checking is enabled.
+when checking the pragma REWRITE UIP