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.

1 files changed, 0 insertions, 51 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index d46ade1028..50721dc67a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -384,9 +384,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
            pushLevelAndCaptureConstraints            $
            tcExtendTyVarEnv univ_tvs                 $
-           tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
-                               | ex_tv <- extra_ex] $
-               -- See Note [Pattern synonym existentials do not scope]
            tcPat PatSyn lpat (mkCheckExpType pat_ty) $
            do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
                     empty_subst = mkEmptyTCvSubst in_scope
@@ -451,54 +448,6 @@ This should work.  But in the matcher we must match against MkT, and then
 instantiate its argument 'x', to get a function of type (Int -> Int).
 Equality is not enough!  Trac #13752 was an example.
 
-Note [Pattern synonym existentials do not scope]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (Trac #14498):
-  pattern SS :: forall (t :: k). () =>
-                => forall (a :: kk -> k) (n :: kk).
-                => TypeRep n -> TypeRep t
-  pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
-
-Here 'k' is implicitly bound in the signature, but (with
--XScopedTypeVariables) it does still scope over the pattern-synonym
-definition.  But what about 'kk', which is oexistential?  It too is
-implicitly bound in the signature; should it too scope?  And if so,
-what type variable is it bound to?
-
-The trouble is that the type variable to which it is bound is itself
-only brought into scope in part the pattern, so it makes no sense for
-'kk' to scope over the whole pattern.  See the discussion on
-Trac #14498, esp comment:16ff. Here is a simpler example:
-  data T where { MkT :: x -> (x->Int) -> T }
-  pattern P :: () => forall x. x -> (x->Int) -> T
-  pattern P a b = (MkT a b, True)
-
-Here it would make no sense to mention 'x' in the True pattern,
-like this:
-  pattern P a b = (MkT a b, True :: x)
-
-The 'x' only makes sense "under" the MkT pattern. Conclusion: the
-existential type variables of a pattern-synonym signature should not
-scope.
-
-But it's not that easy to implement, because we don't know
-exactly what the existentials /are/ until we get to type checking.
-(See Note [The pattern-synonym signature splitting rule], and
-the partition of implicit_tvs in tcCheckPatSynDecl.)
-
-So we do this:
-
-- The reaner brings all the implicitly-bound kind variables into
-  scope, without trying to distinguish universal from existential
-
-- tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
-  implicitly-bound existentials to
-      APromotionErr PatSynExPE
-  It's not really a promotion error, but it's a way to bind the Name
-  (which the renamer has not complained about) to something that, when
-  looked up, will cause a complaint (in this case
-  TcHsType.promotionErr)
-
 
 Note [The pattern-synonym signature splitting rule]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~