Turning off some sProp checks

Question

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination:

(1) Every non-forced argument must be in sProp.
(2) The return types of constructors must be pairwise orthogonal.
(3) Every recursive call must satisfy a syntactic guard condition

I have the following data definition in Agda (I have T, < defined elsewhere, but given as postulates here for a MWE):

{-# OPTIONS --prop #-}

postulate
  T : Set
  _<_ : T → T → Set

data Acc (x : T) : Prop where
  acc : (∀ y → y < x → Acc y) → Acc x

Now I'd like to throw caution to the wind and eliminate Acc to something in Set at the expense of, as I understand it, possible nonterminating type checking. Evidently right now that's not possible since Acc violates (3) (and this is explicitly stated as an example in the paper), yielding the type checking error:

Cannot split on datatype in Prop unless target is in Prop
when checking that the pattern acc p has type Acc x

Is there some way of only turning (3) off? Perhaps with something like {- NON_TERMINATING -}... somewhere? I'm confident I won't actually run into nontermination issues (I've previously proven the wellfoundedness of <, for one), and I'd like to type check the rest of my proofs without disregarding safety entirely.

EDIT: I'd be interested to know if it'd be possible to do the same in Coq as well, which currently gives me this error:

Fixpoints on proof irrelevant inductive types should produce proof irrelevant values.

Answer 1

AFAIK there is no way to turn it off. It is also worth pointing out that the cost is greater than you expected.

data A : Prop where
  a b : A

It is possible to prove eq : (B : Set)(f : A → B) → f a ≡ f b with refl. So if you were allowed to turn off the check, it does not leads to non-terminating type checking. Rather, it produces impossible cases and breaks subject reduction (i.e. if a term is well-typed, then after you perform evaluation of the term, it always remains well-typed).

In particular, in your case it immediately leads to a contradiction. You have a proof of False that is well-typed (of type Empty). But when you normalize it, the resulting term is no longer well-typed.

There are a few ways to solve this:

• Use Set. Why did you use Prop in the first place?
• Use Prop also for your target type. Why does it have to be in Set?
• Postulate an elimination function using the postulate keyword. You should probably not expect any sort of computation, because that always breaks subject reduction.

Answer 2

In Coq, you can probably hack your way around by unsetting the guard condition and writing a fixpoint that is "semantically" guarded but not syntactically so. Something along the lines of what is below.

Inductive sAcc (A : Type) (R : A -> A -> Prop) (x : A) : SProp :=
| sAcc_intro : (forall y : A, R y x -> sAcc A R y) -> sAcc A R x.

#[bypass_check(guard)]
Definition sAcc_rect (A : Type) (R : A -> A -> Prop) (P : A -> Type)
  (f : forall x : A, (forall y : A, R y x -> sAcc A R y) -> (forall y : A, R y x -> P y) -> P x) :
  forall (x : A) (a : sAcc A R x), P x :=

  (fix F (u : unit) (x : A) (a : sAcc A R x) {struct u} : P x :=
    f x (match a with sAcc_intro _ _ _ a => a end)
      (fun y r => F tt y (match a with sAcc_intro _ _ _ k => k y r end))
  ) tt.

You have to be careful though, because this will explode as soon as you try to perform a weak head on this. So you'll have to work around unification and kernel type-checking by making some conversions explicit. Alternatively, you may try to guard the fixpoint by some dummy argument, e.g. by keeping the unit argument abstract.