[Git][ghc/ghc][wip/int-index/emb-type] 5 commits: Equality of forall-types is visibility aware

[Vladislav Zavialov (@int-index)]

Vladislav Zavialov pushed to branch wip/int-index/emb-type at Glasgow Haskell Compiler / GHC


Commits:
cf86f3ec by Matthew Craven at 2023-07-16T01:42:09+02:00
Equality of forall-types is visibility aware

This patch finally (I hope) nails the question of whether
   (forall a. ty) and (forall a -> ty)
are `eqType`: they aren't!

There is a long discussion in #22762, plus useful Notes:

* Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare
* Note [Comparing visiblities] in GHC.Core.TyCo.Compare
* Note [ForAllCo] in GHC.Core.TyCo.Rep

It also establishes a helpful new invariant for ForAllCo,
and ForAllTy, when the bound variable is a CoVar:in that
case the visibility must be coreTyLamForAllTyFlag.

All this is well documented in revised Notes.

- - - - -
7f13acbf by Vladislav Zavialov at 2023-07-16T01:56:27-04:00
List and Tuple<n>: update documentation

Add the missing changelog.md entries and @since-annotations.

- - - - -
2afbddb0 by Andrei Borzenkov at 2023-07-16T10:21:24+04:00
Type patterns (#22478, #18986)

Improved name resolution and type checking of type patterns in constructors:

1. HsTyPat: a new dedicated data type that represents type patterns in
   HsConPatDetails instead of reusing HsPatSigType

2. rnHsTyPat: a new function that renames a type
   pattern and collects its binders into three groups:
    - explicitly bound type variables, excluding locally bound
      variables
    - implicitly bound type variables from kind signatures
      (only if ScopedTypeVariables are enabled)
    - named wildcards (only from kind signatures)
2a. rnHsPatSigTypeBindingVars: removed in favour of rnHsTyPat
2b. rnImplcitTvBndrs: removed because no longer needed

3. collect_pat: updated to collect type variable binders from type patterns
   (this means that types and terms use the same infrastructure to detect
   conflicting bindings, unused variables and name shadowing)
3a. CollVarTyVarBinders: a new CollectFlag constructor that enables
    collection of type variables

4. tcHsTyPat: a new function that typechecks type patterns, capable of
   handling polymorphic kinds.
   See Note [Type patterns: binders and unifiers]

Examples of code that is now accepted:

   f = \(P @a) -> \(P @a) -> ...  -- triggers -Wname-shadowing

   g :: forall a. Proxy a -> ...
   g (P @a) = ...                 -- also triggers -Wname-shadowing

   h (P @($(TH.varT (TH.mkName "t")))) = ...
                                  -- t is bound at splice time

   j (P @(a :: (x,x))) = ...      -- (x,x) is no longer rejected

   data T where
     MkT :: forall (f :: forall k. k -> Type).
       f Int -> f Maybe -> T
   k :: T -> ()
   k (MkT @f (x :: f Int) (y :: f Maybe)) = ()
                                  -- f :: forall k. k -> Type

Examples of code that is rejected with better error messages:

  f (Left @a @a _) = ...
  -- new message:
  --     • Conflicting definitions for ‘a’
  --       Bound at: Test.hs:1:11
  --                 Test.hs:1:14

Examples of code that is now rejected:

  {-# OPTIONS_GHC -Werror=unused-matches #-}
  f (P @a) = ()
  -- Defined but not used: type variable ‘a’

- - - - -
eb1a6ab1 by sheaf at 2023-07-16T09:20:45-04:00
Don't use substTyUnchecked in newMetaTyVar

There were some comments that explained that we needed to use an
unchecked substitution function because of issue #12931, but that
has since been fixed, so we should be able to use substTy instead now.

- - - - -
2237142e by Vladislav Zavialov at 2023-07-16T18:53:21+02:00
WIP: Visible forall in types of terms

- - - - -


30 changed files:

- compiler/GHC/Builtin/Names/TH.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/FVs.hs-boot
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/TyCo/Tidy.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Hs/Decls.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/Instances.hs
- compiler/GHC/Hs/Pat.hs
- compiler/GHC/Hs/Syn/Type.hs
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Hs/Utils.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Pmc/Desugar.hs
- compiler/GHC/HsToCore/Quote.hs


The diff was not included because it is too large.


View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/818356ef5f72d8567e188636141aa8cb439cda76...2237142e2d19299a9e42ddc6272bbac01b2e1865

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/818356ef5f72d8567e188636141aa8cb439cda76...2237142e2d19299a9e42ddc6272bbac01b2e1865
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/20230716/ced20bcd/attachment.html>