[GHC] #8581: Add support for explicitly-bidirectional pattern synonyms

[GHC]

#8581: Add support for explicitly-bidirectional pattern synonyms
-------------------------------------+-------------------------------------
              Reporter:  cactus      |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:  7.10.1
              Priority:  normal      |          Version:
             Component:  Compiler    |         Keywords:  pattern synonyms
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:  5144
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by cactus):

 I think I like the `CE => CP` suggestion. Implementing it will be a bit
 tricky, because currently we typecheck pattern synonyms in two passes:

 * First we typecheck the pattern part, and build an internal
 representation `PatSyn`, which contains (among other things) the builder's
 `Id`, so it has to know its type. But currently that's not a problem,
 since the type is exactly known from the pattern part.

 * Then at a later point, the builder is typechecked against this type
 stored in `PatSyn`.

 So if we want to have any leeway in the builder type compared to the
 matcher type, we have to either typecheck the builder in the first stage
 as well, or not store its type in the `PatSyn`.

 To see why the first solution doesn't work, we need to look at the reason
 builders are typechecked in a separate pass: to support explicitly-
 bidirectional pattern synonyms where the builder refers to something which
 refers to the matcher, e.g. see `testsuite/tests/patsyn/should_run/bidir-
 explicit-scope.hs`:

 {{{
 pattern First x <- x:_ where
   First x = foo [x, x, x]

 foo :: [a] -> [a]
 foo xs@(First x) = replicate (length xs + 1) x

 }}}

 However, we also can't omit the type of the builder from the `PatSyn`
 representation for the same reason: suppose `First` occured in the right-
 hand side of `foo`; how would we know what type to give it, if all we have
 at hand is the `PatSyn` for `First`?

 Maybe there's a way out of all this if the builder type is initialized to
 a fresh skolem tyvar which is filled in when the builder is typechecked;
 but someone more knowledgeable about the typechecker's internals will have
 to chime in on that. I'm worried that, at the very least, it would lead to
 horrible error messages when something goes wrong, since the use sites of
 a pattern synonym builder could now influence the typechecking of the
 definition of said builder.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8581#comment:19>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler