[GHC] #13242: Panic "StgCmmEnv: variable not found" with ApplicativeDo and ExistentialQuantification

[GHC]

#13242: Panic "StgCmmEnv: variable not found" with ApplicativeDo and
ExistentialQuantification
-------------------------------------+-------------------------------------
        Reporter:  ljli              |                Owner:  simonmar
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.3
       Component:  Compiler          |              Version:  8.1
      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 rwbarton):

 Summary of the discussion of this ticket at today's meeting:

 * When we type check (in `tcApplicativeStmts`) a group of independent
 statements
  {{{#!hs
    do pat1 <- exp1
       pat2 <- exp2
       ...
       patN <- expN
  }}}
  stuff bound by `pat1` should ''not'' be visible in `exp2`, and so on.
 Here stuff includes both the (visible) values bound by `pat1`, and also
 (invisible) dictionaries or equality constraints bound by matching on a
 qualified or GADT constructor. However, ''all'' the stuff (both visible
 and invisible) bound by any of the patterns should be in scope after the
 group.

 * We decided how to split a `do` expression into groups of independent
 statements earlier, in the renamer, on syntactic grounds; that is, based
 only on ''visible'' stuff. But there could be invisible dependencies too,
 such as in
  {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ApplicativeDo #-}
 module T12870 where
 data T a = Eq a => T
 f :: (Monad m) => a -> a -> m (T a) -> (Bool -> m b) -> m (b, b)
 f x y mta mb = do
   T <- mta
   r1 <- mb (x == y)
   r2 <- mb (x == y)
   return (r1, r2)
  }}}
  This program compiles today without `ApplicativeDo`, but causes the panic
 discussed here with `ApplicativeDo`.

  In the current scheme we determine the groups of independent statements
 in the renamer, which is too early to detect that the expression `mb (x ==
 y)` relies on the binding of `T`. Plus Simon thinks it would be too
 fragile anyways. (What if there was another `Eq a` instance in scope from
 somewhere else? Which instance do we use? It would affect the grouping.)

  Simon's suggestion was to reject a program like this in the type checking
 stage. It would be a bit unfortunate, because the program would have
 compiled fine without `ApplicativeDo`.

  Here's another suggestion: whenever there is a pattern match that binds
 invisible stuff, just assume that that stuff is used in all following
 statements. Similar to "just disable ApplicativeDo for existential
 patterns", but the issue isn't existentials, but rather dictionaries or
 equality constraints. The original program using `data A = forall a. A a`
 is actually fine to treat as a single group of independent statements,
 since the pattern match on `A _` doesn't bind any invisible stuff.

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