Opened 3 years ago

Last modified 7 months ago

#11982 new bug

Typechecking fails for parallel monad comprehensions with polymorphic let (GHC 7.10.3 through 8.6.3)

Reported by: simonpj Owned by: josefs
Priority: normal Milestone:
Component: Compiler Version: 7.10.3
Keywords: ApplicativeDo Cc: simonmar, niteria
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# LANGUAGE MonadComprehensions, ParallelListComp #-}

module Foo where

foo xs ys = [ (f y True, f x 'c')
            | let f _ z = z, x <- xs
            | y <- ys ]

This fails with

Foo.hs:5:52: error:
    * Cannot instantiate unification variable `t0'
      with a type involving foralls: forall t2 t3. t3 -> t2 -> t2
        GHC doesn't yet support impredicative polymorphism
    * In a stmt of a monad comprehension:
        let f _ z = z, x <- xs |  y <- ys
      In the expression:
        [(f y True, f x 'c') | let f _ z = z, x <- xs |  y <- ys]
      In an equation for `foo':
          foo xs ys
            = [(f y True, f x 'c') | let f _ z = z, x <- xs |  y <- ys]

NB: ApplicativeDo has a related problem: the implementation is quite different and has the effect of monomorphising the let-bound variable.

Change History (21)

comment:1 Changed 3 years ago 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...

comment:2 Changed 3 years ago by simonmar

Cc: simonmar niteria added

comment:3 Changed 3 years ago 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.

comment:4 Changed 2 years ago by RyanGlScott

Keywords: ApplicativeDo added

comment:5 Changed 8 months ago 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

comment:6 Changed 8 months ago by vdukhovni

Summary: Typechecking fails for parallel monad comprehensions with polymorphic letTypechecking fails for parallel monad comprehensions with polymorphic let (GHC 7.10.3 through 8.6.3)
Type of failure: None/UnknownGHC rejects valid program

comment:7 Changed 8 months ago by bgamari

I've added these cases to the testsuite in !185.

comment:8 Changed 8 months ago by simonmar

Owner: set to josefs

comment:9 Changed 8 months ago 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.

comment:10 Changed 8 months ago by vdukhovni

I don't know whether the below observation is at all useful, but it seems that while let-bound polymorphism is restricted by ApplicativeDo, the same does not appear to be the case with "where". Thus changing the code as follows:

 main = do
     line <- getLine
     lock <- newMVar ()
-    let locker :: Locker
+    go line lock
+  where
+    go line lock =
+        f line locker
+      where
+        locker :: Locker
         locker = withMVar lock . const
-    f line locker

makes the module compile. I don't know whether it is possible to perform that kind of transformation automatically.

comment:11 Changed 8 months ago 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.

comment:12 Changed 8 months ago by goldfire

OK. I confess I don't understand your syntax (what do the <- and | mean? the former usually requires do, but there isn't one; and I'm utterly lost on the |), but if your solution is just to rejigger the desugaring, then I'm sure that's pretty harmless. Thanks!

comment:13 Changed 8 months ago 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.

comment:14 Changed 8 months ago 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.

comment:15 Changed 8 months ago 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.

comment:16 Changed 8 months ago by josef

simonpj, I don't agree with how you characterized my comments. You wrote:

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.

I must have explained myself very poorly. The point I was trying to get across is that we don't need full-on impredicative polymorphism. Instead, I believe we can solve the problem for ApplicativeDo by simply changing the algorithm that ApplicativeDo uses to handle let statements, just as simonmar suggested.

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

comment:17 in reply to:  16 Changed 8 months ago by vdukhovni

Replying to 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.

comment:18 Changed 8 months ago by simonpj

Yes to two tickets. So we have

  • Parallel monad comprehensions: no difficulty in principle, but tcSyntaxOp needs to do impredicative instantiation. See comment:14
  • ApplicativeDo. New ticket needed. I strongly suggest that Step 1 is to take the presentation in the paper and extend it to handle let statements. Then it may be clearer what to do. Probably nothing to do with impredicativity.

Note also Simon's comment that "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." It would be good to clean this up too.

comment:19 Changed 8 months ago 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?

comment:20 Changed 8 months ago by simonpj

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?

I had a quick look but didn't find anything, sorry.

comment:21 Changed 7 months ago by Ben Gamari <ben@…>

In def84a1/ghc:

testsuite: Add tests from #11982
Note: See TracTickets for help on using tickets.