Pattern-matching on records in Prop allows eliminating into Set

[ionathanch]

Defining the accessibility predicate as an inductive record in Prop with pattern matching allows me to eliminate it to things in Set:
(I've specialized to order on naturals for convenience)

{-# OPTIONS --prop --safe #-}

open import Agda.Builtin.Equality
open import Data.Nat.Base

{-
data Acc (a : ℕ) : Prop where
  acc : (∀ {b} → b < a → Acc b) → Acc a
-}

record Acc (a : ℕ) : Prop where
  inductive
  pattern
  constructor acc
  field acc< : (∀ b → b < a → Acc b)

open Acc

AccRect : ∀ {P : ℕ → Set} → (∀ a → (∀ b → b < a → Acc b) → (∀ b → b < a → P b) → P a) → ∀ a → Acc a → P a
AccRect f a (acc p) = f a p (λ b b<a → AccRect f b (p b b<a))

AccRectProp : ∀ {P : ℕ → Prop} → (∀ a → (∀ b → b < a → Acc b) → (∀ b → b < a → P b) → P a) → ∀ a → Acc a → P a
AccRectProp f a (acc p) = f a p (λ b b<a → AccRectProp f b (p b b<a))

AccInv : ∀ a → Acc a → ∀ b → b < a → Acc b
AccInv = AccRectProp (λ _ p _ → p)

example : ∀ {P : ℕ → Set} → (f : ∀ a → (∀ b → b < a → P b) → P a) → ∀ a → (access : Acc a) →
  AccRect {P} (λ a _ r → f a r) a access ≡ f a (λ b b<a → AccRect {P} (λ a _ r → f a r) b (AccInv a access b b<a))
example f a access = ?

Replacing the record definition with the data definition yields the usual "Cannot split on datatype in Prop unless target is in Prop" error for AccRect.
The example is from §2.3 of the Definitional Proof-Irrelevance paper, which seems to suggest this shouldn't be allowed to avoid nonterminating type checking, although I haven't been able to reproduce that yet (presumably I need to abstract the order and introduce a premise stating its reflexivity).

[Agda 2.6.2]

[jespercockx]

Yes indeed, induction on Prop-valued arguments should not count as structurally recursive in the termination checker. Thanks for reporting!

[jespercockx]

Actually I was a bit too quick adding the false flag. This does not break consistency, only strong normalization.

[jespercockx]

I fixed this by limiting splitting on inductive record types in Prop for now. In theory another way to fix this would be to allow splitting but restrict termination checking by "masking" arguments in a Prop (similarly to how we mask non-data arguments when --without-K is enabled). But this requires us to have the (normalized) sort of each argument type during termination checking and I'm not sure if we do.