Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#13242 closed bug (fixed)

Panic "StgCmmEnv: variable not found" with ApplicativeDo and ExistentialQuantification

Reported by: ljli Owned by: simonmar
Priority: highest Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: ApplicativeDo Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

-- Panic.hs
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ExistentialQuantification #-}
module Panic where

import Data.STRef
import Control.Monad.ST

data A = forall a. A a

st :: ST s ()
st = do
      A _ <- pure $ A True
      ref <- newSTRef 1
      readSTRef ref
      pure ()
$ ghc Panic.hs
[1 of 1] Compiling Panic            ( Panic.hs, Panic.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.1.20170106 for x86_64-unknown-linux):
	StgCmmEnv: variable not found
  $dMonad_aGQ
  local binds for:
  $trModule
  $tcA
  $tc'A
  $tcA1_rSi
  $tc'A1_rSJ
  $trModule1_rSK
  $trModule2_rSL
  sat_sT5
  sat_sT9
  sat_sTa
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/codeGen/StgCmmEnv.hs:137:9 in ghc:StgCmmEnv

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

The above module fails to compile, giving the pasted panic message. Without the ApplicativeDo pragma compilation succeeds. Reproduced with GHC 8.0.2 and a recent head, courtesy of nixpkgs:

gp84vpgar3n3rqvkwj47yyhxvsvbsmi6-ghc-8.1.20170106

Change History (22)

comment:1 Changed 3 years ago by simonpj

Owner: set to simonmar
Priority: normalhighest

Simon M: this is an outright bug somewhere in ApplicativeDo. Using -dcore-lint nails it immediately in the output of the desugarer:

*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the expression: >>=
                         @ (ST s)
                         $dMonad_aRm
                         @ (STRef s Integer)
                         @ ()
                         (newSTRef @ Integer @ s 1)
                         (\ (ref_aFs :: STRef s Integer) ->
                            >>
                              @ (ST s)
                              $dMonad_a12S
                              @ Integer
                              @ ()
                              (readSTRef @ s @ Integer ref_aFs)
                              (return @ (ST s) $dMonad_a131 @ () ()))
    $dMonad_aRm :: Monad m_aRl[tau:3]
    [LclId] is out of scope
<no location info>: warning:
    In the expression: >>=
                         @ (ST s)
                         $dMonad_aRm
                         @ (STRef s Integer)
                         @ ()
                         (newSTRef @ Integer @ s 1)
                         (\ (ref_aFs :: STRef s Integer) ->
                            >>
                              @ (ST s)
                              $dMonad_a12S
                              @ Integer
                              @ ()
                              (readSTRef @ s @ Integer ref_aFs)
                              (return @ (ST s) $dMonad_a131 @ () ()))
    Argument value doesn't match argument type:
    Fun type:
        Monad (ST s) => forall a b. ST s a -> (a -> ST s b) -> ST s b
    Arg type: Monad m_aRl[tau:3]
    Arg: $dMonad_aRm
*** Offending Program ***
Rec {
$tcA :: TyCon
[LclIdX]
$tcA =
  TyCon
    4740327979976134328##
    15826189822472469109##
    $trModule
    (TrNameS "A"#)

$tc'A :: TyCon
[LclIdX]
$tc'A =
  TyCon
    9840332441209672147##
    16375955839481284679##
    $trModule
    (TrNameS "'A"#)

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "T13242"#)

st :: forall s. ST s ()
[LclIdX]
st =
  \ (@ s_aQu) ->
    let {
      $dApplicative_aR0 :: Applicative (ST s)
      [LclId]
      $dApplicative_aR0 = $fApplicativeST @ s } in
    let {
      $dApplicative_aR7 :: Applicative (ST s)
      [LclId]
      $dApplicative_aR7 = $dApplicative_aR0 } in
    let {
      $dFunctor_aQK :: Functor (ST s)
      [LclId]
      $dFunctor_aQK = $fFunctorST @ s } in
    <*>
      @ (ST s)
      $dApplicative_aR0
      @ ()
      @ ()
      (fmap
         @ (ST s)
         $dFunctor_aQK
         @ A
         @ (() -> ())
         (\ (ds_d13u :: A) (ds_d13v :: ()) ->
            case ds_d13u of wild_00 { A @ a_aRa ds_d13w ->
            let {
              $dNum_a12O :: Num Integer
              [LclId]
              $dNum_a12O = $fNumInteger } in
            let {
              $dMonad_aRm :: Monad (ST s)
              [LclId]
              $dMonad_aRm = $fMonadST @ s } in
            let {
              $dMonad_a12S :: Monad (ST s)
              [LclId]
              $dMonad_a12S = $dMonad_aRm } in
            let {
              $dMonad_a131 :: Monad (ST s)
              [LclId]
              $dMonad_a131 = $dMonad_aRm } in
            let {
              ds_d13x :: ()
              [LclId]
              ds_d13x = ds_d13v } in
            case ds_d13x of wild_00 { () -> () }
            })
         ($ @ 'LiftedRep
            @ A
            @ (ST s A)
            (pure @ (ST s) $dApplicative_aR7 @ A)
            (A @ Bool True)))
      (>>=
         @ (ST s)
         $dMonad_aRm
         @ (STRef s Integer)
         @ ()
         (newSTRef @ Integer @ s 1)
         (\ (ref_aFs :: STRef s Integer) ->
            >>
              @ (ST s)
              $dMonad_a12S
              @ Integer
              @ ()
              (readSTRef @ s @ Integer ref_aFs)
              (return @ (ST s) $dMonad_a131 @ () ())))
end Rec }

comment:2 Changed 3 years ago by simonpj

Milestone: 8.0.3

comment:3 Changed 3 years ago by simonmar

smaller example:

data A = forall a. A a

st :: IO ()
st = do
  A _ <- pure (A True)
  x <- return 1
  pure ()

comment:4 Changed 3 years ago by simonmar

@simonpj I've investigated this and run into something I don't understand, can you help? When we typecheck the above program without ApplicativeDo we get

AbsBindsSig [] []
  {Exported type: st :: IO ()
                  [LclId]
   Bind: st_aNk
           = do A{a_aNN
                  EvBinds{[W] $dMonad_aNP = $dMonad_aNw
                          [W] $dMonad_aNU = $dMonad_aNw
                          [W] $dMonad_aZe = $dMonad_aNw
                          [W] $dNum_aZc = GHC.Num.$fNumInteger @[] []}} _ <- pure @ IO
                                                                               $dApplicative_aNK
                                                                             @ A
                                                                               (A @ Bool True)
                x_aCp <- return @ IO $dMonad_aNU @ Integer 1
                return @ IO $dMonad_aZe @ () ()
   Evidence: EvBinds{}}

Note that $dMonad_aNU, used in the second statement, is bound by the EvBinds in the (existential) pattern in the first statement. ApplicativeDo isn't expecting there to be any dependencies between the two statements, which is why it produces invalid Core.

I don't understand why we're putting these dict bindings in the first pattern, they don't seem to relate to the existential type. I could just disable ApplicativeDo for existential patterns, but if that's necessary I'd like to understand why.

Last edited 3 years ago by simonmar (previous) (diff)

comment:5 Changed 3 years ago by rwbarton

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

  • When we type check (in tcApplicativeStmts) a group of independent statements
      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
    {-# 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.

comment:6 Changed 3 years ago by simonpj

Simon I have realised another problem with ApplicativeDo, not covered by our paper. Consider

data A where
  A :: a -> (a->Int) -> A

st :: A -> A -> IO (Int,Int)
st p q = do
  p1 <- pure p
  A x1 f1 <- pure p1
  q1 <- pure q
  A x2 f2 <- pure q1
  pure (f1 x1, f2 x2)

We'll try to gather (x1,f1) in a pair, and (x2,f2); but that won't work because they each mention an existential type variable. Our desugaring just doesn't work at all for that case.

What to do?

Another awkward wrinkle: what are the dependencies induced by view patterns? And do we account for them?

comment:7 Changed 3 years ago by simonmar

@simonpj One position is to say that it should typecheck if the desugaring (according to the paper) is type-correct, which in this case it isn't. And in fact I think that's what happens:

do1.hs:12:8: error:
    • Couldn't match expected type ‘t0’
                  with actual type ‘(a -> Int, a)’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: A :: forall a. a -> (a -> Int) -> A,
        in a pattern binding in
             'do' block
        at ado1.hs:12:3-9
    • In the pattern: (f1, x1)
      In the expression:
        do { p1 <- pure p;
             A x1 f1 <- pure p1;
             q1 <- pure q;
             A x2 f2 <- pure q1;
             return (f1 x1, f2 x2) }
      In an equation for ‘st’:
          st p q
            = do { p1 <- pure p;
                   A x1 f1 <- pure p1;
                   q1 <- pure q;
                   A x2 f2 <- pure q1;
                   return (f1 x1, f2 x2) }
    • Relevant bindings include
        f1 :: a -> Int (bound at ado1.hs:12:8)
        x1 :: a (bound at ado1.hs:12:5)

Arguably we should do something more clever, but at least it's sound. So I'm less worried about this case than the original one which typechecks but generates invalid Core.

I'll investigate to see if I can make it typecheck the rhs's separately from the patterns.

comment:8 Changed 3 years ago by simonpj

OK here's what I can do easily. Let's say that in a Stmt

  pat <- rhs
  • the Stmt requires constraints needed to typecheck rhs, and to pattern-match pat (e.g. in a view pattern)
  • the Stmt binds the existential type variables and constraints brought into scope by the pattern pat

So for example, given

data T a where
  MkT :: (Eq a, Show b) => a -> b -> T a

Suppose that v :: t is in scope. Then the stmt

  MkT 1 x <- (...show v...) :: T t
  • requires Show t (from the use of show) and Num t (from the literal 1).
  • binds the existential b and constraint Show b.

Now consider

   ...stmts...
   ApplicativeStmts [arg1, arg2, ... argN]
   ...more stmts...

where argi :: ApplicativeArg. Each argi itself contains one or more Stmts. It is easy to ensure that

  • Constraints required by the argi can be solved from constraint bound by ...stmts...
  • Constraints and existentials bound by the argi are not available to solve constraints required either by argj (where i is different from j), or by ...more stmts....
  • Within the stmts of each argi individually, constraints bound by earlier stmts can be used to solve later ones.

That is easy to implement and solves the immediate problem. I'm validating now.


But the rule is terribly unsatisfactory.

  • To typecheck the program you must mentally desugar it into its applicative groups.
  • If you write
    MkT x1 _ <- rhs1
    MkT x2 _ <- rhs2
    
    you really might intend that the Eq t bound by the first stmt is available to solve requirements of rhs2. And with normal monadic deguaring it would be, but not with ApplicativeDo. Worse, there is no way to fix it becuase ApplicativeDo works module-wide.

My solution is: add syntax to allow the programmer to express the program in the form of Figure 2 of our paper, that is, post-rearrangement.

comment:9 Changed 3 years ago by simonpj

Simon, I also want to discuss the implementation. Look at goArgs in tcApplicativeStmts. It uses a CPS structure, so that things brought into scope stay in scope. But that's wrong for constraints (hence this ticket), and it's not really right for bindings either (only the thing_inside needs to see those binders).

So, proposal:

  • Use a mapM to process each of the args indepdendly (mirroring the intended parallel semantics)
  • Now bring into scope all the variables bound by the args (which we can get from their patterns), and typecheck thing_inside.

Can you see anything wrong with this? Should not be hard to try.

comment:10 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 484f8d3/ghc:

Fix ApplicativeDo constraint scoping

This patch fixes Trac #13242, by a bit of fancy footwork
with the LIE variable in which the WantedConstraints are
collected.

I think it can be simplified further, using a 'map'.

comment:11 Changed 3 years ago by simonmar

But the rule is terribly unsatisfactory.

Yes it is. I think I'd also be fine with disabling ApplicativeDo for all statements following an existential pattern match. Or perhaps @rwbarton's suggestion:

whenever there is a pattern match that binds invisible stuff, just assume that that stuff is used in all following statements

But by itself this doesn't solve the problem that the example in this ticket raises, because the A type doesn't bind any dictionaries or constraints.

By all means refactor the implementation of tcApplicativeStmts! Provided the tests pass it should be fine. I remember trying quite hard to simplify the implementation to use fewer fresh type variables, but I couldn't figure out how to do it.

comment:12 Changed 3 years ago by simonmar

@simonpj Could you explain why you needed to fiddle with the LIE? I thought it would be sufficient to typecheck each statement (group) separately rather than typechecking later statements inside the scope of previous ones.

comment:13 Changed 3 years ago by simonpj

I thought it would be sufficient to typecheck each statement (group) separately rather than typechecking later statements inside the scope of previous ones.

Yes; that's what I meant by comment:9. seems to work, and much simpler. Validating now.

Re unsatisfactory nature of the current story: I'll leave it to you to document the behaviour, and perhaps improve it along the lines you suggest.

comment:14 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 254bc33/ghc:

A much nicer solution for typechecking ApplicativeDo

This patch improves the code for TcMatches.tcApplicativeStmts;
see the suggestion in Trac #13242 comment:9.

I now use (mapM goArg args) rather than a CPS-style fold.  The
result is less code, easier to understand, and automatically
fixes the original problem in Trac #13242.

See Note [ApplicativeDo and constraints].

comment:15 Changed 3 years ago by simonpj

Assigning to simonmar for user-manual updates; and possible further work on the design.

comment:16 Changed 3 years ago by simonmar

@simonpj, so the new code doesn't bring constraints into scope from existential bindings, even in statements that sequentially follow the existential pattern match. e.g.

Prelude> data T where A :: forall a . Eq a => a -> T
Prelude> :set -XApplicativeDo 
Prelude> do { A x <- undefined; y <- return (); return (x == x) }

<interactive>:7:48: error:
    • Could not deduce (Eq a) arising from a use of ‘==’
      from the context: Monad f
        bound by the inferred type of it :: Monad f => f Bool
        at <interactive>:7:1-56
      Possible fix:
        add (Eq a) to the context of
          the inferred type of it :: Monad f => f Bool
    • In a stmt of a 'do' block: return (x == x)
      In the expression:
        do A x <- undefined
           y <- return ()
           return (x == x)
      In an equation for ‘it’:
          it
            = do A x <- undefined
                 y <- return ()
                 return (x == x)

I understand why - because the implementation specifically only binds Ids - but it's somewhat surprising. Is this fixable, or should I try to document it?

comment:17 Changed 3 years ago by simonpj

Exactly! (c.f. comment:6)

Is this fixable, or should I try to document it?

The latter I think. It's hard to fix: just try to write the desugaring!!

Last edited 3 years ago by simonpj (previous) (diff)

comment:18 Changed 3 years ago by bgamari

Milestone: 8.0.38.2.1

At this point it is rather unlikely that there will be an 8.0.3. Re-milestoning.

comment:19 Changed 3 years ago by Simon Marlow <marlowsd@…>

In d118807/ghc:

Document interaction between ApplicativeDo and existentials (#13242)

Test Plan: validate

Reviewers: austin, bgamari, erikd

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3256

comment:20 Changed 3 years ago by simonmar

Resolution: fixed
Status: newclosed

comment:21 Changed 2 years ago by RyanGlScott

Keywords: ApplicativeDo added

comment:22 Changed 2 years ago by Ben Gamari <ben@…>

In af403b2/ghc:

ApplicativeDo: document behaviour with strict patterns (#13875)

Test Plan: unit tests, built docs

Reviewers: dfeuer, bgamari, simonpj, austin, erikd

Subscribers: rwbarton, thomie

GHC Trac Issues: #13875, #13242

Differential Revision: https://phabricator.haskell.org/D3691
Note: See TracTickets for help on using tickets.