[GHC] #11982: Typechecking fails for parallel monad comprehensions with polymorphic let (GHC 7.10.3 through 8.6.3)

[GHC]

#11982: Typechecking fails for parallel monad comprehensions with polymorphic let
(GHC 7.10.3 through 8.6.3)
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  josefs
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:  ApplicativeDo
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 There are two different things going on here.

 First, for the program in the Description, there is really no difficulty
 in principle.
 The relevant code is in `TcMatches`:
 {{{
 tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
   = do { let star_star_kind = liftedTypeKind `mkFunTy` liftedTypeKind
        ; m_ty   <- newFlexiTyVarTy star_star_kind

        ...
 }}}
 We have to
 generate code something like
 {{{
 (mzip <stuff1> <stuff2> >>= \((f,y), x) ->
 return (f y True, f x 'c')
 }}}
 Now, the trouble is that `f` is polymophic, so we need to build a tuple
 with polymorphic components, ''and'' we must instantiate `>>=` at a
 polymoprhic type.  Neither of these is truly problematic -- GHC's internal
 language supports impredicative polymorphism, and there is really no
 difficulty with figuring out where the polymorphism is.

 But in fact the instantiation of `(>>=)` goes through the notorious
 `tcSyntaxOp`, which is currently a bug-farm with several open tickets.
 This ticket points out that `tcSyntaxOp` should really be capable of
 impredicative instantiation.  But currently it is not.  Work needed -- but
 much easier that full support for impredicative polymorphism.

 Second, for the program in comment:5, as josef points out in comment:11,
 the ''renamer'' rewrites the program to a form that really would require
 full-on impredicative polymorphism to propagate `f`'s polymorphism.  This
 is really very naughty: the typechecker is supposed to typecheck the
 program the user originally wrote -- and here is a fine example of why
 that is a good principle.

 I think the solution here is for the renamer to annotate with applicative-
 do info, but not really rewrite it.  Then we can typecheck it directly,
 rather than typechecking a rewritten form.

 The exact design of this is beyond the puny limits of my brain right now,
 but that smells like the right direction.  I'd be happy to advise, esp on
 the first bug.

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