#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