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.

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

Check consistency of instances for unboxed records #269

Open
flupe opened this issue Jan 20, 2024 · 1 comment
Open

Check consistency of instances for unboxed records #269

flupe opened this issue Jan 20, 2024 · 1 comment
Labels
enhancement New feature or request error-reporting help wanted Extra attention is needed
Milestone
1.4

Comments

@flupe
Copy link
Contributor

flupe commented Jan 20, 2024 •
edited
Loading

When defining an unboxed record, one gets to define new instances for type classes on the Agda side. Those instances never get compiled, and code that uses instances over boxed values will compile to code that uses underlying instances over the underlying values.

Hence, when defining an instance for a unboxed record, we:

  • need to make sure an instance for the underlying (boxed) type exists.
  • the behavior of the instance for the unboxed record is "consistent" with the one for the underlying type.
@flupe flupe added enhancement New feature or request help wanted Extra attention is needed error-reporting labels Jan 20, 2024
@jespercockx jespercockx added this to the 1.3 milestone Feb 9, 2024
@jespercockx jespercockx modified the milestones: 1.3, 1.4 Mar 22, 2024
@flupe
Copy link
Contributor Author

flupe commented Oct 10, 2024

Related PR: #332

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request error-reporting help wanted Extra attention is needed
Projects
None yet
Milestone
1.4
Development

No branches or pull requests
2 participants
@jespercockx @flupe