Rewrite rule rejected because of projection likeness #4103
Comments
andreasabel
added
type: bug
I don't see how this demonstrates any unsoundness. The rewrite rule is rejected so what's the harm? As to having a rewrite rule on |
|
Well, for instance this reports an unsolved meta unless projection likeness is disabled: {-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
infix 10 _⟼_
postulate
_⟼_ : ∀{a} {A : Set a} → A → A → Set a
{-# BUILTIN REWRITE _⟼_ #-}
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
postulate
F : (A B C : Set) → Set
F-red : ∀ {A B C} → F A B C ⟼ B × C
{-# REWRITE F-red #-}
fst : (A B C : Set) (s : F A B C) → B
fst A B C (x , y) = x
test : ∀{A B C} (p : B × C) → fst A B C p ≡ fst _ _ _ p
test p = reflAgda cannot solve the first |
|
Right. This seems like a bug (though still not a soundness bug): fst : (A B C : Set) (s : F A B C) → B
fst A B C (x , y) = x
|
|
Well, I consider an optimization "sound" if it is merely an optimization, i.e., only changes the timing behavior but not the logical behavior. The projection-likeness optimization speeds up the It seems that this optimization is not essential for running Agda. It seems to be more in the "every little helps" ball park. Given its history of causing hard-to-research bugs, we could consider switching it off by default. Timing dataWith projection-likeness optimization: With |
|
The standard library is probably not the best place to look. The big win is in examples working with heavy encodings where you can easily go from exponential to close-to-linear checking time.
It doesn't change the logical behavior. The erased arguments are there, the problem is that the rewriting machinery doesn't know where to find them. As you mention, projection-likeness existed before rewrite rules, so I find it a bit strange to blame projection-likeness here... |
If that is true (I don't per se doubt it), then it should not be hard to have a corresponding test in the testsuite that exhibits this behavior. In particular, it would execute instantaneously with projection likeness on, but run out of time with So, is there such a test? |
|
Not sure (couldn't find one in 5 min looking). A version of |
It might be easier to find/construct a test case if you pushed 0783117. |
|
OP can be fixed since the rewriting matcher is anyway type-directed, thus, can reconstruct dropped parameters. |
|
|
OK, excellent! |
|
In Agda 2.6.3, there will be a new pragma |
Posted by Michael Shulman on the Agda list:
This produces the error
but should succeed.
The problem is that the type arguments to
fstare erased sindfstis a projection-like function. With{-# OPTIONS -v tc.proj.like:10 -v rewriting:30 #-}Agda tells us
This explains why Agda complains about
Cnot being bound.Projection-likeness is an optimization heuristics. It checks if a function
fhas typewhere
Bis a name that does not reduce (and some other technical conditions). The firstnarguments tofcan be dropped as they can be reconstructed from the type of the following argument.However, this optimization was added before the advent of rewriting, and it seems to be unsound in the presence of rewriting, as this example shows, and maybe even in a more fundamental way. (What for instance happens if we have a rewrite rule for
B?)A workaround with present Agda is to make the projection-likeness analysis on
fstfail, e.g. by permuting the type arguments or adding a dummy argument. (Note that option--no-projection-likehas no effect at the time of writing this because of another bug, thus, cannot be used as a workaround right now.)The text was updated successfully, but these errors were encountered: