Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Weird rewriting error #3971

Closed
KarlusMarxen opened this issue Aug 7, 2019 · 7 comments
Assignees

Comments

@KarlusMarxen
Copy link

@KarlusMarxen KarlusMarxen commented Aug 7, 2019

{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Equality

postulate
  decorate      : {a} (A : Set a)  Set a
  rewriteMe     : {a b} {A : Set a} {B : Set b}
                 decorate (A  B) ≡ (decorate A  decorate B)

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE rewriteMe #-}

results in the following error, "rewriteMe is not a legal rewrite rule, since the following variables are not bound by the left hand side: b
when checking the pragma REWRITE rewriteMe".

Replacing A → B with A × B works, as does changing B's type to Set a.

@jespercockx jespercockx self-assigned this Aug 8, 2019
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Aug 8, 2019

The problem here is quite subtle. The full version of your rewrite rule (with implicit arguments expanded) is decorate {a ⊔ b} (A → B) ≡ (decorate {a} A → decorate {b} B). But just a ⊔ b is not enough to figure out the values of a and b individually.

There is a trick in the rewriting machinery that helps in many cases, which works by annotating the function types in the left-hand side of a rewrite rule with their sorts, i.e. A → B becomes x : A : Set a → B : Set b. However, in this case the trick doesn't work because it's a non-dependent function space, and Agda cannot figure out for a given function type whether the sort of the codomain depends on its input or not (or rather, it could, but this would break the property of Agda that sorts are just annotations that can never block computation).

In this case, a workaround is to state the rewrite rule for a dependent function space (x : A) → B x instead of a non-dependent one. I'll think about whether there is some way to improve the rewriting when matching on non-dependent function types.

@KarlusMarxen

This comment has been minimized.

Copy link
Author

@KarlusMarxen KarlusMarxen commented Aug 8, 2019

Thanks, Jesper. In the real case the functions are dependent, so it's not even a workaround.
Agda's parser does not seem too fond of expressions like x : A : Set a. Given that I have never seen this syntax anywhere, I am probably doing something wrong. So could you please give a minimal working example or a reference to one?

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Aug 8, 2019

Sorry if I wasn't clear, x : A : Set a is not actually valid syntax but I was trying to describe what Agda does internally when checking the rewrite rule.

Could you give the full example (with the dependent function space) where it goes wrong? Then I can try to see what you can do to fix it.

@KarlusMarxen

This comment has been minimized.

Copy link
Author

@KarlusMarxen KarlusMarxen commented Aug 8, 2019

Let's modify the initial example. If I understood you correctly the following should work.

{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Equality

postulate
  decorate      : {a} (A : Set a)  Set a
  rewriteMe     : {a b} {A : Set a} {B : A  Set b}
                 decorate ((x : A)  B x) ≡ (decorate A   x  decorate (B x))

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE rewriteMe #-}

But it fails with the same error. So what should I do to make it work?

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Aug 8, 2019

Oh, I see now, the problem is still there for the dependent function space because the sort of the codomain is still not dependent on the argument. So it seems the current approach of treating sorts as 'irrelevant' for matching is problematic.

Actually, thinking about it made me realize that it is not necessary to consider sorts as irrelevant: since the sort of a type can be computed from that type*, the sort of a pattern will always match whenever the type does. I'll see if I can simply remove the irrelevance bit on the sorts and see if that fixes your problem.

(*) This property would be broken if we ever add cumulativity, but in that case we should anyway rethink the whole interaction between sorts and rewriting, so it's not really a problem.

@KarlusMarxen

This comment has been minimized.

Copy link
Author

@KarlusMarxen KarlusMarxen commented Aug 8, 2019

Great! And since you mentioned it, I don't think there exists a single Agda programmer who wouldn't appreciate universe cumulativity. Has anything changed since your blog post?

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Aug 8, 2019

Currently blocked on #3099, I'm working on it from time to time but finding the source of the bugs uncovered by --double-check is very hard work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.