diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-18 12:03:33 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-18 15:47:19 +0000 |
commit | f1fe5b4adf6a4094ecc600a28f64f7628903d017 (patch) | |
tree | 078df33932b6422ce520aee82c0d153fd4135a09 | |
parent | 1e64fc81295ac27c5e662576da3afacd42186a13 (diff) | |
download | haskell-f1fe5b4adf6a4094ecc600a28f64f7628903d017.tar.gz |
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.
-rw-r--r-- | compiler/basicTypes/PatSyn.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 12 | ||||
-rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 95 | ||||
-rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 5 | ||||
-rw-r--r-- | compiler/typecheck/TcSigs.hs | 43 | ||||
-rw-r--r-- | docs/users_guide/glasgow_exts.rst | 18 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T11265.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T14498.hs | 32 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T14498.stderr | 8 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T9161-1.stderr | 5 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T9161-2.stderr | 5 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T5716.stderr | 10 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T7433.stderr | 10 |
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’ |