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

Closes #309: Ensures we compile pattern variables correctly #329

Merged
merged 1 commit into from
Jun 10, 2024

Conversation

VictorCMiraldo
Copy link
Contributor

The old compileTypeArgs in this module was failing to update the context on recursive calls, causing the De Bruijn indices to get messed up. This PR relies on the existing compileTypeArgs instead. Closes #309

@jespercockx jespercockx self-requested a review June 9, 2024 09:52
@jespercockx
Copy link
Member

jespercockx commented Jun 9, 2024

The test suite fails on the following:

== Comparing output ==
Only in golden: Issue309.hs

Since our test infrastructure is pretty basic (see #153), you need to explicitly add import Issue309 (in two places!) to AllTests.agda.

@VictorCMiraldo
Copy link
Contributor Author

@jespercockx I just added it to the AllTests.agda. How can I run these tests locally to ensure it works?

@jespercockx
Copy link
Member

You can run make test, and if it complains about any changes to the golden files you can run make golden afterwards to update the golden files.

@VictorCMiraldo
Copy link
Contributor Author

Cool! I think I finally got it! 🤞

@jespercockx jespercockx merged commit fdbebb6 into agda:master Jun 10, 2024
7 checks passed
@jespercockx
Copy link
Member

Perfect, thanks for the PR!

@jespercockx jespercockx added this to the 1.3 milestone Sep 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Incorrect compilation of type synonyms
2 participants