#14478: Abstract pattern synonyms (for hsig and hs-boot) -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): OK, so there is a major wrinkle: pattern-synonym signature splitting. The problem is described in this note: {{{ 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). }}} One way we could manage this without introducing a new syntactic construct is to have a user specify both pattern synonym signature AND a stub declaration, literally writing something like: {{{ pattern P :: () => b -> T a pattern P x = ... }}} That's a literal `...`, because if we introduce this syntax, we now can also solve the problem of unidirectional versus bidirectional; to declare only a unidirectional pattern is required, you write: {{{ pattern P :: () => b -> T a pattern P x <- ... }}} It's annoyingly asymmetric with how we do regular value signatures, but the alternative seems worse (inventing a new signature syntax which builds in the arity somehow.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14478#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14478: Abstract pattern synonyms (for hsig and hs-boot) -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I actually like the proposed syntax with the ellipsis. I would just vote for `..` (two dots), because that's already a lexeme (and is what closed type families use). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14478#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler