agda
agda copied to clipboard
Add `MINIMAL` pragmas to `class Pretty`
Maybe the class should have a MINIMAL pragma now that it has default implementations. (Otherwise we can define
instance Pretty Fooand happily busy-loop.)
Originally posted by @andreasabel in https://github.com/agda/agda/pull/7545#discussion_r1794820432
i.e. here
https://github.com/agda/agda/blob/e4215ab0ce06de53e98493484b1938f647b7630f/src/full/Agda/Syntax/Common/Pretty.hs#L67-L74
and here
https://github.com/agda/agda/blob/994e76b688d5d50b3d3351f4157beb40ab956928/src/full/Agda/Compiler/JS/Pretty.hs#L206-L211
There are some other classes that could also use MINIMAL pragmas:
https://github.com/agda/agda/blob/628f6d16dc6fdb96dc3f0f26baf6380e19fd7d8d/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs#L555-L556
https://github.com/agda/agda/blob/628f6d16dc6fdb96dc3f0f26baf6380e19fd7d8d/src/full/Agda/TypeChecking/Reduce.hs#L414-L415
https://github.com/agda/agda/blob/628f6d16dc6fdb96dc3f0f26baf6380e19fd7d8d/src/full/Agda/TypeChecking/Substitute/DeBruijn.hs#L12-L18
https://github.com/agda/agda/blob/628f6d16dc6fdb96dc3f0f26baf6380e19fd7d8d/src/full/Agda/Utils/Benchmark.hs#L136-L142
https://github.com/agda/agda/blob/628f6d16dc6fdb96dc3f0f26baf6380e19fd7d8d/src/full/Agda/Utils/Functor.hs#L46-L52
And there are a lot of Lens classes that mutually define set and modify.
Indeed we have some technical debt there.
I vaguely recall that the MINIMAL pragma wasn't in GHC from the beginning (or not feature complete), but the docs do not detail the history: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html