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

Rewriting doesn’t respect eta #3335

Closed
guillaumebrunerie opened this issue Oct 28, 2018 · 7 comments

Comments

@guillaumebrunerie
Copy link
Contributor

@guillaumebrunerie guillaumebrunerie commented Oct 28, 2018

It seems like rewriting doesn’t respect eta.
The last line of the code below should type check, but it gives an error instead.

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

record Box (P : Set) : Set where
  constructor box
  field
    unbox : P
open Box public

postulate
  A : Set
  a : A
  f : Box A  A
  f= : f (box a) ≡ a
{-# REWRITE f= #-}
  
[a] : Box A
unbox [a] = a

-- Works thanks to eta
test1 : [a] ≡ box a
test1 = refl

-- Should work as well
test2 : f [a] ≡ f (box a)
test2 = refl

Error:

f [a] != a of type A
when checking that the expression refl has type f [a] ≡ f (box a)
@favonia

This comment has been minimized.

Copy link
Contributor

@favonia favonia commented Oct 28, 2018

Could be related: #2979.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 28, 2018

Hmm, this is a much more interesting bug than I expected since it isn't using Prop at all. I recently tried to make the rewriting more type-directed but it seems it's doing something wrong when it tries to match a defined symbol f us against a constructor pattern of an eta-record type. What it should do is eta-expand the value f us, but that's not happening somehow. Working on it...

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 28, 2018

It turned out it was eta-expanding f us, but it was also eta-expanding the record constructor pattern by applying projections to it, which is wrong since patterns don't compute. Taking the fields directly from the record constructor pattern fixes the problem.

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Oct 28, 2018

Whitespace violation detected in test/Succeed/Issue3335.agda.

@andreasabel andreasabel reopened this Oct 28, 2018
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 28, 2018

Oh no, I'm working on my home computer but it seems I didn't set up my environment fully.

@asr

This comment has been minimized.

Copy link
Member

@asr asr commented Oct 28, 2018

The example in the OP type-checks on 2.5.4.1.

@andreasabel

This comment has been minimized.

Copy link
Contributor

@andreasabel andreasabel commented Nov 1, 2018

@asr wrote:

The example in the OP type-checks on 2.5.4.1.

Consequently, it is not a regression released in 2.5.4.1.

@andreasabel andreasabel added this to the 2.6.0 milestone Nov 1, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.