1lab/mikan
13
52
Fork
You've already forked mikan
9

feat: display hiding type in errors #130

Merged
amyliao merged 1 commit from pounce/mikan:hiding_instance_errs into main 2026年06月18日 21:32:42 +02:00
Contributor
Copy link

this commit includes minor changes to the wording of error messages. see
test diff for more info.

resolves: #101

this commit includes minor changes to the wording of error messages. see test diff for more info. resolves: #101
feat: display hiding type in errors
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
1ff85e02c9 
this commit includes minor changes to the wording of error messages. see
test diff for more info.
resolves: #101
amyliao requested changes 2026年06月05日 16:13:57 +02:00
Dismissed
@ -60,6 +60,7 @@ import Mikan.Utils.VarSet (VarSet)
import Mikan.Utils.VarSet qualified as VarSet
import Mikan.Utils.Impossible
import Generic.Data (FiniteEnumeration(..))
Owner
Copy link

This import should go before all the Mikan. imports. (I really gotta write that port of sort-imports...)

This import should go before all the `Mikan.` imports. (I really gotta write that port of `sort-imports`...)
pounce marked this conversation as resolved
@ -1754,3 +1754,2 @@
-- Andreas, 2018年10月18日, issue #3289: postfix projections have no hiding info.
unless (caseMaybe h True $ sameHiding $ projArgInfo proj) $
softTypeError $ WrongHidingInProjection d
whenJust h $ \h -> unless (sameHiding h $ projArgInfo proj) $
Owner
Copy link

Prefer whenJust h \h ->. BlockArguments is enabled globally.

Prefer `whenJust h \h ->`. `BlockArguments` is enabled globally.
pounce marked this conversation as resolved
@ -613,3 +613,3 @@
-- Found a visible argument but expected a hidden one:
-- That's an error, as we cannot insert a visible lambda.
if visible h' then typeError $ WrongHidingInLambda target else do
if visible h' then typeError $ WrongHidingInLambda (getHiding h) target else do
Owner
Copy link

Please include the reproducers from #101 as failing tests with implicit arguments.

Please include the reproducers from #101 as failing tests with implicit arguments.
pounce marked this conversation as resolved
@ -1,4 +1,4 @@
Issue1413WrongHiding.agda:12.1-14: error: [WrongHidingInProjection]
Wrong hiding used for projection Foo.foo
Unexpected implicit projection used Foo.foo
Owner
Copy link

This error message doesn't make a lot of sense. Projections can't be implicit, but they could take an implicit argument. The actual issue is that Foo.foo expects a visible argument but has been given an implicit one, and the error should mention both. The expected visibility is in the projArgInfo proj.

This error message doesn't make a lot of sense. Projections can't be implicit, but they *could* take an implicit argument. The actual issue is that `Foo.foo` expects a visible argument but has been given an implicit one, and the error should mention both. The expected visibility is in the `projArgInfo proj`.
pounce marked this conversation as resolved
@ -1,3 +1,3 @@
Issue3289-rhs.agda:16.11-13: error: [IllegalHidingInPostfixProjection]
Illegal hiding in postfix projection ⦃ .x ⦄
Postfix projection is an instance argument, which is illegal ⦃ .x ⦄
Owner
Copy link

Maybe (fsep etc):

Postfix projections can only be visible arguments, but ⦃ .x ⦄ is an instance argument
Maybe (`fsep` etc): ``` Postfix projections can only be visible arguments, but ⦃ .x ⦄ is an instance argument ```
pounce marked this conversation as resolved
address review comments
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
3f8004b28e
pounce force-pushed hiding_instance_errs from 3f8004b28e
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
to c4efe7fcd8
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
2026年06月05日 17:22:06 +02:00 Compare
update tests
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
26a524af6b
amyliao left a comment
Copy link

Looks good, please rebase on main.

Looks good, please rebase on `main`.
pounce force-pushed hiding_instance_errs from 26a524af6b
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to cb89416d17
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年06月13日 15:38:14 +02:00 Compare
amyliao force-pushed hiding_instance_errs from cb89416d17
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 2a04f41d09
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
ci/woodpecker/push/main Pipeline was successful
2026年06月18日 14:23:02 +02:00 Compare
Sign in to join this conversation.
No reviewers
Labels
Clear labels
1 - scope
language
 Backwards-compatible changes to the surface language, such as adding new features.
1 - scope
language change
 Breaking changes to a documented part of the surface language. These should be documented and specifically called out in the changelog.
1 - scope
performance
 Semantics-preserving performance work.
1 - scope
task
 Changes that are not apparent to the user, e.g. developer documentation and refactors, which do not need to be documented.
A: dead-code
Dead code elimination and --save-metas.
A: errors
Reporting of error and warning messages.
A: highlighting
Highlighting during interaction & literate compilation
A: imports
Handling of imports and interface file de/serialization.
A: infra
Iinfrastructure (e.g. CI, developer documentation, the build system, or the repository itself)
A: instance
Instance declarations, arguments, and resolution
A: lhs
LHS checking, coverage checking, and clause compilation
A: modules
Declaration and instantiation of parametrised modules.
A: parallel
Parallel typechecking.
A: positivity
Positivity checking
A: printing
Pretty-printing, display forms, and the wording of diagnostic messages
A: records
Record declarations, record expressions and copattern matching
A: scoping
Scope checking (ConcreteToAbstract)
A: termination
Termination checking
0 - type
bug
 Issues describing an incorrect behaviour in the project, typos in the documentation, etc.
0 - type
discussion
 An issue raised to gather opinions on a proposed change, or a suggested language change.
0 - type
question
 An issue raised to ask a question.
9 - status
duplicate
 This issue or pull request already exists.
9 - status
info needed
 More information is needed from the submitter to decide how to proceed with the issue report.
9 - status
invalid
 The issue report or pull request does not describe an actual bug, or does otherwise does not meet the contributing guidelines.
good first issue
Interested in contributing? Get started here.
upstream
Related to an upstream repository, already reported there
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
1lab/mikan!130
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "pounce/mikan:hiding_instance_errs"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?