8000 Fix #7495: Check extra split clause patterns are trivial for exactness by szumixie · Pull Request #7496 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fix #7495: Check extra split clause patterns are trivial for exactness #7496

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
Sep 17, 2024
Merged

Fix #7495: Check extra split clause patterns are trivial for exactness #7496

merged 1 commit into from
Sep 17, 2024

Conversation

szumixie
Copy link
Member

Fixes #7495 by checking that the leftover patterns in a split clause are trivial, only then is the clause exact.

@szumixie
Copy link
Member Author

This makes termination check fail for Cubical.HITs.SmashProduct.SymmetricMonoidal.⋀lIdIso for some reason, but it can be fixed by adding a type annotation:

-      inr (false* , Bool⋀→ (inr x)) ≡ inr x
+      Path (Bool*∙ ⋀ A) (inr (false* , Bool⋀→ (inr x))) (inr x)

@andreasabel
Copy link
Member

Thanks!

This makes termination check fail for Cubical.HITs.SmashProduct.SymmetricMonoidal.⋀lIdIso for some reason, but it can be fixed by adding a type annotation:

Sounds surprising. Do you have an idea why?

In any case, the current process would be to first get the change to the cubical library merged, and then merge this PR, with updated submodule cubical.

@andreasabel andreasabel added the exact split Exact splitting label Sep 15, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 15, 2024
@szumixie
Copy link
Member Author

The reason for the failure is that the termination checker doesn't reduce with non-exact clauses.

The definition of ⋀lIdIso has a catchall clause that has less arguments:

Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A
Iso.fun ⋀lIdIso = Bool⋀→

In the helper function in a later clause, unification solves a metavariable with Iso.fun ⋀lIdIso (inr x), which used to reduce away, but not after this patch since Iso.fun ⋀lIdIso = Bool⋀→ is no longer exact.

The reduction is a bug, the following non-terminating function was accepted before this patch because the last clause was considered exact. See #5065.

open import Agda.Builtin.Bool

bad : Bool → Bool
bad true = bad true
bad = λ _ → true

@szumixie szumixie mentioned this pull request Sep 15, 2024
Merged
felixwellen pushed a commit to agda/cubical that referenced this pull request Sep 16, 2024
@szumixie
Remove redundant clause for agda/agda#7496 (#1156)
e2370fb
@andreasabel andreasabel added the type: bug Issues and pull requests about actual bugs label Sep 17, 2024
@andreasabel andreasabel self-assigned this Sep 17, 2024
andreasabel
andreasabel approved these changes Sep 17, 2024
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@andreasabel andreasabel merged commit bd5479b into agda:master Sep 17, 2024
28 checks passed
@szumixie szumixie mentioned this pull request Sep 18, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@andreasabel andreasabel

Labels
exact split Exact splitting type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.

Catchall clauses with less arguments are considered exact
2 participants
@szumixie @andreasabel
0