Fix issue #6930: Allow recursion on proofs again

CHANGELOG.md

@@ -26,7 +26,10 @@ Additions to the Agda syntax.
 Language
 --------
 
-Changes of the type checker etc. that affect the Agda language.
+* A [change](https://github.com/agda/agda/pull/6639) in 2.6.4 that prevented all recursion on proofs,
+  i.e., members of a type `A : Prop ℓ`, has been [reverted](https://github.com/agda/agda/pull/6936).
+  It is possible again to use proofs as termination arguments.
+  (See [issue #6930](https://github.com/agda/agda/issues/6930).)
 
 Reflection
 ----------

src/full/Agda/Termination/TermCheck.hs

@@ -1317,7 +1317,7 @@ instance StripAllProjections Term where
         -- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
         Con c ci <$> stripAllProjections ts
       Def d es   -> Def d <$> stripAllProjections es
-      DontCare t -> DontCare <$> stripAllProjections t
+      DontCare t -> stripAllProjections t
       _ -> return t
 
 -- | Normalize outermost constructor name in a pattern.
@@ -1344,7 +1344,8 @@ compareTerm' v mp@(Masked m p) = do
     (Var i es, _) | Just{} <- allApplyElims es ->
       compareVar i mp
 
-    (DontCare t, _) -> pure Order.unknown
+    (DontCare t, _) ->
+      compareTerm' t mp
 
     -- Andreas, 2014-09-22, issue 1281:
     -- For metas, termination checking should be optimistic.

test/Fail/Issue6639.agda

@@ -0,0 +1,29 @@
+-- Andreas, 2023-10-20, issue #6639, testcase by Amy.
+-- We can't have both of these:
+-- * accept proofs as termination argument using the `c h > h args` structural ordering
+-- * impredicative prop
+
+{-# OPTIONS --prop #-}
+
+data ⊥ : Prop where
+
+-- * Either we have to reject impredicative propositions,
+-- such as this impredicative encoding of truth.
+-- True ≅ (P : Prop) → P → P
+--
+-- {-# NO_UNIVERSE_CHECK #-}
+data True : Prop where
+  c : ((P : Prop) → P → P) → True
+
+true : True
+true = c (λ P p → p)
+
+-- * Or we have to reject the following recursion on proofs in the termination checker.
+-- (Impredicativity is incompatible with the structural ordering `c h > h args`
+-- without further restrictions.)
+--
+false : True → ⊥
+false (c h) = false (h True true)
+
+absurd : ⊥
+absurd = false true

test/Fail/Issue6639.err

@@ -0,0 +1,4 @@
+Issue6639.agda:16,3-4
+Set₁ is not less or equal than Set
+when checking that the type (P : Prop) → P → P of an argument to
+the constructor c fits in the sort Set of the datatype.

test/Succeed/Issue6930.agda

@@ -0,0 +1,99 @@
+-- Andreas, 2023-10-22, issue #6930 raised with test case by Andrew Pitts.
+--
+-- Acc-induction is compatible with strict Prop.
+-- That is, if we define Acc in Prop, we can eliminate it into other propositions.
+
+{-# OPTIONS --prop #-}
+{-# OPTIONS --sized-types #-}
+
+module _ where
+
+open import Agda.Primitive
+
+-- Acc-recursion in types.
+------------------------------------------------------------------------
+
+module wf-Set {l : Level}{A : Set l}(R : A → A → Set l) where
+
+  -- Accessibility predicate
+  data Acc (x : A) : Set l where
+    acc : (∀ y → R y x → Acc y) → Acc x
+
+  -- Well-foundedness
+  iswf : Set l
+  iswf = ∀ x → Acc x
+
+  -- Well-founded induction
+  ind :
+    {n : Level}
+    (w : iswf)
+    (B : A → Set n)
+    (b : ∀ x → (∀ y → R y x → B y) → B x)
+    → -----------------------------------
+    ∀ x → B x
+  ind w B b x = Acc→B x (w x)
+    where
+    Acc→B : ∀ x → Acc x → B x
+    Acc→B x (acc α) = b x (λ y r → Acc→B  y (α y r))
+
+-- Acc-induction in Prop
+------------------------------------------------------------------------
+
+{- The following module checks with 2.6.3, but fails to check with 2.6.4
+   emitting the message:
+
+   "Termination checking failed for the following functions:
+  Problematic calls:
+   Acc→B y _"
+
+and highlighting the last occurrence of Acc→B  -}
+
+module wf-Prop {l : Level}{A : Set l}(R : A → A → Prop l) where
+
+  -- Accessibility predicate
+  data Acc (x : A) : Prop l where
+    acc : (∀ y → R y x → Acc y) → Acc x
+
+  -- Well-foundedness
+  iswf : Prop l
+  iswf = ∀ x → Acc x
+
+  -- Well-founded induction
+  ind :
+    {n : Level}
+    (_ : iswf)
+    (B : A → Prop n)
+    (b : ∀ x → (∀ y → R y x → B y) → B x)
+    → -----------------------------------
+    ∀ x → B x
+  ind w B b x = Acc→B x (w x)
+    where
+    Acc→B : ∀ x → Acc x → B x
+    Acc→B x (acc α) = b x (λ y r → Acc→B  y (α y r))
+
+-- Andreas: Justification of Acc-induction using sized types.
+------------------------------------------------------------------------
+
+module wf-Prop-Sized {l : Level}{A : Set l}(R : A → A → Prop l) where
+  open import Agda.Builtin.Size
+
+  -- Accessibility predicate
+  data Acc (i : Size) (x : A) : Prop l where
+    acc : (j : Size< i) (α : ∀ y → R y x → Acc j y) → Acc i x
+
+  -- Well-foundedness
+  iswf : Prop l
+  iswf = ∀ x → Acc ∞ x
+
+  -- Well-founded induction
+  ind :
+    {n : Level}
+    (w : iswf)
+    (B : A → Prop n)
+    (b : ∀ x → (∀ y → R y x → B y) → B x)
+    → -----------------------------------
+    ∀ x → B x
+  ind w B b x = Acc→B ∞ x (w x)
+    where
+    Acc→B : ∀ i x → Acc i x → B x
+    Acc→B i x (acc j α) = b x (λ y r → Acc→B j y (α y r))