[Git][ghc/ghc][wip/sand-witch/dib-instances] 6 commits: Report scoped kind variables at the type-checking phase (#16635)

[Andrei Borzenkov (@sand-witch)]

Andrei Borzenkov pushed to branch wip/sand-witch/dib-instances at Glasgow Haskell Compiler / GHC


Commits:
78cd1132 by Andrei Borzenkov at 2023-06-15T11:16:11+04:00
Report scoped kind variables at the type-checking phase (#16635)

This patch modifies the renamer to respect ScopedTypeVariables in kind
signatures. This means that kind variables bound by the outermost
`forall` now scope over the type:

  type F = '[Right @a @() () :: forall a. Either a ()]
  --         ^^^^^^^^^^^^^^^          ^^^
  --          in scope here        bound here

However, any use of such variables is a type error, because we don't
have type-level lambdas to bind them in Core. This is described in the
new Note [Type variable scoping errors during type check] in GHC.Tc.Types.

- - - - -
4a41ba75 by Sylvain Henry at 2023-06-15T18:09:15-04:00
JS: testsuite: use correct ticket number

Replace #22356 with #22349 for these tests because #22356 has been fixed
but now these tests fail because of #22349.

- - - - -
15f150c8 by Sylvain Henry at 2023-06-15T18:09:16-04:00
JS: testsuite: update ticket numbers

- - - - -
08d8e9ef by Sylvain Henry at 2023-06-15T18:09:16-04:00
JS: more triage

- - - - -
e8752e12 by Krzysztof Gogolewski at 2023-06-15T18:09:52-04:00
Fix test T18522-deb-ppr

Fixes #23509

- - - - -
63d2c679 by Andrei Borzenkov at 2023-06-16T12:04:18+04:00
Type/data instances: require that variables on the RHS are mentioned on the LHS (#23512)

GHC Proposal #425 "Invisible binders in type declarations" restricts the
scope of type and data family instances as follows:

  In type family and data family instances, require that every variable
  mentioned on the RHS must also occur on the LHS.

For example, here are three equivalent type instance definitions accepted before this patch:

  type family F1 a :: k
  type instance F1 Int = Any :: j -> j

  type family F2 a :: k
  type instance F2 @(j -> j) Int = Any :: j -> j

  type family F3 a :: k
  type instance forall j. F3 Int = Any :: j -> j

- In F1, j is implicitly quantified and it occurs only on the RHS;
- In F2, j is implicitly quantified and it occurs both on the LHS and the RHS;
- In F3, j is explicitly quantified.

Now F1 is rejected with an out-of-scope error, while F2 and F3 continue to be accepted.

- - - - -


30 changed files:

- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Errors/Types/PromotionErr.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Types/BasicTypes.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Types/Error/Codes.hs
- docs/users_guide/9.8.1-notes.rst
- libraries/base/jsbits/errno.js
- rts/js/profiling.js
- testsuite/tests/backpack/cabal/T15594/all.T
- testsuite/tests/backpack/cabal/T16219/all.T
- testsuite/tests/backpack/cabal/T20509/all.T
- testsuite/tests/backpack/cabal/bkpcabal01/all.T
- testsuite/tests/backpack/cabal/bkpcabal02/all.T
- testsuite/tests/backpack/cabal/bkpcabal03/all.T
- testsuite/tests/backpack/cabal/bkpcabal04/all.T
- testsuite/tests/backpack/cabal/bkpcabal05/all.T
- testsuite/tests/backpack/cabal/bkpcabal06/all.T
- testsuite/tests/backpack/cabal/bkpcabal07/all.T
- testsuite/tests/cabal/T12733/all.T
- testsuite/tests/cabal/cabal01/all.T
- testsuite/tests/cabal/cabal03/all.T
- testsuite/tests/cabal/cabal04/all.T
- testsuite/tests/cabal/cabal05/all.T
- testsuite/tests/cabal/cabal06/all.T
- testsuite/tests/cabal/cabal08/all.T


The diff was not included because it is too large.


View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b932b26bfbeb15dd6ab2211fbf4a50f150a12dbe...63d2c67932ed70bc19fd62dcad4763d11af24303

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b932b26bfbeb15dd6ab2211fbf4a50f150a12dbe...63d2c67932ed70bc19fd62dcad4763d11af24303
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230616/4cd1ac90/attachment.html>