crucible: Make CrucibleType into type data
#1490
Conversation
`-XTypeData` enables the declaration of type-level datatypes without the need for `-XDataKinds`-style "promotion" from the value level to the type level. `CrucibleType` is only ever used at the type level, so it is a prime candidate for a declaration as `type data`. In fact, it was one of the use-cases for the GHC proposal introducing the extension! Practically speaking, this lets us reduce a bunch of duplication and boilerplate. This functionality was introduced in GHC 9.6, so using it explicitly drops support for GHC 9.4. This is in line with our versioning policy as described in `doc/dev.md`, which states that we aim to support the three most recent versions of GHC at a time. We currently support GHC 9.6-9.10. https://github.com/ghc-proposals/ghc-proposals/blob/3b4e702f217884cf1c2d9cfbd9cb22ad642b22b0/proposals/0106-type-data.rst https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/9.6.1-notes.html
|
This looks promising. I am slightly hesitant about pulling the trigger here, however. Not because of backwards compatibility with old versions of GHC, but rather because I know of at least one |
|
Gotcha. I see that the bug is fixed, though only as of July 7. The fix is likely not on the most recent GHC patch releases, nor do I see any information in the GHC thread about backporting. What do you think the best way forward is? We could (1) merge as this doesn't seem to be affecting us right now, (2) test with more repos, e.g., Macaw (though apparently only Crucible re-exports this module), (3) wait until our newest supported GHC has a patch for the bug, (4) wait until all of our supported GHCs have the fix, or (5) something else? |
|
The merge request which fixed the GHC issue has been marked to be backported to several GHC release series. (Thus far, it has been backported to GHC 9.10.3, which is slated to be released later this month. Personally, I am inclined to wait until all supported GHCs have this fix, but if you are keen on landing this, then I won't object. |
|
Update: the fix is in 9.{10,12}.3, but has not been backported to GHC 9.6 nor 9.8. That may change, but if it doesn't we can merge this after they both slip out of our support window, after #1693. |
-XTypeDataenables the declaration of type-level datatypes without the need for-XDataKinds-style "promotion" from the value level to the type level.CrucibleTypeis only ever used at the type level, so it is a prime candidate for a declaration astype data. In fact, it was one of the use-cases for the GHC proposal introducing the extension! Practically speaking, this lets us reduce a bunch of duplication and boilerplate.This functionality was introduced in GHC 9.6, so using it explicitly drops support for GHC 9.4. This is in line with our versioning policy as described in
doc/dev.md, which states that we aim to support the three most recent versions of GHC at a time. We currently support GHC 9.6-9.10.See:
https://github.com/ghc-proposals/ghc-proposals/blob/3b4e702f217884cf1c2d9cfbd9cb22ad642b22b0/proposals/0106-type-data.rst https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/9.6.1-notes.html