Skip to content

Conversation

@zeroeightysix
Copy link
Contributor

compileDomType would return DomDropped for types universally quantified in Haskell, but the erased indices check would understand that as the type being erased; which is not the case for Set indices, as I understand it. Is this the right solution?

I've also added a test for this case.

Fixes #437

@jespercockx
Copy link
Member

Hmm, it makes sense to make a more explicit distinction between an erased domain and one that is just left implicit in the Haskell code. However, I think it would make more sense to treat the latter as a DomForall rather than a DomDropped, so it would be better to add an argument to the DomForall constructor (do we want to see this forall explicitly in the generated Haskell code or not?) rather than to the DomDropped constructor.

@zeroeightysix
Copy link
Contributor Author

That does make more sense! I've redone the changes, could you look at them again?

@jespercockx
Copy link
Member

It's perfect now, thank you for the PR!

@jespercockx jespercockx merged commit bb5f086 into agda:master Nov 18, 2025
8 checks passed
@zeroeightysix zeroeightysix deleted the fix/index-not-erased branch November 18, 2025 17:42
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.

Agda2hs wrongly compiles Set-indexed datatypes

2 participants