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

dMatchUpSAKWithDecl erroneously rejects invisible forall without corresponding invisible type variable binder #228

Closed
RyanGlScott opened this issue Jul 14, 2024 · 0 comments · Fixed by #230
Labels

Comments

@RyanGlScott
Copy link
Collaborator

This is a perfectly valid data type:

type D :: forall (a :: Type). Type
data D

Although there is no explicit @a binder in the declaration for D, this is perfectly fine, as GHC is capable of inferring it. th-desugar's dMatchUpSAKWithDecl function, on the other hand, rejects this. I originally encountered this issue in the context of singletons-th, but here is a way to trigger the issue using only the th-desugar API:

{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Data.Kind (Type)
import Language.Haskell.TH hiding (Type)
import Language.Haskell.TH.Desugar

$(do let sak = DForallT (DForallInvis [DKindedTV (mkName "a") SpecifiedSpec (DConT ''Type)]) (DConT ''Type)
     bndrs <- dMatchUpSAKWithDecl sak []
     runIO $ print $ length bndrs
     pure [])

I believe this should work.

RyanGlScott added a commit that referenced this issue Jul 14, 2024
…sponding @-binders

After this patch, `dMatchUpSAKWithDecl` is now able to handle a standalone kind
signature with an invisible `forall` without a corresponding `@`-binder, as
seen in the example below:

```hs
type D :: forall (a :: Type). Type
data D
```

While I was in town, I did some code cleanup in `dMatchUpSAKWithDecl` to make
sure that all of the various error conditions are checked more thoroughly,
documenting what parts of the code rely on which preconditions more precisely.
I also applied the same treatment to `matchUpSAKWithDecl`.

Fixes #228.
RyanGlScott added a commit that referenced this issue Jul 14, 2024
…sponding @-binders

After this patch, `dMatchUpSAKWithDecl` is now able to handle a standalone kind
signature with an invisible `forall` without a corresponding `@`-binder, as
seen in the example below:

```hs
type D :: forall (a :: Type). Type
data D
```

While I was in town, I did some code cleanup in `dMatchUpSAKWithDecl` to make
sure that all of the various error conditions are checked more thoroughly,
documenting what parts of the code rely on which preconditions more precisely.
I also applied the same treatment to `matchUpSAKWithDecl`.

Fixes #228.
RyanGlScott added a commit that referenced this issue Jul 16, 2024
…sponding @-binders

After this patch, `dMatchUpSAKWithDecl` is now able to handle a standalone kind
signature with an invisible `forall` without a corresponding `@`-binder, as
seen in the example below:

```hs
type D :: forall (a :: Type). Type
data D
```

While I was in town, I did some code cleanup in `dMatchUpSAKWithDecl` to make
sure that all of the various error conditions are checked more thoroughly,
documenting what parts of the code rely on which preconditions more precisely.
I also applied the same treatment to `matchUpSAKWithDecl`.

Fixes #228.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
1 participant