8000 Fixed #6999 by nad · Pull Request #7000 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fixed #6999 #7000

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Nov 18, 2023
Merged

Fixed #6999 #7000

merged 1 commit into from
Nov 18, 2023

Conversation

nad
Copy link
Contributor
@nad nad commented Nov 18, 2023

See issue #6999.

@nad nad added this to the 2.6.5 milestone Nov 18, 2023
@nad nad self-assigned this Nov 18, 2023
@nad nad linked an issue Nov 18, 2023 that may be closed by this pull request
Unification failure for function type with erased argument #6999
Closed
@jespercockx
Copy link
Member

Congratulations for getting ticket number #7000, you win a prize! (To be claimed next time we meet in person.) Now let me take a look at the contents of this PR.

@jespercockx
Copy link
Member

I agree that there is definitely something wrong in the occurs checker here, but I don't think this fix is the right one. De modality in the Dom of a pi type determines how arguments to functions of that type can be used, but why should that have anything to do with how variables are used inside the type of that domain? Looking at the debug output (with -vtc.conv:50 and -vtc.meta:50):

compareTerm _P_2 A =< @0 A → Set
compareTerm (not syntactically equal) _P_2 A =< @0 A → Set
attempting shortcut _P_2 A := @0 A → Set
term _P_2 A :=< @0 A → Set
v =  @0 A → Set
v =  @0 A → Set
MetaVars.assign: assigning meta  _P_2  with args  A  to  @0 A → Set
MetaVars.assign: type of meta:  @0 Set → Set₁
Instantiating sort Set₁ to sort Set₁ of solution @0 A → Set
equalSort Set₁ == Set₁
equalLevel (lsuc lzero) (lsuc lzero)
equalLevel
  Agda.Primitive.lsuc Agda.Primitive.lzero ==
  Agda.Primitive.lsuc Agda.Primitive.lzero
is _2@17827391150739521290 a blocked term? 
  no
MetaVars.assign: I want to see whether rhs is blocked
r.h.s. not blocked
v =  @0 A → Set
v =  @0 A → Set
context before projection expansion
  (A : Set)
meta args:  [A]
norm args:  [A]
no projected var found in args:  [A]
context after projection expansion
  (A : Set)
mvar args: 0
fvars lhs (rel): 0
fvars lhs (nonstrict):
fvars lhs (irr):
initOccursCheck: we look into the following definitions:
fails
occursCheck _2@17827391150739521290 (StronglyRigid) of  @0 A → Set
occursCheck _2@17827391150739521290 (StronglyRigid) of  A
offending variable:  A
  of type  Set
  (after singleton test)

The argument A to the meta _P_2 has the default non-erased modality, so I don't understand why it is considered to be an offending variable in the first place.

@nad
Copy link
Contributor Author
nad commented Nov 18, 2023

I agree that there is definitely something wrong in the occurs checker here, but I don't think this fix is the right one. De modality in the Dom of a pi type determines how arguments to functions of that type can be used, but why should that have anything to do with how variables are used inside the type of that domain?

The system has intentionally been set up in that way:

{-# OPTIONS --erasure #-}

Accepted : Se
8000
t₁
Accepted = (@0 A : Set) → @0 A → Set

Rejected : Set₁
Rejected = (@0 A : Set) → A → Set

@jespercockx
Copy link
Member

Ok, I'm still confused about why that is the case (and I apologize for being continually confused with how erasure works for pi types) but given that that's the typing rule I agree that this is the right change to make.

@nad nad merged commit 4460544 into master Nov 18, 2023
@nad nad deleted the issue6999 branch November 18, 2023 10:52
@andreasabel
Copy link
Member

The system has intentionally been set up in that way:

{-# OPTIONS --erasure #-}

Accepted : Set₁
Accepted = (@0 A : Set) → @0 A → Set

Rejected : Set₁
Rejected = (@0 A : Set) → A → Set

I am also confused. I thought Rejected should be rejected only if we have type-case features on like --cubical or some variant thereof. Why is it rejected also in --with-Kmode?

@nad
Copy link
Contributor Author
nad commented Nov 20, 2023

I am also confused. I thought Rejected should be rejected only if we have type-case features on like --cubical or some variant thereof. Why is it rejected also in --with-Kmode?

It would perhaps be fine to allow Rejected when --with-K is active: the theory of our paper allows the type-level grade to be ω even if the term-level grade is 0. I have not had a need for this feature, so I have not implemented it.

@andreasabel andreasabel modified the milestones: 2.7.0, 2.6.4.2 Feb 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jespercockx jespercockx jespercockx approved these changes

@andreasabel andreasabel Awaiting requested review from andreasabel

Assignees

@nad nad

Labels
erasure
Projects
None yet
Milestone
2.6.4.2
Development

Successfully merging this pull request may close these issues.

Unification failure for function type with erased argument
3 participants
@nad @jespercockx @andreasabel
0