[GHC] #5267: Arrow command combinators

[GHC]

#5267: Arrow command combinators
----------------------------------------+-----------------------------------
  Reporter:  peteg                      |          Owner:  ross            
      Type:  bug                        |         Status:  new             
  Priority:  normal                     |      Milestone:  7.4.1           
 Component:  Compiler                   |        Version:  7.0.3           
Resolution:                             |       Keywords:                  
  Testcase:                             |      Blockedby:                  
Difficulty:                             |             Os:  Unknown/Multiple
  Blocking:                             |   Architecture:  Unknown/Multiple
   Failure:  GHC rejects valid program  |  
----------------------------------------+-----------------------------------

Comment(by simonpj):

 Ah, I see.  The relevant code is here (line 254 of `TcArrows`:
 {{{
         ; (inst_binds, expr') <- checkConstraints ArrowSkol [w_tv] [] $
                                  escapeArrowScope (tcMonoExpr expr e_ty)

 }}}
 The test is actually still there (it's in `checkConsraints` in fact).  But
 the bug is in `escapeArrowScope`.  This function is rather drastic: it
 replaces the entire typechecker's environment, both local and global, with
 one saved from outside the arrow form.  That is pretty dire, because the
 environment carries more than just what varialbes are in scope.  In
 particular, it carries
   * A mutable cell to collect type checker constraints
   * The index of the youngest "touchable" type variable
 These two help to implement the skolem-escape check, so replacing them
 wholesale amounts to jumping right outside the existential.

 What is `escapeArrowScope` really meant to do?  Here are the comments from
 `TcRnTypes`:
 {{{
 ---------------------------
 -- Arrow-notation context
 ---------------------------

 {-
 In arrow notation, a variable bound by a proc (or enclosed let/kappa)
 is not in scope to the left of an arrow tail (-<) or the head of (|..|).
 For example

         proc x -> (e1 -< e2)

 Here, x is not in scope in e1, but it is in scope in e2.  This can get
 a bit complicated:

         let x = 3 in
         proc y -> (proc z -> e1) -< e2

 Here, x and z are in scope in e1, but y is not.  We implement this by
 recording the environment when passing a proc (using newArrowScope),
 and returning to that (using `escapeArrowScope`) on the left of -< and the
 head of (|..|).
 }}}
 Well if that's all, the task should be handled 100% by the renamer, with
 no need for the type checker to do anything.  Even in the renamer I'm
 suspicious of the lock-stock-and-barrel replacement of the environment.  I
 think all you need do is to snapshot the state of tcl_rdr, and keep that
 in the `ArrowCtxt`, not the entire environment.  Moreover, I think there
 is no need to call `escapeArrowScope` in the typechecker as well as in the
 renamer.  The renamer alone does the job.

 Have I understood aright?

 There is another problem with `TcArrows`, revealed by removing the
 `escapeArrowScope` calls:
 {{{
                 -- Check that it has the right shape:
                 --      ((w,s1) .. sn)
                 -- where the si do not mention w
            ; checkTc (corner_ty `eqType` mkTyVarTy w_tv &&
                       not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
                      (badFormFun i tup_ty')
 }}}
 You just can't do this with the new type inference engine, because there
 may be many suspended unification constraints so the type might not yet
 have the right shape; only when constraint solving is gone will it have
 the right shape.

 The Right Thing is to unify `corner_ty` with `w_tv`, rather than calling
 `eqType`. But I'm very dubious about the `unscramble` stuff, since it too
 seems to rely on enough unification having taken place.  I don't
 understand this code well enough to sort it out.  Ross, can you see how to
 rewrite it to use unification, or at least functions like
 `matchExpectedListTy` and friends in `TcUinfy`?  Remember that they return
 coercions which must be wrapped around appropriate terms.  I'd be happy to
 dissus by phone or skype if this is obscure.  The basic rule is: you can't
 zonk and then look at the type; I guarantee that will fail as soon as
 things get at all complicated!

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