let/app invariant violated by code generated with mkCoreApp

Dr. ÉRDI Gergő gergo at erdi.hu
Wed Nov 12 12:30:00 UTC 2014


I was able to work around this by changing 'seq''s unfolding to '\@a @(b ::
?) x y. case x of { _DEFAULT -> y }' (the change is in the kind of 'b'),
but that just leads to exposing the *real* problem, which is that unfolding
'seq' in the desugarer leads to it getting optimized away by the simplifier.

Any ideas?



On Wed, Nov 12, 2014 at 7:58 PM, Dr. ÉRDI Gergő <gergo at erdi.hu> wrote:

> Unfortunately, now that I had the opportunity to try to validate my
> change, it turns out it is *not* working, since it breaks
> deSugar/should_run/dsrun014.
>
> My code is pushed to the wip/desugar-unfold branch, but all it does is
> change dsExpr from
>
> dsExpr (HsVar var) = return (varToCoreExpr var)   -- See Note [Desugaring
> vars]
>
> to
>
> dsExpr (HsVar var)            -- See Note [Unfolding while desugaring]
>   | isCompulsoryUnfolding unfolding = return $ unfoldingTemplate unfolding
>   | otherwise = return (varToCoreExpr var)   -- See Note [Desugaring vars]
>   where
>     unfolding = idUnfolding var
>
>
> The important bit of the test in question is:
>
> {-# NOINLINE f #-}
> f :: a -> b -> (# a,b #)
> f x y = x `seq` y `seq` (# x,y #)
>
>
>
> Here's what it is desugared into with master:
>
> f [InlPrag=NOINLINE]
>   :: forall a_avA b_avB. a_avA -> b_avB -> (# a_avA, b_avB #)
> [LclIdX, Str=DmdType]
> f =
>   \ (@ a_aAj) (@ b_aAk) ->
>     letrec {
>       f_aAl :: a_aAj -> b_aAk -> (# a_aAj, b_aAk #)
>       [LclId, Str=DmdType]
>       f_aAl =
>         \ (x_avC :: a_aAj) (y_avD :: b_aAk) ->
>           break<2>()
>           break<1>(x_avC,y_avD)
>           case x_avC of x_avC { __DEFAULT ->
>           break<0>(x_avC,y_avD)
>           case y_avD of y_avD { __DEFAULT -> (# x_avC, y_avD #) }
>           }; } in
>     f_aAl
>
>
>
> and here is the desugaring with the above change to dsExpr:
>
> f [InlPrag=NOINLINE]
>   :: forall a_avA b_avB. a_avA -> b_avB -> (# a_avA, b_avB #)
> [LclIdX, Str=DmdType]
> f =
>   \ (@ a_aAj) (@ b_aAk) ->
>     letrec {
>       f_aAl :: a_aAj -> b_aAk -> (# a_aAj, b_aAk #)
>       [LclId, Str=DmdType]
>       f_aAl =
>         \ (x_avC :: a_aAj) (y_avD :: b_aAk) ->
>           break<2>()
>           break<1>(x_avC,y_avD)
>           case break<0>(x_avC,y_avD)
>                (\ (@ a_12)
>                   (@ b_13)
>                   (tpl_B1 [Occ=Once] :: a_12)
>                   (tpl_B2 [Occ=Once] :: b_13) ->
>                   case tpl_B1 of _ [Occ=Dead] { __DEFAULT -> tpl_B2 })
>                  @ b_aAk @ (# a_aAj, b_aAk #) y_avD (# x_avC, y_avD #)
>           of wild_00 { __DEFAULT ->
>           (\ (@ a_12)
>              (@ b_13)
>              (tpl_B1 [Occ=Once] :: a_12)
>              (tpl_B2 [Occ=Once] :: b_13) ->
>              case tpl_B1 of _ [Occ=Dead] { __DEFAULT -> tpl_B2 })
>             @ a_aAj @ (# a_aAj, b_aAk #) x_avC wild_00
>           }; } in
>     f_aAl
>
>
> This trips up the core linter on the application of the inner lambda on
> the unboxed tuple type:
>
>     In the expression: (\ (@ a_12)
>                           (@ b_13)
>                           (tpl_B1 [Occ=Once] :: a_12)
>                           (tpl_B2 [Occ=Once] :: b_13) ->
>                           case tpl_B1 of _ [Occ=Dead] { __DEFAULT ->
> tpl_B2 })
>                          @ b_aAk @ (# a_aAj, b_aAk #) y_avD (# x_avC,
> y_avD #)
>     Kinds don't match in type application:
>     Type variable: b_13 :: *
>     Arg type: (# a_aAj, b_aAk #) :: #
>     xx #
>
> So.... yeah. Is there a more narrow predicate than isCompulsoryUnfolding
> that I should be checking for?
>
> Bye,
>     Gergo
>
> On Wed, Nov 12, 2014 at 10:23 AM, Dr. ÉRDI Gergő <gergo at erdi.hu> wrote:
>
>> Yep, that seems to work. I'll add a note explaining why we need
>> unfoldings here.
>> On Nov 11, 2014 10:14 PM, "Simon Peyton Jones" <simonpj at microsoft.com>
>> wrote:
>>
>>> Oh bother, that is _so_ tiresome. The desugarer establishes the let/app
>>> invariant, so we get
>>>
>>>         I# x_help
>>>
>>> but if x_help has a compulsory unfolding to (x void), returning an Int#,
>>> that violates the let/app invariant.  Sigh.  This is a ridiculous amount of
>>> work for a tiny corner (pattern synonyms for unboxed constants).
>>>
>>> Harump.  Let's see.  We are talking only of things like this
>>>
>>>         pattern P = 4#
>>>
>>> correct?  Perhaps it may be simpler to make the psWrapper in PatSyn be
>>>         psWrapper :: Either Id Literal
>>> and treat such patterns specially from the moment we first see them?
>>> That would eliminate all this void stuff entirely.
>>>
>>> Pursuing the current line, though, I suppose that the desugarer could
>>> inline compulsory unfoldings during desugaring itself.  In this line, add a
>>> case for when var has a compulsory unfolding.
>>>
>>> dsExpr (HsVar var)            = return (varToCoreExpr var)   -- See Note
>>> [Desugaring vars]
>>>
>>> That would, I suppose, be the quickest pathc.
>>>
>>> Simon
>>>
>>> |  -----Original Message-----
>>> |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Dr.
>>> |  ERDI Gergo
>>> |  Sent: 08 November 2014 14:03
>>> |  To: GHC Devs
>>> |  Subject: let/app invariant violated by code generated with mkCoreApp
>>> |
>>> |  Hi,
>>> |
>>> |  I'm trying to attach (f Void#) as a compulsory unfolding to an Id.
>>> |  Here's what I tried originally:
>>> |
>>> |       let unfolding = mkCoreApp (Var worker_id) (Var voidPrimId)
>>> |           wrapper_id' = setIdUnfolding wrapper_id $
>>> |  mkCompulsoryUnfolding unfolding
>>> |
>>> |  However, when I try to use wrapper_id' in the desugarer, the Core
>>> |  linter looks at me strange. This is the original Core:
>>> |
>>> |  f :: Int
>>> |  [LclIdX, Str=DmdType]
>>> |  f = break<1>() GHC.Types.I# Main.$WPAT
>>> |
>>> |  and this is the error message ($WPAT is the wrapper_id', PAT is the
>>> |  worker_id in this example)
>>> |
>>> |  <no location info>: Warning:
>>> |       In the expression: I# (PAT void#)
>>> |       This argument does not satisfy the let/app invariant: PAT void#
>>> |
>>> |  Now, I thought I'd make sure mkCoreApp generated correct Core by
>>> |  writing it out by hand:
>>> |
>>> |       let unfolding = Case (Var voidPrimId) voidArgId pat_ty
>>> |  [(DEFAULT,[],App (Var worker_id) (Var voidArgId))]
>>> |
>>> |  however, bizarrely, this *still* results in *the same* error message,
>>> |  as if something was transforming it back to a straight App.
>>> |
>>> |  Anyone have any hints what I'm doing wrong here?
>>> |
>>> |  Bye,
>>> |       Gergo
>>> |
>>> |  --
>>> |
>>> |     .--= ULLA! =-----------------.
>>> |      \     http://gergo.erdi.hu   \
>>> |       `---= gergo at erdi.hu =-------'
>>> |  You are in a twisty maze of little install diskettes.
>>> |  _______________________________________________
>>> |  ghc-devs mailing list
>>> |  ghc-devs at haskell.org
>>> |  http://www.haskell.org/mailman/listinfo/ghc-devs
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141112/69b3494d/attachment.html>


More information about the ghc-devs mailing list