Fix scoping of pattern-synonym existentials

This patch fixes Trac #14998, where we eventually decided that
the existential type variables of the signature of a pattern
synonym should not scope over the pattern synonym.

See Note [Pattern synonym existentials do not scope] in TcPatSyn.

compiler/basicTypes/PatSyn.hs

@@ -285,7 +285,7 @@ done by TcPatSyn.patSynBuilderOcc.
 Note [Pattern synonyms and the data type Type]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The type of a pattern synonym is of the form (See Note
-[Pattern synonym signatures]):
+[Pattern synonym signatures] in TcSigs):
 
     forall univ_tvs. req => forall ex_tvs. prov => ...
 

compiler/typecheck/TcHsType.hs

@@ -2426,11 +2426,13 @@ promotionErr name err
   where
     reason = case err of
                FamDataConPE   -> text "it comes from a data family instance"
-               NoDataKindsTC  -> text "Perhaps you intended to use DataKinds"
-               NoDataKindsDC  -> text "Perhaps you intended to use DataKinds"
-               NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
-               NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
-               PatSynPE       -> text "Pattern synonyms cannot be promoted"
+               NoDataKindsTC  -> text "perhaps you intended to use DataKinds"
+               NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
+               NoTypeInTypeTC -> text "perhaps you intended to use TypeInType"
+               NoTypeInTypeDC -> text "perhaps you intended to use TypeInType"
+               PatSynPE       -> text "pattern synonyms cannot be promoted"
+               PatSynExPE     -> sep [ text "the existential variables of a pattern synonym"
+                                     , text "signature do not scope over the pattern" ]
                _ -> text "it is defined and used in the same recursive group"
 
 {-

compiler/typecheck/TcPatSyn.hs

@@ -177,6 +177,9 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(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
@@ -240,6 +243,98 @@ 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 varaible 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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a pattern signature, we must split
+     the kind-generalised variables, and
+     the implicitly-bound variables
+into universal and existential.  The rule is this
+(see discussion on Trac #11224):
+
+     The universal tyvars are the ones mentioned in
+          - univ_tvs: the user-specified (forall'd) universals
+          - req_theta
+          - res_ty
+     The existential tyvars are all the rest
+
+For example
+
+   pattern P :: () => b -> T a
+   pattern P x = ...
+
+Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
+how do we split the arg_tys from req_ty?  Consider
+
+   pattern Q :: () => b -> S c -> T a
+   pattern Q x = ...
+
+This is an odd example because Q has only one syntactic argument, and
+so presumably is defined by a view pattern matching a function.  But
+it can happen (Trac #11977, #12108).
+
+We don't know Q's arity from the pattern signature, so we have to wait
+until we see the pattern declaration itself before deciding res_ty is,
+and hence which variables are existential and which are universal.
+
+And that in turn is why TcPatSynInfo has a separate field,
+patsig_implicit_bndrs, to capture the implicitly bound type variables,
+because we don't yet know how to split them up.
+
+It's a slight compromise, because it means we don't really know the
+pattern synonym's real signature until we see its declaration.  So,
+for example, in hs-boot file, we may need to think what to do...
+(eg don't have any implicitly-bound variables).
+
+
 Note [Checking against a pattern signature]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When checking the actual supplied pattern against the pattern synonym

compiler/typecheck/TcRnTypes.hs

@@ -1092,6 +1092,9 @@ data PromotionErr
   | PatSynPE         -- Pattern synonyms
                      -- See Note [Don't promote pattern synonyms] in TcEnv
 
+  | PatSynExPE       -- Pattern synonym existential type variable
+                     -- See Note [Pattern synonym existentials do not scope] in TcPatSyn
+
   | RecDataConPE     -- Data constructor in a recursive loop
                      -- See Note [Recursion and promoting data constructors] in TcTyClsDecls
   | NoDataKindsTC    -- -XDataKinds not enabled (for a tycon)
@@ -1245,6 +1248,7 @@ instance Outputable PromotionErr where
   ppr ClassPE        = text "ClassPE"
   ppr TyConPE        = text "TyConPE"
   ppr PatSynPE       = text "PatSynPE"
+  ppr PatSynExPE     = text "PatSynExPE"
   ppr FamDataConPE   = text "FamDataConPE"
   ppr RecDataConPE   = text "RecDataConPE"
   ppr NoDataKindsTC  = text "NoDataKindsTC"
@@ -1263,6 +1267,7 @@ pprPECategory :: PromotionErr -> SDoc
 pprPECategory ClassPE        = text "Class"
 pprPECategory TyConPE        = text "Type constructor"
 pprPECategory PatSynPE       = text "Pattern synonym"
+pprPECategory PatSynExPE     = text "Pattern synonym existential"
 pprPECategory FamDataConPE   = text "Data constructor"
 pprPECategory RecDataConPE   = text "Data constructor"
 pprPECategory NoDataKindsTC  = text "Type constructor"

compiler/typecheck/TcSigs.hs

@@ -295,51 +295,10 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
   universal and existential vars.
 
 * After we kind-check the pieces and convert to Types, we do kind generalisation.
-
-Note [The pattern-synonym signature splitting rule]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Given a pattern signature, we must split
-     the kind-generalised variables, and
-     the implicitly-bound variables
-into universal and existential.  The rule is this
-(see discussion on Trac #11224):
-
-     The universal tyvars are the ones mentioned in
-          - univ_tvs: the user-specified (forall'd) universals
-          - req_theta
-          - res_ty
-     The existential tyvars are all the rest
-
-For example
-
-   pattern P :: () => b -> T a
-   pattern P x = ...
-
-Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
-how do we split the arg_tys from req_ty?  Consider
-
-   pattern Q :: () => b -> S c -> T a
-   pattern Q x = ...
-
-This is an odd example because Q has only one syntactic argument, and
-so presumably is defined by a view pattern matching a function.  But
-it can happen (Trac #11977, #12108).
-
-We don't know Q's arity from the pattern signature, so we have to wait
-until we see the pattern declaration itself before deciding res_ty is,
-and hence which variables are existential and which are universal.
-
-And that in turn is why TcPatSynInfo has a separate field,
-patsig_implicit_bndrs, to capture the implicitly bound type variables,
-because we don't yet know how to split them up.
-
-It's a slight compromise, because it means we don't really know the
-pattern synonym's real signature until we see its declaration.  So,
-for example, in hs-boot file, we may need to think what to do...
-(eg don't have any implicitly-bound variables).
 -}
 
 tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
+-- See Note [Pattern synonym signatures]
 tcPatSynSig name sig_ty
   | HsIB { hsib_vars = implicit_hs_tvs
          , hsib_body = hs_ty }  <- sig_ty

docs/users_guide/glasgow_exts.rst

@@ -5297,6 +5297,8 @@ Note also the following points
 
      P :: () => CProv => t1 -> t2 -> .. -> tN -> t
 
+-  The GHCi :ghci-cmd:`:info` command shows pattern types in this format.
+
 -  You may specify an explicit *pattern signature*, as we did for
    ``ExNumPat`` above, to specify the type of a pattern, just as you can
    for a function. As usual, the type signature can be less polymorphic
@@ -5313,7 +5315,21 @@ Note also the following points
          pattern Left' x  = Left x
          pattern Right' x = Right x
 
--  The GHCi :ghci-cmd:`:info` command shows pattern types in this format.
+-  The rules for lexically-scoped type variables (see
+   :ref:`scoped-type-variables`) apply to pattern-synonym signatures.
+   As those rules specify, only the type variables from an explicit,
+   syntactically-visible outer `forall` (the universals) scope over
+   the definition of the pattern synonym; the existentials, bound by
+   the inner forall, do not.  For example ::
+
+         data T a where
+            MkT :: Bool -> b -> (b->Int) -> a -> T a
+
+         pattern P :: forall a. forall b. b -> (b->Int) -> a -> T a
+         pattern P x y v <- MkT True x y (v::a)
+
+   Here the universal type variable `a` scopes over the definition of `P`,
+   but the existential `b` does not.  (c.f. disussion on Trac #14998.)
 
 -  For a bidirectional pattern synonym, a use of the pattern synonym as
    an expression has the type

testsuite/tests/patsyn/should_fail/T11265.stderr

 
 T11265.hs:6:12: error:
     • Pattern synonym ‘A’ cannot be used here
-        (Pattern synonyms cannot be promoted)
+        (pattern synonyms cannot be promoted)
     • In the first argument of ‘F’, namely ‘A’
       In the instance declaration for ‘F A’

testsuite/tests/patsyn/should_fail/T14498.hs

+{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds #-}
+
+module T14498 where
+
+import Type.Reflection
+import Data.Kind
+
+data Dict c where Dict :: c => Dict c
+
+asTypeable :: TypeRep a -> Dict (Typeable a)
+asTypeable rep =
+  withTypeable rep
+    Dict
+
+pattern Typeable :: () => Typeable a => TypeRep a
+pattern Typeable <- (asTypeable -> Dict)
+  where Typeable = typeRep
+
+data N = O | S N
+
+type SN = (TypeRep :: N -> Type)
+
+pattern SO = (Typeable :: TypeRep (O::N))
+
+pattern SS ::
+     forall (t :: k').
+     ()
+  => forall (a :: kk -> k') (n :: kk).
+     (t ~ a n)
+  =>
+  TypeRep n -> TypeRep t
+pattern SS n <- (App (Typeable :: TypeRep (a ::kk -> k')) n)

testsuite/tests/patsyn/should_fail/T14498.stderr

+
+T14498.hs:32:48: error:
+    • Pattern synonym existential ‘kk’ cannot be used here
+        (the existential variables of a pattern synonym
+         signature do not scope over the pattern)
+    • In the kind ‘kk -> k'’
+      In the first argument of ‘TypeRep’, namely ‘(a :: kk -> k')’
+      In the type ‘TypeRep (a :: kk -> k')’

testsuite/tests/patsyn/should_fail/T9161-1.stderr

 
 T9161-1.hs:6:14: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
-        (Pattern synonyms cannot be promoted)
-    • In the type signature:
-        wrongLift :: PATTERN
+        (pattern synonyms cannot be promoted)
+    • In the type signature: wrongLift :: PATTERN

testsuite/tests/patsyn/should_fail/T9161-2.stderr

 
 T9161-2.hs:8:20: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
-        (Pattern synonyms cannot be promoted)
+        (pattern synonyms cannot be promoted)
     • In the first argument of ‘Proxy’, namely ‘PATTERN’
-      In the type signature:
-        wrongLift :: Proxy PATTERN ()
+      In the type signature: wrongLift :: Proxy PATTERN ()

testsuite/tests/patsyn/should_fail/all.T

@@ -39,3 +39,4 @@ test('T13470', normal, compile_fail, [''])
 test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
+test('T14498', normal, compile_fail, [''])

testsuite/tests/polykinds/T5716.stderr

 
 T5716.hs:13:33: error:
-    Data constructor ‘U1’ cannot be used here
-      (Perhaps you intended to use TypeInType)
-    In the first argument of ‘I’, namely ‘(U1 DFInt)’
-    In the type ‘I (U1 DFInt)’
-    In the definition of data constructor ‘I1’
+    • Data constructor ‘U1’ cannot be used here
+        (perhaps you intended to use TypeInType)
+    • In the first argument of ‘I’, namely ‘(U1 DFInt)’
+      In the type ‘I (U1 DFInt)’
+      In the definition of data constructor ‘I1’

testsuite/tests/polykinds/T7433.stderr

 
-T7433.hs:2:10:
-    Data constructor ‘Z’ cannot be used here
-      (Perhaps you intended to use DataKinds)
-    In the type ‘ 'Z’
-    In the type declaration for ‘T’
+T7433.hs:2:10: error:
+    • Data constructor ‘Z’ cannot be used here
+        (perhaps you intended to use DataKinds)
+    • In the type ‘ 'Z’
+      In the type declaration for ‘T’