[ fix #4038 ] Don't block matching of meta against lambda pattern

4 files changed, 55 insertions, 6 deletions

diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
index 79a5cff..8ae3066 100644
--- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
+++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
@@ -242,6 +242,9 @@ instance Match Type NLPat Term where
           traceSDoc "rewriting.match" 30 (sep
             [ "blocking tag from reduction: " <+> text (show b') ]) $ do
           matchingBlocked (b `mappend` b')
+        maybeBlock w = case w of
+          MetaV m es -> matchingBlocked $ Blocked m ()
+          _          -> no ""
     case p of
       PVar i bvs -> traceSDoc "rewriting.match" 60 ("matching a PVar: " <+> text (show i)) $ do
         let allowedVars :: IntSet
@@ -260,7 +263,6 @@ instance Match Type NLPat Term where
             let t' = telePi  tel $ renameP __IMPOSSIBLE__ perm t
                 v' = teleLam tel $ renameP __IMPOSSIBLE__ perm v
             in tellSub r (i-n) t' v'
-      _ | MetaV m es <- v -> matchingBlocked $ Blocked m ()
 
       PDef f ps -> traceSDoc "rewriting.match" 60 ("matching a PDef: " <+> prettyTCM f) $ do
         v <- addContext k $ constructorForm =<< unLevel v
@@ -296,23 +298,23 @@ instance Match Type NLPat Term where
             match r gamma k (ct, Con c ci []) ps' (map Apply vs)
           MetaV m es -> do
             matchingBlocked $ Blocked m ()
-          _  -> no ""
+          v -> maybeBlock v
       PLam i p' -> case unEl t of
         Pi a b -> do
           let body = raise 1 v `apply` [Arg i (var 0)]
               k'   = ExtendTel a (Abs (absName b) k)
           match r gamma k' (absBody b) (absBody p') body
         MetaV m es -> matchingBlocked $ Blocked m ()
-        _ -> no ""
+        v -> maybeBlock v
       PPi pa pb -> case v of
         Pi a b -> do
           match r gamma k () pa a
           let k' = ExtendTel a (Abs (absName b) k)
           match r gamma k' () (absBody pb) (absBody b)
-        _ -> no ""
+        v -> maybeBlock v
       PSort ps -> case v of
         Sort s -> match r gamma k () ps s
-        _ -> no ""
+        v -> maybeBlock v
       PBoundVar i ps -> case v of
         Var i' es | i == i' -> do
           let ti = unDom $ indexWithDefault __IMPOSSIBLE__ (flattenTel k) i
@@ -330,7 +332,7 @@ instance Match Type NLPat Term where
           let flds = map argFromDom $ recFields def
               ps'  = map (fmap $ \fld -> PBoundVar i (ps ++ [Proj ProjSystem fld])) flds
           match r gamma k (ct, Con c ci []) (map Apply ps') (map Apply vs)
-        _ -> no ""
+        v -> maybeBlock v
       PTerm u -> traceSDoc "rewriting.match" 60 ("matching a PTerm" <+> addContext (gamma `abstract` k) (prettyTCM u)) $
         tellEq gamma k t u v
 
diff --git a/test/interaction/Issue4038.agda b/test/interaction/Issue4038.agda
new file mode 100644
index 0000000..829777b
--- /dev/null
+++ b/test/interaction/Issue4038.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --rewriting --confluence-check #-}
+
+open import Agda.Primitive using (Level; _⊔_; Setω; lzero; lsuc)
+
+infix 4 _≡_
+
+data _≡_ {ℓ : Level} {A : Set ℓ} (a : A) : A → Set ℓ where
+  refl : a ≡ a
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+run : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
+run refl x = x
+
+ap : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {a₁ a₂} → a₁ ≡ a₂ → f a₁ ≡ f a₂
+ap f refl = refl
+
+transport1 : ∀ {a b} {A : Set a} (B : A → Set b) {x y : A} (p : x ≡ y) → B x → B y
+transport1 B p = run (ap B p)
+
+ap-const : ∀ {a b} {A : Set a} {B : Set b} (f : B) {a₁ a₂ : A} (p : a₁ ≡ a₂) → ap (\ _ → f) p ≡ refl
+ap-const f refl = refl
+{-# REWRITE ap-const #-}
+
+ap2 : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : ∀ a → B a → RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → fn a₁ b₁ ≡ fn a₂ b₂
+ap2 fn refl refl = refl
+
+transport2 : ∀ {a b rv} {A : Set a} {B : A → Set b} (RV : ∀ a → B a → Set rv) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → RV a₁ b₁  → RV a₂ b₂
+transport2 RV pa pb = run (ap2 RV pa pb)
+
+ap2-const : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → ap2 {a} {b} {rv} {A} {B} {RV} (λ _ _ → fn) pa pb ≡ refl
+ap2-const fn refl refl = refl
+{-# REWRITE ap2-const #-}
+
+ap2-const' : ∀ {a b rv} {A : Set a} {B : A → Set b} {RV : Set rv} (fn : RV) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} (pb : transport1 B pa b₁ ≡ b₂) → ap2 {a} {b} {rv} {A} {B} {RV} (λ _ _ → fn) pa pb ≡ refl
+ap2-const' {a} {b} {rv} {A} {B} {RV} fn pa pb = {!ap2 {a} {b} {_} {A} {_} {_} (λ _ _ → fn ≡ fn) pa _!}
diff --git a/test/interaction/Issue4038.in b/test/interaction/Issue4038.in
new file mode 100644
index 0000000..5a5afef
--- /dev/null
+++ b/test/interaction/Issue4038.in
@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 1 (cmd_compute DefaultCompute) "ap2 {a} {b} {_} {A} {_} {_} (λ _ _ → fn ≡ fn) pa _"
\ No newline at end of file
diff --git a/test/interaction/Issue4038.out b/test/interaction/Issue4038.out
new file mode 100644
index 0000000..e74b6ba
--- /dev/null
+++ b/test/interaction/Issue4038.out
@@ -0,0 +1,9 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : ap2 (λ _ _ → fn) pa pb ≡ refl " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-info-action "*Error*" "Panic: no such interaction point: InteractionId {interactionId = 1}" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")