search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

[refactor] __FROM_JUST__ = fromMaybe __IMPOSSIBLE__ #7281

Open omelkonian opened 1 month ago

omelkonian commented 1 month ago

Good for the eyes; hope it's worth the rebasing overhead.

andreasabel commented 1 month ago

I think this goes in the opposite direction of what we have been doing before. We want the reported error line of the __IMPOSSIBLE__ as far on the outside as possible. The further outside you handle an exception, the more context you have for analysing what could have closed it.

omelkonian commented 1 month ago

@andreasabel Now fixed the error-location callstack being at the point we want and renamed to __FROM_JUST__ to make it shout.

andreasabel commented 57 minutes ago

Forgive me, but I still cannot get excited about this repainting effort. How about getting used to seeing fromMaybe __IMPOSSIBLE__? Replacing this with __FROM_JUST__ is only minor cosmetics. (And I could cite the Fairbairn threshold...) Also, doesn't the error message still mention __IMPOSSIBLE__ rather than __FROM_JUST__?

Ok to close?