agda icon indicating copy to clipboard operation
agda copied to clipboard

Add `MINIMAL` pragmas to `class Pretty`

Open lawcho opened this issue 1 year ago • 2 comments

Maybe the class should have a MINIMAL pragma now that it has default implementations. (Otherwise we can define instance Pretty Foo and 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

lawcho avatar Oct 10 '24 11:10 lawcho

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.

szumixie avatar Oct 10 '24 13:10 szumixie

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

andreasabel avatar Oct 10 '24 14:10 andreasabel