Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use TypeAbstractions in singled data type definitions #565

Open
RyanGlScott opened this issue Jun 9, 2023 · 2 comments
Open

Use TypeAbstractions in singled data type definitions #565

RyanGlScott opened this issue Jun 9, 2023 · 2 comments

Comments

@RyanGlScott
Copy link
Collaborator

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]:

  • At present, Template Haskell does not have a way to distinguish among the
    specificities bound by a data type header. Without this knowledge, it is
    unclear how one could work around this issue. Thankfully, this issue is
    only likely to surface in very limited circumstances, so the damage is somewhat
    minimal.
  • This will not kind-check because MkProxy only accepts /one/ visible kind argument,
    whereas this supplies it with two. To avoid this issue, we instead use the type
    `forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/
    technically wrong due to the fact that it explicitly quantifies `k`, but at the
    very least it typechecks. If Template Haskell gained the ability to distinguish
    among the specificities of type variables bound by a data type header
    (perhaps by way of a language feature akin to
    https://github.com/ghc-proposals/ghc-proposals/pull/326), then we could revisit
    this design choice.

(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 within singletons, but this is the one that first comes to mind.

@RyanGlScott
Copy link
Collaborator Author

RyanGlScott commented Oct 12, 2023

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
Copy link
Collaborator Author

See also #583.

@RyanGlScott RyanGlScott changed the title Explore using TypeAbstractions in singletons-th–generated code Use TypeAbstractions in singled data type definitions May 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant