Rewrite rules with non-linear patterns do not work in presence of Prop

[jespercockx]

Reported by Simon Boulier:

{-# OPTIONS --prop --rewriting #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  refl : x ≐ x

postulate
  subst : ∀ {ℓ ℓ′} {A : Set ℓ} (P : A → Set ℓ′)
        → (x y : A) → x ≐ y → P x → P y
  subst-rew : ∀ {ℓ ℓ′} {A : Set ℓ} (P : A → Set ℓ′)
            → {x : A} (e : x ≐ x) (p : P x) → subst P x x e p ≡ p
{-# REWRITE subst-rew #-}

data Box (A : Prop) : Set where
  box : A -> Box A

foo : (A : Prop)(x y : A)(P : Box A → Set)(p : P (box x)) → subst P (box x) (box y) refl p ≐ p
foo A x y P p = refl -- refl does not type check

The problem is that the rewriting implementation uses untyped equality for checking the non-linear parts of patterns, which doesn't do the right thing in the presence of Prop's.

[jespercockx]

I'm working on a fix, but it won't be ready for 2.6.0 since it required a lot of refactoring of the conversion checker.

[jespercockx]

I finished my fix and pushed it to my fork of Agda (https://github.com/jespercockx/agda/tree/MonadConversion). However, the fix depends on #3589 which still needs some work, so the fix will have to wait a bit before it gets into master.

[SimonBoulier]

Wow, great!
I will test it when I have a bit of time.

[SimonBoulier]

It works well, thank you :-)