[GHC] #14478: Abstract pattern synonyms (for hsig and hs-boot)

[GHC]

#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