Opened 2 years ago

Last modified 14 months ago

#14231 new bug

Core lint error "in result of Static argument"

Reported by: mpickering Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: StaticArgumentTransformation Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4945
Wiki Page:

Description (last modified by osa1)

Whilst investigating #14211 I encountered a core lint error.

{-# LANGUAGE CPP                       #-}
{-# LANGUAGE RankNTypes                #-}

module Async where

data AsyncT m a =
    AsyncT {
        runAsyncT :: forall r.
               Maybe Int                          -- state
            -> m r                                          -- stop
            -> (a -> Maybe Int -> Maybe (AsyncT m a) -> m r)  -- yield
            -> m r
    }

------------------------------------------------------------------------------
-- Monad
------------------------------------------------------------------------------

{-# INLINE bindWith #-}
bindWith
    :: (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c)
    -> AsyncT m a
    -> (a -> AsyncT m b)
    -> AsyncT m b
bindWith k (AsyncT m) f = AsyncT $ \_ stp yld ->
  m Nothing stp (\a _ m -> (\x -> (runAsyncT x) Nothing stp yld) $ maybe (f a) (\r -> f a `k` (bindWith k r f)) m )

Compile with ghc -O2 -fno-worker-wrapper -fstatic-argument-transformation -dcore-lint.

Error:

*** Core Lint errors : in result of Static argument ***
<no location info>: warning:
In the expression: bindWith @ m_aV5 @ a_aV6 @ b_aV7 k_aSU x_aX3 f_aSW
    Mismatch in type between binder and occurrence
    Var: bindWith_rpi
    Binder type: forall (m1 :: * -> *) a1 b1 . 
    
    (forall c .   AsyncT m_aV5 c -> AsyncT m_aV5 c -> AsyncT m_aV5 c)
    -> AsyncT m_aV5 a_aV6 -> (a_aV6 -> AsyncT m_aV5 b_aV7) -> AsyncT m_aV5 b_aV7
    Occurrence type: forall (m :: * -> *) a b . 
    
    (forall c .   AsyncT m c -> AsyncT m c -> AsyncT m c)
    -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b
      Before subst: forall (m :: * -> *) a b . 
    
    (forall c .   AsyncT m c -> AsyncT m c -> AsyncT m c)
    -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b
*** Offending Program ***

Change History (16)

comment:1 Changed 2 years ago by simonpj

Keywords: StaticArgumentTransformation added

That indeed looks like a (not very serious) bug.

But Matthew, I think you are studying SAT anyway. Maybe this one will come out in the wash as you do so? If so it may not be worth fixing the current pass?

comment:2 Changed 2 years ago by mpickering

I think this is happening because of Note [Shadow binder] which sounds quite dubious.

Note [Shadow binding]                                                           
 ~~~~~~~~~~~~~~~~~~~~~                                                           
 The calls to the inner map inside body[map] should get inlined                  
 by the local re-binding of 'map'.  We call this the "shadow binding".           
                                                                                
 But we can't use the original binder 'map' unchanged, because                   
 it might be exported, in which case the shadow binding won't be                 
 discarded as dead code after it is inlined.                                     
                                                                                 
 So we use a hack: we make a new SysLocal binder with the *same* unique          
 as binder.  (Another alternative would be to reset the export flag.) 

Then the shadowed binder is constructed from the unique of the old binder and the type of the shadowed_rhs.

          shadow_bndr = mkSysLocal (occNameFS (getOccName binder))              
                                   (idUnique binder)                            
                                   (exprType shadow_rhs) 

It seems that the idea here is that we want to replace the self-recursive call with a call to the sat_worker. The mechanism for this is to create a local binding which shadows the top-level id which will be inlined in a later pass.

In other parts of the compiler the way this would be achieved is to create a new top-level definition for the satted version of the function and then a RULE which rewrites the old version to the new version. Would that be preferable here as well?

comment:3 Changed 2 years ago by simonpj

Would that be preferable here as well?

I'm not sure. If it's still relevant, could you give a standalone example to show what you mean?

comment:4 Changed 15 months ago by monoidal

Simplification of the bug report:

module Async where

bindWith :: (a -> a) -> a -> a
bindWith k f = k (bindWith k f)

and as previously ghc -O2 -fno-worker-wrapper -fstatic-argument-transformation -dcore-lint.

comment:5 Changed 15 months ago by osa1

Version: 8.2.18.5

Confirmed on GHC HEAD.

comment:6 Changed 15 months ago by osa1

Description: modified (diff)

comment:7 Changed 15 months ago by osa1

Looking at this again; I realized that we don't need any flags to trigger some lint warnings in the original program (the Async module):

$ ghc-stage2 Async.hs -dcore-lint -fforce-recomp -O0
[1 of 1] Compiling Async            ( Async.hs, Async.o )
*** Core Lint warnings : in result of Simplifier ***
Async.hs:25:1: warning:
    [RHS of bindWith :: forall (m :: * -> *) a b.
                        (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c)
                        -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b]
    INLINE binder is (non-rule) loop breaker: bindWith

*** Core Lint warnings : in result of Simplifier ***
Async.hs:25:1: warning:
    [RHS of bindWith :: forall (m :: * -> *) a b.
                        (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c)
                        -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b]
    INLINE binder is (non-rule) loop breaker: bindWith

This warning disappears if I remove the INLINE pragma. Not sure if this is a bug (it's a warning, not an error) but maybe useful to know.

comment:8 Changed 15 months ago by osa1

This module has a few problems:

  • The nofib results in the module documentation are not valid anymore. I just run nofib with GHC 8.4.2 and this pass made 0 difference in allocations.
  • The running example used in documentation doesn't really work anymore. For some reason this pass doesn't transform the map function.
  • The pass reuses ids in binder position (i.e. binds same ids with same uniques etc. multiple times), without cloning them (probably to avoid renaming). I think this may break invariants in other places in the compiler although I'm not sure.

Now, for this specific ticket, here's the function before SAT:

bindWith :: forall a. (a -> a) -> a -> a
bindWith
  = \ (@ a_a17W) (k_atr :: a_a17W -> a_a17W) (f_ats :: a_a17W) ->
      k_atr (bindWith @ a_a17W k_atr f_ats)

After SAT:

bindWith :: forall a. (a -> a) -> a -> a
bindWith
  = \ (@ a_a17W) (k_atr :: a_a17W -> a_a17W) (f_ats :: a_a17W) ->
      letrec {
        sat_worker_s198 :: a_a17W
        [LclId]
        sat_worker_s198
          = let {
              bindWith_r1 :: forall a. (a_a17W -> a_a17W) -> a_a17W -> a_a17W
              [LclId]
              bindWith_r1
                = \ (@ a_s195) (k_s196 :: a_a17W -> a_a17W) (f_s197 :: a_a17W) ->
                    sat_worker_s198 } in
            k_atr (bindWith @ a_a17W k_atr f_ats); } in
      sat_worker_s198,

(The printer doesn't make it clear but bindWith_r1 and bindWith have the same unique)

The problem is if you ignore uniques all those a type variables are the same, but from the type checker's perspective they're not, which can be seen in the linter error. With -dsuppress-uniques:

Mismatch in type between binder and occurrence
Var: bindWith
Binder type: forall a. (a -> a) -> a -> a
Occurrence type: forall a. (a -> a) -> a -> a
  Before subst: forall a. (a -> a) -> a -> a

With uniques:

Mismatch in type between binder and occurrence
Var: bindWith_r1
Binder type: forall a. (a_a17W -> a_a17W) -> a_a17W -> a_a17W
Occurrence type: forall a. (a -> a) -> a -> a
  Before subst: forall a. (a -> a) -> a -> a

SAT never actually builds types, it builds terms and then calls exprType. The incorrect type forall a. (a_a17W -> a_a17W) -> a_a17W -> a_a17W is given to this term by exprType:

\ (@ a_s195) (k_s196 :: a_a17W -> a_a17W) (f_s197 :: a_a17W) ->
    sat_worker_s198

Arguments of this lambda is generated by this (probably broken) clone function:

clone (bndr, NotStatic) = return bndr
clone (bndr, _        ) = do { uniq <- newUnique
                             ; return (setVarUnique bndr uniq) }

Where the second element of the pair is defined like this:

data App = VarApp Id | TypeApp Type | CoApp Coercion
data Staticness = Static App | NotStatic

So this clones types, coercion, and term binders just by generating a new unique for them. I'm not sure if this is right way to clone binders. Then, as I said above, it reuses some ids in binder position without cloning them. I suspect one or both of them are causing this bug.

comment:9 in reply to:  7 Changed 15 months ago by monoidal

Replying to osa1:

Looking at this again; I realized that we don't need any flags to trigger some lint warnings in the original program (the Async module):

This is a different issue; GHC won't inline a self-recursive definition (e.g. x :: a; x = x) even if it's marked as INLINE. We could have better messaging about this, I believe this is ticket #9418.

comment:10 Changed 15 months ago by osa1

Differential Rev(s): Phab:D4945
Status: newpatch

In comment:8 I mentioned two problems:

  1. Weird shadowing code to avoid renaming.
  2. Weird binder cloning.

It turns out only fixing (1) is enough to close this ticket. It's easy to fix (2) too (we just need to clone all binders of a definition with CoreSubst.cloneIdBndrs) but my patch doesn't include that for now.

I validated GHC HEAD with -fstatic-argument-transformation and got a bunch of failures. I'll validate again with Phab:D4945 (and with -fSAT), and then validate again with my fix for (2) to see if that fixes any existing failures. (I don't have a reproducer for (2) yet)

comment:11 Changed 15 months ago by osa1

I "fixed" (2), but that made some tests that were previously (just (1)) passing fail. Maybe I misunderstood what it's supposed to do.

With my fix for (1) currently these tests are failing when running the test suite with EXTRA_HC_OPTS="-fstatic-argument-transformation -dcore-lint":

ManyAlternatives ManyConstructors MultiLayerModules T10370 T10547 T10858 T10989
T12150 T12227 T12234 T12425 T12545 T12707 T13035 T13056 T13143 T13379 T13701
T13719 T13825-ghci T14052 T14683 T14697 T15164 T1969 T2182ghci T3064 T3294
T3591 T4029 T4801 T4945 T5030 T5321FD T5321Fun T5631 T5642 T5837 T6048 T6106
T783 T8353 T8425 T9020 T9233 T9293 T9630 T9675 T9872a T9872b T9872c T9872d
T9961 break008 break009 break026 determ017 ghci.prog009 ghci.prog010 ghci024
ghci025 ghci038 ghci057 ghci058 inline-check joao-circular parsing001 print007
prog001 prog002 prog003 prog012 prog013 rule2 spec001

comment:12 Changed 15 months ago by osa1

These are all stat failures: (not good enough)

  • T10858
  • T1969
  • T3294
  • T4801
  • T3064
  • T5030
  • T5631
  • parsing001
  • T783
  • T5321Fun
  • T5321FD
  • T5642
  • T5837
  • T6048
  • T9020
  • T9675
  • T9872a
  • T9872b
  • T9872c
  • T9872d
  • T9961
  • T9233
  • T10370
  • T10547
  • T12227
  • T12425
  • T12234
  • T12545
  • T13035
  • T13056
  • T12707
  • T12150
  • T13379
  • MultiLayerModules
  • ManyConstructors
  • ManyAlternatives
  • T13701
  • T13719
  • T14697
  • T14683
  • T9630
  • T15164
  • T14052

Lint errors:

  • determ017
  • joao-circular
  • spec001
  • T4945
  • T13143
  • T3591
  • T8425

Debug output differs because with this pass we do more inlinings etc.

  • inline-check
  • rule2

These are all -fghci-leak-check warnings:

  • prog001
  • prog002
  • prog003
  • ghci.prog009
  • ghci.prog010
  • prog012
  • prog013
  • ghci024
  • ghci025
  • ghci038
  • ghci057
  • T2182ghci
  • T6106
  • ghci058
  • T8353
  • T9293
  • T10989
  • T13825-ghci
  • print007
  • break008
  • break009
  • break026
  • T4029

comment:13 Changed 15 months ago by simonpj

Crumbs -- code in SAT.hs is extremely impenetrable. But it is mainly doing the right thing; the "weird cloning" is nearly right.

Here's an example

   f :: forall a b. (a,b) -> b -> Int
   f = /\a b. \(x:(a,b)) (y:b). <body>
where
   <body> is an expression
       mentioning a, b, x, y
       and with recursive calls like (f <ty> b <e> y)
           where presumably <e> :: (<ty>,b)

Here the second type argument b, and the second value argument y::b, are static. The first type arg a and value arg x::(a,b) are dynamic. The body of f may mention any or all of a, b, x, y.

We want to generate this:

   f :: forall a b. (a,b) -> b -> Int
   f = /\a b. \(x:(a,b)) (y:b).
       letrec fwrk = /\a \(x:(a,b).
                        REPLACE (f <ty> b <e> y) WITH (fwrk <ty> <e>)
                        IN  <body>
       in fwrk a x

Here fwrk is the local, recursive worker, which has free variables b' and y::b. Notice that the binders of fwrk, namely a and x::(a,b) must be identical (same unique) as the originals, because they are mentioned in <body>.

What is this "REPLACE" business? We want to replace a recusive call to f with a call to fwrk. The easy way to do this is with a non-recursive let, later inlined:

    f = /\a b \(x::(a,b) (y::b). fwrk a x

We must use the same unique for f: we are deliberately shadowing its outer binding. Contrary to the claims in Note [Binder type capture] I don't think it matters whether or not we clone the lambda binders; we are free to alpha-rename the lambda as we please, including re-using existing binders.

So the bugs seem to be:

  • In bindWith (comment:8) we are abstracting over the type variable, but it is static. This is the real source of the problem. In my example above, note that b was static but a was not.
  • Once we fix this we don't need to clone those binders at all; Note [Binder type capture] is moot.

I also commented on a bug in the Phab.

Last edited 15 months ago by simonpj (previous) (diff)

comment:14 Changed 15 months ago by osa1

In bindWith (comment:8) we are abstracting over the type variable, but it is static. This is the real source of the problem. In my example above, note that b was static but a was not.

We introduce two new bindings:

  • bindWith_r1 this is the wrapper (or "shadowing" binding). This has to have the exact same type with the original binder (bindWith) because it'll shadow the original definition. This has a type arg because the original bindWith has one.
  • sat_worker_s198 this is the actual worker function without static argument and because all arguments to bindWith are static this has no args.

So in the actual worker we don't abstract over the static type argument. It seems to me that there isn't a problem with abstracting over static arguments.

comment:15 Changed 15 months ago by simonpj

Aargh. I'm an idiot. My claim that cloning is unnecessary is utterly wrong. Here's a fixed version of the latter part of comment:13.

We want to generate this:

   f :: forall a b. (a,b) -> b -> Int
   f = /\a b. \(x:(a,b)) (y:b).
       letrec fwrk = /\a \(x:(a,b).
                        REPLACE (f <ty> b <e> y) WITH (fwrk <ty> <e>)
                        IN  <body>
       in fwrk a x

Here fwrk is the local, recursive worker, which has free variables b' and y::b. Notice that the binders of fwrk, namely a and x::(a,b) must be identical (same unique) as the originals, because they are mentioned in <body>.

What is this "REPLACE" business? We want to replace a recusive call to f with a call to fwrk. The easy way to do this is with a non-recursive let, later inlined:

   f = /\a b. \(x:(a,b)) (y:b).
       letrec fwrk :: forall a. (a,b) -> Int
              fwrk = /\a \(x:(a,b).
                        let f :: forall a b1. (a,b) -> b -> Int
                            f = /\a _ \(x::(a,b) (_::b). fwrk a x
                        in <body>
       in fwrk a x

We must use the same unique for that inner f: we are deliberately shadowing its outer binding.

Notice too that I used underscores (i.e. freshly-cloned variables that are never referred to) for the static variables. Reason: fwrk t expects an argument of type (t,b), where b scopes globally over the entire definition of fwrk. We cannot write

                        let f :: forall a b. (a,b) -> b -> Int
                            f = /\a b \(x::(a,b) (y::b). fwrk a x

becuase then the call to fwrk is ill-typed. This is what Note [Binder type capture] is about. We should clone the static binders; and it does no harm to clone everything I suppose.


So what is wrong in commnet:8. Here's the actual error message

    In the expression: bindWith @ a_a17R k_atm f_atn
    Mismatch in type between binder and occurrence
    Var: bindWith_rqJ
    Binder type: forall a. (a_a17R -> a_a17R) -> a_a17R -> a_a17R
    Occurrence type: forall a. (a -> a) -> a -> a
      Before subst: forall a. (a -> a) -> a -> a

Ah! Indeed in our running example, the REPLACE binding for f has type

                        let f :: forall a b1. (a,b) -> b -> Int
                            f = /\a _ \(x::(a,b) (_::b). fwrk a x

and indeed that is not the type of the top-level f. But each occurrence of f has the top of the top-level f and Lint is objecting that there seems to be an inconsistency. If we just let it inline, everything would be fine.

How tiresome. Using a let-binding to do the REPLACE stuff is not as convenient as it seems :-(.

comment:16 Changed 14 months ago by monoidal

Status: patchnew
Note: See TracTickets for help on using tickets.