#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.

...

...

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

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. 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