[GHC] #16315: Pattern synonym implicit existential quantification

[GHC]

#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  patsyn/should_compile/T14498
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/361
-------------------------------------+-------------------------------------

Comment (by Marge Bot <ben+marge-bot@…>):

 In [changeset:"5bc195b1fe788e9a900a15fbe473967850517c3e/ghc"
 5bc195b1/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="5bc195b1fe788e9a900a15fbe473967850517c3e"
 Treat kind/type variables identically, demolish FKTV

 Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024
 -no-kind-vars.rst
 Fixes Trac #16334, Trac #16315

 With this patch, scoping rules for type and kind variables have been
 unified: kind variables no longer receieve special treatment. This
 simplifies both the language and the implementation.

 User-facing changes
 -------------------

 * Kind variables are no longer implicitly quantified when an explicit
   forall is used:

     p ::             Proxy (a :: k)    -- still accepted
     p :: forall k a. Proxy (a :: k)    -- still accepted
     p :: forall   a. Proxy (a :: k)    -- no longer accepted

   In other words, now we adhere to the "forall-or-nothing" rule more
   strictly.

   Related function: RnTypes.rnImplicitBndrs

 * The -Wimplicit-kind-vars warning has been deprecated.

 * Kind variables are no longer implicitly quantified in constructor
   declarations:

     data T a        = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- no
 longer accepted
     data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- still
 accepted

   Related function: RnTypes.extractRdrKindSigVars

 * Implicitly quantified kind variables are no longer put in front of
   other variables:

     f :: Proxy (a :: k) -> Proxy (b :: j)

     f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b   -- old order
     f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b   -- new order

   This is a breaking change for users of TypeApplications. Note that
   we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
   See "Ordering of specified variables" in the User's Guide.

   Related function: RnTypes.rnImplicitBndrs

 * In type synonyms and type family equations, free variables on the RHS
   are no longer implicitly quantified unless used in an outermost kind
   annotation:

     type T = Just (Nothing :: Maybe a)         -- no longer accepted
     type T = Just Nothing :: Maybe (Maybe a)   -- still accepted

   The latter form is a workaround due to temporary lack of an explicit
   quantification method. Ideally, we would write something along these
   lines:

     type T @a = Just (Nothing :: Maybe a)

   Related function: RnTypes.extractHsTyRdrTyVarsKindVars

 * Named wildcards in kinds are fixed (Trac #16334):

     x :: (Int :: _t)    -- this compiles, infers (_t ~ Type)

   Related function: RnTypes.partition_nwcs

 Implementation notes
 --------------------

 * One of the key changes is the removal of FKTV in RnTypes:

   - data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
   -                          , fktv_tys    :: [Located RdrName] }
   + type FreeKiTyVars = [Located RdrName]

   We used to keep track of type and kind variables separately, but
   now that they are on equal footing when it comes to scoping, we
   can put them in the same list.

 * extract_lty and family are no longer parametrized by TypeOrKind,
   as we now do not distinguish kind variables from type variables.

 * PatSynExPE and the related Note [Pattern synonym existentials do not
 scope]
   have been removed (Trac #16315). With no implicit kind quantification,
   we can no longer trigger the error.

 * reportFloatingKvs and the related Note [Free-floating kind vars]
   have been removed. With no implicit kind quantification,
   we can no longer trigger the error.
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler