Refine the fix of #142
Maintainers usually reply within 1 day
@jespercockx is already working on this.
Since Nov 14, 2026.
Assessment
This issue has not been assessed yet.
Description
In the recently merged #455 , @zeroeightysix mentioned the following:
The reason I say this isn't very useful yet is because you're not allowed to actually learn anything from the equality yet, due to https://github.com/agda/agda2hs/pull/168.
We should refine the fix of #142 in #168 so that it allows refining types by matching on equality constraints (and later also GADTs once they are added, see #242) while still preventing the problematic cast example in the original issue.
In an ideal world, we would fix this by allowing dot patterns in non-erased positions if they were created by a match on a constructor in a non-erased position, while still rejecting dot patterns created by matches on constructors in erased positions. Unfortunately, Agda does not keep track of the specific constructor pattern that lead to the creation of a dot pattern, so this logic is impossible to implement without redoing significant parts of Agda's LHS checking. However, what we can do is only reject dot patterns in non-erased positions if there are any constructor patterns in erased positions in the current clause, and allow them otherwise. This is an over-approximation, but my guess is that it would allow most realistic use cases (and the ones that would be rejected would have an easy workaround by introducing a helper function for the erased match).
- Dominant language
- Agda
- Stars
- 211
- Forks
- 51
- Avg merge
- 1d 11h
- Merged PRs (30d)
- 9
Getting set up
This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from agda/agda2hs
-
enhancement
Difficulty 5/5 Over a week Newbie friendliness 8/100
Maintainers usually reply within 1 day
-
bug library
Difficulty 4/5 3-5 days Newbie friendliness 45/100
agda/agda2hs#488 · 1 comment ·
Maintainers usually reply within 1 day
-
bug library
Difficulty 4/5 3-5 days Newbie friendliness 49/100
agda/agda2hs#487 · 3 comments ·
Maintainers usually reply within 1 day
-
Skipping compilation for up-to-date files results in mis-compilationPossibly taken @jespercockx claimed this 1 day ago. Openbug
Difficulty 3/5 1-2 days Newbie friendliness 52/100
agda/agda2hs#486 · 2 comments · 1 assignee ·
Maintainers usually reply within 1 day
-
Compile reexport of individual itemsPossibly taken @wasabi315 claimed this 10 days ago. Openenhancement
agda/agda2hs#484 · 1 assignee ·
Maintainers usually reply within 1 day