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 /compiler/typecheck/TcPatSyn.hs | |
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.
Diffstat (limited to 'compiler/typecheck/TcPatSyn.hs')
-rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 95 |
1 files changed, 95 insertions, 0 deletions
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 |