You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
GHC recently landed !9480, an implementation of GHC proposal #425. This introduces invisible @k-binders for type-level declarations, guarded behind the TypeAbstractions extension. For example:
data D @k @j (a :: k) (b :: j) = ...
^^ ^^
With this, we can finally address singletons-th limitations that are described in Note [Preserve the order of type variables during singling]:
Looking at this a bit more, I think that we would first need to resolve goldfirere/th-desugar#199 before we could address this issue. This sounds doable, but I think it would take some time to get right. Moreover, I'd like to release a new version of singletons soon that is compatible with GHC 9.8, and I don't want to hold up the release on this issue. For that reason, I'll defer this to later.
RyanGlScott
changed the title
Explore using TypeAbstractions in singletons-th–generated code
Use TypeAbstractions in singled data type definitions
May 10, 2024
GHC recently landed !9480, an implementation of GHC proposal #425. This introduces invisible
@k
-binders for type-level declarations, guarded behind theTypeAbstractions
extension. For example:With this, we can finally address
singletons-th
limitations that are described inNote [Preserve the order of type variables during singling]
:singletons/singletons-th/src/Data/Singletons/TH/Single/Type.hs
Lines 249 to 253 in 2c91ce4
singletons/singletons-th/src/Data/Singletons/TH/Single/Type.hs
Lines 320 to 328 in 2c91ce4
(Historical note: ghc-proposals/ghc-proposals#326 was an earlier iteration of what eventually became GHC proposal #425.)
It's possible that there are other use cases for
TypeAbstractions
withinsingletons
, but this is the one that first comes to mind.The text was updated successfully, but these errors were encountered: