summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/basicTypes/PatSyn.hs2
-rw-r--r--compiler/typecheck/TcHsType.hs12
-rw-r--r--compiler/typecheck/TcPatSyn.hs95
-rw-r--r--compiler/typecheck/TcRnTypes.hs5
-rw-r--r--compiler/typecheck/TcSigs.hs43
-rw-r--r--docs/users_guide/glasgow_exts.rst18
-rw-r--r--testsuite/tests/patsyn/should_fail/T11265.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T14498.hs32
-rw-r--r--testsuite/tests/patsyn/should_fail/T14498.stderr8
-rw-r--r--testsuite/tests/patsyn/should_fail/T9161-1.stderr5
-rw-r--r--testsuite/tests/patsyn/should_fail/T9161-2.stderr5
-rw-r--r--testsuite/tests/patsyn/should_fail/all.T1
-rw-r--r--testsuite/tests/polykinds/T5716.stderr10
-rw-r--r--testsuite/tests/polykinds/T7433.stderr10
14 files changed, 182 insertions, 66 deletions
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs
index 5a74a5b68a..35ba8e9ae4 100644
--- a/compiler/basicTypes/PatSyn.hs
+++ b/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 => ...
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 4e60b954d1..49d488a7a2 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/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"
{-
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 283127215c..2bd30f4c06 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/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
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5f14b455ad..f9e29a1142 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/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"
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 8678dd33c8..1c0affc133 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/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
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 7861a1740f..6c444cc873 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/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
diff --git a/testsuite/tests/patsyn/should_fail/T11265.stderr b/testsuite/tests/patsyn/should_fail/T11265.stderr
index eda5d35a9d..7161c272b1 100644
--- a/testsuite/tests/patsyn/should_fail/T11265.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11265.stderr
@@ -1,6 +1,6 @@
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’
diff --git a/testsuite/tests/patsyn/should_fail/T14498.hs b/testsuite/tests/patsyn/should_fail/T14498.hs
new file mode 100644
index 0000000000..0744310aee
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14498.hs
@@ -0,0 +1,32 @@
+{-# 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)
diff --git a/testsuite/tests/patsyn/should_fail/T14498.stderr b/testsuite/tests/patsyn/should_fail/T14498.stderr
new file mode 100644
index 0000000000..668f9a1efc
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14498.stderr
@@ -0,0 +1,8 @@
+
+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')’
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.stderr b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
index 04d9b31bf7..fff6efe286 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
@@ -1,6 +1,5 @@
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
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.stderr b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
index 409b922776..cc429313aa 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
@@ -1,7 +1,6 @@
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 ()
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 388e67b27b..4bf631f982 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/polykinds/T5716.stderr b/testsuite/tests/polykinds/T5716.stderr
index d85166b0bb..0e3596da32 100644
--- a/testsuite/tests/polykinds/T5716.stderr
+++ b/testsuite/tests/polykinds/T5716.stderr
@@ -1,7 +1,7 @@
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’
diff --git a/testsuite/tests/polykinds/T7433.stderr b/testsuite/tests/polykinds/T7433.stderr
index 1cd2ad2f29..4dce12a653 100644
--- a/testsuite/tests/polykinds/T7433.stderr
+++ b/testsuite/tests/polykinds/T7433.stderr
@@ -1,6 +1,6 @@
-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’
View Lorry Controller Status