[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 jstolarek):

 Simon, I think I need some help with typechecking. I defined `thenA`
 (Ross' `bind_`) to have the type `Arrow a => a (e,s) b -> a (e,s) c -> a
 (e,s) c`. Now I'm trying to typecheck `thenA` operator stored inside
 `BodyStmtA` constructor (a new arrow equivalent of monadic `BodyStmt`). I
 wrote something like this:
 {{{
 tcArrDoStmt env _ (BodyStmtA rhs then_op _) res_ty thing_inside
   = do  { (rhs', elt_ty) <- tc_arr_rhs env rhs
         ; thing    <- thing_inside res_ty
         ; s <- newFlexiTyVarTy liftedTypeKind
         ; b <- newFlexiTyVarTy liftedTypeKind
         ; c <- newFlexiTyVarTy liftedTypeKind
         ; then_op' <- tcSyntaxOp DoOrigin then_op
                            (mkFunTys [ mkCmdArrTy env (mkBoxedTupleTy
 [elt_ty, s]) b
                                      , mkCmdArrTy env (mkBoxedTupleTy
 [elt_ty, s]) c]
                                       (mkCmdArrTy env (mkBoxedTupleTy
 [elt_ty, s]) c))
         ; return (BodyStmtA rhs' then_op' elt_ty, thing) }
 }}}
 The test function I'm compiling looks like this:
 {{{
 test :: Arrow a => a i i
 test = proc n -> do
          (arr id) -< n
          returnA -< n
 }}}
 Using `-dcore-lint` during complation reveals offences similar to the ones
 I experienced earlier:
 {{{
     Argument value doesn't match argument type:
     Fun type:
         a_auK (i_auL, GHC.Prim.Any) GHC.Prim.Any
         -> a_auK (i_auL, GHC.Prim.Any) GHC.Prim.Any
         -> a_auK (i_auL, GHC.Prim.Any) GHC.Prim.Any
     Arg type: a_auK (i_auL, ()) i_auL
     Arg:
         ds_dvR
           @ (i_auL, ())
           @ i_auL
           @ i_auL
           (ds_dvQ
              @ (i_auL, ())
              @ i_auL
              (\ (ds_dw0 :: (i_auL, ())) ->
                 case ds_dw0 of _ [Occ=Dead] { (ds_dvZ, _ [Occ=Dead]) ->
 ds_dvZ }))
           (Control.Arrow.arr
              @ a_auK $dArrow_auX @ i_auL @ i_auL (T7828.id @ i_auL))
 }}}
 I tried to write the typechecking of `thenA` to match the actual type,
 just like you wrote in [ticket:7828#comment:29]. But I don't see how could
 I replace my new type variables `s`, `b` and `c` with something concrete.
 I believe that `s` should be allowed to be anything (polymorphism in the
 environment), so I don't know what could it be other than a new tyvar.
 Tracing the calls lead me to believe that `res_ty` is the type of the
 whole `do` expression, so I don't think it has anything to do with the
 type of `thenA`. Can I ask for your guidance here?

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