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/TcSigs.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/TcSigs.hs')
-rw-r--r-- | compiler/typecheck/TcSigs.hs | 43 |
1 files changed, 1 insertions, 42 deletions
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 |