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 )
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
Keywords: | StaticArgumentTransformation added |
---|
comment:2 Changed 2 years ago by
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
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
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:6 Changed 15 months ago by
Description: | modified (diff) |
---|
comment:7 follow-up: 9 Changed 15 months ago by
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
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 Changed 15 months ago by
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
Differential Rev(s): | → Phab:D4945 |
---|---|
Status: | new → patch |
In comment:8 I mentioned two problems:
- Weird shadowing code to avoid renaming.
- 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
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
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
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 thatb
was static buta
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.
comment:14 Changed 15 months ago by
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 originalbindWith
has one.
sat_worker_s198
this is the actual worker function without static argument and because all arguments tobindWith
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
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
Status: | patch → new |
---|
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?