[GHC] #7828: RebindableSyntax and Arrow

[GHC]

#7828: RebindableSyntax and Arrow
----------------------------------------------+----------------------------
        Reporter:  AlessandroVermeulen        |            Owner:
            Type:  bug                        |  jstolarek
        Priority:  normal                     |           Status:  new
       Component:  Compiler (Type checker)    |        Milestone:  7.10.1
      Resolution:                             |          Version:  7.6.2
Operating System:  Unknown/Multiple           |         Keywords:
 Type of failure:  GHC rejects valid program  |     Architecture:
       Test Case:                             |  Unknown/Multiple
        Blocking:                             |       Difficulty:  Unknown
                                              |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by jstolarek):

 I did some more reading and I finally understand Ross' answers :-) Section
 3.2 of John Hughes' "Programming with Arrows" was really helpful in
 understanding the idea of the stack. But I don't yet understand the
 implementation and I still have problems reading the comments. I figured a
 good way of improving my understanding will be implementing a prototype
 solution outlined in [ticket:7828#comment:9 comment 9]. I wanted to begin
 by implementing it only for selected language constructs and I got stuck
 on typechecking !BindStmt in !TcMatches. Currently there is only the
 monadic !BindStmt. In my prototype I want to distinguish between the
 monadic and arrow !BindStmt. This means I need to write typechecking for
 the latter (in !TcMatches). I'm not sure how to do that as I don't know
 what is the type signature for arrow bind. I tried to deduce that based on
 the comments in !DsArrows, but I'm not sure if this is a correct approach.
 Can I once again ask for help in reading the comments?

 {{{
 -- D; xs1 |-a c : () --> t
 -- D; xs' |-a do { ss } : t'   xs2 = xs' - defs(p)
 -- -----------------------------------
 -- D; xs  |-a do { p <- c; ss } : t'
 --
 --        ---> premap (\ (xs) -> (((xs1),()),(xs2)))
 --            (first c >>> arr (\ (p, (xs2)) -> (xs'))) >>> ss
 }}}
 I'm totally confused by `(\ (xs) -> (((xs1),()),(xs2)))`. Where do `xs1`
 and `xs2` come from, if we only bind `xs` as the input to `do { p <- c; ss
 }`? Also, do I understand correctly that bind expression generated in
 desugaring of arrow do-notation does not have a source-level equivalent?
 If so is it even correct to represent it using the !BindStmt constructor?

 In my prototype I'm ignoring Ross' proposal of the new desugaring.

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