[ fix agda#6006 ] Postpone check for unsolved metas until building of…

… pattern

src/full/Agda/TypeChecking/Rewriting.hs

@@ -211,9 +211,9 @@ checkRewriteRule q = do
   let failureWrongTarget :: TCM a
       failureWrongTarget = typeError . GenericDocError =<< hsep
         [ prettyTCM q , " does not target rewrite relation" ]
-  let failureMetas :: TCM a
-      failureMetas       = typeError . GenericDocError =<< hsep
-        [ prettyTCM q , " is not a legal rewrite rule, since it contains unsolved meta variables" ]
+  let failureMetas :: Blocker -> TCM a
+      failureMetas b     = typeError . GenericDocError =<< hsep
+        [ prettyTCM q , " is not a legal rewrite rule, since it contains the unsolved meta variable(s)" , prettyTCM b ]
   let failureNotDefOrCon :: TCM a
       failureNotDefOrCon = typeError . GenericDocError =<< hsep
         [ prettyTCM q , " is not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor" ]
@@ -248,10 +248,6 @@ checkRewriteRule q = do
       gamma1 <- instantiateFull gamma1
       let gamma = gamma0 `abstract` gamma1
 
-      unless (noMetas (telToList gamma1)) $ do
-        reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetasList $ telToList gamma1)
-        failureMetas
-
       -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
       -- This is necessary to replace copies created by imports by their
       -- original definition.
@@ -276,13 +272,9 @@ checkRewriteRule q = do
 
         checkNoLhsReduction f hd es
 
-        unless (noMetas (es, rhs, b)) $ do
-          reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetasList es)
-          reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetasList rhs)
-          reportSDoc "rewriting" 30 $ "metas in b  : " <+> text (show $ allMetasList b)
-          failureMetas
+        ps <- catchPatternErr failureMetas $
+          patternFrom Relevant 0 (t , Def f []) es
 
-        ps <- patternFrom Relevant 0 (t , Def f []) es
         reportSDoc "rewriting" 30 $
           "Pattern generated from lhs: " <+> prettyTCM (PDef f ps)
 

src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs

@@ -6,6 +6,8 @@
 
 module Agda.TypeChecking.Rewriting.NonLinPattern where
 
+import Prelude hiding ( null )
+
 import Control.Monad        ( (>=>), forM )
 import Control.Monad.Reader ( asks )
 
@@ -15,6 +17,7 @@ import qualified Data.IntSet as IntSet
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Internal.Defs
+import Agda.Syntax.Internal.MetaVars ( AllMetas, unblockOnAllMetasIn )
 
 import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Free
@@ -57,22 +60,22 @@ instance PatternFrom (Type, Term) Elims [Elim' NLPat] where
   patternFrom r k (t,hd) = \case
     [] -> return []
     (Apply u : es) -> do
-      ~(Pi a b) <- unEl <$> reduce t
+      ~(Pi a b) <- unEl <$> abortIfBlocked t
       p   <- patternFrom r k a u
-      t'  <- t `piApplyM` u
+      t'  <- piApplyM' (blockOnMetasIn t >> __IMPOSSIBLE__) t u
       let hd' = hd `apply` [ u ]
       ps  <- patternFrom r k (t',hd') es
       return $ Apply p : ps
     (IApply x y i : es) -> do
-      ~(PathType s q l b u v) <- pathView =<< reduce t
+      ~(PathType s q l b u v) <- pathView =<< abortIfBlocked t
       let t' = El s $ unArg b `apply` [ defaultArg i ]
       let hd' = hd `applyE` [IApply x y i]
       interval <- primIntervalType
       p   <- patternFrom r k interval i
       ps  <- patternFrom r k (t',hd') es
       return $ IApply (PTerm x) (PTerm y) p : ps
     (Proj o f : es) -> do
-      ~(Just (El _ (Pi a b))) <- getDefType f =<< reduce t
+      ~(Just (El _ (Pi a b))) <- getDefType f =<< abortIfBlocked t
       let t' = b `absApp` hd
       hd' <- applyDef o f (argFromDom a $> hd)
       ps  <- patternFrom r k (t',hd') es
@@ -88,7 +91,7 @@ instance PatternFrom () Type NLPType where
 
 instance PatternFrom () Sort NLPSort where
   patternFrom r k _ s = do
-    s <- reduce s
+    s <- abortIfBlocked s
     case s of
       Type l   -> PType <$> patternFrom r k () l
       Prop l   -> PProp <$> patternFrom r k () l
@@ -117,11 +120,11 @@ instance PatternFrom () Level NLPat where
 
 instance PatternFrom Type Term NLPat where
   patternFrom r0 k t v = do
-    t <- reduce t
+    t <- abortIfBlocked t
     etaRecord <- isEtaRecordType t
-    prop <- fromRight __IMPOSSIBLE__ <.> runBlocked $ isPropM t
+    prop <- isPropM t
     let r = if prop then Irrelevant else r0
-    v <- unLevel =<< reduce v
+    v <- unLevel =<< abortIfBlocked v
     reportSDoc "rewriting.build" 60 $ sep
       [ "building a pattern from term v = " <+> prettyTCM v
       , " of type " <+> prettyTCM t
@@ -144,10 +147,11 @@ instance PatternFrom Type Term NLPat where
        -- The arguments of `var i` should be distinct bound variables
        -- in order to build a Miller pattern
        | Just vs <- allApplyElims es -> do
-           TelV tel _ <- telViewPath =<< typeOfBV i
-           unless (size tel >= size vs) __IMPOSSIBLE__
+           TelV tel rest <- telViewPath =<< typeOfBV i
+           unless (size tel >= size vs) $ blockOnMetasIn rest >> __IMPOSSIBLE__
            let ts = applySubst (parallelS $ reverse $ map unArg vs) $ map unDom $ flattenTel tel
            mbvs <- forM (zip ts vs) $ \(t , v) -> do
+             blockOnMetasIn (v,t)
              isEtaVar (unArg v) t >>= \case
                Just j | j < k -> return $ Just $ v $> j
                _              -> return Nothing
@@ -188,7 +192,7 @@ instance PatternFrom Type Term NLPat where
       (_ , Sort s)     -> PSort <$> patternFrom r k () s
       (_ , Level l)    -> __IMPOSSIBLE__
       (_ , DontCare{}) -> __IMPOSSIBLE__
-      (_ , MetaV{})    -> __IMPOSSIBLE__
+      (_ , MetaV m _)  -> __IMPOSSIBLE__
       (_ , Dummy s _)  -> __IMPOSSIBLE_VERBOSE__ s
 
 -- | Convert from a non-linear pattern to a term.
@@ -353,3 +357,10 @@ instance Free NLPSort where
     PSizeUniv -> mempty
     PLockUniv -> mempty
     PIntervalUniv -> mempty
+
+-- Throws a pattern violation if the given term contains any
+-- metavariables.
+blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m ()
+blockOnMetasIn t = case unblockOnAllMetasIn t of
+  UnblockOnAll ms | null ms -> return ()
+  b -> patternViolation b

test/Fail/Issue6006.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --type-in-type --rewriting #-}
+
+infix 10 _≡_
+
+data _≡_ {A : Set} (a : A) : A → Set where
+  reflᵉ : a ≡ a
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+postulate
+  T : Set
+  C : T
+  F : T → T
+
+a : T → T
+a x = ?
+
+postulate
+  r : ∀ x → F (a x) ≡ C
+
+{-# REWRITE r #-}

test/Fail/Issue6006.err

@@ -0,0 +1,3 @@
+Issue6006.agda:21,1-18
+r  is not a legal rewrite rule, since it contains the unsolved meta variable(s) _10
+when checking the pragma REWRITE r

test/Fail/RewriteRuleOpenMeta.err

@@ -1,3 +1,3 @@
 RewriteRuleOpenMeta.agda:13,1-18
-r  is not a legal rewrite rule, since it contains unsolved meta variables
+r  is not a legal rewrite rule, since it contains the unsolved meta variable(s) _7
 when checking the pragma REWRITE r