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

Irrelevance annotations discarded #2301

Closed
stedolan opened this Issue Nov 11, 2016 · 2 comments

Comments

Projects
None yet
3 participants
@stedolan

stedolan commented Nov 11, 2016

Agda (both stable-2.5 and current master) typechecks the following:

data Box (A : Set) : Set where
  wrap : A  Box A

weird :  {A}  .A  Box A
weird = wrap

Since the first argument to wrap is not actually irrelevant, this lets us write a function that discards irrelevance annotations:

make-relevant :  {A}  .A  A
make-relevant a = unwrap (weird a)
  where
    unwrap :  {A}  Box A  A
    unwrap (wrap a) = a

or proves things we shouldn't:

open import Agda.Builtin.Equality

data Bool : Set where
  tt ff : Bool

absurd : {X : Set}  X
absurd {X} = different same
  where
    different : weird tt ≡ weird ff  X
    different ()
    
    irr-eq :  {A B : Set} {x y : A} (f : .A  B)  f x ≡ f y
    irr-eq f = refl
    
    same : weird tt ≡ weird ff
    same = irr-eq weird

(This is a simplified version of some strangeness that came up during a talk at SPLS, when an audience member pointed out that a function didn't use a vital parameter and yet still typechecked)

@fredrikNordvallForsberg

This comment has been minimized.

Show comment
Hide comment
@fredrikNordvallForsberg

fredrikNordvallForsberg Nov 11, 2016

Member

Hello from the audience member: this only seems to work because wrap is a constructor; the following is not allowed, as expected:

data Box (A : Set) : Set where
  wrap : A  Box A

wrap' :  {A}  A  Box A
wrap' = wrap

weird :  {A}  .A  Box A
weird = wrap'

Similarly weird x = wrap x is not accepted.

Member

fredrikNordvallForsberg commented Nov 11, 2016

Hello from the audience member: this only seems to work because wrap is a constructor; the following is not allowed, as expected:

data Box (A : Set) : Set where
  wrap : A  Box A

wrap' :  {A}  A  Box A
wrap' = wrap

weird :  {A}  .A  Box A
weird = wrap'

Similarly weird x = wrap x is not accepted.

@andreasabel andreasabel added this to the 2.5.2 milestone Nov 11, 2016

@andreasabel andreasabel self-assigned this Nov 11, 2016

@andreasabel

This comment has been minimized.

Show comment
Hide comment
@andreasabel

andreasabel Nov 11, 2016

Contributor

This bug goes back to at least 2.3.2.
compareTel does not take Relevance into account properly (and never did, I think).

Contributor

andreasabel commented Nov 11, 2016

This bug goes back to at least 2.3.2.
compareTel does not take Relevance into account properly (and never did, I think).

@andreasabel andreasabel added the false label Jan 2, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment