Skip to content

Conversation

@NathanielB123
Copy link
Contributor

@NathanielB123 NathanielB123 commented Nov 3, 2025

We delay applying pars from getContextArgs until after we have checked for dot patterns.
Relaxes the dot pattern error to only apply to arguments compiled to (implicit or explicit) foralls

Also stop throwing __IMPOSSIBLE__ on instances inside modules.

@NathanielB123 NathanielB123 changed the title [ agda#306 ] Correctly error on dot patterns corresponding to module arguments [ fix #306 ] Correctly error on dot patterns corresponding to module arguments Nov 3, 2025
Delay applying getContextArgs until after we have checked for dot
patterns
Also stop throwing __IMPOSSIBLE__ on instances inside modules
@jespercockx
Copy link
Member

Thank you very much for the PR!

@jespercockx
Copy link
Member

It looks like the CI is failing because of the golden output for AllTests.hs being not up-to-date. You should be able to fix it by running make golden. (Also, my apologies for the horrible test infrastructure, see #153).

@NathanielB123
Copy link
Contributor Author

Oops, should be fixed now

checkForced now also checks the pattern is non-erased, so that should
probably be made clear with the name
Actually, given we check for dotted patterns earlier in compileClause',
I don't think there is any need to checkNonErasedForced in compilePats?
@NathanielB123 NathanielB123 force-pushed the module-param-dot branch 4 times, most recently from 01e7af0 to 1b6ca61 Compare November 4, 2025 15:25
@jespercockx jespercockx merged commit 401ad9c into agda:master Nov 4, 2025
8 checks passed
@NathanielB123
Copy link
Contributor Author

NathanielB123 commented Nov 4, 2025

Oh oops - I just realised I missed compiling any remaining dot patterns to wildcards... The current behaviour isn't the end of the world (just hits bad pattern), but probably not ideal - should I open a new PR?

@jespercockx
Copy link
Member

Oh I should've given it a bit more time then. Yes, please open a new PR if you want! Compiling the remaining dot patterns to wildcards makes sense, or in the case of module parameters you could also use the name of the module parameter (even though the argument will be unused). Or a third option would be to prefix the name of the module parameter with an underscore, which seems to be standard Haskell practice to indicate an unused argument that still has a name.

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.

Dot patterns in arguments corresponding to module parameters should not be allowed

2 participants