[GHC] #13906: ApplicativeDo doesn't handle existentials as well as it could

30 Jun 2017

      #13906: ApplicativeDo doesn't handle existentials as well as it could
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.0.1
           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:
-------------------------------------+-------------------------------------
 `ApplicativeDo` doesn't work nicely with existentials or GADTs. This was
 first considered in #13242, but I think it's worth reconsidering in light
 of #13875. In particular, we no longer need to think specially about
 whether a particular pattern match reveals evidence, as any pattern match
 that does so must necessarily be strict. Simon Marlow explains (in
 revised, I-think-unmerged, documentation) that

 {{{#!hs
     data T where A :: forall a . Eq a => a -> T

     test = do
       A x <- undefined
       _ <- return 'a'
       _ <- return 'b'
       return (x == x)
 }}}

 will not typecheck because it is first rearranged to

 {{{#!hs
     test =
       (\x _ -> x == x)
         <$> do A x <- undefined; _ <- return 'a'; return x
         <*> return 'b'
 }}}

 This is weird! The more human-obvious rearrangement would work just fine:

 {{{#!hs
     test = do
       A x <- undefined
       (\_ _ -> x == x) <$> return 'a' <*> return 'b'
 }}}

 How can we get there? I think it's actually easy. Suppose we have

 {{{#!hs
   do
     p1 <- e1
     p2 <- e2
     p3 <- e3
     p4 <- e4
     p5 <- e5
     e6
 }}}

 Before starting the detailed dependency analysis and such, let's look just
 at ''which patterns are strict''. If a pattern is strict, then ''every''
 following action must be seen as depending on it, and therefore its
 bindings and evidence can scope over everything else. Let's say that `p3`
 is strict. Then we can immediately transform the expression to

 {{{#!hs
   do
     p1 <- e1
     p2 <- e2
     e3 >>= \case
               p3 -> do
                       p4 <- e4
                       p5 <- e5
                       e6
               -- if refutable
               _ -> fail ...
 }}}

 and then continue the process in the inner `do` block.

 If this is done as an initial pass, then further rearrangement doesn't
 need to consider the possibility of strict patterns; there won't be any.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13906
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler