Rewrite rule on constructor uses wrong type for matching

[jespercockx]

The rewriting machinery does not correctly instantiate the parameters of a constructor when applying a rewrite rule. Here's an example where things go wrong:

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

record R : Set where
  constructor mkR
  field
    f : Nat

data Box : Set → Set₁ where
  box : (A : Set) → Box A

data D (A : Set) : Set₁ where
  c : Box A → R → D A

postulate
  r   : R
  dr  : ∀ {A} → D A
  rew : ∀ {A} {x} → c {A} (box A) (mkR x) ≡ dr
{-# REWRITE rew #-}

test : c {Bool} (box Bool) r ≡ dr
test = refl

This throws an error:

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:281:17-77: Non-exhaustive patterns in Just (_,
                                                                    ct)

[jespercockx]

See also #3211 and #3538

[jespercockx]

The partial fix of #3211 in 1b6ba6d by @andreasabel is not quite right: it uses typeOfConst to instantiate the parameters in the type of the constructor, which works as long as you are in the same module as where the constructor was declared (as in the test case for #3211), but does not do anything once the parameters go out of scope. To get the real type of the constructor we want to rewrite, we need access to the type of the thing we are rewriting, which we do not have access to.

[jespercockx]

Here is a particularly nasty variant:

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Box : Set → Set₁ where
  box : (A : Set) → Box A

data D (A : Set) : Set₁ where
  c : A → Box A → D A

postulate
  any : {A : Set} → A
  one : {A : Set} → D A
  rew : ∀ A → c any (box A) ≡ one
{-# REWRITE rew #-}

test : c tt (box ⊤) ≡ one
test = refl

This doesn't crash Agda, but the rewrite rule fails to fire:

c tt (box ⊤) != one of type D ⊤
when checking that the expression refl has type c tt (box ⊤) ≡ one

When looking at the debug output, it is clear what goes wrong:

attempting to rewrite term  c tt (box ⊤)
 having head  c  of type  {A : Set} → A → Box A → D A
 with rule  rew (A : Set)  |- 
            (c (any A) (box A))  -->  one  :  D A
matching pattern  (any A)
  with term       tt
  of type         Set
mismatch between (any A)  and  tt  of type  Set 

The type of the constructor c is not instantiated, so Agda matches the arguments [tt, (box ⊤)] against the patterns [any A, box A] as eliminations of c : {A : Set} → A → Box A → D A. Clearly then matching fails because tt and any A are not even of type Set.

The reason why I call this example particularly nasty is that the only way to determine the value of the parameter here is by matching the second argument of the constructor. This smells very much like a general solution would require an approach where matching problems can be solved in any order, much like we do for the LHS unifier (with higher-order matching as a fun side-dish).

[jespercockx]

My vote for solving this is by getting rid of the feature "rewrite rules on constructors of parametrized datatypes" (and hence also "rewrite rules on constructors coming from a parametrized module"). If you really want rewrite rules on constructors, you should use indices instead so they are not erased until after typechecking.

One exception we could perhaps make is to allow rewrite rules on constructors that do not make any use of the parameters in their type. This would enable the reduced example of #3538.

@andreasabel You are the only known user of rewrite rules on constructors. Would this be sufficient for your use cases?

[andreasabel]

Well, rewriting on constructors violates the invariant that constructor parameters are not needed for computation and thus need not be stored. Keeping the constructor parameters just for the sake of rewriting is likely forbiddingly expensive.

My hope with rewrite rules on constructors was to get definitional quotients in some special cases in a cheap way.

c tt (box ⊤) != one of type D ⊤

It is probably ok that the rewrite rule c any (box A) ≡ one fails here since it does not really match unless we consider eta for the unit type in this particular instance A = Top. I would have intuitively expected that any behaves like a constructor to be matched on.

One exception we could perhaps make is to allow rewrite rules on constructors that do not make any use of the parameters in their type. This would enable the reduced example of #3538.

But in this example, the module parameter Form is also used when defining Cxt, and Cxt is a parameter to the type whose constructors get rewritten.

[jespercockx]

But in this example, the module parameter Form is also used when defining Cxt, and Cxt is a parameter to the type whose constructors get rewritten.

Right, I missed that. So then my brutal solution is not sufficient after all.

It is probably ok that the rewrite rule c any (box A) ≡ one fails here since it does not really match unless we consider eta for the unit type in this particular instance A = Top. I would have intuitively expected that any behaves like a constructor to be matched on.

The problem is that this would lose stability of reduction under eta-conversion: c any (box ⊤) and c tt (box ⊤) are definitionally equal, but only the former would reduce to one.

Currently the matching algorithm used for rewriting is type-directed and it uses the type of the specific term that's being matched. Perhaps it would be possible to instead use the (less informative) type of the pattern, which we can make available during reduction. But this would still not solve the problem with stability under eta-conversion above.

To solve that problem, a solution would perhaps be to require that the type of each "properly matching" subpattern of a rewrite rule should be a rigid type that cannot compute further when it is instantiated. For example, in your example the rule lift-id≤ would be accepted since it matches on id≤ whose type has the rigid head symbol _≤_. However my example ∀ A → c any (box A) ≡ one would be rejected since the type of any is A which can become any type when A is instantiated.

This restriction would be similar to the restriction from normal pattern matching that the type of each constructor pattern is a datatype which does not compute further. With this restriction, it would be safe to use the type of the pattern instead of the type of the term under match. I will try to see if I can make this work, and how restrictive it is in practice.

[jespercockx]

I fixed the problem in the OP by inserting dummy terms in case there are missing module parameters. However, this means rewriting is currently still not stable under eta-conversion, I will need some more time to implement the proper checks to rule out my second example.

[jespercockx]

Here is another example that violates the rule I came up with two messages ago and causes weird behaviour as a result (from https://agda.zulipchat.com/#narrow/stream/238741-general/topic/rewriting.20eta-contraction.20for.20a.20datatype/near/289788505):

{-# OPTIONS --rewriting -v rewriting:70 #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data _⇨_ (A B : Set) : Set where
  Λ : (A → B) → (A ⇨ B)

_∙_ : {A B : Set} (f : A ⇨ B) (a : A) → B
(Λ f) ∙ a = f a

_∘_ : {A B C : Set} (g : B ⇨ C) (f : A ⇨ B) → (A ⇨ C)
_∘_ {A} {B} {C} g f = Λ {A} {C} (λ x → g ∙ (f ∙ x))

postulate
  Λη : {A B : Set} (f : A ⇨ B) → (Λ (λ x → f ∙ x)) ≡ f

{-# REWRITE Λη #-}

oops : {A B : Set} (f : ⊤ ⇨ B) → Set
oops {A} {B} f = {! _∘_ {A} {⊤} {B} f (Λ (λ _ → tt)) !}

The term in the hole has type A ⇨ B, but normalizes to f, whose type ⊤ ⇨ B is not convertible with A ⇨ B.

[jespercockx]

I tried to implement the solution I suggested two posts ago, but this turns out to be a rather annoying and gnarly property to analyze. However, then I realized that the core problem here is actually that the pattern variable that is bound in the parameter position is also bound somewhere else in the pattern, i.e. it occurs non-linearly. This turns out to be easy to prevent and rules out all the bad examples while keeping the good ones. Phew!

[andreasabel]

(This fix was indeed not released with 2.6.2.2.)