[ fix agda#5396 agda#5531 ] Replace some impossible's by failure if -…

…-rewriting is enabled

src/full/Agda/TypeChecking/CompiledClause/Match.hs

@@ -3,6 +3,8 @@ module Agda.TypeChecking.CompiledClause.Match where
 
 import qualified Data.Map as Map
 
+import Agda.Interaction.Options (optRewriting)
+
 import Agda.Syntax.Internal
 import Agda.Syntax.Common
 
@@ -13,6 +15,7 @@ import Agda.TypeChecking.Reduce.Monad as RedM
 import Agda.TypeChecking.Substitute
 
 import Agda.Utils.Maybe
+import Agda.Utils.Monad
 import Agda.Utils.Pretty (prettyShow)
 
 import Agda.Utils.Impossible
@@ -197,6 +200,8 @@ match' [] = {- new line here since __IMPOSSIBLE__ does not like the ' in match'
     if f `elem` pds
     then return (NoReduction $ NotBlocked MissingClauses [])
     else do
-      traceSLn "impossible" 10
+      ifM (optRewriting <$> pragmaOptions)
+      {-then-} (return (NoReduction $ NotBlocked ReallyNotBlocked [])) -- See #5396
+      {-else-} $ traceSLn "impossible" 10
         ("Incomplete pattern matching when applying " ++ prettyShow f)
         __IMPOSSIBLE__

src/full/Agda/TypeChecking/Reduce/Fast.hs

@@ -72,6 +72,7 @@ import Agda.Utils.Float
 import Agda.Utils.Lens
 import Agda.Utils.List
 import Agda.Utils.Maybe
+import Agda.Utils.Monad
 import Agda.Utils.Null (empty)
 import Agda.Utils.Functor
 import Agda.Utils.Pretty
@@ -1373,6 +1374,7 @@ reduceTm rEnv bEnv !constInfo normalisation ReductionFlags{..} =
         -- Bad work-around for #3870: don't fail hard during instance search.
       | speculative          = rewriteAM (Eval (mkValue (NotBlocked MissingClauses ()) cl) ctrl)
       | f `elem` partialDefs = rewriteAM (Eval (mkValue (NotBlocked MissingClauses ()) cl) ctrl)
+      | hasRewriting         = rewriteAM (Eval (mkValue (NotBlocked ReallyNotBlocked ()) cl) ctrl)  -- See #5396
       | otherwise            = runReduce $
           traceSLn "impossible" 10 ("Incomplete pattern matching when applying " ++ prettyShow f)
                    __IMPOSSIBLE__

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

@@ -165,20 +165,24 @@ instance Match (Type, Elims -> Term) [Elim' NLPat] Elims where
      , "  with               " <+> addContext k (prettyTCM v)
      , "  eliminating head   " <+> addContext k (prettyTCM $ hd []) <+> ":" <+> addContext k (prettyTCM t)]) $ do
    case (p,v) of
-    (Apply p, Apply v) -> do
-      ~(Pi a b) <- addContext k $ unEl <$> reduce t
-      match r gamma k a p v
-      let t'  = absApp b (unArg v)
-          hd' = hd . (Apply v:)
-      match r gamma k (t',hd') ps vs
-
-    (IApply x y p , IApply u v i) -> do
-      ~(PathType s q l b _u _v) <- addContext k $ pathView =<< reduce t
-      Right interval <- runExceptT primIntervalType
-      match r gamma k interval p i
-      let t' = El s $ unArg b `apply` [ defaultArg i ]
-      let hd' = hd . (IApply u v i:)
-      match r gamma k (t',hd') ps vs
+    (Apply p, Apply v) -> (addContext k $ unEl <$> reduce t) >>= \case
+      Pi a b -> do
+        match r gamma k a p v
+        let t'  = absApp b (unArg v)
+            hd' = hd . (Apply v:)
+        match r gamma k (t',hd') ps vs
+      t -> traceSDoc "rewriting.match" 20
+        ("application at non-pi type (possible non-confluence?) " <+> prettyTCM t) mzero
+
+    (IApply x y p , IApply u v i) -> (addContext k $ pathView =<< reduce t) >>= \case
+      PathType s q l b _u _v -> do
+        Right interval <- runExceptT primIntervalType
+        match r gamma k interval p i
+        let t' = El s $ unArg b `apply` [ defaultArg i ]
+        let hd' = hd . (IApply u v i:)
+        match r gamma k (t',hd') ps vs
+      t -> traceSDoc "rewriting.match" 20
+        ("interval application at non-pi type (possible non-confluence?) " <+> prettyTCM (pathUnview t)) mzero
 
     (Proj o f, Proj o' f') | f == f' -> do
       ~(Just (El _ (Pi a b))) <- addContext k $ getDefType f =<< reduce t

src/full/Agda/TypeChecking/Sort.hs

@@ -27,7 +27,7 @@ import Control.Monad.Except
 import Data.Functor
 import Data.Maybe
 
-import Agda.Interaction.Options (optCumulativity)
+import Agda.Interaction.Options (optCumulativity, optRewriting)
 
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -208,7 +208,9 @@ sortOf t = do
         case unEl (ignoreBlocking ba) of
           Pi b c -> sortOfE (c `absApp` v) (hd . (e:)) es
           _ | Blocked m _ <- ba -> patternViolation m
-            | otherwise         -> __IMPOSSIBLE__
+            | otherwise         -> ifM (optRewriting <$> pragmaOptions)
+                {-then-} (patternViolation neverUnblock)  -- Not IMPOSSIBLE because of possible non-confluent rewriting (see #5531)
+                {-else-} __IMPOSSIBLE__
       Proj o f -> do
         a <- reduce a
         ~(El _ (Pi b c)) <- fromMaybe __IMPOSSIBLE__ <$> getDefType f a

test/Fail/Issue5396.agda

@@ -0,0 +1,28 @@
+{-# OPTIONS --rewriting #-}
+
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Nat
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+not : Bool → Bool
+not true = false
+not false = true
+
+data Unit : Set where
+  unit : Unit
+
+postulate
+  X : Unit → Set
+  X-Nat : X unit ≡ Nat
+  X-Bool : (u : Unit) → X u ≡ Bool
+{-# REWRITE X-Nat #-}
+
+0' : (u : Unit) → X u
+0' unit = 0
+
+{-# REWRITE X-Bool #-}
+
+test : (u : Unit) → not (0' u) ≡ true
+test unit = refl

test/Fail/Issue5396.err

@@ -0,0 +1,4 @@
+Issue5396.agda:28,13-17
+not 0 != true of type Bool
+when checking that the expression refl has type
+not (0' unit) ≡ true

test/Fail/Issue5531.agda

@@ -0,0 +1,50 @@
+{-# OPTIONS --type-in-type --rewriting #-}
+
+open import Agda.Builtin.Sigma
+open import Agda.Builtin.Equality
+
+coe : {A B : Set} → A ≡ B → A → B
+coe refl x = x
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+Tel = Set
+U = Set
+
+variable
+  Δ : Tel
+  A B : Δ → U
+  δ₀ δ₁ : Δ
+
+postulate
+  IdTel : (Δ : Tel)(δ₀ δ₁ : Δ) → Tel
+  Id : (A : Δ → U){δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → A δ₀ → A δ₁ → U
+  ap : {A : Δ → U}(a : (δ : Δ) → A δ)
+       → {δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → Id A δ₂ (a δ₀) (a δ₁)
+
+  idTel-sigma : {a₀ : A δ₀}{a₁ : A δ₁}
+                → IdTel (Σ Δ A) (δ₀ , a₀) (δ₁ , a₁)
+                  ≡ Σ (IdTel Δ δ₀ δ₁) (λ δ₂ → Id A δ₂ a₀ a₁)
+  {-# REWRITE idTel-sigma #-}
+
+  id-u : {A₀ A₁ : U}{δ₂ : IdTel Δ δ₀ δ₁}
+         → Id {Δ = Δ}(λ _ → U) δ₂ A₀ A₁ ≡ (A₀ → A₁ → U)
+  {-# REWRITE id-u #-}
+
+  id-ap : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
+          → Id A δ₂ a₀ a₁ ≡ ap {A = λ _ → U} A δ₂ a₀ a₁
+
+  ap-sigma : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
+             {B : (δ : Δ) → A δ → U}
+             {b₀ : B δ₀ a₀}{b₁ : B δ₁ a₁}→
+             ap {Δ = Δ}{A = λ _ → U} (λ δ → Σ (A δ) (B δ))
+                δ₂ (a₀ , b₀) (a₁ , b₁) ≡
+                Σ (Id A δ₂ a₀ a₁) λ a₂ → Id {Δ = Σ Δ A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁
+  {-# REWRITE ap-sigma #-}
+  {-# REWRITE id-ap #-}
+
+  ap-proj₁ : {δ₂ : IdTel Δ δ₀ δ₁}
+             {B : (δ : Δ) → A δ → U}
+             {ab : (δ : Δ) → Σ (A δ) (B δ)}
+             → ap {Δ = Δ}{A = A}(λ δ → fst (ab δ)) δ₂
+               ≡ fst (ap ab δ₂)

test/Fail/Issue5531.err

@@ -0,0 +1,4 @@
+Issue5531.agda:50,23-31
+ap (λ z → Σ (_A_208 z) (B z)) _239 (ab _δ₀_236) (ab _δ₁_237) !=<
+Σ _A_232 _B_233
+when checking that the expression ap ab δ₂ has type Σ _A_232 _B_233