Add SmartWithUIP test case

We already reject it!

Author: NathanielB123

src/full/Agda/TypeChecking/Coverage.hs

@@ -1443,8 +1443,10 @@ split' checkEmpty ind allowPartialCover inserttrailing
 
   where
     inContextOfT, inContextOfDelta2 :: (MonadAddContext tcm) => tcm a -> tcm a
-    inContextOfT      = addContext tel . escapeContext impossible (x + 1)
-    inContextOfDelta2 = addContext tel . escapeContext impossible x
+    inContextOfT      = addContext tel .
+      refreshLocalRewriteRules . escapeContext impossible (x + 1)
+    inContextOfDelta2 = addContext tel .
+      refreshLocalRewriteRules . escapeContext impossible x
 
     -- Debug printing
     debugInit tel x ps cps = liftTCM $ inTopContext $ do

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

@@ -130,7 +130,7 @@ unsafeEscapeContext n = unsafeModifyContext $ cxDrop n
 -- | Delete the last @n@ bindings from the context. Any occurrences of
 --   these variables are replaced with the given @err@.
 --
---   Does not (currently) delete local rewrite rules
+--   Does not (currently) delete local rewrite rules (but perhaps it should)
 escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a
 escapeContext err n = updateContext (strengthenS err n) $ cxDrop n
 

src/full/Agda/TypeChecking/Rules/Data.hs

@@ -703,9 +703,7 @@ checkNoLocalRewrites :: QName -> TCM ()
 checkNoLocalRewrites d = do
   def <- getConstInfo d
   case theDef def of
-    Datatype { dataPars = npars
-             , dataIxs = nixs
-             , dataSort = s}
+    Datatype { dataPars = npars }
      -> do
       let t = defType def
       TelV params t' <- telViewUpTo npars t

test/Fail/SmartWithUIP.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --smart-with #-}
+
+open import Agda.Builtin.Equality
+import Agda.Builtin.Equality.Rewrite
+
+-- Example due to Jesper Cockx
+
+data Unit : Set where ⟨⟩ : Unit
+
+variable
+  A B : Set
+  x y : A
+
+PathOver : (P : A → Set) (eq : x ≡ y) → P x → P y → Set
+PathOver P refl p q = p ≡ q
+
+hide : Unit → A → A
+hide ⟨⟩ x = x
+
+unitp : (u : Unit) → u ≡ ⟨⟩
+unitp ⟨⟩ = refl
+
+unitElim : (P : Unit → Set) → P ⟨⟩ → (u : Unit) → P u
+unitElim P d ⟨⟩ = d
+
+local-reflect : (u : Unit) (eq : hide u x ≡ x)
+              → PathOver (λ v → hide v x ≡ x) (unitp u) eq refl
+local-reflect {x = x} u eq
+  rewrite eq rewrite unitp u = refl
+
+uip : (eq : x ≡ x) → eq ≡ refl
+uip eq = local-reflect ⟨⟩ eq

test/Fail/SmartWithUIP.err

@@ -0,0 +1,23 @@
+SmartWithUIP.agda:28.1-27: warning: -W[no]RewriteLHSReduces
+_ : hide ⟨⟩ x ≡ x  is not a legal rewrite rule, since the left-hand
+side
+  hide ⟨⟩ x
+reduces to
+  x
+when checking that the pattern refl has type u ≡ ⟨⟩
+
+SmartWithUIP.agda:28.1-29.36: warning: -W[no]SmartWithOccursFail
+_ : u ≡ w  is not a legal rewrite rule, since the LHS occurs in the
+RHS or an earlier 'smart with' rewrite rule
+when checking that the clause
+SmartWithUIP.-rewrite58 {_} {x = x} u eq _ refl rewrite unitp u
+  = refl
+has type
+{x.A : Set} {x : x.A} (u : Unit) (eq : hide u x ≡ x) (w : x.A)
+{@rewrite w-eq : hide u x ≡ w} (prf : hide u x ≡ x)
+{@rewrite prf-eq : eq ≡ prf} →
+PathOver (λ v → hide v x ≡ x) (unitp u) eq refl
+
+SmartWithUIP.agda:28.1-27: error: [InvalidatedLocalRewriteRule]
+Local rewrite rule invalidated after a pattern-match
+when checking that the pattern refl has type u ≡ ⟨⟩