[GHC] #7828: RebindableSyntax and Arrow

[GHC]

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

Comment (by ross):

 Replying to [comment:42 jstolarek]:
 > I'm able to compile
 >
 > {{{
 > test :: Arrow a => a i i
 > test = proc n -> do
 >          returnA -< n
 > }}}
 >
 > using the new desugaring, which was not possible earlier.

 I wouldn't have expected any change in the handling of this.

 > But I'm still stuck on this:
 >
 > {{{
 > test :: Arrow a => a i i
 > test = proc n -> do
 >          returnA -< n
 >          returnA -< n
 > }}}

 If we're allowing rebinding, that should be type-checked and desugared
 exactly as if it were written

 {{{
 test :: Arrow a => a i i
 test = proc n -> (returnA -< n) `thenA` (returnA -< n)
 }}}

 Here's the type inference (backwards, the way the checker does it):

 {{{
 D |- proc n -> (returnA -< n) `thenA` (returnA -< n) :: a i t
 ----------------------------------------------------------------
 (ProcExpr)
     D; n::i |-a (returnA -< n) `thenA` (returnA -< n) : () --> t
     ------------------------------------------------------------ (ArrForm)
         D |- thenA :: forall e. a1 (e,s1) i -> a2 (e,s2) i -> a (e,()) t
         D; n::i |-a1 returnA -< n : s1 --> i
         ------------------------------------ (ArrApp)
             D |- returnA :: a1 i i
             D, n::i |- n :: i
         D; n::i |-a2 returnA -< n : s2 --> i
         ------------------------------------ (ArrApp)
             D |- returnA :: a2 i i
             D, n::i |- n :: i
 }}}
 For the default `thenA`,
 {{{
 thenA :: Arrow a => a (e,s) b -> a (e,s) c -> a (e,s) c
 u `thenA` v = arr id &&& u >>> arr fst >>> v
 }}}
 we have a1 = a2 = a, s1 = s2 = () and t = i, but with rebinding they'd be
 taken from the type of `thenA`, which could be anything matching the type
 in the above inference.

 > I noticed that desugaring of `cmd` stored in the `BodyStmt` always
 passes `()` as the type of the stack.

 That's true for the default, but if we have rebinding it will be
 determined by the type of `thenA`/`bind`.

 > Ross, I also tried to implement desugaring of `bind`. When generating
 the desugared Core for `cmd 'bind' \ p -> do { ss }` I have problem with
 the `\p ->` part. So, given the desugared `do { ss }`, `cmd` and the
 `bind` operator how should the generated command lambda look like? I'm
 still at a loss to undestand how to explicitly manipulate the stack from
 within Core.

 Here's the type inference:
 {{{
 D; xs |-a cmd1 `bind` \ p -> cmd2 : s --> t
 ------------------------------------------- (ArrForm)
     D |- bind :: forall e. a1 (e,s1) t1 -> a2 (e,(b,s2)) t1 -> a (e,s) t
     D; xs |-a1 :: cmd1 : s1 --> t1
     D; xs |-a2 :: \ p -> cmd2 : (b,s2) --> t2
     ----------------------------------------- (Lam)
         D; xs, p::b |-a2 cmd2 : s2 --> t2
 }}}
 In this case the manipulation of the stack is done by the translation of
 `CmdLam` and by the code inside the vanilla Haskell implementation of
 `bind`.

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