[GHC] #13027: Core lint errors compiling containers HEAD with GHC HEAD

[GHC]

#13027: Core lint errors compiling containers HEAD with GHC HEAD
-------------------------------------+-------------------------------------
        Reporter:  erikd             |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Building GHC      |            Test Case:
  failed                             |  simplCore/should_compile/T13027
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Thank you!   Sigh.

 Several things.

 '''First (1)'''.  Consider
 {{{
 data T a = MkT !a a

 f :: Int -> T Int
 f x = MkT (x+1) x
 }}}
 We'll generate a wrapper for `MkT`, called `$WMkT`, that does the
 evaluation.
 So the Core looks like this:
 {{{
 $WMkT :: a -> T a
 $WMkT = /\a. \x:a y:a. case x of z { DEFAULT -> MkT y z }

 f = \x. $WMkT (x+1) x
 }}}
 After inlining the wrapper we get
 {{{
 f x = case x+1 of y -> MkT y x
 }}}
 Here in Core the `MkT` is the "worker" constructor.  It does ''not''
 perform evaluation (that is done by the wrapper); it is purely passive.

 But when we pattern match against a `MkT` we know that the payload is
 already evaluated.  So if we started with
 {{{
 g (MkT x y) = MkT x (y+1)
 }}}
 we would initially get
 {{{
 g = \v. case v of
           MkT x y -> case x of r { DEFAULT ->
                        MkT r (y+1)
 }}}
 But since `x` is surely evaluated (since it is gotten from `MkT`)
 we can drop the `case x` to get
 {{{
 g = \v. case v of
           MkT x y -> MkT r (y+1)
 }}}
 So far so good.

 But if GHC went wrong, we could construct the expression
 {{{
 MkT (x+1) y
 }}}
 in which the first argument is not evaluated.  That is not
 supposed to happen!  And arguably Lint should, thereore, check that the
 argument of a strict data constructor (the constructor not the
 wrapper!) is definitely evaluated. But Lint doesn't check that
 check.  Yet.

 '''Second (2)'''.  The same applies to the argument to `dataToTag#`. The
 argument should be evaluated, and Lint should really check that it is.   I
 don't know if there are any other primops with this property. I think
 probably not.

 '''Third (3)'''.  Should the arguments to `reallyUnsafePtrEq'` be
 evaluated?  Probably not. Maybe it's ok to compare unevaluated thunks.
 But then in fact `reallyUnsafePtrEq#` ''is'' ok-for-speculation evan if
 its args are not evaluated. But `exprOkForSpeculation` doesn't understand
 that.

 '''Fourth (4)'''. The Lint error in comment:17 is to do with propagation
 of evaluated-ness.  Consider this Core
 {{{
 f = \x. case x of y { DEFAULT -> MkT y y }
 }}}
 This is fine.  But now CPR analyis spots that f has the CPR property and
 does a worker/wrapper split
 (it would need to have a bigger body for this to actually happen, but you
 get the idea):
 {{{
 $wf = \x -> case x of y { DEFAULT -> (# y, y #) }
 f = \x. case $wf x of (# a, b #) -> MkT a b  -- Wrapper
 }}}
 Now this is NOT fine.  Look at that application of `MkT` in the wrapper
 for `f`:
 we know that `a` will be evaluated (because it's a result of `$wf`) but
 that is
 not immediately apparent.  We need to mark `a` as evaluated somehow.

 We have a way to do that: just grep for {{{`setIdUnfolding`
 evaldUnfolding}}} in the
 compiler.  But we aren't doing that right now.

 Now, Lint doesn't complain about f's wrapper because of (1)
 above (although I argue that it should).   But it ''does'' complain
 in this example program, when `exprOkForSpeculation` fails.

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