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

Dynamic typing for diagnostics #121

Merged
amyliao merged 7 commits from aliao/diagnostic-class into main 2026年06月05日 14:32:18 +02:00

Implements the refactoring described in #100: There is a new Diagnostic class, in Mikan.TypeChecking.Monad.Diagnostic, which packages both the information necessary for generating a diagnostic message (and for toggling warnings) and support for subtyping inspired by Control.Exception.Exception. Existential and "serialised" wrappers for Diagnostic take the place of TypeError in TCErr and Warning in TCWarning, respectively.

Additionally, some errors which were only in TypeError as wrappers (SplitError, UnquoteError, ExecError, NicifierError and InteractionError) have been moved into their own Diagnostic instance, defined in their own "service" modules (e.g. Unquote gets Unquote.Errors). This follows the pattern I introduced for Conversion.Errors.

The diff is pretty large but should be reviewable commit-by-commit.

Implements the refactoring described in #100: There is a new `Diagnostic` class, in `Mikan.TypeChecking.Monad.Diagnostic`, which packages both the information necessary for generating a diagnostic message (and for toggling warnings) *and* support for subtyping inspired by `Control.Exception.Exception`. Existential and "serialised" wrappers for `Diagnostic` take the place of `TypeError` in `TCErr` and `Warning` in `TCWarning`, respectively. Additionally, some errors which were only in `TypeError` as wrappers (`SplitError`, `UnquoteError`, `ExecError`, `NicifierError` and `InteractionError`) have been moved into their own `Diagnostic` instance, defined in their own "service" modules (e.g. `Unquote` gets `Unquote.Errors`). This follows the pattern I introduced for `Conversion.Errors`. The diff is pretty large but should be reviewable commit-by-commit.
amyliao force-pushed aliao/diagnostic-class from 7360bc6226
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
to e662c2b484
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年06月01日 12:25:03 +02:00 Compare
amyliao force-pushed aliao/diagnostic-class from 3e57afa3b0
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 26131683e2
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
2026年06月01日 13:23:11 +02:00 Compare
amyliao force-pushed aliao/diagnostic-class from 9ca291f046
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
to 64e2dad95a
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年06月01日 13:59:32 +02:00 Compare
amyliao force-pushed aliao/diagnostic-class from 64e2dad95a
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 93a1502bf2
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
2026年06月01日 14:04:33 +02:00 Compare
chore: explicit source imports in Diagnostic
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
08afbcd61c
amyliao changed title from (削除) WIP: Dynamic typing for diagnostics (削除ここまで) to Dynamic typing for diagnostics 2026年06月01日 14:16:09 +02:00
chore: explain CannotEliminateWithProjection
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
f4b7dde789
 
This adds a `WhyWrongProj` type explaining the possible failures of
disambiguateProjection and ensures that the printed error message
mentions *why* the copattern is unusable at that position. This
includes:
- Having something that isn't a projection at all in a copattern
- Something that *used to be* a projection in a copattern
- Having a projection pattern at the wrong record type, with a special
 case for the record having no fields
- Having a projection pattern at a non-record type, with a nudge towards
 adding arguments to the left of the split if the expected type is a
 function into some record type.
Author
Owner
Copy link

f4b7dde789 was reviewed in #125.

f4b7dde7897d835ba5bdcad20e3b142966ff664f was reviewed in #125.
amyliao force-pushed aliao/diagnostic-class from f4b7dde789
Some checks failed
ci/woodpecker/pr/test Pipeline was canceled
to b3e594b874
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年06月02日 12:24:14 +02:00 Compare
amyliao force-pushed aliao/diagnostic-class from b3e594b874
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 73721c9bd7
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
ci/woodpecker/push/main Pipeline was successful
2026年06月03日 23:19:19 +02:00 Compare
Author
Owner
Copy link

Not extremely scientific but it looks like the performance impact of this branch on #127 is fairly minor:

-- before
 INIT time 0.000s ( 0.000s elapsed)
 MUT time 221.339s (222.790s elapsed)
 GC time 67.523s ( 68.148s elapsed)
 EXIT time 0.000s ( 0.000s elapsed)
 Total time 288.862s (290.938s elapsed)
-- after
 INIT time 0.000s ( 0.000s elapsed)
 MUT time 222.576s (224.156s elapsed)
 GC time 67.320s ( 67.988s elapsed)
 EXIT time 0.000s ( 0.000s elapsed)
 Total time 289.897s (292.144s elapsed)

I think this is an acceptable loss for how easy #122 is on top of this branch. If I were a betting woman I would put the performance impact on the thrown together implementation of warningHighlighting'. I don't really have a good solution for this yet, since in my head it feels pretty entangled with coming up with a structured representation of "see also" spans in diagnostic messages, and I'm pretty stuck on that.

Not extremely scientific but it looks like the performance impact of this branch on #127 is fairly minor: ``` -- before INIT time 0.000s ( 0.000s elapsed) MUT time 221.339s (222.790s elapsed) GC time 67.523s ( 68.148s elapsed) EXIT time 0.000s ( 0.000s elapsed) Total time 288.862s (290.938s elapsed) -- after INIT time 0.000s ( 0.000s elapsed) MUT time 222.576s (224.156s elapsed) GC time 67.320s ( 67.988s elapsed) EXIT time 0.000s ( 0.000s elapsed) Total time 289.897s (292.144s elapsed) ``` I think this is an acceptable loss for how easy #122 is on top of this branch. If I were a betting woman I would put the performance impact on the thrown together implementation of `warningHighlighting'`. I don't really have a good solution for this yet, since in my head it feels pretty entangled with coming up with a structured representation of "see also" spans in diagnostic messages, and I'm pretty stuck on that.
@ -0,0 +128,4 @@
syntaxError :: (HasCallStack, MonadTCError m) => String -> m a
syntaxError = locatedTypeError SyntaxError
-- TODO: All of these instances complicate the module cycle quite a bit,
Owner
Copy link

We should probably take a long, hard look at PrettyTCM sometime soon... when I was looking at reducing the module cycle knot it was the most problematic node in the graph outside of reduction.

We should probably take a long, hard look at `PrettyTCM` sometime soon... when I was looking at reducing the module cycle knot it was the most problematic node in the graph outside of reduction.
@ -44,4 +42,0 @@
-- We don't need to serialise warnings that turn into errors
-- [TODO: Reed M, 29/04/2026] These should be renumbered at some point.
instance EmbPrj Warning where
icod_ = \case
Owner
Copy link

Very nice, really hated this code!

Very nice, really hated this code!
amyliao deleted branch aliao/diagnostic-class 2026年06月05日 14:32:19 +02:00
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
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!121
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "aliao/diagnostic-class"

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?