Rewrite rule rejected because of projection likeness

[andreasabel]

Posted by Michael Shulman on the Agda list:

{-# OPTIONS --rewriting #-}

infix 10 _⟼_
postulate
  _⟼_ : {A : Set} → A → A → Set
{-# BUILTIN REWRITE _⟼_ #-}

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B
fst : (A B : Set) (s : A × B) → A
fst A B (x , y) = x

postulate
  foo : {A : Set} (B : A → Set) → Set
  foo0 : {A : Set} (B C : A → Set) → foo B
  bar : {A : Set} (B : A → Set) (f : (x : A) → B x) → foo B
  bar-fst : (A : Set) (B C : A → Set) (u : (x : A) → B x × C x)
    → bar B (λ (x : A) → fst (B x) (C x) (u x)) ⟼  foo0 B C
{-# REWRITE bar-fst #-}

This produces the error

bar-fst  is not a legal rewrite rule, since the following variables
are not bound by the left hand side:  C
when checking the pragma REWRITE bar-fst

but should succeed.

The problem is that the type arguments to fst are erased sind fst is a projection-like function. With

{-# OPTIONS -v tc.proj.like:10 -v rewriting:30 #-}

Agda tells us

...
fst  :  (A B : Set) → A × B → A
 is projection like in argument 2 for type ...
...
attempting to add rewrite rule of type 
(A : Set) (B : A → Set) (C : A → Set) (u : (x : A) → B x × C x)
 |-  bar B (λ x → fst _ _ (u x)) ⟼ foo0 B C
Pattern generated from lhs:  (bar A (λ _ → B _) (λ x → (fst u x)))

This explains why Agda complains about C not being bound.

Projection-likeness is an optimization heuristics. It checks if a function f has type

(x1 : An) ... (xn : An) -> B x1 ... xn -> C

where B is a name that does not reduce (and some other technical conditions). The first n arguments to f can 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 fst fail, e.g. by permuting the type arguments or adding a dummy argument. (Note that option --no-projection-like has no effect at the time of writing this because of another bug, thus, cannot be used as a workaround right now.)

[UlfNorell]

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?)

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 B, is that something you can do without breaking everything?

[andreasabel]

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 = refl

Agda cannot solve the first _ to A because it has optimized away the first argument of fst.

[UlfNorell]

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

fst shouldn't be projection-like since the reduced type of the principal argument doesn't mention A.

[andreasabel]

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 library-testby around 3-4%, from around 620sec to around 600sec on my machine. The speed-up seems to be in the garbage collector (fewer runs), but what is puzzling me is that the optimization does not seem to have an effect on the total allocated memory (0.396 TB in both cases). ??

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 data

With projection-likeness optimization:

 Checking EverythingSafe (/Users/abel/agda-erasure/std-lib/EverythingSafe.agda).
Total                        578,504ms            
Miscellaneous                 10,862ms            
Typing                        68,685ms (281,506ms)
Typing.CheckRHS               95,387ms            
Typing.TypeSig                40,985ms            
Typing.Generalize             31,162ms            
Typing.CheckLHS               14,007ms  (29,831ms)
Typing.CheckLHS.UnifyIndices  15,824ms            
Typing.OccursCheck             9,193ms            
Typing.With                    6,259ms            
Serialization                120,052ms (183,286ms)
Serialization.BinaryEncode    51,036ms            
Serialization.BuildInterface   7,370ms            
Serialization.Compress         3,166ms            
Serialization.Sort             1,659ms            
Parsing                        6,029ms  (26,513ms)
Parsing.OperatorsExpr         16,536ms            
Parsing.OperatorsPattern       3,947ms            
Highlighting                  21,437ms            
Positivity                    15,356ms            
Scoping                        7,842ms  (10,975ms)
Scoping.InverseScopeLookup     3,132ms            
DeadCode                       9,781ms            
Coverage                       8,681ms            
Termination                    1,973ms   (4,192ms)
Termination.Compare            1,100ms            
Termination.RecCheck             917ms            
Termination.Graph                200ms            
Import                         3,762ms            
Injectivity                    1,464ms            
Deserialization                  497ms            
ProjectionLikeness               186ms            

 396,351,663,432 bytes allocated in the heap
  55,083,201,056 bytes copied during GC
   1,362,480,664 bytes maximum residency (78 sample(s))
       7,284,176 bytes maximum slop
            1568 MB total memory in use (1 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     171675 colls,     0 par   84.301s  87.762s     0.0005s    0.1944s
  Gen  1        78 colls,     0 par   198.826s  204.732s     2.6248s    5.6443s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.000s  (  0.002s elapsed)
  MUT     time  285.222s  (303.716s elapsed)
  GC      time  283.127s  (292.494s elapsed)
  EXIT    time    0.000s  (  0.007s elapsed)
  Total   time  568.350s  (596.218s elapsed)

  Alloc rate    1,389,623,421 bytes per MUT second

  Productivity  50.2% of total user, 50.9% of total elapsed

With --no-projection-like:

 Checking EverythingSafe (/Users/abel/agda-erasure/std-lib/EverythingSafe.agda).
Total                        601,308ms            
Miscellaneous                 11,003ms            
Typing                        64,840ms (280,140ms)
Typing.CheckRHS              103,380ms            
Typing.TypeSig                54,356ms            
Typing.CheckLHS               17,012ms  (27,037ms)
Typing.CheckLHS.UnifyIndices  10,024ms            
Typing.Generalize             14,912ms            
Typing.OccursCheck             9,568ms            
Typing.With                    6,045ms            
Serialization                100,991ms (183,742ms)
Serialization.BinaryEncode    60,058ms            
Serialization.BuildInterface  13,392ms            
Serialization.Sort             6,218ms            
Serialization.Compress         3,081ms            
Parsing                        3,768ms  (23,594ms)
Parsing.OperatorsExpr         16,048ms            
Parsing.OperatorsPattern       3,776ms            
Highlighting                  21,216ms            
Scoping                       11,795ms  (20,597ms)
Scoping.InverseScopeLookup     8,801ms            
Positivity                    18,979ms            
DeadCode                      12,531ms            
Coverage                      12,284ms            
Termination                    1,838ms   (7,526ms)
Termination.Graph              3,754ms            
Termination.Compare            1,014ms            
Termination.RecCheck             919ms            
Injectivity                    5,617ms            
Import                         3,553ms            
Deserialization                  479ms            
ProjectionLikeness                31ms            
ModuleName                        10ms            

 396,627,934,680 bytes allocated in the heap
  54,637,449,616 bytes copied during GC
   1,442,408,160 bytes maximum residency (82 sample(s))
       5,929,248 bytes maximum slop
            1568 MB total memory in use (1 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     168711 colls,     0 par   85.338s  88.915s     0.0005s    0.1417s
  Gen  1        82 colls,     0 par   229.129s  236.050s     2.8787s    8.4033s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.000s  (  0.002s elapsed)
  MUT     time  276.608s  (292.777s elapsed)
  GC      time  314.468s  (324.965s elapsed)
  EXIT    time    0.000s  (  0.006s elapsed)
  Total   time  591.076s  (617.750s elapsed)

  Alloc rate    1,433,901,234 bytes per MUT second

  Productivity  46.8% of total user, 47.4% of total elapsed

[UlfNorell]

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.

Well, I consider an optimization "sound" if it is merely an optimization, i.e., only changes the timing behavior but not the logical behavior.

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...

[andreasabel]

The big win is in examples working with heavy encodings where you can easily go from exponential to close-to-linear checking time.

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 --no-projection-likeness. Such a test would secure projection-likeness as a feature against accidential breakage by refactorings etc.

So, is there such a test?

[UlfNorell]

Not sure (couldn't find one in 5 min looking). A version of benchmark/categories/Language.agda with a datatype for Σ should do it I believe.

[nad]

(Note that option --no-projection-like has no effect at the time of writing this because of another bug, thus, cannot be used as a workaround right now.)

It might be easier to find/construct a test case if you pushed 0783117.

[andreasabel]

OP can be fixed since the rewriting matcher is anyway type-directed, thus, can reconstruct dropped parameters.

[nad]

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 --no-projection-likeness.

$ cd benchmark/proj
[…]/benchmark/proj
$ time agda --ignore-interfaces Data.agda
Checking Data ([…]/benchmark/proj/Data.agda).

real    0m0,315s
user    0m0,203s
sys     0m0,055s
$ time agda --ignore-interfaces --no-projection-like Data.agda
Checking Data ([…]/benchmark/proj/Data.agda).
agda: out of memory (requested 1048576 bytes)

real    0m59,700s
user    0m57,663s
sys     0m1,937s

[andreasabel]

OK, excellent!

[andreasabel]

In Agda 2.6.3, there will be a new pragma {-# NO_PROJECTION_LIKE #-} to disable projection-likeness for individual functions.