#11982: Typechecking fails for parallel monad comprehensions with polymorphic let -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): That error looks correct to me, for a rather narrow definition of correct. Both parallel list comprehension and `ApplicativeDo` end up desugaring to manipulations on tuples, right? The tuples hold the bound variables. So your example requires building a tuple with a polymorphic element, hence impredicativity. I'm unaware of a specification of these features beyond implementation in terms of tuples, which is why failing here may be the correct behavior. That said, I'm sure you want this to be accepted. Perhaps it wouldn't be too hard to enable impredicativity in just the right spot... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11982: Typechecking fails for parallel monad comprehensions with polymorphic let -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes the ''output'' of typechecking is impredicative, but the input is not, and plainly should not be rejected. But we may not want to just "enable impredicativity" because that ma allow too much. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11982: Typechecking fails for parallel monad comprehensions with polymorphic let -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: ApplicativeDo Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by vdukhovni): [ Help to pin down the cause by 宮里 洸司 (Koji Miyazato) much appreciated ] Probably the same underlying cause, where a let-bound universally quantified function that transforms IO actions to run under a lock, leads to type errors when ApplicativeDo is in use (sometimes for unrelated code in the same module). Removing ApplicativeDo allows the code to compile, as does inlining the let-bound polymorphic value into the call site. {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ApplicativeDo #-} module Main where import Control.Concurrent.MVar type Locker = forall a. IO a -> IO a main :: IO () main = do line <- getLine lock <- newMVar () let locker :: Locker locker = withMVar lock . const f line locker f :: String -> Locker -> IO () f line locker = locker $ putStrLn line }}} This fails with: {{{ appdobug.hs:14:13: error: • Couldn't match type ‘a’ with ‘a0’ ‘a’ is a rigid type variable bound by a type expected by the context: Locker at appdobug.hs:14:6-18 Expected type: IO a -> IO a Actual type: IO a0 -> IO a0 • In the second argument of ‘f’, namely ‘locker’ In a stmt of a 'do' block: f line locker In the expression: do line <- getLine lock <- newMVar () let locker :: Locker locker = withMVar lock . const f line locker • Relevant bindings include locker :: IO a0 -> IO a0 (bound at appdobug.hs:13:10) }}} With the value of 'locker' inlined as below, what one would expect to be the "same" code now compiles. The behaviour is sufficiently surprising to perhaps merit another look at this issue. {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ApplicativeDo #-} module Main where import Control.Concurrent.MVar type Locker = forall a. IO a -> IO a main :: IO () main = do line <- getLine lock <- newMVar () f line $ withMVar lock . const f :: String -> Locker -> IO () f line locker = locker $ putStrLn line }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11982: Typechecking fails for parallel monad comprehensions with polymorphic let (GHC 7.10.3 through 8.6.3) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) 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 bgamari): I've added these cases to the testsuite in [[https://gitlab.haskell.org/ghc/ghc/merge_requests/185|!185]]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Thanks, @josefs, for looking at this. Do you have an implementation plan in mind? I haven't looked at this beyond reading the ticket, but a solution that doesn't allow incorrect impredicativity looks subtle to design and implement. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 josef): @goldfile can you elaborate on what you mean by incorrect impredicativity? I don't have a concrete plan yet, but it seems to me that, at least in the case of ApplicativeDo, this is mostly a matter of making sure that the algorithm which groups statements doesn't place the LetStmts in unfortunate positions. In the example by @vdukhovni the renamer produces the following very unfortunate code: {{{ Poly.main :: IO () Poly.main = do join (line_a1Wh <- getLine | locker_a1Wj <- do lock_a1Wi <- newMVar () let locker_a1Wj :: Poly.Locker locker_a1Wj = withMVar lock_a1Wi . const return locker_a1Wj) Poly.f line_a1Wh locker_a1Wj }}} It would have been much better if the let statement had been pulled out from inside the join and just on top of the last line. Indeed, if we change the example slightly we can actually make GHC accept the program: {{{ main :: IO () main = do line <- getLine lock <- newMVar () let locker :: Locker locker = withMVar lock . const res <- f line locker return res }}} The above program produces the following after renaming: {{{ main_a1Yv = do join (line_a1XS <- getLine | lock_a1XT <- newMVar ()) let locker_a1XU :: Locker locker_a1Z3 = withMVar lock_a1XT . const res_a1XV <- f line_a1XS locker_a1XU return res_a1XV }}} Just what we want! @vdukhovni, transforming let into where doesn't work in the general case unfortunately. Suppose that you had used either of the variables `line` or `lock` in your let statement. There would have been no way of transforming that into a where clause since those variables are not in scope in the where clause. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 vdukhovni): Indeed changing the last line from: {{{ f line locker }}} to {{{ ret <- f line locker return ret }}} resolves the bug for my code example. I hope this generalizes. Don't know how it applies to the original parallel list comprehension example. I did not expect the "where" alternative to generalize, but note that in this case I was able to arrange for all the relevant variables to be in scope by passing them into a closure precisely for that purpose. The idea was mostly to highlight the discrepancy in the behaviour between a "let" and a "where" that should ideally behave identically. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonmar): Just to address the second point here, the transformations that the renamer does for ApplicativeDo really are just annotations, not actual transformations, in the sense that you can easily get back the original program by just flattening out the `ApplicativeStmt`. It's done this way for exactly the reason you mentioned Simon - the typechecker needs to typecheck the code the user wrote. We also have to collect enough pieces that the desugarer can build the transformed Core expression, so the ApplicativeStmt has all the <$>, <*> and return identifiers. In the renamer there's an ad-hoc algorithm to group the `let` statements with the other statements in a `do`. I was never really happy with this, but it's important to do *something* otherwise `let` statements cause a loss of parallelism. We have tests for this - see `test9` in `testsuite/tests/ado/ado001.hs`. The paper doesn't deal with `let` unfortunately because we didn't include `let` statements in the grammar. It would be nice to fully understand and document what we do here. I also have a suspicion that we're not treating the last statement of the `do` in the way that the paper suggests - adding an extra `return` statement if the last statement is not a `return`. I think I was just lazy, because doing it in the way the paper suggests but without actually transforming the code (see discussion above) is a bit tricky. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 vdukhovni): Replying to [comment:16 josef]:

In fact, I think that this ticket should be split up so that we have a separate ticket for ApplicativeDo. The remedies for parallel monad comprehension and ApplicativeDo seem very different. I'll create a new ticket for ApplicativeDo unless someone yells.

FWIW, I certainly have no objections, apologies if I made a mistake in linking the issues in the first place. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonmar): Actually I do think that `ApplicativeDo` has a similar problem to parallel list comprehensions. It's true that in the example given in comment:5 above we could fix `ApplicativeDo` to do a slightly different transformation and not run into the problem. But that won't work in general, e.g. {{{ test :: IO (Int, Char, Int) test = do x <- return 'a' y <- return 'a' let f | y == 'c' = id | otherwise = id z <- return (f 3) return (f 3, f 'a', z) }}} This is accepted without `ApplicativeDo`, but rejected with it, because we need `f` to be polymorphic. The renamer produces: {{{ ==================== Renamer ==================== Test.test :: IO (Int, Char, Int) Test.test = do x_a3Dl <- return 'a' | (f_a3Dn, z_a3Do) <- do y_a3Dm <- return 'a' let f_a3Dn | y_a3Dm == 'c' = id | otherwise = id z_a3Do <- return (f_a3Dn 3) (f_a3Dn, z_a3Do) return (f_a3Dn 3, f_a3Dn 'a', z_a3Do) }}} so we would need to instantiate the tuple type with polymorphic arguments. Simon - I vaguely remember that we discussed this when reviewing the code for ApplicativeDo and we decided to punt on it at the time, but unfortunately I can't find any record of it, do you remember by any chance? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Ben Gamari ): In [changeset:"def84a10dd9db34d86284cb0b8358261034eecc4/ghc" def84a1/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="def84a10dd9db34d86284cb0b8358261034eecc4" testsuite: Add tests from #11982 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11982#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler