[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:  #1537,
                                              |  #3613
----------------------------------------------+----------------------------

Comment (by ross):

 Replying to [comment:33 jstolarek]:
 > > A command can have the form \ p -> cmd, and that's what we have here
 >
 > Ah, so you used `\` to denote the command abstraction (`proc`), not a
 lambda abstraction? That got me confused.

 Not quite.  There are three different grammar items here:
 {{{
 exp  ::=  \ pat -> exp
 exp  ::=  proc pat -> cmd
 cmd  ::=  \ pat -> cmd
 }}}
 In the last one you're already in the command world, and you want to take
 a value off the stack and give names to its components for use in the
 subcommand.

 > > > So if I want to typecheck the arrow desugaring I need to typecheck
 *exactly* the form to which it will later be desugared, including all the
 explicit stacks, etc?
 > >
 > > Yes you do, and that will be harder in the arrow case, because the
 local environment is an explicit input to the resulting arrow, and the
 desugarer feels free to trim unused variables from that environment, which
 will change its type.
 >
 > And that means that at the typechecking stage I have to exactly follow
 the whole desugaring algorithm, right? Sounds non-trivial.

 If you want to rebind at the level of `arr`, etc, partly (as Simon says)
 and yes it is.

 Replying to [comment:34 simonpj]:
 > I'm not following all of this, but my instinct is this.  The semantics
 of the program should not depend on the details of desugaring.  So the
 various calls to `arr`, `(>>>)` in the desugarer should not dispatch to
 different instances depending on the size of the tuple.  So the type
 checker should be able to construct functions `arr-at-T`, `(>>>)-at-T`
 (for the ambient arrow T) ''that are polymorphic in the environment
 argument''.

 Yes indeed.  And because of the multiple occurrences of `arr` and `>>>` in
 the translations, this will severely constrain the types of any
 replacements, to the point that I wonder if the rebinding will solve the
 original users' issues.

 > I am having trouble getting to grips with this because I know of no
 document that gives:
 >  * The syntax of the arrow sub-language (including comprehensions)
 >  * The typing rules for that language
 >  * The desugaring for that language
 >
 > Having such a document would be extremely helpful in making sure we were
 all on staring from the same baseline.

 Well there is http://www.haskell.org/ghc/docs/papers/arrow-rules.pdf, but
 it needs updating to the new stack representation.  I'll do that.

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